[STATEMENT]
lemma diff_inv_axiom2:
  assumes "picard_lindeloef (\<lambda>t. f) UNIV UNIV 0"
    and "\<And>s. {t::real. t \<ge> 0} \<subseteq> picard_lindeloef.ex_ivl (\<lambda>t. f) UNIV UNIV 0 s"
    and "diff_invariant I (\<lambda>t. f) (\<lambda>s. {t::real. t \<ge> 0}) UNIV 0 G"
  shows "fb\<^sub>\<F> (x\<acute>= f & G) {s. I s} = fb\<^sub>\<F> (\<lambda>s. {x. s = x \<and> G s}) {s. I s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 {s. I s} = fb\<^sub>\<F> (\<lambda>s. {x. s = x \<and> G s}) {s. I s}
[PROOF STEP]
proof(unfold ffb_g_orbital, subst ffb_eq, clarsimp simp: set_eq_iff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
let "?ex_ivl s" = "picard_lindeloef.ex_ivl (\<lambda>t. f) UNIV UNIV 0 s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
let "?lhs s" =
    "\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. t \<ge> 0}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
obtain X where xivp1: "X \<in> Sols (\<lambda>t. f) (\<lambda>s. ?ex_ivl s) UNIV 0 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. s2p (Sols (\<lambda>t. f) (ll_on_open.existence_ivl UNIV (\<lambda>t. f) UNIV 0) UNIV 0 s) X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using picard_lindeloef.flow_in_ivp_sols_ex_ivl[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
s2p UNIV ?s \<Longrightarrow> s2p (Sols (\<lambda>t. f) (ll_on_open.existence_ivl UNIV (\<lambda>t. f) UNIV 0) UNIV 0 ?s) (ll_on_open.flow UNIV (\<lambda>t. f) UNIV 0 ?s)

goal (1 subgoal):
 1. (\<And>X. s2p (Sols (\<lambda>t. f) (ll_on_open.existence_ivl UNIV (\<lambda>t. f) UNIV 0) UNIV 0 s) X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2p (Sols (\<lambda>t. f) (ll_on_open.existence_ivl UNIV (\<lambda>t. f) UNIV 0) UNIV 0 s) X

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
have xivp2: "X \<in> Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X
[PROOF STEP]
by (rule in_ivp_sols_subset[OF _ _ xivp1], simp_all add: assms(2))
[PROOF STATE]
proof (state)
this:
s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
hence shyp: "X 0 = s"
[PROOF STATE]
proof (prove)
using this:
s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X

goal (1 subgoal):
 1. X 0 = s
[PROOF STEP]
using ivp_solsD
[PROOF STATE]
proof (prove)
using this:
s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X
s2p (Sols ?f ?U ?S ?t\<^sub>0 ?s) ?X \<Longrightarrow>  D ?X = (\<lambda>t. ?f t (?X t)) on ?U ?s
s2p (Sols ?f ?U ?S ?t\<^sub>0 ?s) ?X \<Longrightarrow> ?X ?t\<^sub>0 = ?s
s2p (Sols ?f ?U ?S ?t\<^sub>0 ?s) ?X \<Longrightarrow> s2p (?U ?s \<rightarrow> ?S) ?X
s2p (Sols ?f ?U ?S ?t\<^sub>0 ?s) ?X \<Longrightarrow> s2p (?U ?s) ?t\<^sub>0

goal (1 subgoal):
 1. X 0 = s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X 0 = s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
have dinv: "\<forall>s. I s \<longrightarrow> ?lhs s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
diff_invariant I (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 G

goal (1 subgoal):
 1. \<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))
[PROOF STEP]
unfolding diff_invariant_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s. \<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (X \<tau>)) \<longrightarrow> I (X t))

goal (1 subgoal):
 1. \<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
assume "?lhs s" and "G s"
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)
G s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
hence "I s"
[PROOF STATE]
proof (prove)
using this:
\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)
G s

goal (1 subgoal):
 1. I s
[PROOF STEP]
by (erule_tac x=X in ballE, erule_tac x=0 in allE, auto simp: shyp xivp2)
[PROOF STATE]
proof (state)
this:
I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t); G s\<rbrakk> \<Longrightarrow> I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
hence "?lhs s \<longrightarrow> (G s \<longrightarrow> I s)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t); G s\<rbrakk> \<Longrightarrow> I s

goal (1 subgoal):
 1. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
