Theory Big_Step_Value_ML
subsection ‹Big-step semantics with conflation of constants and variables›
theory Big_Step_Value_ML
imports Big_Step_Value
begin
definition mk_rec_env :: "(name, sclauses) fmap ⇒ (name, value) fmap ⇒ (name, value) fmap" where
"mk_rec_env css Γ' = fmmap_keys (λname cs. Vrecabs css name Γ') css"
context special_constants begin
inductive veval' :: "(name, value) fmap ⇒ sterm ⇒ value ⇒ bool" (‹_/ ⊢⇩v/ _ ↓/ _› [50,0,50] 50) where
const: "name |∉| C ⟹ fmlookup Γ name = Some val ⟹ Γ ⊢⇩v Sconst name ↓ val" |
var: "fmlookup Γ name = Some val ⟹ Γ ⊢⇩v Svar name ↓ val" |
abs: "Γ ⊢⇩v Sabs cs ↓ Vabs cs Γ" |
comb: "
Γ ⊢⇩v t ↓ Vabs cs Γ' ⟹ Γ ⊢⇩v u ↓ u' ⟹
vfind_match cs u' = Some (env, _, rhs) ⟹
Γ' ++⇩f env ⊢⇩v rhs ↓ val ⟹
Γ ⊢⇩v t $⇩s u ↓ val" |
rec_comb: "
Γ ⊢⇩v t ↓ Vrecabs css name Γ' ⟹
fmlookup css name = Some cs ⟹
Γ ⊢⇩v u ↓ u' ⟹
vfind_match cs u' = Some (env, _, rhs) ⟹
Γ' ++⇩f mk_rec_env css Γ' ++⇩f env ⊢⇩v rhs ↓ val ⟹
Γ ⊢⇩v t $⇩s u ↓ val" |
constr: "name |∈| C ⟹ list_all2 (veval' Γ) ts us ⟹ Γ ⊢⇩v name $$ ts ↓ Vconstr name us"
lemma veval'_sabs_svarE:
assumes "Γ ⊢⇩v Sabs cs $⇩s Svar n ↓ v"
obtains u' env pat rhs
where "fmlookup Γ n = Some u'"
"vfind_match cs u' = Some (env, pat, rhs)"
"Γ ++⇩f env ⊢⇩v rhs ↓ v"
using assms proof cases
case (constr name ts)
hence "strip_comb (Sabs cs $⇩s Svar n) = strip_comb (name $$ ts)"
by simp
hence False
apply (fold app_sterm_def)
apply (simp add: strip_list_comb_const)
apply (simp add: const_sterm_def)
done
thus ?thesis by simp
next
case rec_comb
hence False by cases
thus ?thesis by simp
next
case (comb cs' Γ' u' env pat rhs)
moreover have "fmlookup Γ n = Some u'"
using ‹Γ ⊢⇩v Svar n ↓ u'›
proof cases
case (constr name ts)
hence False
by (fold free_sterm_def) simp
thus ?thesis by simp
qed auto
moreover have "cs = cs'" "Γ = Γ'"
using ‹Γ ⊢⇩v Sabs cs ↓ Vabs cs' Γ'›
by (cases; auto)+
ultimately show ?thesis
using that by auto
qed
lemma veval'_wellformed:
assumes "Γ ⊢⇩v t ↓ v" "wellformed t" "wellformed_venv Γ"
shows "vwellformed v"
using assms proof induction
case comb
show ?case
apply (rule comb)
using comb by (auto simp: list_all_iff dest: vfind_match_elem intro: vwellformed.vmatch_env)
next
case (rec_comb Γ t css name Γ' cs u u' env pat rhs val)
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
show ?case
proof (rule rec_comb)
show "wellformed_venv (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
proof (intro fmpred_add)
show "wellformed_venv Γ'"
using rec_comb by auto
next
show "wellformed_venv env"
using rec_comb by (auto dest: vfind_match_elem intro: vwellformed.vmatch_env)
next
show "wellformed_venv (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using rec_comb by (auto intro: fmdomI)
qed
next
have "vwellformed (Vrecabs css name Γ')"
unfolding mk_rec_env_def
using rec_comb by (auto intro: fmdom'I)
thus "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› rec_comb by (auto simp: list_all_iff)
qed
next
case (constr name Γ ts us)
have "list_all vwellformed us"
using ‹list_all2 _ _ _› ‹wellformed (_ $$ _)›
proof (induction ts us rule: list.rel_induct)
case (Cons v vs u us)
thus ?case
using constr by (auto simp: app_sterm_def wellformed.list_comb)
qed simp
thus ?case
by (simp add: list_all_iff)
qed auto
lemma (in constants) veval'_shadows:
assumes "Γ ⊢⇩v t ↓ v" "not_shadows_vconsts_env Γ" "¬ shadows_consts t"
shows "not_shadows_vconsts v"
using assms proof induction
case comb
show ?case
apply (rule comb)
using comb by (auto simp: list_all_iff dest: vfind_match_elem intro: not_shadows_vconsts.vmatch_env)
next
case (rec_comb Γ t css name Γ' cs u u' env pat rhs val)
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
show ?case
proof (rule rec_comb)
show "not_shadows_vconsts_env (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
proof (intro fmpred_add)
show "not_shadows_vconsts_env env"
using rec_comb by (auto dest: vfind_match_elem intro: not_shadows_vconsts.vmatch_env)
next
show "not_shadows_vconsts_env (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using rec_comb by (auto intro: fmdomI)
next
show "not_shadows_vconsts_env Γ'"
using rec_comb by auto
qed
next
have "not_shadows_vconsts (Vrecabs css name Γ')"
using rec_comb by auto
thus "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› rec_comb by (auto simp: list_all_iff)
qed
next
case (constr name Γ ts us)
have "list_all (not_shadows_vconsts) us"
using ‹list_all2 _ _ _› ‹¬ shadows_consts (name $$ ts)›
proof (induction ts us rule: list.rel_induct)
case (Cons v vs u us)
thus ?case
using constr by (auto simp: shadows.list_comb app_sterm_def)
qed simp
thus ?case
by (simp add: list_all_iff)
qed (auto simp: list_all_iff list_ex_iff)
lemma veval'_closed:
assumes "Γ ⊢⇩v t ↓ v" "closed_except t (fmdom Γ)" "closed_venv Γ"
assumes "wellformed t" "wellformed_venv Γ"
shows "vclosed v"
using assms proof induction
case (comb Γ t cs Γ' u u' env pat rhs val)
hence "vclosed (Vabs cs Γ')"
by (auto simp: closed_except_def)
have "(pat, rhs) ∈ set cs" "vmatch (mk_pat pat) u' = Some env"
by (rule vfind_match_elem; fact)+
hence "fmdom env = patvars (mk_pat pat)"
by (simp add: vmatch_dom)
have "vwellformed (Vabs cs Γ')"
apply (rule veval'_wellformed)
using comb by auto
hence "linear pat"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
hence "fmdom env = frees pat"
unfolding ‹fmdom env = _›
by (simp add: mk_pat_frees)
show ?case
proof (rule comb)
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ')›
by (auto simp: list_all_iff)
next
show "closed_venv (Γ' ++⇩f env)"
apply rule
using ‹vclosed (Vabs cs Γ')› apply auto[]
apply (rule vclosed.vmatch_env)
apply (rule vfind_match_elem)
using comb by (auto simp: closed_except_def)
next
show "closed_except rhs (fmdom (Γ' ++⇩f env))"
using ‹vclosed (Vabs cs Γ')› ‹fmdom env = frees pat› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
next
show "wellformed_venv (Γ' ++⇩f env)"
apply rule
using ‹vwellformed (Vabs cs Γ')› apply auto[]
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
using comb by auto
qed
next
case (rec_comb Γ t css name Γ' cs u u' env pat rhs val)
have "(pat, rhs) ∈ set cs" "vmatch (mk_pat pat) u' = Some env"
by (rule vfind_match_elem; fact)+
hence "fmdom env = patvars (mk_pat pat)"
by (simp add: vmatch_dom)
have "vwellformed (Vrecabs css name Γ')"
apply (rule veval'_wellformed)
using rec_comb by auto
hence "wellformed_clauses cs"
using rec_comb by auto
hence "linear pat"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
hence "fmdom env = frees pat"
unfolding ‹fmdom env = _›
by (simp add: mk_pat_frees)
show ?case
proof (rule rec_comb)
show "closed_venv (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
proof (intro fmpred_add)
show "closed_venv Γ'"
using rec_comb by (auto simp: closed_except_def)
next
show "closed_venv env"
using rec_comb by (auto simp: closed_except_def dest: vfind_match_elem intro: vclosed.vmatch_env)
next
show "closed_venv (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using rec_comb by (auto simp: closed_except_def intro: fmdomI)
qed
next
have "vclosed (Vrecabs css name Γ')"
using mk_rec_env_def
using rec_comb by (auto simp: closed_except_def intro: fmdom'I)
hence "closed_except rhs (fmdom Γ' |∪| frees pat)"
apply simp
apply (elim conjE)
apply (drule fmpredD[where m = css])
apply (rule rec_comb)
using ‹(pat, rhs) ∈ set cs›
unfolding list_all_iff by auto
thus "closed_except rhs (fmdom (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env))"
unfolding closed_except_def
using ‹fmdom env = frees pat›
by auto
next
show "wellformed rhs"
using ‹wellformed_clauses cs› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
next
show "wellformed_venv (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
proof (intro fmpred_add)
show "wellformed_venv Γ'"
using ‹vwellformed (Vrecabs css name Γ')› by auto
next
show "wellformed_venv env"
using rec_comb by (auto dest: vfind_match_elem intro: veval'_wellformed vwellformed.vmatch_env)
next
show "wellformed_venv (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using ‹vwellformed (Vrecabs css name Γ')› by (auto intro: fmdomI)
qed
qed
next
case (constr name Γ ts us)
have "list_all vclosed us"
using ‹list_all2 _ _ _› ‹closed_except (_ $$ _) _› ‹wellformed (_ $$ _)›
proof (induction ts us rule: list.rel_induct)
case (Cons v vs u us)
with constr show ?case
unfolding closed.list_comb wellformed.list_comb
by (auto simp: Sterm.closed_except_simps)
qed simp
thus ?case
by (simp add: list_all_iff)
qed (auto simp: Sterm.closed_except_simps)
primrec vwelldefined' :: "value ⇒ bool" where
"vwelldefined' (Vconstr name vs) ⟷ list_all vwelldefined' vs" |
"vwelldefined' (Vabs cs Γ) ⟷
pred_fmap id (fmmap vwelldefined' Γ) ∧
list_all (λ(pat, t). consts t |⊆| (fmdom Γ |∪| C)) cs ∧
fdisjnt C (fmdom Γ)" |
"vwelldefined' (Vrecabs css name Γ) ⟷
pred_fmap id (fmmap vwelldefined' Γ) ∧
pred_fmap (λcs.
list_all (λ(pat, t). consts t |⊆| fmdom Γ |∪| (C |∪| fmdom css)) cs ∧
fdisjnt C (fmdom Γ)) css ∧
name |∈| fmdom css ∧
fdisjnt C (fmdom css)"
lemma vmatch_welldefined':
assumes "vmatch pat v = Some env" "vwelldefined' v"
shows "fmpred (λ_. vwelldefined') env"
using assms proof (induction pat v arbitrary: env rule: vmatch_induct)
case (constr name ps name' vs)
hence
"map_option (foldl (++⇩f) fmempty) (those (map2 vmatch ps vs)) = Some env"
"name = name'" "length ps = length vs"
by (auto split: if_splits)
then obtain envs where "env = foldl (++⇩f) fmempty envs" "map2 vmatch ps vs = map Some envs"
by (blast dest: those_someD)
moreover have "fmpred (λ_. vwelldefined') env" if "env ∈ set envs" for env
proof -
from that have "Some env ∈ set (map2 vmatch ps vs)"
unfolding ‹map2 _ _ _ = _› by simp
then obtain p v where "p ∈ set ps" "v ∈ set vs" "vmatch p v = Some env"
by (auto elim: map2_elemE)
hence "vwelldefined' v"
using constr by (simp add: list_all_iff)
show ?thesis
by (rule constr; safe?) fact+
qed
ultimately show ?case
by auto
qed auto
lemma sconsts_list_comb:
"consts (list_comb f xs) |⊆| S ⟷ consts f |⊆| S ∧ list_all (λx. consts x |⊆| S) xs"
by (induction xs arbitrary: f) auto
lemma sconsts_sabs:
"consts (Sabs cs) |⊆| S ⟷ list_all (λ(_, t). consts t |⊆| S) cs"
apply (auto simp: list_all_iff ffUnion_alt_def dest!: ffUnion_least_rev)
apply (subst (asm) list_all_iff_fset[symmetric])
apply (auto simp: list_all_iff fset_of_list_elem)
done
lemma (in constants) veval'_welldefined':
assumes "Γ ⊢⇩v t ↓ v" "fdisjnt C (fmdom Γ)"
assumes "consts t |⊆| fmdom Γ |∪| C" "fmpred (λ_. vwelldefined') Γ"
assumes "wellformed t" "wellformed_venv Γ"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ"
shows "vwelldefined' v"
using assms proof induction
case (abs Γ cs)
thus ?case
unfolding sconsts_sabs
by (auto simp: list_all_iff list_ex_iff)
next
case (comb Γ t cs Γ' u u' env pat rhs val)
hence "(pat, rhs) ∈ set cs"
by (auto dest: vfind_match_elem)
moreover have "vwelldefined' (Vabs cs Γ')"
using comb by auto
ultimately have "consts rhs |⊆| fmdom Γ' |∪| C"
by (auto simp: list_all_iff)
have "vwellformed (Vabs cs Γ')"
apply (rule veval'_wellformed)
using comb by auto
hence "linear pat"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
hence "frees pat = patvars (mk_pat pat)"
by (simp add: mk_pat_frees)
hence "fmdom env = frees pat"
apply simp
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply (rule comb)
done
have "not_shadows_vconsts (Vabs cs Γ')"
apply (rule veval'_shadows)
using comb by auto
have "vwelldefined' (Vabs cs Γ')"
using comb by auto
show ?case
proof (rule comb)
show "consts rhs |⊆| fmdom (Γ' ++⇩f env) |∪| C"
using ‹consts rhs |⊆| fmdom Γ' |∪| C›
by auto
next
have "vwelldefined' u'"
using comb by auto
hence "fmpred (λ_. vwelldefined') env"
using comb
by (auto intro: vmatch_welldefined' dest: vfind_match_elem)
thus "fmpred (λ_. vwelldefined') (Γ' ++⇩f env)"
using ‹vwelldefined' (Vabs cs Γ')› by auto
next
have "fdisjnt C (fmdom Γ')"
using ‹vwelldefined' (Vabs cs Γ')›
by simp
moreover have "fdisjnt C (fmdom env)"
unfolding ‹fmdom env = frees pat›
using ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vabs cs Γ')›
by (auto simp: list_all_iff all_consts_def fdisjnt_alt_def)
ultimately show "fdisjnt C (fmdom (Γ' ++⇩f env))"
unfolding fdisjnt_alt_def by auto
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ')›
by (auto simp: list_all_iff)
next
have "wellformed_venv Γ'"
using ‹vwellformed (Vabs cs Γ')› by simp
moreover have "wellformed_venv env"
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
using comb by auto
ultimately show "wellformed_venv (Γ' ++⇩f env)"
by blast
next
have "not_shadows_vconsts_env Γ'"
using ‹not_shadows_vconsts (Vabs cs Γ')› by simp
moreover have "not_shadows_vconsts_env env"
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
using comb by auto
ultimately show "not_shadows_vconsts_env (Γ' ++⇩f env)"
by blast
next
show "¬ shadows_consts rhs"
using ‹not_shadows_vconsts (Vabs cs Γ')› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
qed
next
case (rec_comb Γ t css name Γ' cs u u' env pat rhs val)
hence "(pat, rhs) ∈ set cs"
by (auto dest: vfind_match_elem)
moreover have "vwelldefined' (Vrecabs css name Γ')"
using rec_comb by auto
ultimately have "consts rhs |⊆| fmdom Γ' |∪| (C |∪| fmdom css)"
using ‹fmlookup css name = Some cs›
by (auto simp: list_all_iff dest!: fmpredD[where m = css])
have "vwellformed (Vrecabs css name Γ')"
apply (rule veval'_wellformed)
using rec_comb by auto
hence "wellformed_clauses cs"
using rec_comb by auto
hence "linear pat"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
hence "frees pat = patvars (mk_pat pat)"
by (simp add: mk_pat_frees)
hence "fmdom env = frees pat"
apply simp
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply (rule rec_comb)
done
have "not_shadows_vconsts (Vrecabs css name Γ')"
apply (rule veval'_shadows)
using rec_comb by auto
have "vwelldefined' (Vrecabs css name Γ')"
using rec_comb by auto
show ?case
proof (rule rec_comb)
show "consts rhs |⊆| fmdom (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env) |∪| C"
using ‹consts rhs |⊆| _› unfolding mk_rec_env_def
by auto
next
have "fmpred (λ_. vwelldefined') Γ'"
using ‹vwelldefined' (Vrecabs css name Γ')› by auto
moreover have "fmpred (λ_. vwelldefined') (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using rec_comb by (auto intro: fmdomI)
moreover have "fmpred (λ_. vwelldefined') env"
using rec_comb by (auto dest: vfind_match_elem intro: vmatch_welldefined')
ultimately show "fmpred (λ_. vwelldefined') (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
by blast
next
have "fdisjnt C (fmdom Γ')"
using rec_comb by auto
moreover have "fdisjnt C (fmdom env)"
unfolding ‹fmdom env = frees pat›
using ‹fmlookup css name = Some cs› ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vrecabs css name Γ')›
apply auto
apply (drule fmpredD[where m = css])
by (auto simp: list_all_iff all_consts_def fdisjnt_alt_def)
moreover have "fdisjnt C (fmdom (mk_rec_env css Γ'))"
unfolding mk_rec_env_def
using ‹vwelldefined' (Vrecabs css name Γ')›
by simp
ultimately show "fdisjnt C (fmdom (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env))"
unfolding fdisjnt_alt_def by auto
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹wellformed_clauses cs›
by (auto simp: list_all_iff)
next
have "wellformed_venv Γ'"
using ‹vwellformed (Vrecabs css name Γ')› by simp
moreover have "wellformed_venv (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using ‹vwellformed (Vrecabs css name Γ')›
by (auto intro: fmdomI)
moreover have "wellformed_venv env"
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
using rec_comb by auto
ultimately show "wellformed_venv (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
by blast
next
have "not_shadows_vconsts_env Γ'"
using ‹not_shadows_vconsts (Vrecabs css name Γ')› by simp
moreover have "not_shadows_vconsts_env (mk_rec_env css Γ')"
unfolding mk_rec_env_def
using ‹not_shadows_vconsts (Vrecabs css name Γ')›
by (auto intro: fmdomI)
moreover have "not_shadows_vconsts_env env"
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
using rec_comb by auto
ultimately show "not_shadows_vconsts_env (Γ' ++⇩f mk_rec_env css Γ' ++⇩f env)"
by blast
next
show "¬ shadows_consts rhs"
using rec_comb ‹not_shadows_vconsts (Vrecabs css name Γ')› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
qed
next
case (constr name Γ ts us)
have "list_all vwelldefined' us"
using ‹list_all2 _ _ _› ‹consts (name $$ ts) |⊆| _›
using ‹wellformed (name $$ ts)› ‹¬ shadows_consts (name $$ ts)›
proof (induction ts us rule: list.rel_induct)
case (Cons v vs u us)
with constr show ?case
unfolding wellformed.list_comb shadows.list_comb
by (auto simp: consts_list_comb)
qed simp
thus ?case
by (simp add: list_all_iff)
qed auto
end
subsubsection (in special_constants) ‹Correctness wrt @{const veval}›
context vrules begin
text ‹
The following relation can be characterized as follows:
▪ Values have to have the same structure. (We prove an interpretation of @{const value_struct_rel}.)
▪ For closures, the captured environments must agree on constants and variables occurring in the
body.
The first @{typ value} argument is from @{const veval} (i.e. from
@{theory CakeML_Codegen.Big_Step_Value}), the second from @{const veval'}.
›
coinductive vrelated :: "value ⇒ value ⇒ bool" (‹⊢⇩v/ _ ≈ _› [0, 50] 50) where
constr: "list_all2 vrelated ts us ⟹ ⊢⇩v Vconstr name ts ≈ Vconstr name us" |
abs:
"fmrel_on_fset (frees (Sabs cs)) vrelated Γ⇩1 Γ⇩2 ⟹
fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) Γ⇩2 ⟹
⊢⇩v Vabs cs Γ⇩1 ≈ Vabs cs Γ⇩2" |
rec_abs:
"pred_fmap (λcs.
fmrel_on_fset (frees (Sabs cs)) vrelated Γ⇩1 Γ⇩2 ∧
fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) (Γ⇩2 ++⇩f mk_rec_env css Γ⇩2)) css ⟹
name |∈| fmdom css ⟹
⊢⇩v Vrecabs css name Γ⇩1 ≈ Vrecabs css name Γ⇩2"
text ‹
Perhaps unexpectedly, @{term vrelated} is not reflexive. The reason is that it does not just check
syntactic equality including captured environments, but also adherence to the external rules.
›
sublocale vrelated: value_struct_rel vrelated
proof
fix t⇩1 t⇩2
assume "⊢⇩v t⇩1 ≈ t⇩2"
thus "veq_structure t⇩1 t⇩2"
apply (induction t⇩1 arbitrary: t⇩2)
apply (erule vrelated.cases; auto)
apply (erule list.rel_mono_strong)
apply simp
apply (erule vrelated.cases; auto)
apply (erule vrelated.cases; auto)
done
next
fix name name' and ts us :: "value list"
show "⊢⇩v Vconstr name ts ≈ Vconstr name' us ⟷ (name = name' ∧ list_all2 vrelated ts us)"
proof safe
assume "⊢⇩v Vconstr name ts ≈ Vconstr name' us"
thus "name = name'" "list_all2 vrelated ts us"
by (cases; auto)+
qed (auto intro: vrelated.intros)
qed
text ‹
The technically involved relation @{term vrelated} implies a weaker, but more intuitive property:
If @{prop "⊢⇩v t ≈ u"} then ‹t› and ‹u› are equal after termification (i.e. conversion with
@{term value_to_sterm}). In fact, if both terms are ground terms, it collapses to equality. This
follows directly from the interpretation of @{const value_struct_rel}.
›
lemma veval'_correct:
assumes "Γ⇩2 ⊢⇩v t ↓ v⇩2" "wellformed t" "wellformed_venv Γ⇩2"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ⇩2"
assumes "welldefined t"
assumes "fmpred (λ_. vwelldefined) Γ⇩1"
assumes "fmrel_on_fset (frees t) vrelated Γ⇩1 Γ⇩2"
assumes "fmrel_on_fset (consts t) vrelated (fmap_of_list rs) Γ⇩2"
obtains v⇩1 where "rs, Γ⇩1 ⊢⇩v t ↓ v⇩1" "⊢⇩v v⇩1 ≈ v⇩2"
apply atomize_elim
using assms proof (induction arbitrary: Γ⇩1)
case (const name Γ⇩2 val⇩2)
hence "fmrel_on_fset {|name|} vrelated (fmap_of_list rs) Γ⇩2"
by simp
have "rel_option vrelated (fmlookup (fmap_of_list rs) name) (fmlookup Γ⇩2 name)"
apply (rule fmrel_on_fsetD[where S = "{|name|}"])
apply simp
apply fact
done
then obtain val⇩1 where "fmlookup (fmap_of_list rs) name = Some val⇩1" "⊢⇩v val⇩1 ≈ val⇩2"
using const by cases auto
hence "(name, val⇩1) ∈ set rs"
by (auto dest: fmap_of_list_SomeD)
show ?case
apply (intro conjI exI)
apply (rule veval.const)
apply fact+
done
next
case (var Γ⇩2 name val⇩2)
hence "fmrel_on_fset {|name|} vrelated Γ⇩1 Γ⇩2"
by simp
have "rel_option vrelated (fmlookup Γ⇩1 name) (fmlookup Γ⇩2 name)"
apply (rule fmrel_on_fsetD[where S = "{|name|}"])
apply simp
apply fact
done
then obtain val⇩1 where "fmlookup Γ⇩1 name = Some val⇩1" "⊢⇩v val⇩1 ≈ val⇩2"
using var by cases auto
show ?case
apply (intro conjI exI)
apply (rule veval.var)
apply fact+
done
next
case abs
thus ?case
by (auto intro!: veval.abs vrelated.abs)
next
case (comb Γ⇩2 t cs Γ'⇩2 u u'⇩2 env⇩2 pat rhs val⇩2)
hence "∃v. rs, Γ⇩1 ⊢⇩v t ↓ v ∧ ⊢⇩v v ≈ Vabs cs Γ'⇩2"
by (auto intro: fmrel_on_fsubset)
then obtain v where "⊢⇩v v ≈ Vabs cs Γ'⇩2" "rs, Γ⇩1 ⊢⇩v t ↓ v"
by blast
moreover then obtain Γ'⇩1
where "v = Vabs cs Γ'⇩1"
and "fmrel_on_fset (frees (Sabs cs)) vrelated Γ'⇩1 Γ'⇩2"
and "fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) Γ'⇩2"
by cases auto
ultimately have "rs, Γ⇩1 ⊢⇩v t ↓ Vabs cs Γ'⇩1"
by simp
have "∃u⇩1'. rs, Γ⇩1 ⊢⇩v u ↓ u⇩1' ∧ ⊢⇩v u⇩1' ≈ u'⇩2"
using comb by (auto intro: fmrel_on_fsubset)
then obtain u'⇩1 where "⊢⇩v u'⇩1 ≈ u'⇩2" "rs, Γ⇩1 ⊢⇩v u ↓ u'⇩1"
by blast
have "rel_option (rel_prod (fmrel vrelated) (=)) (vfind_match cs u'⇩1) (vfind_match cs u'⇩2)"
by (rule vrelated.vfind_match_rel') fact
then obtain env⇩1 where "vfind_match cs u'⇩1 = Some (env⇩1, pat, rhs)" "fmrel vrelated env⇩1 env⇩2"
using ‹vfind_match cs u'⇩2 = _›
by cases auto
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
have "vwellformed (Vabs cs Γ'⇩2)"
apply (rule veval'_wellformed)
apply fact
using ‹wellformed (t $⇩s u)› apply simp
apply fact+
done
hence "wellformed_venv Γ'⇩2"
by simp
have "vwelldefined v"
apply (rule veval_welldefined)
apply fact+
using comb by simp
hence "vwelldefined (Vabs cs Γ'⇩1)"
unfolding ‹v = _› .
have "linear pat"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ'⇩2)›
by (auto simp: list_all_iff)
have "fmdom env⇩1 = patvars (mk_pat pat)"
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply fact
done
with ‹linear pat› have "fmdom env⇩1 = frees pat"
by (simp add: mk_pat_frees)
have "fmdom env⇩2 = patvars (mk_pat pat)"
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply fact
done
with ‹linear pat› have "fmdom env⇩2 = frees pat"
by (simp add: mk_pat_frees)
note fset_of_list_map[simp del]
have "∃val⇩1. rs, Γ'⇩1 ++⇩f env⇩1 ⊢⇩v rhs ↓ val⇩1 ∧ ⊢⇩v val⇩1 ≈ val⇩2"
proof (rule comb)
show "fmrel_on_fset (frees rhs) vrelated (Γ'⇩1 ++⇩f env⇩1) (Γ'⇩2 ++⇩f env⇩2)"
proof
fix name
assume "name |∈| frees rhs"
show "rel_option vrelated (fmlookup (Γ'⇩1 ++⇩f env⇩1) name) (fmlookup (Γ'⇩2 ++⇩f env⇩2) name)"
proof (cases "name |∈| frees pat")
case True
hence "name |∈| fmdom env⇩1" "name |∈| fmdom env⇩2"
using ‹fmdom env⇩1 = frees pat› ‹fmdom env⇩2 = frees pat›
by simp+
hence "fmlookup (Γ'⇩1 ++⇩f env⇩1) name = fmlookup env⇩1 name" "fmlookup (Γ'⇩2 ++⇩f env⇩2) name = fmlookup env⇩2 name"
by auto
thus ?thesis
using ‹fmrel vrelated env⇩1 env⇩2›
by auto
next
case False
hence "name |∉| fmdom env⇩1" "name |∉| fmdom env⇩2"
using ‹fmdom env⇩1 = frees pat› ‹fmdom env⇩2 = frees pat›
by simp+
hence "fmlookup (Γ'⇩1 ++⇩f env⇩1) name = fmlookup Γ'⇩1 name" "fmlookup (Γ'⇩2 ++⇩f env⇩2) name = fmlookup Γ'⇩2 name"
by auto
moreover have "name |∈| frees (Sabs cs)"
using False ‹name |∈| frees rhs› ‹(pat, rhs) ∈ set cs›
apply (auto simp: ffUnion_alt_def)
apply (rule fBexI[where x = "frees rhs |-| frees pat"])
apply (auto simp: fset_of_list_elem)
done
ultimately show ?thesis
using ‹fmrel_on_fset (frees (Sabs cs)) vrelated Γ'⇩1 Γ'⇩2›
by (auto dest: fmrel_on_fsetD)
qed
qed
next
have "not_shadows_vconsts (Vabs cs Γ'⇩2)"
apply (rule veval'_shadows)
apply fact+
using comb by auto
thus "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
show "not_shadows_vconsts_env (Γ'⇩2 ++⇩f env⇩2)"
apply rule
using ‹not_shadows_vconsts (Vabs cs Γ'⇩2)› apply simp
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
apply fact
apply fact
using comb by auto
show "fmrel_on_fset (consts rhs) vrelated (fmap_of_list rs) (Γ'⇩2 ++⇩f env⇩2)"
proof
fix name
assume "name |∈| consts rhs"
hence "name |∈| consts (Sabs cs)"
using ‹(pat, rhs) ∈ set cs›
by (auto intro!: fBexI simp: fset_of_list_elem ffUnion_alt_def)
hence "rel_option vrelated (fmlookup (fmap_of_list rs) name) (fmlookup Γ'⇩2 name)"
using ‹fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) Γ'⇩2›
by (auto dest: fmrel_on_fsetD)
moreover have "name |∉| fmdom env⇩2"
proof
assume "name |∈| fmdom env⇩2"
hence "fmlookup env⇩2 name ≠ None"
by (meson fmdom_notI)
then obtain v where "fmlookup env⇩2 name = Some v"
by blast
hence "name |∈| fmdom env⇩2"
by (auto intro: fmdomI)
hence "name |∈| frees pat"
using ‹fmdom env⇩2 = frees pat›
by simp
have "welldefined rhs"
using ‹vwelldefined (Vabs cs Γ'⇩1)› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
hence "name |∈| fst |`| fset_of_list rs |∪| C"
using ‹name |∈| consts rhs›
by (auto simp: all_consts_def)
moreover have "¬ shadows_consts pat"
using ‹not_shadows_vconsts (Vabs cs Γ'⇩2)› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff shadows_consts_def all_consts_def)
ultimately show False
using ‹name |∈| frees pat›
unfolding shadows_consts_def fdisjnt_alt_def all_consts_def
by auto
qed
ultimately show "rel_option vrelated (fmlookup (fmap_of_list rs) name) (fmlookup (Γ'⇩2 ++⇩f env⇩2) name)"
by simp
qed
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ'⇩2)›
by (auto simp: list_all_iff)
next
have "wellformed_venv Γ'⇩2"
by fact
moreover have "wellformed_venv env⇩2"
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
apply fact
using ‹wellformed (t $⇩s u)› apply simp
apply fact+
done
ultimately show "wellformed_venv (Γ'⇩2 ++⇩f env⇩2)"
by blast
next
show "welldefined rhs"
using ‹vwelldefined (Vabs cs Γ'⇩1)› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
next
have "fmpred (λ_. vwelldefined) Γ'⇩1"
using ‹vwelldefined (Vabs cs Γ'⇩1)› by simp
moreover have "fmpred (λ_. vwelldefined) env⇩1"
apply (rule vwelldefined.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval_welldefined)
apply fact
apply fact
using comb apply simp
done
ultimately show "fmpred (λ_. vwelldefined) (Γ'⇩1 ++⇩f env⇩1)"
by blast
qed
then obtain val⇩1 where "rs, Γ'⇩1 ++⇩f env⇩1 ⊢⇩v rhs ↓ val⇩1" "⊢⇩v val⇩1 ≈ val⇩2"
by blast
show ?case
apply (intro conjI exI)
apply (rule veval.comb)
apply fact+
done
next
case (rec_comb Γ⇩2 t css name Γ'⇩2 cs u u'⇩2 env⇩2 pat rhs val⇩2)
hence "∃v. rs, Γ⇩1 ⊢⇩v t ↓ v ∧ ⊢⇩v v ≈ Vrecabs css name Γ'⇩2"
by (auto intro: fmrel_on_fsubset)
then obtain v where "⊢⇩v v ≈ Vrecabs css name Γ'⇩2" "rs, Γ⇩1 ⊢⇩v t ↓ v"
by blast
moreover then obtain Γ'⇩1
where "v = Vrecabs css name Γ'⇩1"
and "fmrel_on_fset (frees (Sabs cs)) vrelated Γ'⇩1 Γ'⇩2"
and "fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2)"
using ‹fmlookup css name = Some cs›
by cases auto
ultimately have "rs, Γ⇩1 ⊢⇩v t ↓ Vrecabs css name Γ'⇩1"
by simp
have "∃u⇩1'. rs, Γ⇩1 ⊢⇩v u ↓ u⇩1' ∧ ⊢⇩v u⇩1' ≈ u'⇩2"
using rec_comb by (auto intro: fmrel_on_fsubset)
then obtain u'⇩1 where "⊢⇩v u'⇩1 ≈ u'⇩2" "rs, Γ⇩1 ⊢⇩v u ↓ u'⇩1"
by blast
have "rel_option (rel_prod (fmrel vrelated) (=)) (vfind_match cs u'⇩1) (vfind_match cs u'⇩2)"
by (rule vrelated.vfind_match_rel') fact
then obtain env⇩1 where "vfind_match cs u'⇩1 = Some (env⇩1, pat, rhs)" "fmrel vrelated env⇩1 env⇩2"
using ‹vfind_match cs u'⇩2 = _›
by cases auto
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
have "vwellformed (Vrecabs css name Γ'⇩2)"
apply (rule veval'_wellformed)
apply fact
using ‹wellformed (t $⇩s u)› apply simp
apply fact+
done
hence "wellformed_venv Γ'⇩2" "vwellformed (Vabs cs Γ'⇩2)"
using rec_comb by auto
have "vwelldefined v"
apply (rule veval_welldefined)
apply fact+
using rec_comb by simp
hence "vwelldefined (Vrecabs css name Γ'⇩1)"
unfolding ‹v = _› .
hence "vwelldefined (Vabs cs Γ'⇩1)"
using rec_comb by auto
have "linear pat"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ'⇩2)›
by (auto simp: list_all_iff)
have "fmdom env⇩1 = patvars (mk_pat pat)"
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply fact
done
with ‹linear pat› have "fmdom env⇩1 = frees pat"
by (simp add: mk_pat_frees)
have "fmdom env⇩2 = patvars (mk_pat pat)"
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply fact
done
with ‹linear pat› have "fmdom env⇩2 = frees pat"
by (simp add: mk_pat_frees)
note fset_of_list_map[simp del]
have "∃val⇩1. rs, Γ'⇩1 ++⇩f env⇩1 ⊢⇩v rhs ↓ val⇩1 ∧ ⊢⇩v val⇩1 ≈ val⇩2"
proof (rule rec_comb)
have "not_shadows_vconsts (Vrecabs css name Γ'⇩2)"
apply (rule veval'_shadows)
apply fact+
using rec_comb by auto
thus "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› rec_comb
by (auto simp: list_all_iff)
hence "fdisjnt all_consts (frees rhs)"
by (rule shadows_consts_frees)
have "not_shadows_vconsts_env Γ'⇩2"
using ‹not_shadows_vconsts (Vrecabs css name Γ'⇩2)›
by simp
moreover have "not_shadows_vconsts_env (mk_rec_env css Γ'⇩2)"
unfolding mk_rec_env_def
using ‹not_shadows_vconsts (Vrecabs css name Γ'⇩2)›
by (auto intro: fmdomI)
moreover have "not_shadows_vconsts_env env⇩2"
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
apply fact
apply fact
using rec_comb by auto
ultimately show "not_shadows_vconsts_env (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2)"
by auto
have "not_shadows_vconsts (Vabs cs Γ'⇩2)"
using ‹not_shadows_vconsts (Vrecabs _ _ _)› rec_comb
by auto
show "fmrel_on_fset (frees rhs) vrelated (Γ'⇩1 ++⇩f env⇩1) (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2)"
proof
fix name
assume "name |∈| frees rhs"
moreover have "fmdom css |⊆| all_consts"
using ‹vwelldefined (Vrecabs _ _ _)› unfolding all_consts_def
by auto
ultimately have "name |∉| fmdom css"
using ‹fdisjnt _ (frees rhs)›
unfolding fdisjnt_alt_def
by (metis (full_types) fempty_iff finterI fset_rev_mp)
show "rel_option vrelated (fmlookup (Γ'⇩1 ++⇩f env⇩1) name) (fmlookup (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2) name)"
proof (cases "name |∈| frees pat")
case True
hence "name |∈| fmdom env⇩1" "name |∈| fmdom env⇩2"
using ‹fmdom env⇩1 = frees pat› ‹fmdom env⇩2 = frees pat›
by simp+
hence
"fmlookup (Γ'⇩1 ++⇩f env⇩1) name = fmlookup env⇩1 name"
"fmlookup (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2) name = fmlookup env⇩2 name"
by auto
thus ?thesis
using ‹fmrel vrelated env⇩1 env⇩2›
by auto
next
case False
hence "name |∉| fmdom env⇩1" "name |∉| fmdom env⇩2"
using ‹fmdom env⇩1 = frees pat› ‹fmdom env⇩2 = frees pat›
by simp+
hence
"fmlookup (Γ'⇩1 ++⇩f env⇩1) name = fmlookup Γ'⇩1 name"
"fmlookup (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2) name = fmlookup Γ'⇩2 name"
unfolding mk_rec_env_def using ‹name |∉| fmdom css›
by auto
moreover have "name |∈| frees (Sabs cs)"
using False ‹name |∈| frees rhs› ‹(pat, rhs) ∈ set cs›
apply (auto simp: ffUnion_alt_def)
apply (rule fBexI[where x = "frees rhs |-| frees pat"])
apply (auto simp: fset_of_list_elem)
done
ultimately show ?thesis
using ‹fmrel_on_fset (frees (Sabs cs)) vrelated Γ'⇩1 Γ'⇩2›
by (auto dest: fmrel_on_fsetD)
qed
qed
show "fmrel_on_fset (consts rhs) vrelated (fmap_of_list rs) (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2)"
proof
fix name
assume "name |∈| consts rhs"
hence "name |∈| consts (Sabs cs)"
using ‹(pat, rhs) ∈ set cs›
by (auto intro!: fBexI simp: fset_of_list_elem ffUnion_alt_def)
hence "rel_option vrelated (fmlookup (fmap_of_list rs) name) (fmlookup (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2) name)"
using ‹fmrel_on_fset (consts (Sabs cs)) vrelated (fmap_of_list rs) (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2)›
by (auto dest: fmrel_on_fsetD)
moreover have "name |∉| fmdom env⇩2"
proof
assume "name |∈| fmdom env⇩2"
hence "fmlookup env⇩2 name ≠ None"
by (meson fmdom_notI)
then obtain v where "fmlookup env⇩2 name = Some v"
by blast
hence "name |∈| fmdom env⇩2"
by (auto intro: fmdomI)
hence "name |∈| frees pat"
using ‹fmdom env⇩2 = frees pat›
by simp
have "vwelldefined (Vabs cs Γ'⇩1)"
using ‹vwelldefined (Vrecabs css _ Γ'⇩1)›
using rec_comb
by auto
hence "welldefined rhs"
using ‹(pat, rhs) ∈ set cs› rec_comb
by (auto simp: list_all_iff)
hence "name |∈| fst |`| fset_of_list rs |∪| C"
using ‹name |∈| consts rhs› all_consts_def
by blast
moreover have "¬ shadows_consts pat"
using ‹not_shadows_vconsts (Vabs cs Γ'⇩2)› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff shadows_consts_def all_consts_def)
ultimately show False
using ‹name |∈| frees pat›
unfolding shadows_consts_def fdisjnt_alt_def all_consts_def
by auto
qed
ultimately show "rel_option vrelated (fmlookup (fmap_of_list rs) name) (fmlookup (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2) name)"
by simp
qed
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ'⇩2)›
by (auto simp: list_all_iff)
next
have "wellformed_venv Γ'⇩2"
by fact
moreover have "wellformed_venv env⇩2"
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
apply fact
using ‹wellformed (t $⇩s u)› apply simp
apply fact+
done
moreover have "wellformed_venv (mk_rec_env css Γ'⇩2)"
unfolding mk_rec_env_def
using ‹vwellformed (Vrecabs _ _ _)›
by (auto intro: fmdomI)
ultimately show "wellformed_venv (Γ'⇩2 ++⇩f mk_rec_env css Γ'⇩2 ++⇩f env⇩2)"
by blast
next
show "welldefined rhs"
using ‹vwelldefined (Vabs cs Γ'⇩1)› ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
next
have "fmpred (λ_. vwelldefined) Γ'⇩1"
using ‹vwelldefined (Vabs cs Γ'⇩1)› by simp
moreover have "fmpred (λ_. vwelldefined) env⇩1"
apply (rule vwelldefined.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval_welldefined)
apply fact
apply fact
using rec_comb apply simp
done
ultimately show "fmpred (λ_. vwelldefined) (Γ'⇩1 ++⇩f env⇩1)"
by blast
qed
then obtain val⇩1 where "rs, Γ'⇩1 ++⇩f env⇩1 ⊢⇩v rhs ↓ val⇩1" "⊢⇩v val⇩1 ≈ val⇩2"
by blast
show ?case
apply (intro conjI exI)
apply (rule veval.rec_comb)
apply fact+
done
next
case (constr name Γ⇩2 ts us⇩2)
have "list_all2 (λt u⇩2. (∃u⇩1. rs, Γ⇩1 ⊢⇩v t ↓ u⇩1 ∧ ⊢⇩v u⇩1 ≈ u⇩2)) ts us⇩2"
using ‹list_all2 _ ts us⇩2›
proof (rule list.rel_mono_strong, elim conjE impE allE exE)
fix t u⇩2
assume "t ∈ set ts" "u⇩2 ∈ set us⇩2"
assume "Γ⇩2 ⊢⇩v t ↓ u⇩2"
show "wellformed t" "welldefined t" "¬ shadows_consts t"
using constr ‹t ∈ set ts›
unfolding welldefined.list_comb wellformed.list_comb shadows.list_comb
by (auto simp: list_all_iff list_ex_iff)
show
"wellformed_venv Γ⇩2"
"not_shadows_vconsts_env Γ⇩2"
"fmpred (λ_. vwelldefined) Γ⇩1"
by fact+
have "consts t |∈| fset_of_list (map consts ts)"
using ‹t ∈ set ts› by (simp add: fset_of_list_elem)
hence "consts t |⊆| consts (name $$ ts)"
unfolding consts_list_comb
by (metis ffUnion_subset_elem le_supI2)
thus "fmrel_on_fset (consts t) vrelated (fmap_of_list rs) Γ⇩2"
using constr by (blast intro: fmrel_on_fsubset)
have "frees t |∈| fset_of_list (map frees ts)"
using ‹t ∈ set ts› by (simp add: fset_of_list_elem)
hence "frees t |⊆| frees (name $$ ts)"
unfolding frees_list_comb const_sterm_def freess_def
by (auto intro!: ffUnion_subset_elem)
thus "fmrel_on_fset (frees t) vrelated Γ⇩1 Γ⇩2"
using constr by (blast intro: fmrel_on_fsubset)
qed auto
then obtain us⇩1 where "list_all2 (veval rs Γ⇩1) ts us⇩1" "list_all2 vrelated us⇩1 us⇩2"
by induction auto
thus ?case
using constr
by (auto intro: veval.constr vrelated.constr)
qed
lemma veval'_correct':
assumes "Γ⇩2 ⊢⇩v t ↓ v⇩2" "wellformed t" "wellformed_venv Γ⇩2"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ⇩2"
assumes "welldefined t"
assumes "closed t"
assumes "fmrel_on_fset (consts t) vrelated (fmap_of_list rs) Γ⇩2"
obtains v⇩1 where "rs, fmempty ⊢⇩v t ↓ v⇩1" "⊢⇩v v⇩1 ≈ v⇩2"
proof (rule veval'_correct[where Γ⇩1 = fmempty])
show "fmpred (λ_. vwelldefined) fmempty" by simp
next
show "fmrel_on_fset (frees t) vrelated fmempty Γ⇩2"
using ‹closed t› unfolding closed_except_def by auto
qed (rule assms)+
end
subsubsection ‹Preservation of extensional equality›
lemma (in constants) veval'_agree_eq:
assumes "Γ ⊢⇩v t ↓ v" "fmrel_on_fset (ids t) erelated Γ' Γ"
assumes "closed_venv Γ" "closed_except t (fmdom Γ)"
assumes "wellformed t" "wellformed_venv Γ" "fdisjnt C (fmdom Γ)"
assumes "consts t |⊆| fmdom Γ |∪| C" "fmpred (λ_. vwelldefined') Γ"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ"
obtains v' where "Γ' ⊢⇩v t ↓ v'" "v' ≈⇩e v"
using assms proof (induction arbitrary: Γ' thesis)
case (const name Γ val)
hence "name |∈| ids (Sconst name)"
unfolding ids_def by simp
with const have "rel_option erelated (fmlookup Γ' name) (fmlookup Γ name)"
by (auto dest: fmrel_on_fsetD)
then obtain val' where "fmlookup Γ' name = Some val'" "val' ≈⇩e val"
using ‹fmlookup Γ name = Some val›
by cases auto
thus ?case
using const by (auto intro: veval'.const)
next
case (var Γ name val)
hence "name |∈| ids (Svar name)"
unfolding ids_def by simp
with var have "rel_option erelated (fmlookup Γ' name) (fmlookup Γ name)"
by (auto dest: fmrel_on_fsetD)
then obtain val' where "fmlookup Γ' name = Some val'" "val' ≈⇩e val"
using ‹fmlookup Γ name = Some val›
by cases auto
thus ?case
using var by (auto intro: veval'.var)
next
case (abs Γ cs)
hence "Vabs cs Γ' ≈⇩e Vabs cs Γ"
by (auto intro: erelated.abs)
thus ?case
using abs by (auto intro: veval'.abs)
next
case (comb Γ t cs Γ⇩Λ u v⇩2 env pat rhs val)
have "fmrel_on_fset (ids t) erelated Γ' Γ"
apply (rule fmrel_on_fsubset)
apply fact
unfolding ids_def by auto
then obtain v⇩1' where "Γ' ⊢⇩v t ↓ v⇩1'" "v⇩1' ≈⇩e Vabs cs Γ⇩Λ"
using comb by (auto simp: closed_except_def)
then obtain Γ⇩Λ' where "v⇩1' = Vabs cs Γ⇩Λ'" "fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ"
by (auto elim: erelated.cases)
have "fmrel_on_fset (ids u) erelated Γ' Γ"
apply (rule fmrel_on_fsubset)
apply fact
unfolding ids_def by auto
then obtain v⇩2' where "Γ' ⊢⇩v u ↓ v⇩2'" "v⇩2' ≈⇩e v⇩2"
apply -
apply (erule comb.IH(2))
using comb by (auto simp: closed_except_def)
have "rel_option (rel_prod (fmrel erelated) (=)) (vfind_match cs v⇩2') (vfind_match cs v⇩2)"
using ‹v⇩2' ≈⇩e v⇩2› by (rule erelated.vfind_match_rel')
then obtain env' where "fmrel erelated env' env" "vfind_match cs v⇩2' = Some (env', pat, rhs)"
using comb by cases auto
have "vclosed (Vabs cs Γ⇩Λ)"
apply (rule veval'_closed)
using comb by (auto simp: closed_except_def)
have "vclosed v⇩2"
apply (rule veval'_closed)
using comb by (auto simp: closed_except_def)
have "closed_except (Sabs cs) (fmdom Γ⇩Λ)"
using ‹vclosed (Vabs cs Γ⇩Λ)› by (auto simp: Sterm.closed_except_simps)
hence "frees (Sabs cs) |⊆| fmdom Γ⇩Λ"
unfolding closed_except_def .
have "vwellformed (Vabs cs Γ⇩Λ)"
apply (rule veval'_wellformed)
apply fact
using comb by auto
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
hence "linear pat"
using ‹vwellformed (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
hence "frees pat = patvars (mk_pat pat)"
by (simp add: mk_pat_frees)
hence "fmdom env = frees pat"
apply simp
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply (rule comb)
done
have "vwelldefined' (Vabs cs Γ⇩Λ)"
apply (rule veval'_welldefined')
apply fact
using comb by auto
hence "consts rhs |⊆| fmdom Γ⇩Λ |∪| C" "fdisjnt C (fmdom Γ⇩Λ)"
using ‹(pat, rhs) ∈ set cs›
by (auto simp: list_all_iff)
have "not_shadows_vconsts (Vabs cs Γ⇩Λ)"
apply (rule veval'_shadows)
using comb by auto
obtain val' where "Γ⇩Λ' ++⇩f env' ⊢⇩v rhs ↓ val'" "val' ≈⇩e val"
proof (erule comb.IH)
show "closed_venv (Γ⇩Λ ++⇩f env)"
apply rule
using ‹vclosed (Vabs cs Γ⇩Λ)› apply simp
apply (rule vclosed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply fact
done
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
next
show "wellformed_venv (Γ⇩Λ ++⇩f env)"
apply rule
using ‹vwellformed (Vabs cs Γ⇩Λ)› apply simp
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply (rule comb)
apply (rule veval'_wellformed)
apply fact
using comb by auto
next
show "closed_except rhs (fmdom (Γ⇩Λ ++⇩f env))"
using ‹(pat, rhs) ∈ set cs› ‹vclosed (Vabs cs Γ⇩Λ)› ‹fmdom env = frees pat›
by (auto simp: list_all_iff)
have "fmdom env = fmdom env'"
using ‹fmrel erelated env' env›
by (metis fmrel_fmdom_eq)
show "fmrel_on_fset (ids rhs) erelated (Γ⇩Λ' ++⇩f env') (Γ⇩Λ ++⇩f env)"
proof
fix id
assume "id |∈| ids rhs"
thus "rel_option erelated (fmlookup (Γ⇩Λ' ++⇩f env') id) (fmlookup (Γ⇩Λ ++⇩f env) id)"
unfolding ids_def
proof (cases rule: funion_strictE)
case A
hence "id |∈| fmdom env |∪| fmdom Γ⇩Λ"
using ‹closed_except rhs (fmdom (Γ⇩Λ ++⇩f env))›
unfolding closed_except_def
by auto
thus ?thesis
proof (cases rule: funion_strictE)
case A
hence "id |∈| fmdom env'"
using ‹fmdom env = frees pat› ‹fmdom env = fmdom env'› by simp
with A show ?thesis
using ‹fmrel erelated env' env› by auto
next
case B
hence "id |∉| frees pat"
using ‹fmdom env = frees pat› by simp
hence "id |∈| frees (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
using ‹id |∈| frees rhs› apply simp
unfolding fset_of_list_elem
apply (rule ‹(pat, rhs) ∈ set cs›)
done
hence "id |∈| ids (Sabs cs)"
unfolding ids_def by simp
have "id |∉| fmdom env'"
using B unfolding ‹fmdom env = fmdom env'› by simp
thus ?thesis
using ‹id |∉| fmdom env›
apply simp
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids (Sabs cs)›)
apply (rule ‹fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ›)
done
qed
next
case B
have "id |∈| consts (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply simp
apply fact
unfolding fset_of_list_elem
apply (rule ‹(pat, rhs) ∈ set cs›)
done
hence "id |∈| ids (Sabs cs)"
unfolding ids_def by auto
show ?thesis
using ‹fmdom env = fmdom env'›
apply auto
apply (rule fmrelD)
apply (rule ‹fmrel erelated env' env›)
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids (Sabs cs)›)
apply (rule ‹fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ›)
done
qed
qed
next
show "fmpred (λ_. vwelldefined') (Γ⇩Λ ++⇩f env)"
proof
have "vwelldefined' (Vabs cs Γ⇩Λ)"
apply (rule veval'_welldefined')
apply fact
using comb by auto
thus "fmpred (λ_. vwelldefined') Γ⇩Λ"
by simp
next
have "vwelldefined' v⇩2"
apply (rule veval'_welldefined')
apply fact
using comb by auto
show "fmpred (λ_. vwelldefined') env"
apply (rule vmatch_welldefined')
apply (rule vfind_match_elem)
apply fact+
done
qed
next
have "fdisjnt C (fmdom Γ⇩Λ)"
using ‹vwelldefined' (Vabs cs Γ⇩Λ)› by simp
moreover have "fdisjnt C (fmdom env)"
unfolding ‹fmdom env = _›
using ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff all_consts_def fdisjnt_alt_def)
ultimately show "fdisjnt C (fmdom (Γ⇩Λ ++⇩f env))"
unfolding fdisjnt_alt_def by auto
next
show "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
next
have "not_shadows_vconsts_env Γ⇩Λ"
using ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)› by auto
moreover have "not_shadows_vconsts_env env"
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
using comb by auto
ultimately show "not_shadows_vconsts_env (Γ⇩Λ ++⇩f env)"
by blast
next
show "consts rhs |⊆| fmdom (Γ⇩Λ ++⇩f env) |∪| C"
using ‹consts rhs |⊆| _›
by auto
qed
moreover have "Γ' ⊢⇩v t $⇩s u ↓ val'"
proof (rule veval'.comb)
show "Γ' ⊢⇩v t ↓ Vabs cs Γ⇩Λ'"
using ‹Γ' ⊢⇩v t ↓ v⇩1'›
unfolding ‹v⇩1' = _› .
qed fact+
ultimately show ?case
using comb by metis
next
case (rec_comb Γ t css name Γ⇩Λ cs u v⇩2 env pat rhs val)
have "fmrel_on_fset (ids t) erelated Γ' Γ"
apply (rule fmrel_on_fsubset)
apply fact
unfolding ids_def by auto
then obtain v⇩1' where "Γ' ⊢⇩v t ↓ v⇩1'" "v⇩1' ≈⇩e Vrecabs css name Γ⇩Λ"
using rec_comb by (auto simp: closed_except_def)
then obtain Γ⇩Λ'
where "v⇩1' = Vrecabs css name Γ⇩Λ'"
and "pred_fmap (λcs. fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ) css"
by (auto elim: erelated.cases)
have "fmrel_on_fset (ids u) erelated Γ' Γ"
apply (rule fmrel_on_fsubset)
apply fact
unfolding ids_def by auto
then obtain v⇩2' where "Γ' ⊢⇩v u ↓ v⇩2'" "v⇩2' ≈⇩e v⇩2"
apply -
apply (erule rec_comb.IH(2))
using rec_comb by (auto simp: closed_except_def)
have "rel_option (rel_prod (fmrel erelated) (=)) (vfind_match cs v⇩2') (vfind_match cs v⇩2)"
using ‹v⇩2' ≈⇩e v⇩2› by (rule erelated.vfind_match_rel')
then obtain env' where "fmrel erelated env' env" "vfind_match cs v⇩2' = Some (env', pat, rhs)"
using rec_comb by cases auto
have "vclosed (Vrecabs css name Γ⇩Λ)"
apply (rule veval'_closed)
using rec_comb by (auto simp: closed_except_def)
hence "vclosed (Vabs cs Γ⇩Λ)"
using rec_comb by (auto simp: closed_except_def)
have "vclosed v⇩2"
apply (rule veval'_closed)
using rec_comb by (auto simp: closed_except_def)
have "closed_except (Sabs cs) (fmdom Γ⇩Λ)"
using ‹vclosed (Vabs cs Γ⇩Λ)› by (auto simp: Sterm.closed_except_simps)
hence "frees (Sabs cs) |⊆| fmdom Γ⇩Λ"
unfolding closed_except_def .
have "vwellformed (Vrecabs css name Γ⇩Λ)"
apply (rule veval'_wellformed)
apply fact
using rec_comb by auto
hence "vwellformed (Vabs cs Γ⇩Λ)"
using rec_comb by (auto simp: closed_except_def)
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
hence "linear pat"
using ‹vwellformed (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
hence "frees pat = patvars (mk_pat pat)"
by (simp add: mk_pat_frees)
hence "fmdom env = frees pat"
apply simp
apply (rule vmatch_dom)
apply (rule vfind_match_elem)
apply (rule rec_comb)
done
have "vwelldefined' (Vrecabs css name Γ⇩Λ)"
apply (rule veval'_welldefined')
apply fact
using rec_comb by auto
hence "consts rhs |⊆| fmdom Γ⇩Λ |∪| (C |∪| fmdom css)" "fdisjnt C (fmdom Γ⇩Λ)"
using ‹(pat, rhs) ∈ set cs› ‹fmlookup css name = Some cs›
by (auto simp: list_all_iff dest!: fmpredD[where m = css])
have "not_shadows_vconsts (Vrecabs css name Γ⇩Λ)"
apply (rule veval'_shadows)
using rec_comb by auto
hence "not_shadows_vconsts (Vabs cs Γ⇩Λ)"
using rec_comb by auto
obtain val' where "Γ⇩Λ' ++⇩f mk_rec_env css Γ⇩Λ' ++⇩f env' ⊢⇩v rhs ↓ val'" "val' ≈⇩e val"
proof (erule rec_comb.IH)
show "closed_venv (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env)"
apply rule
apply rule
using ‹vclosed (Vabs cs Γ⇩Λ)› apply simp
unfolding mk_rec_env_def
using ‹vclosed (Vrecabs css name Γ⇩Λ)› apply (auto intro: fmdomI)[]
apply (rule vclosed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply fact
done
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹vwellformed (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
next
show "wellformed_venv (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env)"
apply rule
apply rule
using ‹vwellformed (Vabs cs Γ⇩Λ)› apply simp
unfolding mk_rec_env_def
using ‹vwellformed (Vrecabs css name Γ⇩Λ)› apply (auto intro: fmdomI)[]
apply (rule vwellformed.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_wellformed)
apply fact
using rec_comb by auto
next
have "closed_except rhs (fmdom (Γ⇩Λ ++⇩f env))"
using ‹(pat, rhs) ∈ set cs› ‹vclosed (Vabs cs Γ⇩Λ)› ‹fmdom env = frees pat›
by (auto simp: list_all_iff closed_except_def)
thus "closed_except rhs (fmdom (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env))"
unfolding closed_except_def
by auto
have "fmdom env = fmdom env'"
using ‹fmrel erelated env' env›
by (metis fmrel_fmdom_eq)
have "fmrel_on_fset (ids rhs) erelated (mk_rec_env css Γ⇩Λ') (mk_rec_env css Γ⇩Λ)"
unfolding mk_rec_env_def
apply rule
apply simp
unfolding option.rel_map
apply (rule option.rel_refl)
apply (rule erelated.intros)
apply (rule ‹pred_fmap (λcs. fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ) css›)
done
have "fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ"
using ‹pred_fmap (λcs. fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ) css› rec_comb
by auto
have "fmdom (mk_rec_env css Γ⇩Λ) = fmdom (mk_rec_env css Γ⇩Λ')"
unfolding mk_rec_env_def by auto
show "fmrel_on_fset (ids rhs) erelated (Γ⇩Λ' ++⇩f mk_rec_env css Γ⇩Λ' ++⇩f env') (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env)"
proof
fix id
assume "id |∈| ids rhs"
thus "rel_option erelated (fmlookup (Γ⇩Λ' ++⇩f mk_rec_env css Γ⇩Λ' ++⇩f env') id) (fmlookup (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env) id)"
unfolding ids_def
proof (cases rule: funion_strictE)
case A
hence "id |∈| fmdom env |∪| fmdom Γ⇩Λ"
using ‹closed_except rhs (fmdom (Γ⇩Λ ++⇩f env))›
unfolding closed_except_def
by auto
thus ?thesis
proof (cases rule: funion_strictE)
case A
hence "id |∈| fmdom env'"
using ‹fmdom env = frees pat› ‹fmdom env = fmdom env'› by simp
with A show ?thesis
using ‹fmrel erelated env' env› by auto
next
case B
hence "id |∉| frees pat"
using ‹fmdom env = frees pat› by simp
hence "id |∈| frees (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
using ‹id |∈| frees rhs› apply simp
unfolding fset_of_list_elem
apply (rule ‹(pat, rhs) ∈ set cs›)
done
hence "id |∈| ids (Sabs cs)"
unfolding ids_def by simp
have "id |∉| fmdom env'"
using B unfolding ‹fmdom env = fmdom env'› by simp
thus ?thesis
using ‹id |∉| fmdom env› ‹fmdom (mk_rec_env css Γ⇩Λ) = fmdom (mk_rec_env css Γ⇩Λ')›
apply auto
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids rhs›)
apply (rule ‹fmrel_on_fset (ids rhs) erelated (mk_rec_env css Γ⇩Λ') (mk_rec_env css Γ⇩Λ)›)
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids (Sabs cs)›)
apply (rule ‹fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ›)
done
qed
next
case B
have "id |∈| consts (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply simp
apply fact
unfolding fset_of_list_elem
apply (rule ‹(pat, rhs) ∈ set cs›)
done
hence "id |∈| ids (Sabs cs)"
unfolding ids_def by auto
show ?thesis
using ‹fmdom env = fmdom env'› ‹fmdom (mk_rec_env css Γ⇩Λ) = fmdom (mk_rec_env css Γ⇩Λ')›
apply auto
apply (rule fmrelD)
apply (rule ‹fmrel erelated env' env›)
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids rhs›)
apply (rule ‹fmrel_on_fset (ids rhs) erelated (mk_rec_env css Γ⇩Λ') (mk_rec_env css Γ⇩Λ)›)
apply (rule fmrelD)
apply (rule ‹fmrel erelated env' env›)
apply (rule fmrel_on_fsetD)
apply (rule ‹id |∈| ids (Sabs cs)›)
apply (rule ‹fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩Λ' Γ⇩Λ›)
done
qed
qed
next
show "fmpred (λ_. vwelldefined') (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env)"
proof (intro fmpred_add)
have "vwelldefined' (Vrecabs css name Γ⇩Λ)"
apply (rule veval'_welldefined')
apply fact
using rec_comb by auto
thus "fmpred (λ_. vwelldefined') Γ⇩Λ" "fmpred (λ_. vwelldefined') (mk_rec_env css Γ⇩Λ)"
unfolding mk_rec_env_def
by (auto intro: fmdomI)
next
have "vwelldefined' v⇩2"
apply (rule veval'_welldefined')
apply fact
using rec_comb by auto
show "fmpred (λ_. vwelldefined') env"
apply (rule vmatch_welldefined')
apply (rule vfind_match_elem)
apply fact+
done
qed
next
have "fdisjnt C (fmdom env)"
unfolding ‹fmdom env = _›
using ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff all_consts_def fdisjnt_alt_def)
moreover have "fdisjnt C (fmdom css)"
using ‹vwelldefined' (Vrecabs css name Γ⇩Λ)› by simp
ultimately show "fdisjnt C (fmdom (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env))"
using ‹fdisjnt C (fmdom Γ⇩Λ)›
unfolding fdisjnt_alt_def mk_rec_env_def by auto
next
show "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)›
by (auto simp: list_all_iff)
next
have "not_shadows_vconsts_env Γ⇩Λ"
using ‹not_shadows_vconsts (Vabs cs Γ⇩Λ)› by auto
moreover have "not_shadows_vconsts_env env"
apply (rule not_shadows_vconsts.vmatch_env)
apply (rule vfind_match_elem)
apply fact
apply (rule veval'_shadows)
using rec_comb by auto
moreover have "not_shadows_vconsts_env (mk_rec_env css Γ⇩Λ)"
unfolding mk_rec_env_def
using ‹not_shadows_vconsts (Vrecabs css name Γ⇩Λ)›
by (auto intro: fmdomI)
ultimately show "not_shadows_vconsts_env (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env)"
by blast
next
show "consts rhs |⊆| fmdom (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env) |∪| C"
using ‹consts rhs |⊆| _› unfolding mk_rec_env_def
by auto
qed
moreover have "Γ' ⊢⇩v t $⇩s u ↓ val'"
proof (rule veval'.rec_comb)
show "Γ' ⊢⇩v t ↓ Vrecabs css name Γ⇩Λ'"
using ‹Γ' ⊢⇩v t ↓ v⇩1'›
unfolding ‹v⇩1' = _› .
qed fact+
ultimately show ?case
using rec_comb by metis
next
case (constr name Γ ts us)
have "list_all (λt. fmrel_on_fset (ids t) erelated Γ' Γ ∧ closed_except t (fmdom Γ) ∧ wellformed t ∧ consts t |⊆| fmdom Γ |∪| C ∧ ¬ shadows_consts t) ts"
apply (rule list_allI)
apply rule
apply (rule fmrel_on_fsubset)
apply (rule constr)
subgoal
unfolding ids_list_comb
by (induct ts; auto)
subgoal
apply (intro conjI)
subgoal
using ‹closed_except (name $$ ts) (fmdom Γ)›
unfolding closed.list_comb by (auto simp: list_all_iff)
subgoal
using ‹wellformed (name $$ ts)›
unfolding wellformed.list_comb by (auto simp: list_all_iff)
subgoal
using ‹consts (name $$ ts) |⊆| fmdom Γ |∪| C›
unfolding consts_list_comb
by (metis Ball_set constr.prems(8) special_constants.sconsts_list_comb)
subgoal
using ‹¬ shadows_consts (name $$ ts)›
unfolding shadows.list_comb by (auto simp: list_ex_iff)
done
done
obtain us' where "list_all3 (λt u u'. Γ' ⊢⇩v t ↓ u' ∧ u' ≈⇩e u) ts us us'"
using ‹list_all2 _ _ _› ‹list_all _ ts›
proof (induction arbitrary: thesis rule: list.rel_induct)
case (Cons t ts u us)
then obtain us' where "list_all3 (λt u u'. Γ' ⊢⇩v t ↓ u' ∧ u' ≈⇩e u) ts us us'"
by auto
have
"fmrel_on_fset (ids t) erelated Γ' Γ" "closed_except t (fmdom Γ)"
"wellformed t" "consts t |⊆| fmdom Γ |∪| C" "¬ shadows_consts t"
using Cons by auto
then obtain u' where "Γ' ⊢⇩v t ↓ u'" "u' ≈⇩e u"
using ‹closed_venv Γ› ‹wellformed_venv Γ› ‹fdisjnt C (fmdom Γ)› ‹fmpred (λ_. vwelldefined') Γ›
using ‹not_shadows_vconsts_env Γ› Cons.hyps
by blast
show ?case
apply (rule Cons.prems)
apply (rule list_all3_cons)
apply fact
apply (rule conjI)
apply fact+
done
qed auto
show ?case
apply (rule constr.prems)
apply (rule veval'.constr[where us = us'])
apply fact
using ‹list_all3 _ ts us us'›
apply (induct; auto)
apply (rule erelated.intros)
using ‹list_all3 _ ts us us'›
apply (induct; auto)
done
qed
end