Theory CakeML_Correctness
subsection ‹Correctness of compilation›
theory CakeML_Correctness
imports
CakeML_Backend
"../Rewriting/Big_Step_Value_ML"
begin
context cakeml' begin
lemma mk_rec_env_related:
assumes "fmrel (λcs (n, e). related_fun cs n e) css (fmap_of_list (map (map_prod Name (map_prod Name id)) funs))"
assumes "fmrel_on_fset (fbind (fmran css) (ids ∘ Sabs)) related_v Γ⇩Λ (fmap_of_ns (sem_env.v env⇩Λ))"
shows "fmrel related_v (mk_rec_env css Γ⇩Λ) (cake_mk_rec_env funs env⇩Λ)"
proof (rule fmrelI)
fix name
have "rel_option (λcs (n, e). related_fun cs n e) (fmlookup css name) (map_of (map (map_prod Name (map_prod Name id)) funs) name)"
using assms by (auto simp: fmap_of_list.rep_eq)
then have "rel_option (λcs (n, e). related_fun cs (Name n) e) (fmlookup css name) (map_of funs (as_string name))"
unfolding name.map_of_rekey'
by cases auto
have *: "related_v (Vrecabs css name Γ⇩Λ) (Recclosure env⇩Λ funs (as_string name))"
using assms by (auto intro: related_v.rec_closure)
show "rel_option related_v (fmlookup (mk_rec_env css Γ⇩Λ) name) (fmlookup (cake_mk_rec_env funs env⇩Λ) name)"
unfolding mk_rec_env_def cake_mk_rec_env_def fmap_of_list.rep_eq
apply (simp add: map_of_map_keyed name.map_of_rekey option.rel_map)
apply (rule option.rel_mono_strong)
apply fact
apply (rule *)
done
qed
lemma mk_exp_correctness:
"ids t |⊆| S ⟹ all_consts |⊆| S ⟹ ¬ shadows_consts t ⟹ related_exp t (mk_exp S t)"
"ids (Sabs cs) |⊆| S ⟹ all_consts |⊆| S ⟹ ¬ shadows_consts (Sabs cs) ⟹ list_all2 (rel_prod related_pat related_exp) cs (mk_clauses S cs)"
"ids t |⊆| S ⟹ all_consts |⊆| S ⟹ ¬ shadows_consts t ⟹ related_exp t (mk_con S t)"
proof (induction rule: mk_exp_mk_clauses_mk_con.induct)
case (2 S name)
show ?case
proof (cases "name |∈| C")
case True
hence "related_exp (name $$ []) (mk_exp S (Sconst name))"
by (auto intro: related_exp.intros simp del: list_comb.simps)
thus ?thesis
by (simp add: const_sterm_def)
qed (auto intro: related_exp.intros)
next
case (4 S cs)
have "fresh_fNext (S |∪| all_consts) |∉| S |∪| all_consts"
by (rule fNext_not_member)
hence "fresh_fNext S |∉| S |∪| all_consts"
using ‹all_consts |⊆| S› by (simp add: sup_absorb1)
hence "fresh_fNext S |∉| ids (Sabs cs) |∪| all_consts"
using 4 by auto
show ?case
apply (simp add: Let_def)
apply (rule related_exp.fun)
apply (rule "4.IH"[unfolded mk_clauses.simps])
apply (rule refl)
apply fact+
using ‹fresh_fNext S |∉| ids (Sabs cs) |∪| all_consts› by auto
next
case (5 S t)
show ?case
apply (simp add: mk_con.simps split!: prod.splits sterm.splits if_splits)
subgoal premises prems for args c
proof -
from prems have "t = c $$ args"
apply (fold const_sterm_def)
by (metis fst_conv list_strip_comb snd_conv)
show ?thesis
unfolding ‹t = _›
apply (rule related_exp.constr)
apply fact
apply (simp add: list.rel_map)
apply (rule list.rel_refl_strong)
apply (rule 5(1))
apply (rule prems(1)[symmetric])
apply (rule refl)
subgoal by (rule prems)
subgoal by assumption
subgoal
using ‹ids t |⊆| S› unfolding ‹t = _›
apply (auto simp: ids_list_comb)
by (meson ffUnion_subset_elem fimage_eqI fset_of_list_elem fset_rev_mp)
subgoal by (rule 5)
subgoal
using ‹¬ shadows_consts t› unfolding ‹t = _›
unfolding shadows.list_comb
by (auto simp: list_ex_iff)
done
qed
using 5 by (auto split: prod.splits sterm.splits)
next
case (6 S cs)
have "list_all2 (λx y. rel_prod related_pat related_exp x (case y of (pat, t) ⇒ (mk_ml_pat (mk_pat pat), mk_con (frees pat |∪| S) t))) cs cs"
proof (rule list.rel_refl_strong, safe intro!: rel_prod.intros)
fix pat rhs
assume "(pat, rhs) ∈ set cs"
hence "consts rhs |⊆| S"
using ‹ids (Sabs cs) |⊆| S›
unfolding ids_def
apply auto
apply (drule ffUnion_least_rev)+
apply (auto simp: fset_of_list_elem elim!: fBallE)
done
have "frees rhs |⊆| frees pat |∪| S"
using ‹ids (Sabs cs) |⊆| S› ‹(pat, rhs) ∈ set cs›
unfolding ids_def
apply auto
apply (drule ffUnion_least_rev)+
apply (auto simp: fset_of_list_elem elim!: fBallE)
done
have "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› 6
by (auto simp: list_ex_iff)
show "related_exp rhs (mk_con (frees pat |∪| S) rhs)"
apply (rule 6)
apply fact
subgoal by simp
subgoal
unfolding ids_def
using ‹consts rhs |⊆| S› ‹frees rhs |⊆| frees pat |∪| S›
by auto
subgoal using 6(3) by auto
subgoal by fact
done
qed
thus ?case
by (simp add: list.rel_map)
qed (auto intro: related_exp.intros simp: ids_def fdisjnt_alt_def)
context begin
private lemma semantic_correctness0:
fixes exp
assumes "cupcake_evaluate_single env exp r" "is_cupcake_all_env env"
assumes "fmrel_on_fset (ids t) related_v Γ (fmap_of_ns (sem_env.v env))"
assumes "related_exp t exp"
assumes "wellformed t" "wellformed_venv Γ"
assumes "closed_venv Γ" "closed_except t (fmdom Γ)"
assumes "fmpred (λ_. vwelldefined') Γ" "consts t |⊆| fmdom Γ |∪| C"
assumes "fdisjnt C (fmdom Γ)"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ"
shows "if_rval (λml_v. ∃v. Γ ⊢⇩v t ↓ v ∧ related_v v ml_v) r"
using assms proof (induction arbitrary: Γ t)
case (con1 env cn es ress ml_vs ml_v')
obtain name ts where "cn = Some (Short (as_string name))" "name |∈| C" "t = name $$ ts" "list_all2 related_exp ts es"
using ‹related_exp t (Con cn es)›
by cases auto
with con1 obtain tid where "ml_v' = Conv (Some (id_to_n (Short (as_string name)), tid)) (rev ml_vs)"
by (auto split: option.splits)
have "ress = map Rval ml_vs"
using con1 by auto
define ml_vs' where "ml_vs' = rev ml_vs"
note IH = ‹list_all2_shortcircuit _ _ _›[
unfolded ‹ress = _› list_all2_shortcircuit_rval list_all2_rev1,
folded ml_vs'_def]
moreover have
"list_all wellformed ts" "list_all (λt. ¬ shadows_consts t) ts"
"list_all (λt. consts t |⊆| fmdom Γ |∪| C) ts" "list_all (λt. closed_except t (fmdom Γ)) ts"
subgoal
using ‹wellformed t› unfolding ‹t = _› wellformed.list_comb by simp
subgoal
using ‹¬ shadows_consts t› unfolding ‹t = _› shadows.list_comb
by (simp add: list_all_iff list_ex_iff)
subgoal
using ‹consts t |⊆| fmdom Γ |∪| C›
unfolding list_all_iff
by (metis Ball_set ‹t = name $$ ts› con1.prems(9) special_constants.sconsts_list_comb)
subgoal
using ‹closed_except t (fmdom Γ)› unfolding ‹t = _› closed.list_comb by simp
done
moreover have
"list_all (λt'. fmrel_on_fset (ids t') related_v Γ (fmap_of_ns (sem_env.v env))) ts"
proof (standard, rule fmrel_on_fsubset)
fix t'
assume "t' ∈ set ts"
thus "ids t' |⊆| ids t"
unfolding ‹t = _›
apply (simp add: ids_list_comb)
apply (subst (2) ids_def)
apply simp
apply (rule fsubset_finsertI2)
apply (auto simp: fset_of_list_elem intro!: ffUnion_subset_elem)
done
show "fmrel_on_fset (ids t) related_v Γ (fmap_of_ns (sem_env.v env))"
by fact
qed
ultimately obtain us where "list_all2 (veval' Γ) ts us" "list_all2 related_v us ml_vs'"
using ‹list_all2 related_exp ts es›
proof (induction es ml_vs' arbitrary: ts thesis rule: list.rel_induct)
case (Cons e es ml_v ml_vs ts0)
then obtain t ts where "ts0 = t # ts" "related_exp t e" by (cases ts0) auto
with Cons have "list_all2 related_exp ts es" by simp
with Cons obtain us where "list_all2 (veval' Γ) ts us" "list_all2 related_v us ml_vs"
unfolding ‹ts0 = _›
by auto
from Cons.hyps[simplified, THEN conjunct2, rule_format, of t Γ]
obtain u where "Γ ⊢⇩v t ↓ u " "related_v u ml_v"
proof
show
"is_cupcake_all_env env" "related_exp t e" "wellformed_venv Γ" "closed_venv Γ"
"fmpred (λ_. vwelldefined') Γ" "fdisjnt C (fmdom Γ)"
"not_shadows_vconsts_env Γ"
by fact+
next
show
"wellformed t" "¬ shadows_consts t" "closed_except t (fmdom Γ)"
"consts t |⊆| fmdom Γ |∪| C" "fmrel_on_fset (ids t) related_v Γ (fmap_of_ns (sem_env.v env))"
using Cons unfolding ‹ts0 = _›
by auto
qed blast
show ?case
apply (rule Cons(3)[of "u # us"])
unfolding ‹ts0 = _›
apply auto
apply fact+
done
qed auto
show ?case
apply simp
apply (intro exI conjI)
unfolding ‹t = _›
apply (rule veval'.constr)
apply fact+
unfolding ‹ml_v' = _›
apply (subst ml_vs'_def[symmetric])
apply simp
apply (rule related_v.conv)
apply fact
done
next
case (var1 env id ml_v)
from ‹related_exp t (Var id)› obtain name where "id = Short (as_string name)"
by cases auto
with var1 have "cupcake_nsLookup (sem_env.v env) (as_string name) = Some ml_v"
by auto
from ‹related_exp t (Var id)› consider
(var) "t = Svar name"
| (const) "t = Sconst name" "name |∉| C"
unfolding ‹id = _›
apply (cases t)
using name.expand by blast+
thus ?case
proof cases
case var
hence "name |∈| ids t"
unfolding ids_def by simp
have "rel_option related_v (fmlookup Γ name) (cupcake_nsLookup (sem_env.v env) (as_string name))"
using ‹fmrel_on_fset (ids t) _ _ _›
apply -
apply (drule fmrel_on_fsetD[OF ‹name |∈| ids t›])
apply simp
done
then obtain v where "related_v v ml_v" "fmlookup Γ name = Some v"
using ‹cupcake_nsLookup (sem_env.v env) _ = _›
by cases auto
show ?thesis
unfolding ‹t = _›
apply simp
apply (rule exI)
apply (rule conjI)
apply (rule veval'.var)
apply fact+
done
next
case const
hence "name |∈| ids t"
unfolding ids_def by simp
have "rel_option related_v (fmlookup Γ name) (cupcake_nsLookup (sem_env.v env) (as_string name))"
using ‹fmrel_on_fset (ids t) _ _ _›
apply -
apply (drule fmrel_on_fsetD[OF ‹name |∈| ids t›])
apply simp
done
then obtain v where "related_v v ml_v" "fmlookup Γ name = Some v"
using ‹cupcake_nsLookup (sem_env.v env) _ = _›
by cases auto
show ?thesis
unfolding ‹t = _›
apply simp
apply (rule exI)
apply (rule conjI)
apply (rule veval'.const)
apply fact+
done
qed
next
case (fn env n u)
obtain n' where "n = as_string n'"
by (metis name.sel)
obtain cs ml_cs
where "t = Sabs cs" "u = Mat (Var (Short (as_string n'))) ml_cs" "n' |∉| ids (Sabs cs)" "n' |∉| all_consts"
and "list_all2 (rel_prod related_pat related_exp) cs ml_cs"
using ‹related_exp t (Fun n u)› unfolding ‹n = _›
by cases (auto dest: name.expand)
obtain ns where "fmap_of_ns (sem_env.v env) = fmap_of_list ns"
apply (cases env)
apply simp
subgoal for v by (cases v) simp
done
show ?case
apply simp
apply (rule exI)
apply (rule conjI)
unfolding ‹t = _›
apply (rule veval'.abs)
unfolding ‹n = _›
apply (rule related_v.closure)
unfolding ‹u = _›
apply (subst related_fun_alt_def; rule conjI)
apply fact
apply (rule conjI; fact)
using ‹fmrel_on_fset (ids t) _ _ _›
unfolding ‹t = _› ‹fmap_of_ns (sem_env.v env) = _›
by simp
next
case (app1 env exps ress ml_vs env' exp' bv)
from ‹related_exp t _› obtain exp⇩1 exp⇩2 t⇩1 t⇩2
where "rev exps = [exp⇩2, exp⇩1]" "exps = [exp⇩1, exp⇩2]" "t = t⇩1 $⇩s t⇩2"
and "related_exp t⇩1 exp⇩1" "related_exp t⇩2 exp⇩2"
by cases auto
moreover from app1 have "ress = map Rval ml_vs"
by auto
ultimately obtain ml_v⇩1 ml_v⇩2 where "ml_vs = [ml_v⇩2, ml_v⇩1]"
using app1(1)
by (smt list_all2_shortcircuit_rval list_all2_Cons1 list_all2_Nil)
have "is_cupcake_exp exp⇩1" "is_cupcake_exp exp⇩2"
using app1 unfolding ‹exps = _› by (auto dest: related_exp_is_cupcake)
moreover have "fmrel_on_fset (ids t⇩1) related_v Γ (fmap_of_ns (sem_env.v env))"
using app1 unfolding ids_def ‹t = _›
by (auto intro: fmrel_on_fsubset)
moreover have "fmrel_on_fset (ids t⇩2) related_v Γ (fmap_of_ns (sem_env.v env))"
using app1 unfolding ids_def ‹t = _›
by (auto intro: fmrel_on_fsubset)
ultimately have
"cupcake_evaluate_single env exp⇩1 (Rval ml_v⇩1)" "cupcake_evaluate_single env exp⇩2 (Rval ml_v⇩2)" and
"∃t⇩1'. Γ ⊢⇩v t⇩1 ↓ t⇩1' ∧ related_v t⇩1' ml_v⇩1" "∃t⇩2'. Γ ⊢⇩v t⇩2 ↓ t⇩2' ∧ related_v t⇩2' ml_v⇩2"
using app1 ‹related_exp t⇩1 exp⇩1› ‹related_exp t⇩2 exp⇩2›
unfolding ‹ress = _› ‹exps = _› ‹ml_vs = _› ‹t = _›
by (auto simp: closed_except_def)
then obtain v⇩1 v⇩2
where "Γ ⊢⇩v t⇩1 ↓ v⇩1" "related_v v⇩1 ml_v⇩1"
and "Γ ⊢⇩v t⇩2 ↓ v⇩2" "related_v v⇩2 ml_v⇩2"
by blast
have "is_cupcake_value ml_v⇩1"
by (rule cupcake_single_preserve) fact+
moreover have "is_cupcake_value ml_v⇩2"
by (rule cupcake_single_preserve) fact+
ultimately have "list_all is_cupcake_value (rev ml_vs)"
unfolding ‹ml_vs = _› by simp
hence "is_cupcake_exp exp'" "is_cupcake_all_env env'"
using ‹do_opapp _ = _› by (metis cupcake_opapp_preserve)+
have "vclosed v⇩1"
proof (rule veval'_closed)
show "closed_except t⇩1 (fmdom Γ)"
using ‹closed_except _ (fmdom Γ)›
unfolding ‹t = _›
by (simp add: closed_except_def)
next
show "wellformed t⇩1"
using ‹wellformed t› unfolding ‹t = _›
by simp
qed fact+
have "vclosed v⇩2"
apply (rule veval'_closed)
apply fact
using app1 unfolding ‹t = _› by (auto simp: closed_except_def)
have "vwellformed v⇩1"
apply (rule veval'_wellformed)
apply fact
using app1 unfolding ‹t = _› by auto
have "vwellformed v⇩2"
apply (rule veval'_wellformed)
apply fact
using app1 unfolding ‹t = _› by auto
have "vwelldefined' v⇩1"
apply (rule veval'_welldefined')
apply fact
using app1 unfolding ‹t = _› by auto
have "vwelldefined' v⇩2"
apply (rule veval'_welldefined')
apply fact
using app1 unfolding ‹t = _› by auto
have "not_shadows_vconsts v⇩1"
apply (rule veval'_shadows)
apply fact
using app1 unfolding ‹t = _› by auto
have "not_shadows_vconsts v⇩2"
apply (rule veval'_shadows)
apply fact
using app1 unfolding ‹t = _› by auto
show ?case
proof (rule if_rvalI)
fix ml_v
assume "bv = Rval ml_v"
show "∃v. Γ ⊢⇩v t ↓ v ∧ related_v v ml_v"
using ‹do_opapp _ = _›
proof (cases rule: do_opapp_cases)
case (closure env⇩Λ n)
then have closure':
"ml_v⇩1 = Closure env⇩Λ (as_string (Name n)) exp'"
"env' = update_v (λ_. nsBind (as_string (Name n)) ml_v⇩2 (sem_env.v env⇩Λ)) env⇩Λ"
unfolding ‹ml_vs = _› by auto
obtain Γ⇩Λ cs
where "v⇩1 = Vabs cs Γ⇩Λ" "related_fun cs (Name n) exp'"
and "fmrel_on_fset (ids (Sabs cs)) related_v Γ⇩Λ (fmap_of_ns (sem_env.v env⇩Λ))"
using ‹related_v v⇩1 ml_v⇩1› unfolding ‹ml_v⇩1 = _›
by cases auto
then obtain ml_cs
where "exp' = Mat (Var (Short (as_string (Name n)))) ml_cs" "Name n |∉| ids (Sabs cs)" "Name n |∉| all_consts"
and "list_all2 (rel_prod related_pat related_exp) cs ml_cs"
by (auto elim: related_funE)
hence "cupcake_evaluate_single env' (Mat (Var (Short (as_string (Name n)))) ml_cs) (Rval ml_v)"
using ‹cupcake_evaluate_single env' exp' bv›
unfolding ‹bv = _›
by simp
then obtain m_env v' ml_rhs ml_pat
where "cupcake_evaluate_single env' (Var (Short (as_string (Name n)))) (Rval v')"
and "cupcake_match_result (sem_env.c env') v' ml_cs Bindv = Rval (ml_rhs, ml_pat, m_env)"
and "cupcake_evaluate_single (env' ⦇ sem_env.v := nsAppend (alist_to_ns m_env) (sem_env.v env') ⦈) ml_rhs (Rval ml_v)"
by cases auto
have
"closed_venv (fmupd (Name n) v⇩2 Γ⇩Λ)" "wellformed_venv (fmupd (Name n) v⇩2 Γ⇩Λ)"
"not_shadows_vconsts_env (fmupd (Name n) v⇩2 Γ⇩Λ)" "fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 Γ⇩Λ)"
using ‹vclosed v⇩1› ‹vclosed v⇩2›
using ‹vwellformed v⇩1› ‹vwellformed v⇩2›
using ‹not_shadows_vconsts v⇩1› ‹not_shadows_vconsts v⇩2›
using ‹vwelldefined' v⇩1› ‹vwelldefined' v⇩2›
unfolding ‹v⇩1 = _›
by auto
have "closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))"
using ‹vclosed v⇩1› unfolding ‹v⇩1 = _›
apply (auto simp: Sterm.closed_except_simps list_all_iff)
apply (auto simp: closed_except_def)
done
have "consts (Sabs cs) |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ) |∪| C"
using ‹vwelldefined' v⇩1› unfolding ‹v⇩1 = _›
unfolding sconsts_sabs
by (auto simp: list_all_iff)
have "¬ shadows_consts (Sabs cs)"
using ‹not_shadows_vconsts v⇩1› unfolding ‹v⇩1 = _›
by (auto simp: list_all_iff list_ex_iff)
have "fdisjnt C (fmdom Γ⇩Λ)"
using ‹vwelldefined' v⇩1› unfolding ‹v⇩1 = _›
by simp
have "if_rval (λml_v. ∃v. fmupd (Name n) v⇩2 Γ⇩Λ ⊢⇩v Sabs cs $⇩s Svar (Name n) ↓ v ∧ related_v v ml_v) bv"
proof (rule app1(2))
show "fmrel_on_fset (ids (Sabs cs $⇩s Svar (Name n))) related_v (fmupd (Name n) v⇩2 Γ⇩Λ) (fmap_of_ns (sem_env.v env'))"
unfolding closure'
apply (simp del: frees_sterm.simps(3) consts_sterm.simps(3) name.sel add: ids_def split!: sem_env.splits)
apply (rule fmrel_on_fset_updateI)
apply (fold ids_def)
using ‹fmrel_on_fset (ids (Sabs cs)) related_v Γ⇩Λ _› apply simp
apply (rule ‹related_v v⇩2 ml_v⇩2›)
done
next
show "wellformed (Sabs cs $⇩s Svar (Name n))"
using ‹vwellformed v⇩1› unfolding ‹v⇩1 = _›
by simp
next
show "related_exp (Sabs cs $⇩s Svar (Name n)) exp'"
unfolding ‹exp' = _›
using ‹list_all2 (rel_prod related_pat related_exp) cs ml_cs›
by (auto intro:related_exp.intros simp del: name.sel)
next
show "closed_except (Sabs cs $⇩s Svar (Name n)) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))"
using ‹closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))› by (simp add: closed_except_def)
next
show "¬ shadows_consts (Sabs cs $⇩s Svar (Name n))"
using ‹¬ shadows_consts (Sabs cs)› ‹Name n |∉| all_consts› by simp
next
show "consts (Sabs cs $⇩s Svar (Name n)) |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ) |∪| C"
using ‹consts (Sabs cs) |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ) |∪| C› by simp
next
show "fdisjnt C (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))"
using ‹Name n |∉| all_consts› ‹fdisjnt C (fmdom Γ⇩Λ)›
unfolding fdisjnt_alt_def all_consts_def by auto
qed fact+
then obtain v where "fmupd (Name n) v⇩2 Γ⇩Λ ⊢⇩v Sabs cs $⇩s Svar (Name n) ↓ v" "related_v v ml_v"
unfolding ‹bv = _›
by auto
then obtain env pat rhs
where "vfind_match cs v⇩2 = Some (env, pat, rhs)"
and "fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env ⊢⇩v rhs ↓ v"
by (auto elim: veval'_sabs_svarE)
hence "(pat, rhs) ∈ set cs" "vmatch (mk_pat pat) v⇩2 = Some env"
by (metis vfind_match_elem)+
hence "linear pat" "wellformed rhs"
using ‹vwellformed v⇩1› unfolding ‹v⇩1 = _›
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 ‹vmatch (mk_pat pat) v⇩2 = Some env›)
done
obtain v' where "Γ⇩Λ ++⇩f env ⊢⇩v rhs ↓ v'" "v' ≈⇩e v"
proof (rule veval'_agree_eq)
show "fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env ⊢⇩v rhs ↓ v" by fact
next
have *: "Name n |∉| ids rhs" if "Name n |∉| fmdom env"
proof
assume "Name n |∈| ids rhs"
thus False
unfolding ids_def
proof (cases rule: funion_strictE)
case A
moreover have "Name n |∉| frees pat"
using that unfolding ‹fmdom env = frees pat› .
ultimately have "Name n |∈| frees (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply (auto simp: fset_of_list_elem)
apply (rule ‹(pat, rhs) ∈ set cs›)
done
thus ?thesis
using ‹Name n |∉| ids (Sabs cs)› unfolding ids_def
by blast
next
case B
hence "Name n |∈| consts (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply (auto simp: fset_of_list_elem)
apply (rule ‹(pat, rhs) ∈ set cs›)
done
thus ?thesis
using ‹Name n |∉| ids (Sabs cs)› unfolding ids_def
by blast
qed
qed
show "fmrel_on_fset (ids rhs) erelated (Γ⇩Λ ++⇩f env) (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env)"
apply rule
apply auto
apply (rule option.rel_refl; rule erelated_refl)
using * apply auto[]
apply (rule option.rel_refl; rule erelated_refl)+
done
next
show "closed_venv (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env)"
apply rule
apply fact
apply (rule vclosed.vmatch_env)
apply fact
apply fact
done
next
show "wellformed_venv (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env)"
apply rule
apply fact
apply (rule vwellformed.vmatch_env)
apply fact
apply fact
done
next
show "closed_except rhs (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env))"
using ‹fmdom env = frees pat› ‹(pat, rhs) ∈ set cs›
using ‹closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))›
by (auto simp: Sterm.closed_except_simps list_all_iff)
next
show "wellformed rhs" by fact
next
show "consts rhs |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env) |∪| C"
using ‹consts (Sabs cs) |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ) |∪| C› ‹(pat, rhs) ∈ set cs›
unfolding sconsts_sabs
by (auto simp: list_all_iff)
next
have "fdisjnt C (fmdom env)"
using ‹(pat, rhs) ∈ set cs› ‹¬ shadows_consts (Sabs cs)›
unfolding ‹fmdom env = frees pat›
by (auto simp: list_ex_iff fdisjnt_alt_def all_consts_def)
thus "fdisjnt C (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env))"
using ‹Name n |∉| all_consts› ‹fdisjnt C (fmdom Γ⇩Λ)›
unfolding fdisjnt_alt_def
by (auto simp: all_consts_def)
next
show "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› ‹¬ shadows_consts (Sabs cs)›
by (auto simp: list_ex_iff)
next
have "not_shadows_vconsts_env env"
by (rule not_shadows_vconsts.vmatch_env) fact+
thus "not_shadows_vconsts_env (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env)"
using ‹not_shadows_vconsts_env (fmupd (Name n) v⇩2 Γ⇩Λ)› by blast
next
have "fmpred (λ_. vwelldefined') env"
by (rule vmatch_welldefined') fact+
thus "fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 Γ⇩Λ ++⇩f env)"
using ‹fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 Γ⇩Λ)› by blast
qed blast
show ?thesis
apply (intro exI conjI)
unfolding ‹t = _›
apply (rule veval'.comb)
using ‹Γ ⊢⇩v t⇩1 ↓ v⇩1› unfolding ‹v⇩1 = _›
apply blast
apply fact
apply fact+
apply (rule related_v_ext)
apply fact+
done
next
case (recclosure env⇩Λ funs name n)
with recclosure have recclosure':
"ml_v⇩1 = Recclosure env⇩Λ funs name"
"env' = update_v (λ_. nsBind (as_string (Name n)) ml_v⇩2 (build_rec_env funs env⇩Λ (sem_env.v env⇩Λ))) env⇩Λ"
unfolding ‹ml_vs = _› by auto
obtain Γ⇩Λ css
where "v⇩1 = Vrecabs css (Name name) Γ⇩Λ"
and "fmrel_on_fset (fbind (fmran css) (ids ∘ Sabs)) related_v Γ⇩Λ (fmap_of_ns (sem_env.v env⇩Λ))"
and "fmrel (λcs (n, e). related_fun cs n e) css (fmap_of_list (map (map_prod Name (map_prod Name id)) funs))"
using ‹related_v v⇩1 ml_v⇩1› unfolding ‹ml_v⇩1 = _›
by cases auto
from ‹fmrel _ _ _› have "rel_option (λcs (n, e). related_fun cs (Name n) e) (fmlookup css (Name name)) (find_recfun name funs)"
apply -
apply (subst option.rel_sel)
apply auto
apply (drule fmrel_fmdom_eq)
apply (drule fmdom_notI)
using ‹v⇩1 = Vrecabs css (Name name) Γ⇩Λ› ‹vwellformed v⇩1› apply auto[1]
using recclosure(3) apply auto[1]
apply (erule fmrel_cases[where x = "Name name"])
apply simp
apply (subst (asm) fmlookup_of_list)
apply (simp add: name.map_of_rekey')
by blast
then obtain cs where "fmlookup css (Name name) = Some cs" "related_fun cs (Name n) exp'"
using ‹find_recfun _ _ = _›
by cases auto
then obtain ml_cs
where "exp' = Mat (Var (Short (as_string (Name n)))) ml_cs" "Name n |∉| ids (Sabs cs)" "Name n |∉| all_consts"
and "list_all2 (rel_prod related_pat related_exp) cs ml_cs"
by (auto elim: related_funE)
hence "cupcake_evaluate_single env' (Mat (Var (Short n)) ml_cs) (Rval ml_v)"
using ‹cupcake_evaluate_single env' exp' bv›
unfolding ‹bv = _›
by simp
then obtain m_env v' ml_rhs ml_pat
where "cupcake_evaluate_single env' (Var (Short n)) (Rval v')"
and "cupcake_match_result (sem_env.c env') v' ml_cs Bindv = Rval (ml_rhs, ml_pat, m_env)"
and "cupcake_evaluate_single (env' ⦇ sem_env.v := nsAppend (alist_to_ns m_env) (sem_env.v env') ⦈) ml_rhs (Rval ml_v)"
by cases auto
have "closed_venv (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))"
using ‹vclosed v⇩1› ‹vclosed v⇩2›
using ‹fmlookup css (Name name) = Some cs›
unfolding ‹v⇩1 = _› mk_rec_env_def
apply auto
apply rule
apply rule
apply (auto intro: fmdomI)
done
have "wellformed_venv (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))"
using ‹vwellformed v⇩1› ‹vwellformed v⇩2›
using ‹fmlookup css (Name name) = Some cs›
unfolding ‹v⇩1 = _› mk_rec_env_def
apply auto
apply rule
apply rule
apply (auto intro: fmdomI)
done
have "not_shadows_vconsts_env (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))"
using ‹not_shadows_vconsts v⇩1› ‹not_shadows_vconsts v⇩2›
using ‹fmlookup css (Name name) = Some cs›
unfolding ‹v⇩1 = _› mk_rec_env_def
apply auto
apply rule
apply rule
apply (auto intro: fmdomI)
done
have "fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))"
using ‹vwelldefined' v⇩1› ‹vwelldefined' v⇩2›
using ‹fmlookup css (Name name) = Some cs›
unfolding ‹v⇩1 = _› mk_rec_env_def
apply auto
apply rule
apply rule
apply (auto intro: fmdomI)
done
have "closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))"
using ‹vclosed v⇩1› unfolding ‹v⇩1 = _›
apply (auto simp: Sterm.closed_except_simps list_all_iff)
using ‹fmlookup css (Name name) = Some cs›
apply (auto simp: closed_except_def dest!: fmpredD[where m = css])
done
have "consts (Sabs cs) |⊆| fmdom (fmupd (Name n) v⇩2 Γ⇩Λ) |∪| (C |∪| fmdom css)"
using ‹vwelldefined' v⇩1› unfolding ‹v⇩1 = _›
unfolding sconsts_sabs
using ‹fmlookup css (Name name) = Some cs›
by (auto simp: list_all_iff dest!: fmpredD[where m = css])
have "¬ shadows_consts (Sabs cs)"
using ‹not_shadows_vconsts v⇩1› unfolding ‹v⇩1 = _›
using ‹fmlookup css (Name name) = Some cs›
by (auto simp: list_all_iff list_ex_iff)
have "fdisjnt C (fmdom Γ⇩Λ)"
using ‹vwelldefined' v⇩1› unfolding ‹v⇩1 = _›
using ‹fmlookup css (Name name) = Some cs›
by auto
have "if_rval (λml_v. ∃v. fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ⊢⇩v Sabs cs $⇩s Svar (Name n) ↓ v ∧ related_v v ml_v) bv"
proof (rule app1(2))
have "fmrel_on_fset (ids (Sabs cs)) related_v Γ⇩Λ (fmap_of_ns (sem_env.v env⇩Λ))"
apply (rule fmrel_on_fsubset)
apply fact
apply (subst funion_image_bind_eq[symmetric])
apply (rule ffUnion_subset_elem)
apply (subst fimage_iff)
apply (rule fBexI)
apply simp
apply (rule fmranI)
apply fact
done
have "fmrel_on_fset (ids (Sabs cs)) related_v (mk_rec_env css Γ⇩Λ) (cake_mk_rec_env funs env⇩Λ)"
apply rule
apply (rule mk_rec_env_related[THEN fmrelD])
apply (rule ‹fmrel _ css _›)
apply (rule ‹fmrel_on_fset (fbind _ _) related_v Γ⇩Λ _›)
done
show "fmrel_on_fset (ids (Sabs cs $⇩s Svar (Name n))) related_v (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ)) (fmap_of_ns (sem_env.v env'))"
unfolding recclosure'
apply (simp del: frees_sterm.simps(3) consts_sterm.simps(3) name.sel add: ids_def split!: sem_env.splits)
apply (rule fmrel_on_fset_updateI)
unfolding build_rec_env_fmap
apply (rule fmrel_on_fset_addI)
apply (fold ids_def)
subgoal
using ‹fmrel_on_fset (ids (Sabs cs)) related_v Γ⇩Λ _› by simp
subgoal
using ‹fmrel_on_fset (ids (Sabs cs)) related_v (mk_rec_env css Γ⇩Λ) _› by simp
apply (rule ‹related_v v⇩2 ml_v⇩2›)
done
next
show "wellformed (Sabs cs $⇩s Svar (Name n))"
using ‹vwellformed v⇩1› unfolding ‹v⇩1 = _›
using ‹fmlookup css (Name name) = Some cs›
by auto
next
show "related_exp (Sabs cs $⇩s Svar (Name n)) exp'"
unfolding ‹exp' = _›
apply (rule related_exp.intros)
apply fact
apply (rule related_exp.intros)
done
next
show "closed_except (Sabs cs $⇩s Svar (Name n)) (fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ)))"
using ‹closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))›
by (auto simp: list_all_iff closed_except_def)
next
show "¬ shadows_consts (Sabs cs $⇩s Svar (Name n))"
using ‹¬ shadows_consts (Sabs cs)› ‹Name n |∉| all_consts› by simp
next
show "consts (Sabs cs $⇩s Svar (Name n)) |⊆| fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ)) |∪| C"
using ‹consts (Sabs cs) |⊆| _› unfolding mk_rec_env_def
by auto
next
show "fdisjnt C (fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ)))"
using ‹Name n |∉| all_consts› ‹fdisjnt C (fmdom Γ⇩Λ)› ‹vwelldefined' v⇩1›
unfolding mk_rec_env_def ‹v⇩1 = _›
by (auto simp: fdisjnt_alt_def all_consts_def)
qed fact+
then obtain v
where "fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ⊢⇩v Sabs cs $⇩s Svar (Name n) ↓ v" "related_v v ml_v"
unfolding ‹bv = _›
by auto
then obtain env pat rhs
where "vfind_match cs v⇩2 = Some (env, pat, rhs)"
and "fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env ⊢⇩v rhs ↓ v"
by (auto elim: veval'_sabs_svarE)
hence "(pat, rhs) ∈ set cs" "vmatch (mk_pat pat) v⇩2 = Some env"
by (metis vfind_match_elem)+
hence "linear pat" "wellformed rhs"
using ‹vwellformed v⇩1› unfolding ‹v⇩1 = _›
using ‹fmlookup css (Name name) = Some 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 ‹vmatch (mk_pat pat) v⇩2 = Some env›)
done
obtain v' where "Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env ⊢⇩v rhs ↓ v'" "v' ≈⇩e v"
proof (rule veval'_agree_eq)
show "fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env ⊢⇩v rhs ↓ v" by fact
next
have *: "Name n |∉| ids rhs" if "Name n |∉| fmdom env"
proof
assume "Name n |∈| ids rhs"
thus False
unfolding ids_def
proof (cases rule: funion_strictE)
case A
moreover have "Name n |∉| frees pat"
using that unfolding ‹fmdom env = frees pat› .
ultimately have "Name n |∈| frees (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply (auto simp: fset_of_list_elem)
apply (rule ‹(pat, rhs) ∈ set cs›)
done
thus ?thesis
using ‹Name n |∉| ids (Sabs cs)› unfolding ids_def
by blast
next
case B
hence "Name n |∈| consts (Sabs cs)"
apply auto
unfolding ffUnion_alt_def
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply (auto simp: fset_of_list_elem)
apply (rule ‹(pat, rhs) ∈ set cs›)
done
thus ?thesis
using ‹Name n |∉| ids (Sabs cs)› unfolding ids_def
by blast
qed
qed
show "fmrel_on_fset (ids rhs) erelated (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ ++⇩f env) (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env)"
apply rule
apply auto
apply (rule option.rel_refl; rule erelated_refl)
using * apply auto[]
apply (rule option.rel_refl; rule erelated_refl)+
using * apply auto[]
apply (rule option.rel_refl; rule erelated_refl)+
done
next
show "closed_venv (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env)"
apply rule
apply fact
apply (rule vclosed.vmatch_env)
apply fact
apply fact
done
next
show "wellformed_venv (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env)"
apply rule
apply fact
apply (rule vwellformed.vmatch_env)
apply fact
apply fact
done
next
show "closed_except rhs (fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env))"
using ‹fmdom env = frees pat› ‹(pat, rhs) ∈ set cs›
using ‹closed_except (Sabs cs) (fmdom (fmupd (Name n) v⇩2 Γ⇩Λ))›
apply (auto simp: Sterm.closed_except_simps list_all_iff)
apply (erule ballE[where x = "(pat, rhs)"])
apply (auto simp: closed_except_def)
done
next
show "wellformed rhs" by fact
next
show "consts rhs |⊆| fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env) |∪| C"
using ‹consts (Sabs cs) |⊆| _› ‹(pat, rhs) ∈ set cs›
unfolding sconsts_sabs mk_rec_env_def
by (auto simp: list_all_iff)
next
have "fdisjnt C (fmdom env)"
using ‹(pat, rhs) ∈ set cs› ‹¬ shadows_consts (Sabs cs)›
unfolding ‹fmdom env = frees pat›
by (auto simp: list_ex_iff all_consts_def fdisjnt_alt_def)
moreover have "fdisjnt C (fmdom css)"
using ‹vwelldefined' v⇩1› unfolding ‹v⇩1 = _›
by simp
ultimately show "fdisjnt C (fmdom (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env))"
using ‹Name n |∉| all_consts› ‹fdisjnt C (fmdom Γ⇩Λ)›
unfolding fdisjnt_alt_def mk_rec_env_def
by (auto simp: all_consts_def)
next
show "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› ‹¬ shadows_consts (Sabs cs)›
by (auto simp: list_ex_iff)
next
have "not_shadows_vconsts_env env"
by (rule not_shadows_vconsts.vmatch_env) fact+
thus "not_shadows_vconsts_env (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env)"
using ‹not_shadows_vconsts_env (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))› by blast
next
have "fmpred (λ_. vwelldefined') env"
by (rule vmatch_welldefined') fact+
thus "fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ) ++⇩f env)"
using ‹fmpred (λ_. vwelldefined') (fmupd (Name n) v⇩2 (Γ⇩Λ ++⇩f mk_rec_env css Γ⇩Λ))› by blast
qed simp
show ?thesis
apply (intro exI conjI)
unfolding ‹t = _›
apply (rule veval'.rec_comb)
using ‹Γ ⊢⇩v t⇩1 ↓ v⇩1› unfolding ‹v⇩1 = _› apply blast
apply fact+
apply (rule related_v_ext)
apply fact+
done
qed
qed
next
case (mat1 env ml_scr ml_scr' ml_cs ml_rhs ml_pat env' ml_res)
obtain scr cs
where "t = Sabs cs $⇩s scr" "related_exp scr ml_scr"
and "list_all2 (rel_prod related_pat related_exp) cs ml_cs"
using ‹related_exp t (Mat ml_scr ml_cs)›
by cases
have "sem_env.c env = as_static_cenv"
using ‹is_cupcake_all_env env›
by (auto elim: is_cupcake_all_envE)
obtain scr' where "Γ ⊢⇩v scr ↓ scr'" "related_v scr' ml_scr'"
using mat1(4) unfolding if_rval.simps
proof
show
"is_cupcake_all_env env" "related_exp scr ml_scr" "wellformed_venv Γ"
"closed_venv Γ" "fmpred (λ_. vwelldefined') Γ" "fdisjnt C (fmdom Γ)"
"not_shadows_vconsts_env Γ"
by fact+
next
show "fmrel_on_fset (ids scr) related_v Γ (fmap_of_ns (sem_env.v env))"
apply (rule fmrel_on_fsubset)
apply fact
unfolding ‹t = _› ids_def
apply auto
done
next
show
"wellformed scr" "consts scr |⊆| fmdom Γ |∪| C"
"closed_except scr (fmdom Γ)" "¬ shadows_consts scr"
using mat1 unfolding ‹t = _› by (auto simp: closed_except_def)
qed blast
have "list_all (λ(pat, _). linear pat) cs"
using mat1 unfolding ‹t = _› by (auto simp: list_all_iff)
obtain rhs pat Γ'
where "ml_pat = mk_ml_pat (mk_pat pat)" "related_exp rhs ml_rhs"
and "vfind_match cs scr' = Some (Γ', pat, rhs)"
and "var_env Γ' env'"
using ‹list_all2 _ cs ml_cs› ‹list_all _ cs› ‹related_v scr' ml_scr'› mat1(2)
unfolding ‹sem_env.c env = as_static_cenv›
by (auto elim: match_all_related)
hence "vmatch (mk_pat pat) scr' = Some Γ'"
by (auto dest: vfind_match_elem)
hence "patvars (mk_pat pat) = fmdom Γ'"
by (auto simp: vmatch_dom)
have "(pat, rhs) ∈ set cs"
by (rule vfind_match_elem) fact
have "linear pat"
using ‹(pat, rhs) ∈ set cs› ‹wellformed t› unfolding ‹t = _›
by (auto simp: list_all_iff)
hence "fmdom Γ' = frees pat"
using ‹patvars (mk_pat pat) = fmdom Γ'›
by (simp add: mk_pat_frees)
show ?case
proof (rule if_rvalI)
fix ml_rhs'
assume "ml_res = Rval ml_rhs'"
obtain rhs' where "Γ ++⇩f Γ' ⊢⇩v rhs ↓ rhs'" "related_v rhs' ml_rhs'"
using mat1(5) unfolding ‹ml_res = _› if_rval.simps
proof
show "is_cupcake_all_env (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈)"
proof (rule cupcake_v_update_preserve)
have "list_all (is_cupcake_value ∘ snd) env'"
proof (rule match_all_preserve)
show "cupcake_c_ns (sem_env.c env)"
unfolding ‹sem_env.c env = _› by (rule static_cenv)
next
have "is_cupcake_exp (Mat ml_scr ml_cs)"
apply (rule related_exp_is_cupcake)
using mat1 by auto
thus "cupcake_clauses ml_cs"
by simp
show "is_cupcake_value ml_scr'"
apply (rule cupcake_single_preserve)
apply (rule mat1)
apply (rule mat1)
using ‹is_cupcake_exp (Mat ml_scr ml_cs)› by simp
qed fact+
hence "is_cupcake_ns (alist_to_ns env')"
by (rule cupcake_alist_to_ns_preserve)
moreover have "is_cupcake_ns (sem_env.v env)"
by (rule is_cupcake_all_envD) fact
ultimately show "is_cupcake_ns (nsAppend (alist_to_ns env') (sem_env.v env))"
by (rule cupcake_nsAppend_preserve)
qed fact
next
show "related_exp rhs ml_rhs"
by fact
next
have *: "fmdom (fmap_of_list (map (map_prod Name id) env')) = fmdom Γ'"
using ‹var_env Γ' env'›
by (metis fmrel_fmdom_eq)
have **: "id |∈| ids t" if "id |∈| ids rhs" "id |∉| fmdom Γ'" for id
using ‹id |∈| ids rhs› unfolding ids_def
proof (cases rule: funion_strictE)
case A
from that have "id |∉| frees pat"
unfolding ‹fmdom Γ' = frees pat› by simp
hence "id |∈| frees t"
using ‹(pat, rhs) ∈ set cs›
unfolding ‹t = _›
apply auto
apply (subst ffUnion_alt_def)
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
using A apply (auto simp: fset_of_list_elem)
done
thus "id |∈| frees t |∪| consts t" by simp
next
case B
hence "id |∈| consts t"
using ‹(pat, rhs) ∈ set cs›
unfolding ‹t = _›
apply auto
apply (subst ffUnion_alt_def)
apply simp
apply (rule fBexI[where x = "(pat, rhs)"])
apply (auto simp: fset_of_list_elem)
done
thus "id |∈| frees t |∪| consts t" by simp
qed
have "fmrel_on_fset (ids rhs) related_v (Γ ++⇩f Γ') (fmap_of_ns (sem_env.v env) ++⇩f fmap_of_list (map (map_prod Name id) env'))"
apply rule
apply simp
apply safe
subgoal
apply (rule fmrelD)
apply (rule ‹var_env Γ' env'›)
done
subgoal
unfolding *[symmetric]
using fmdom_of_list fset_of_list_map fset.set_map image_image fst_map_prod
by simp
subgoal using *
by (metis (no_types, opaque_lifting) comp_def fimageI fmdom_fmap_of_list fset_of_list_map fst_comp_map_prod)
subgoal using **
by (metis fmlookup_ns fmrel_on_fsetD mat1.prems(2))
done
thus "fmrel_on_fset (ids rhs) related_v (Γ ++⇩f Γ') (fmap_of_ns (sem_env.v (env ⦇ sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) ⦈)))"
by (auto split: sem_env.splits)
next
show "wellformed_venv (Γ ++⇩f Γ')"
apply rule
apply fact
apply (rule vwellformed.vmatch_env)
apply fact
apply (rule veval'_wellformed)
apply fact
using mat1 unfolding ‹t = _› by auto
next
show "closed_venv (Γ ++⇩f Γ')"
apply rule
apply fact
apply (rule vclosed.vmatch_env)
apply fact
apply (rule veval'_closed)
apply fact
using mat1 unfolding ‹t = _› by (auto simp: closed_except_def)
next
show "fmpred (λ_. vwelldefined') (Γ ++⇩f Γ')"
apply rule
apply fact
apply (rule vmatch_welldefined')
apply fact
apply (rule veval'_welldefined')
apply fact
using mat1 unfolding ‹t = _› by auto
next
show "not_shadows_vconsts_env (Γ ++⇩f Γ')"
apply rule
apply fact
apply (rule not_shadows_vconsts.vmatch_env)
apply fact
apply (rule veval'_shadows)
apply fact
using mat1 unfolding ‹t = _› by auto
next
show "wellformed rhs"
using ‹(pat, rhs) ∈ set cs› ‹wellformed t› unfolding ‹t = _›
by (auto simp: list_all_iff)
next
show "closed_except rhs (fmdom (Γ ++⇩f Γ'))"
apply simp
unfolding ‹fmdom Γ' = frees pat›
using ‹(pat, rhs) ∈ set cs› ‹closed_except t (fmdom Γ)› unfolding ‹t = _›
by (auto simp: Sterm.closed_except_simps list_all_iff)
next
have "consts (Sabs cs) |⊆| fmdom Γ |∪| C"
using mat1 unfolding ‹t = _› by auto
show "consts rhs |⊆| fmdom (Γ ++⇩f Γ') |∪| C"
apply simp
unfolding ‹fmdom Γ' = frees pat›
using ‹(pat, rhs) ∈ set cs› ‹consts (Sabs cs) |⊆| _›
unfolding sconsts_sabs
by (auto simp: list_all_iff)
next
have "fdisjnt C (fmdom Γ')"
unfolding ‹fmdom Γ' = frees pat›
using ‹¬ shadows_consts t› ‹(pat, rhs) ∈ set cs›
unfolding ‹t = _›
by (auto simp: list_ex_iff fdisjnt_alt_def all_consts_def)
thus "fdisjnt C (fmdom (Γ ++⇩f Γ'))"
using ‹fdisjnt C (fmdom Γ)›
unfolding fdisjnt_alt_def by auto
next
show "¬ shadows_consts rhs"
using ‹(pat, rhs) ∈ set cs› ‹¬ shadows_consts t› unfolding ‹t = _›
by (auto simp: list_ex_iff)
qed blast
show "∃t'. Γ ⊢⇩v t ↓ t' ∧ related_v t' ml_rhs'"
unfolding ‹t = _›
apply (intro exI conjI seval.intros)
apply (rule veval'.intros)
apply (rule veval'.intros)
apply fact+
done
qed
qed auto
theorem semantic_correctness:
fixes exp
assumes "cupcake_evaluate_single env exp (Rval ml_v)" "is_cupcake_all_env env"
assumes "fmrel_on_fset (ids t) related_v Γ (fmap_of_ns (sem_env.v env))"
assumes "related_exp t exp"
assumes "wellformed t" "wellformed_venv Γ"
assumes "closed_venv Γ" "closed_except t (fmdom Γ)"
assumes "fmpred (λ_. vwelldefined') Γ" "consts t |⊆| fmdom Γ |∪| C"
assumes "fdisjnt C (fmdom Γ)"
assumes "¬ shadows_consts t" "not_shadows_vconsts_env Γ"
obtains v where "Γ ⊢⇩v t ↓ v" "related_v v ml_v"
using semantic_correctness0[OF assms]
by auto
end end
end