assume "G s \<longrightarrow> I s"
[PROOF STATE]
proof (state)
this:
G s \<longrightarrow> I s

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
hence "?lhs s"
[PROOF STATE]
proof (prove)
using this:
G s \<longrightarrow> I s

goal (1 subgoal):
 1. \<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)
[PROOF STEP]
apply(clarify, subgoal_tac "\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X t. \<lbrakk>G s \<longrightarrow> I s; s2p (Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s) X; 0 \<le> t; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s \<longrightarrow> I s; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)\<rbrakk> \<Longrightarrow> I (X t)
 2. \<And>X t. \<lbrakk>G s \<longrightarrow> I s; s2p (Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s) X; 0 \<le> t; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)
[PROOF STEP]
apply(erule_tac x=0 in allE, frule ivp_solsD(2), simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X t. \<lbrakk>s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X; 0 \<le> t; I s; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s; X 0 = s\<rbrakk> \<Longrightarrow> I (X t)
 2. \<And>X t. \<lbrakk>G s \<longrightarrow> I s; s2p (Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s) X; 0 \<le> t; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)
[PROOF STEP]
using dinv
[PROOF STATE]
proof (prove)
using this:
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t))

goal (2 subgoals):
 1. \<And>X t. \<lbrakk>s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X; 0 \<le> t; I s; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s; X 0 = s\<rbrakk> \<Longrightarrow> I (X t)
 2. \<And>X t. \<lbrakk>G s \<longrightarrow> I s; s2p (Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s) X; 0 \<le> t; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>); G s \<longrightarrow> I s\<rbrakk> \<Longrightarrow> \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
G s \<longrightarrow> I s \<Longrightarrow> \<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)

goal (1 subgoal):
 1. \<And>x. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 x. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G x \<longrightarrow> I x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s
G s \<longrightarrow> I s \<Longrightarrow> \<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)
[PROOF STEP]
show "?lhs s = (G s \<longrightarrow> I s)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) \<longrightarrow> G s \<longrightarrow> I s
G s \<longrightarrow> I s \<Longrightarrow> \<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)

