[STATEMENT]
lemma finals_iff: "finals es \<longleftrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finals es = ((\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es'))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finals es \<Longrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
 2. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
finals es

goal (2 subgoals):
 1. finals es \<Longrightarrow> (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
 2. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
finals es

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')
[PROOF STEP]
by induct(auto simp add: Cons_eq_append_conv Cons_eq_map_conv, metis)
[PROOF STATE]
proof (state)
this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es') \<Longrightarrow> finals es
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
(\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')

goal (1 subgoal):
 1. finals es
[PROOF STEP]
by(induct es) auto
[PROOF STATE]
proof (state)
this:
finals es

goal:
No subgoals!
[PROOF STEP]
qed