[STATEMENT]
lemma vmatch_welldefined':
  assumes "vmatch pat v = Some env" "vwelldefined' v"
  shows "fmpred (\<lambda>_. vwelldefined') env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vmatch pat v = Some env
vwelldefined' v

goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
proof (induction pat v arbitrary: env rule: vmatch_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
case (constr name ps name' vs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>name = name' \<and> length ps = length vs; ?x1 \<in> set ps; ?y1 \<in> set vs; vmatch ?x1 ?y1 = Some ?env1; vwelldefined' ?y1\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1
vmatch (Patconstr name ps) (Vconstr name' vs) = Some env
vwelldefined' (Vconstr name' vs)

goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
hence
    "map_option (foldl (++\<^sub>f) fmempty) (those (map2 vmatch ps vs)) = Some env"
    "name = name'" "length ps = length vs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>name = name' \<and> length ps = length vs; ?x1 \<in> set ps; ?y1 \<in> set vs; vmatch ?x1 ?y1 = Some ?env1; vwelldefined' ?y1\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1
vmatch (Patconstr name ps) (Vconstr name' vs) = Some env
vwelldefined' (Vconstr name' vs)

goal (1 subgoal):
 1. map_option (foldl (++\<^sub>f) fmempty) (those (Term_Utils.map2 vmatch ps vs)) = Some env &&& name = name' &&& length ps = length vs
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
map_option (foldl (++\<^sub>f) fmempty) (those (Term_Utils.map2 vmatch ps vs)) = Some env
name = name'
length ps = length vs

goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_option (foldl (++\<^sub>f) fmempty) (those (Term_Utils.map2 vmatch ps vs)) = Some env
name = name'
length ps = length vs
[PROOF STEP]
obtain envs where "env = foldl (++\<^sub>f) fmempty envs" "map2 vmatch ps vs = map Some envs"
[PROOF STATE]
proof (prove)
using this:
map_option (foldl (++\<^sub>f) fmempty) (those (Term_Utils.map2 vmatch ps vs)) = Some env
name = name'
length ps = length vs

goal (1 subgoal):
 1. (\<And>envs. \<lbrakk>env = foldl (++\<^sub>f) fmempty envs; Term_Utils.map2 vmatch ps vs = map Some envs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: those_someD)
[PROOF STATE]
proof (state)
this:
env = foldl (++\<^sub>f) fmempty envs
Term_Utils.map2 vmatch ps vs = map Some envs

goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
env = foldl (++\<^sub>f) fmempty envs
Term_Utils.map2 vmatch ps vs = map Some envs

goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
have "fmpred (\<lambda>_. vwelldefined') env" if "env \<in> set envs" for env
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
env \<in> set envs
[PROOF STEP]
have "Some env \<in> set (map2 vmatch ps vs)"
[PROOF STATE]
proof (prove)
using this:
env \<in> set envs

goal (1 subgoal):
 1. Some env \<in> set (Term_Utils.map2 vmatch ps vs)
[PROOF STEP]
unfolding \<open>map2 _ _ _ = _\<close>
[PROOF STATE]
proof (prove)
using this:
env \<in> set envs

goal (1 subgoal):
 1. Some env \<in> set (map Some envs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some env \<in> set (Term_Utils.map2 vmatch ps vs)

goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some env \<in> set (Term_Utils.map2 vmatch ps vs)
[PROOF STEP]
obtain p v where "p \<in> set ps" "v \<in> set vs" "vmatch p v = Some env"
[PROOF STATE]
proof (prove)
using this:
Some env \<in> set (Term_Utils.map2 vmatch ps vs)

goal (1 subgoal):
 1. (\<And>p v. \<lbrakk>p \<in> set ps; v \<in> set vs; vmatch p v = Some env\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: map2_elemE)
[PROOF STATE]
proof (state)
this:
p \<in> set ps
v \<in> set vs
vmatch p v = Some env

goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
hence "vwelldefined' v"
[PROOF STATE]
proof (prove)
using this:
p \<in> set ps
v \<in> set vs
vmatch p v = Some env

goal (1 subgoal):
 1. vwelldefined' v
[PROOF STEP]
using constr
[PROOF STATE]
proof (prove)
using this:
p \<in> set ps
v \<in> set vs
vmatch p v = Some env
\<lbrakk>name = name' \<and> length ps = length vs; ?x1 \<in> set ps; ?y1 \<in> set vs; vmatch ?x1 ?y1 = Some ?env1; vwelldefined' ?y1\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1
vmatch (Patconstr name ps) (Vconstr name' vs) = Some enva__
vwelldefined' (Vconstr name' vs)

goal (1 subgoal):
 1. vwelldefined' v
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
vwelldefined' v

goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
by (rule constr; safe?) fact+
[PROOF STATE]
proof (state)
this:
fmpred (\<lambda>_. vwelldefined') env

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?env1 \<in> set envs \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1

goal (4 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>name ps name' vs env. \<lbrakk>\<And>x y env. \<lbrakk>name = name' \<and> length ps = length vs; x \<in> set ps; y \<in> set vs; vmatch x y = Some env; vwelldefined' y\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env; vmatch (Patconstr name ps) (Vconstr name' vs) = Some env; vwelldefined' (Vconstr name' vs)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 4. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
env = foldl (++\<^sub>f) fmempty envs
Term_Utils.map2 vmatch ps vs = map Some envs
?env1 \<in> set envs \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
env = foldl (++\<^sub>f) fmempty envs
Term_Utils.map2 vmatch ps vs = map Some envs
?env1 \<in> set envs \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') ?env1

goal (1 subgoal):
 1. fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fmpred (\<lambda>_. vwelldefined') env

goal (3 subgoals):
 1. \<And>name v env. \<lbrakk>vmatch (Patvar name) v = Some env; vwelldefined' v\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 2. \<And>v va vb vc env. \<lbrakk>vmatch (Patconstr v va) (Vabs vb vc) = Some env; vwelldefined' (Vabs vb vc)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
 3. \<And>v va vb vc vd env. \<lbrakk>vmatch (Patconstr v va) (Vrecabs vb vc vd) = Some env; vwelldefined' (Vrecabs vb vc vd)\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_. vwelldefined') env
[PROOF STEP]
qed auto


[STATEMENT]
lemma sconsts_list_comb:
   "consts (list_comb f xs) |\<subseteq>| S \<longleftrightarrow> consts f |\<subseteq>| S \<and> list_all (\<lambda>x. consts x |\<subseteq>| S) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consts (list_comb f xs) |\<subseteq>| S) = (consts f |\<subseteq>| S \<and> list_all (\<lambda>x. consts x |\<subseteq>| S) xs)
[PROOF STEP]
by (induction xs arbitrary: f) auto


[STATEMENT]
lemma sconsts_sabs:
  "consts (Sabs cs) |\<subseteq>| S \<longleftrightarrow> list_all (\<lambda>(_, t). consts t |\<subseteq>| S) cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consts (Sabs cs) |\<subseteq>| S) = list_all (\<lambda>(uu_, t). consts t |\<subseteq>| S) cs
[PROOF STEP]
apply (auto simp: list_all_iff ffUnion_alt_def dest!: ffUnion_least_rev)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>fBall (fset_of_list cs) (\<lambda>x. (case x of (uu_, x) \<Rightarrow> consts x) |\<subseteq>| S); (a, b) \<in> set cs; x |\<in>| consts b\<rbrakk> \<Longrightarrow> x |\<in>| S
 2. \<And>x a b. \<lbrakk>\<forall>x\<in>set cs. case x of (uu_, t) \<Rightarrow> consts t |\<subseteq>| S; (a, b) |\<in>| fset_of_list cs; x |\<in>| consts b\<rbrakk> \<Longrightarrow> x |\<in>| S
[PROOF STEP]
apply (subst (asm) list_all_iff_fset[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>list_all (\<lambda>x. (case x of (uu_, x) \<Rightarrow> consts x) |\<subseteq>| S) cs; (a, b) \<in> set cs; x |\<in>| consts b\<rbrakk> \<Longrightarrow> x |\<in>| S
 2. \<And>x a b. \<lbrakk>\<forall>x\<in>set cs. case x of (uu_, t) \<Rightarrow> consts t |\<subseteq>| S; (a, b) |\<in>| fset_of_list cs; x |\<in>| consts b\<rbrakk> \<Longrightarrow> x |\<in>| S
[PROOF STEP]
apply (auto simp: list_all_iff fset_of_list_elem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done