goal (1 subgoal):
 1. (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G s \<longrightarrow> I s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)) = (G s \<longrightarrow> I s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_inv_rule:
  assumes "P \<le> {s. I s}" and "diff_invariant I f U S t\<^sub>0 G" and "{s. I s} \<le> Q"
  shows "P \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(rule ffb_g_orbital_inv[OF assms(1) _ assms(3)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}
[PROOF STEP]
unfolding ffb_diff_inv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_invariant I f U S t\<^sub>0 G
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
diff_invariant I f U S t\<^sub>0 G

goal (1 subgoal):
 1. diff_invariant I f U S t\<^sub>0 G
[PROOF STEP]
.


[STATEMENT]
lemma veval'_sabs_svarE:
  assumes "\<Gamma> \<turnstile>\<^sub>v Sabs cs $\<^sub>s Svar n \<down> v"
  obtains u' env pat rhs
    where "fmlookup \<Gamma> n = Some u'"
          "vfind_match cs u' = Some (env, pat, rhs)"
          "\<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs $\<^sub>s Svar n \<down> v

goal (1 subgoal):
 1. (\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name ts us. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; Sabs cs $\<^sub>s Svar n = name $$ ts; v = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (constr name ts)
[PROOF STATE]
proof (state)
this:
Sabs cs $\<^sub>s Svar n = name $$ ts
v = Vconstr name us_
name |\<in>| C
list_all2 (veval' \<Gamma>) ts us_

goal (3 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name ts us. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; Sabs cs $\<^sub>s Svar n = name $$ ts; v = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "strip_comb (Sabs cs $\<^sub>s Svar n) = strip_comb (name $$ ts)"
[PROOF STATE]
proof (prove)
using this:
Sabs cs $\<^sub>s Svar n = name $$ ts
v = Vconstr name us_
name |\<in>| C
list_all2 (veval' \<Gamma>) ts us_

goal (1 subgoal):
 1. strip_comb (Sabs cs $\<^sub>s Svar n) = strip_comb (name $$ ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strip_comb (Sabs cs $\<^sub>s Svar n) = strip_comb (name $$ ts)

goal (3 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name ts us. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; Sabs cs $\<^sub>s Svar n = name $$ ts; v = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
strip_comb (Sabs cs $\<^sub>s Svar n) = strip_comb (name $$ ts)

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (fold app_sterm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_comb (app (Sabs cs) (Svar n)) = strip_comb (name $$ ts) \<Longrightarrow> False
[PROOF STEP]
apply (simp add: strip_list_comb_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sabs cs = const name \<and> [Svar n] = ts \<Longrightarrow> False
[PROOF STEP]
apply (simp add: const_sterm_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name ts us. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; Sabs cs $\<^sub>s Svar n = name $$ ts; v = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal (2 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case rec_comb
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css_ name_ \<Gamma>'_
fmlookup css_ name_ = Some cs_
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'_
vfind_match cs_ u'_ = Some (env_, uv_, rhs_)
\<Gamma>'_ ++\<^sub>f mk_rec_env css_ \<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> v

goal (2 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css_ name_ \<Gamma>'_
fmlookup css_ name_ = Some cs_
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'_
vfind_match cs_ u'_ = Some (env_, uv_, rhs_)
\<Gamma>'_ ++\<^sub>f mk_rec_env css_ \<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
 2. \<And>css name \<Gamma>' csa u' env uv_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vrecabs css name \<Gamma>'; fmlookup css name = Some csa; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (comb cs' \<Gamma>' u' env pat rhs)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'
vfind_match cs' u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'
vfind_match cs' u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "fmlookup \<Gamma> n = Some u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmlookup \<Gamma> n = Some u'
[PROOF STEP]
using \<open>\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'\<close>
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'

goal (1 subgoal):
 1. fmlookup \<Gamma> n = Some u'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fmlookup \<Gamma> n = Some u' \<Longrightarrow> fmlookup \<Gamma> n = Some u'
 2. \<And>name ts us. \<lbrakk>Svar n = name $$ ts; u' = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> fmlookup \<Gamma> n = Some u'
[PROOF STEP]
case (constr name ts)
[PROOF STATE]
proof (state)
this:
Svar n = name $$ ts
u' = Vconstr name us_
name |\<in>| C
list_all2 (veval' \<Gamma>) ts us_

goal (2 subgoals):
 1. fmlookup \<Gamma> n = Some u' \<Longrightarrow> fmlookup \<Gamma> n = Some u'
 2. \<And>name ts us. \<lbrakk>Svar n = name $$ ts; u' = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> fmlookup \<Gamma> n = Some u'
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
Svar n = name $$ ts
u' = Vconstr name us_
name |\<in>| C
list_all2 (veval' \<Gamma>) ts us_

goal (1 subgoal):
 1. False
[PROOF STEP]
by (fold free_sterm_def) simp
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. fmlookup \<Gamma> n = Some u' \<Longrightarrow> fmlookup \<Gamma> n = Some u'
 2. \<And>name ts us. \<lbrakk>Svar n = name $$ ts; u' = Vconstr name us; name |\<in>| C; list_all2 (veval' \<Gamma>) ts us\<rbrakk> \<Longrightarrow> fmlookup \<Gamma> n = Some u'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. fmlookup \<Gamma> n = Some u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fmlookup \<Gamma> n = Some u'

goal (1 subgoal):
 1. fmlookup \<Gamma> n = Some u' \<Longrightarrow> fmlookup \<Gamma> n = Some u'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
fmlookup \<Gamma> n = Some u'

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fmlookup \<Gamma> n = Some u'

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "cs = cs'" "\<Gamma> = \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs = cs' &&& \<Gamma> = \<Gamma>'
[PROOF STEP]
using \<open>\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'\<close>
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'

goal (1 subgoal):
 1. cs = cs' &&& \<Gamma> = \<Gamma>'
[PROOF STEP]
by (cases; auto)+
[PROOF STATE]
proof (state)
this:
cs = cs'
\<Gamma> = \<Gamma>'

goal (1 subgoal):
 1. \<And>csa \<Gamma>' u' env uu_ rhs. \<lbrakk>\<And>u' env pat rhs. \<lbrakk>fmlookup \<Gamma> n = Some u'; vfind_match cs u' = Some (env, pat, rhs); \<Gamma> ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis; \<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs csa \<Gamma>'; \<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'; vfind_match csa u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'
vfind_match cs' u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v
fmlookup \<Gamma> n = Some u'
cs = cs'
\<Gamma> = \<Gamma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'
vfind_match cs' u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v
fmlookup \<Gamma> n = Some u'
cs = cs'
\<Gamma> = \<Gamma>'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v Sabs cs \<down> Vabs cs' \<Gamma>'
\<Gamma> \<turnstile>\<^sub>v Svar n \<down> u'
vfind_match cs' u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> v
fmlookup \<Gamma> n = Some u'
cs = cs'
\<Gamma> = \<Gamma>'
\<lbrakk>fmlookup \<Gamma> n = Some ?u'1; vfind_match cs ?u'1 = Some (?env1, ?pat1, ?rhs1); \<Gamma> ++\<^sub>f ?env1 \<turnstile>\<^sub>v ?rhs1 \<down> v\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma veval'_wellformed:
  assumes "\<Gamma> \<turnstile>\<^sub>v t \<down> v" "wellformed t" "wellformed_venv \<Gamma>"
  shows "vwellformed v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> v
pre_strong_term_class.wellformed t
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. vwellformed v
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
case comb
[PROOF STATE]
proof (state)
this:
\<Gamma>_ \<turnstile>\<^sub>v t_ \<down> Vabs cs_ \<Gamma>'_
\<Gamma>_ \<turnstile>\<^sub>v u_ \<down> u'_
vfind_match cs_ u'_ = Some (env_, uu_, rhs_)
\<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> val_
\<lbrakk>pre_strong_term_class.wellformed t_; wellformed_venv \<Gamma>_\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs_ \<Gamma>'_)
\<lbrakk>pre_strong_term_class.wellformed u_; wellformed_venv \<Gamma>_\<rbrakk> \<Longrightarrow> vwellformed u'_
\<lbrakk>pre_strong_term_class.wellformed rhs_; wellformed_venv (\<Gamma>'_ ++\<^sub>f env_)\<rbrakk> \<Longrightarrow> vwellformed val_
pre_strong_term_class.wellformed (t_ $\<^sub>s u_)
wellformed_venv \<Gamma>_

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed val_
[PROOF STEP]
apply (rule comb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pre_strong_term_class.wellformed rhs_
 2. wellformed_venv (\<Gamma>'_ ++\<^sub>f env_)
[PROOF STEP]
using comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma>_ \<turnstile>\<^sub>v t_ \<down> Vabs cs_ \<Gamma>'_
\<Gamma>_ \<turnstile>\<^sub>v u_ \<down> u'_
vfind_match cs_ u'_ = Some (env_, uu_, rhs_)
\<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> val_
\<lbrakk>pre_strong_term_class.wellformed t_; wellformed_venv \<Gamma>_\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs_ \<Gamma>'_)
\<lbrakk>pre_strong_term_class.wellformed u_; wellformed_venv \<Gamma>_\<rbrakk> \<Longrightarrow> vwellformed u'_
\<lbrakk>pre_strong_term_class.wellformed rhs_; wellformed_venv (\<Gamma>'_ ++\<^sub>f env_)\<rbrakk> \<Longrightarrow> vwellformed val_
pre_strong_term_class.wellformed (t_ $\<^sub>s u_)
wellformed_venv \<Gamma>_

goal (2 subgoals):
 1. pre_strong_term_class.wellformed rhs_
 2. wellformed_venv (\<Gamma>'_ ++\<^sub>f env_)
[PROOF STEP]
by (auto simp: list_all_iff dest: vfind_match_elem intro: vwellformed.vmatch_env)
[PROOF STATE]
proof (state)
this:
vwellformed val_

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
case (rec_comb \<Gamma> t css name \<Gamma>' cs u u' env pat rhs val)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
have "(pat, rhs) \<in> set cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pat, rhs) \<in> set cs
[PROOF STEP]
by (rule vfind_match_elem) fact
[PROOF STATE]
proof (state)
this:
(pat, rhs) \<in> set cs

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val; pre_strong_term_class.wellformed (t $\<^sub>s u); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed val
[PROOF STEP]
proof (rule rec_comb)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pre_strong_term_class.wellformed rhs
 2. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
show "wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
proof (intro fmpred_add)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. wellformed_venv \<Gamma>'
 2. wellformed_venv (mk_rec_env css \<Gamma>')
 3. wellformed_venv env
[PROOF STEP]
show "wellformed_venv \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv \<Gamma>'
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. wellformed_venv \<Gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wellformed_venv \<Gamma>'

goal (2 subgoals):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
 2. wellformed_venv env
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
 2. wellformed_venv env
[PROOF STEP]
show "wellformed_venv env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv env
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. wellformed_venv env
[PROOF STEP]
by (auto dest: vfind_match_elem intro: vwellformed.vmatch_env)
[PROOF STATE]
proof (state)
this:
wellformed_venv env

goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
show "wellformed_venv (mk_rec_env css \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (mk_rec_env css \<Gamma>')
[PROOF STEP]
unfolding mk_rec_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. wellformed_venv (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
by (auto intro: fmdomI)
[PROOF STATE]
proof (state)
this:
wellformed_venv (mk_rec_env css \<Gamma>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
have "vwellformed (Vrecabs css name \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed (Vrecabs css name \<Gamma>')
[PROOF STEP]
unfolding mk_rec_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwellformed (Vrecabs css name \<Gamma>')
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. vwellformed (Vrecabs css name \<Gamma>')
[PROOF STEP]
by (auto intro: fmdom'I)
[PROOF STATE]
proof (state)
this:
vwellformed (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
thus "wellformed rhs"
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close> rec_comb
[PROOF STATE]
proof (prove)
using this:
vwellformed (Vrecabs css name \<Gamma>')
(pat, rhs) \<in> set cs
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>pre_strong_term_class.wellformed t; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vrecabs css name \<Gamma>')
\<lbrakk>pre_strong_term_class.wellformed u; wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed u'
\<lbrakk>pre_strong_term_class.wellformed rhs; wellformed_venv (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)\<rbrakk> \<Longrightarrow> vwellformed val
pre_strong_term_class.wellformed (t $\<^sub>s u)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
pre_strong_term_class.wellformed rhs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vwellformed val

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
case (constr name \<Gamma> ts us)
[PROOF STATE]
proof (state)
this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us
pre_strong_term_class.wellformed (name $$ ts)
wellformed_venv \<Gamma>

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
have "list_all vwellformed us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all vwellformed us
[PROOF STEP]
using \<open>list_all2 _ _ _\<close> \<open>wellformed (_ $$ _)\<close>
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us
pre_strong_term_class.wellformed (name $$ ts)

goal (1 subgoal):
 1. list_all vwellformed us
[PROOF STEP]
proof (induction ts us rule: list.rel_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pre_strong_term_class.wellformed (name $$ []) \<Longrightarrow> list_all vwellformed []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (pre_strong_term_class.wellformed a21 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed b21); pre_strong_term_class.wellformed (name $$ a22) \<Longrightarrow> list_all vwellformed b22; pre_strong_term_class.wellformed (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all vwellformed (b21 # b22)
[PROOF STEP]
case (Cons v vs u us)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed u)
pre_strong_term_class.wellformed (name $$ vs) \<Longrightarrow> list_all vwellformed us
pre_strong_term_class.wellformed (name $$ (v # vs))

goal (2 subgoals):
 1. pre_strong_term_class.wellformed (name $$ []) \<Longrightarrow> list_all vwellformed []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (pre_strong_term_class.wellformed a21 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed b21); pre_strong_term_class.wellformed (name $$ a22) \<Longrightarrow> list_all vwellformed b22; pre_strong_term_class.wellformed (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all vwellformed (b21 # b22)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed u)
pre_strong_term_class.wellformed (name $$ vs) \<Longrightarrow> list_all vwellformed us
pre_strong_term_class.wellformed (name $$ (v # vs))

goal (1 subgoal):
 1. list_all vwellformed (u # us)
[PROOF STEP]
using constr
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (pre_strong_term_class.wellformed v \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed u)
pre_strong_term_class.wellformed (name $$ vs) \<Longrightarrow> list_all vwellformed us
pre_strong_term_class.wellformed (name $$ (v # vs))
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us__
pre_strong_term_class.wellformed (name $$ ts)
wellformed_venv \<Gamma>

goal (1 subgoal):
 1. list_all vwellformed (u # us)
[PROOF STEP]
by (auto simp: app_sterm_def wellformed.list_comb)
[PROOF STATE]
proof (state)
this:
list_all vwellformed (u # us)

goal (1 subgoal):
 1. pre_strong_term_class.wellformed (name $$ []) \<Longrightarrow> list_all vwellformed []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
list_all vwellformed us

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (pre_strong_term_class.wellformed x1 \<longrightarrow> wellformed_venv \<Gamma> \<longrightarrow> vwellformed x2)) ts us; pre_strong_term_class.wellformed (name $$ ts); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vconstr name us)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
list_all vwellformed us

goal (1 subgoal):
 1. vwellformed (Vconstr name us)
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
vwellformed (Vconstr name us)

goal (3 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Sconst name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; pre_strong_term_class.wellformed (Svar name); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed val
 3. \<And>\<Gamma> cs. \<lbrakk>pre_strong_term_class.wellformed (Sabs cs); wellformed_venv \<Gamma>\<rbrakk> \<Longrightarrow> vwellformed (Vabs cs \<Gamma>)
[PROOF STEP]
qed auto