Theory CakeML_Backend
section ‹CakeML backend›
theory CakeML_Backend
imports
CakeML_Setup
"../Terms/Value"
"../Rewriting/Rewriting_Sterm"
begin
subsection ‹Compilation›
fun mk_ml_pat :: "pat ⇒ Ast.pat" where
"mk_ml_pat (Patvar s) = Ast.Pvar (as_string s)" |
"mk_ml_pat (Patconstr s args) = Ast.Pcon (Some (Short (as_string s))) (map mk_ml_pat args)"
lemma mk_pat_cupcake[intro]: "is_cupcake_pat (mk_ml_pat pat)"
by (induct pat) (auto simp: list_all_iff)
context begin
private fun frees' :: "term ⇒ name list" where
"frees' (Free x) = [x]" |
"frees' (t⇩1 $ t⇩2) = frees' t⇩2 @ frees' t⇩1 " |
"frees' (Λ t) = frees' t" |
"frees' _ = []"
private lemma frees'_eq[simp]: "fset_of_list (frees' t) = frees t"
by (induction t) auto
private lemma frees'_list_comb: "frees' (list_comb f xs) = concat (rev (map frees' xs)) @ frees' f"
by (induction xs arbitrary: f) (auto simp: app_term_def)
private lemma frees'_distinct: "linear pat ⟹ distinct (frees' pat)"
proof (induction pat)
case (App t u)
hence "distinct (frees' u @ frees' t)"
by (fastforce intro: distinct_append_fset fdisjnt_swap)
thus ?case
by simp
qed auto
private fun pat_bindings' :: "Ast.pat ⇒ name list" where
"pat_bindings' (Ast.Pvar n) = [Name n]" |
"pat_bindings' (Ast.Pcon _ ps) = concat (rev (map pat_bindings' ps))" |
"pat_bindings' (Ast.Pref p) = pat_bindings' p" |
"pat_bindings' (Ast.Ptannot p _) = pat_bindings' p" |
"pat_bindings' _ = []"
private lemma pat_bindings'_eq:
"map Name (pats_bindings ps xs) = concat (rev (map pat_bindings' ps)) @ map Name xs"
"map Name (pat_bindings p xs) = pat_bindings' p @ map Name xs"
by (induction ps xs and p xs rule: pats_bindings_pat_bindings.induct) (auto simp: ac_simps)
private lemma pat_bindings'_empty_eq: "map Name (pat_bindings p []) = pat_bindings' p"
by (simp add: pat_bindings'_eq)
private lemma pat_bindings'_eq_frees: "linear p ⟹ pat_bindings' (mk_ml_pat (mk_pat p)) = frees' p"
proof (induction rule: mk_pat.induct)
case (1 t)
show ?case
using ‹linear t› proof (cases rule: linear_strip_comb_cases)
case (comb s args)
have "map (pat_bindings' ∘ mk_ml_pat ∘ mk_pat) args = map frees' args"
proof (rule list.map_cong0, unfold comp_apply)
fix x
assume "x ∈ set args"
moreover hence "linear x"
using 1 comb by (metis linears_linear linears_strip_comb snd_conv)
ultimately show "pat_bindings' (mk_ml_pat (mk_pat x)) = frees' x"
using 1 comb by auto
qed
hence "concat (rev (map (pat_bindings' ∘ mk_ml_pat ∘ mk_pat) args)) = concat (rev (map frees' args))"
by metis
with comb show ?thesis
apply (fold const_term_def)
apply (auto simp: strip_list_comb_const frees'_list_comb comp_assoc)
apply (unfold const_term_def)
apply simp
done
qed auto
qed
lemma mk_pat_distinct: "linear pat ⟹ distinct (pat_bindings (mk_ml_pat (mk_pat pat)) [])"
by (metis pat_bindings'_eq_frees pat_bindings'_empty_eq frees'_distinct distinct_map)
end
locale cakeml = pre_constants
begin
fun
mk_exp :: "name fset ⇒ sterm ⇒ exp" and
mk_clauses :: "name fset ⇒ (term × sterm) list ⇒ (Ast.pat × exp) list" and
mk_con :: "name fset ⇒ sterm ⇒ exp" where
"mk_exp _ (Svar s) = Ast.Var (Short (as_string s))" |
"mk_exp _ (Sconst s) = (if s |∈| C then Ast.Con (Some (Short (as_string s))) [] else Ast.Var (Short (as_string s)))" |
"mk_exp S (t⇩1 $⇩s t⇩2) = Ast.App Ast.Opapp [mk_con S t⇩1, mk_con S t⇩2]" |
"mk_exp S (Sabs cs) = (
let n = fresh_fNext S in
Ast.Fun (as_string n) (Ast.Mat (Ast.Var (Short (as_string n))) (mk_clauses S cs)))" |
"mk_con S t =
(case strip_comb t of
(Sconst c, args) ⇒
if c |∈| C then Ast.Con (Some (Short (as_string c))) (map (mk_con S) args) else mk_exp S t
| _ ⇒ mk_exp S t)" |
"mk_clauses S cs = map (λ(pat, t). (mk_ml_pat (mk_pat pat), mk_con (frees pat |∪| S) t)) cs"
context begin
private lemma mk_exp_cupcake0:
"wellformed t ⟹ is_cupcake_exp (mk_exp S t)"
"wellformed_clauses cs ⟹ cupcake_clauses (mk_clauses S cs) ∧ cake_linear_clauses (mk_clauses S cs)"
"wellformed t ⟹ is_cupcake_exp (mk_con S t)"
proof (induction rule: mk_exp_mk_clauses_mk_con.induct)
case (5 S t)
show ?case
apply (simp 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
apply (auto simp: list_all_iff simp del: mk_con.simps)
apply (rule 5(1))
apply (rule prems(1)[symmetric])
apply (rule refl)
apply (rule prems)
apply assumption
using ‹wellformed t› ‹t = _›
apply (auto simp: wellformed.list_comb list_all_iff)
done
qed
using 5 by (auto split: prod.splits sterm.splits)
qed (auto simp: Let_def list_all_iff intro: mk_pat_distinct)
declare mk_con.simps[simp del]
lemma mk_exp_cupcake:
"wellformed t ⟹ is_cupcake_exp (mk_exp S t)"
"wellformed t ⟹ is_cupcake_exp (mk_con S t)"
by (metis mk_exp_cupcake0)+
end
definition mk_letrec_body where
"mk_letrec_body S rs = (
map (λ(name, rhs).
(as_string name, (
let n = fresh_fNext S in
(as_string n, Ast.Mat (Ast.Var (Short (as_string n))) (mk_clauses S (sterm.clauses rhs)))))) rs
)"
definition compile_group :: "name fset ⇒ srule list ⇒ Ast.dec" where
"compile_group S rs = Ast.Dletrec empty_locs (mk_letrec_body S rs)"
definition compile :: "srule list ⇒ Ast.prog" where
"compile rs = [Ast.Tdec (compile_group all_consts rs)]"
end
declare cakeml.mk_con.simps[code]
declare cakeml.mk_exp.simps[code]
declare cakeml.mk_clauses.simps[code]
declare cakeml.mk_letrec_body_def[code]
declare cakeml.compile_group_def[code]
declare cakeml.compile_def[code]
locale cakeml' = cakeml + constants
context srules begin
sublocale srules_as_cake?: cakeml' C_info "fst |`| fset_of_list rs" by standard
lemma mk_letrec_cupcake:
"list_all (λ(_, _, exp). is_cupcake_exp exp) (mk_letrec_body S rs)"
unfolding mk_letrec_body_def
using all_rules
apply (auto simp: Let_def list_all_iff intro!: mk_pat_cupcake mk_exp_cupcake mk_pat_distinct)
subgoal for a b
apply (erule ballE[where x = "(a, b)"]; cases b)
apply (auto simp: list_all_iff is_abs_def term_cases_def)
done
subgoal for a b
apply (erule ballE[where x = "(a, b)"]; cases b)
apply (auto simp: list_all_iff is_abs_def term_cases_def)
done
done
end
definition compile' where
"compile' C_info rs = cakeml.compile C_info (fst |`| fset_of_list rs) rs"
lemma (in srules) compile'_compile_eq: "compile' C_info rs = compile rs"
unfolding compile'_def ..
subsection ‹Computability›
export_code cakeml.compile
checking Scala
subsection ‹Correctness of semantic functions›
abbreviation related_pat :: "term ⇒ Ast.pat ⇒ bool" where
"related_pat t p ≡ (p = mk_ml_pat (mk_pat t))"
context cakeml' begin
inductive related_exp :: "sterm ⇒ exp ⇒ bool" where
var: "related_exp (Svar name) (Ast.Var (Short (as_string name)))" |
const: "name |∉| C ⟹ related_exp (Sconst name) (Ast.Var (Short (as_string name)))" |
constr: "name |∈| C ⟹ list_all2 related_exp ts es ⟹
related_exp (name $$ ts) (Ast.Con (Some (Short (as_string name))) es)" |
app: "related_exp t⇩1 u⇩1 ⟹ related_exp t⇩2 u⇩2 ⟹ related_exp (t⇩1 $⇩s t⇩2) (Ast.App Ast.Opapp [u⇩1, u⇩2])" |
"fun": "list_all2 (rel_prod related_pat related_exp) cs ml_cs ⟹
n |∉| ids (Sabs cs) ⟹ n |∉| all_consts ⟹
related_exp (Sabs cs) (Ast.Fun (as_string n) (Ast.Mat (Ast.Var (Short (as_string n))) ml_cs))" |
mat: "list_all2 (rel_prod related_pat related_exp) cs ml_cs ⟹
related_exp scr ml_scr ⟹
related_exp (Sabs cs $⇩s scr) (Ast.Mat ml_scr ml_cs)"
lemma related_exp_is_cupcake:
assumes "related_exp t e" "wellformed t"
shows "is_cupcake_exp e"
using assms proof induction
case ("fun" cs ml_cs n)
hence "list_all (λ(pat, t). linear pat ∧ wellformed t) cs" by simp
moreover have "cupcake_clauses ml_cs ∧ cake_linear_clauses ml_cs"
using ‹list_all2 _ cs ml_cs› ‹list_all _ cs›
proof induction
case (Cons c cs ml_c ml_cs)
obtain ml_p ml_e where "ml_c = (ml_p, ml_e)" by fastforce
obtain p t where "c = (p, t)" by fastforce
have "ml_p = mk_ml_pat (mk_pat p)"
using Cons unfolding ‹ml_c = _› ‹c = _› by simp
thus ?case
using Cons unfolding ‹ml_c = _› ‹c = _› by (auto intro: mk_pat_distinct)
qed simp
ultimately show ?case
by auto
next
case (mat cs ml_cs scr ml_scr)
hence "list_all (λ(pat, t). linear pat ∧ wellformed t) cs" by simp
moreover have "cupcake_clauses ml_cs ∧ cake_linear_clauses ml_cs"
using ‹list_all2 _ cs ml_cs› ‹list_all _ cs›
proof induction
case (Cons c cs ml_c ml_cs)
obtain ml_p ml_e where "ml_c = (ml_p, ml_e)" by fastforce
obtain p t where "c = (p, t)" by fastforce
have "ml_p = mk_ml_pat (mk_pat p)"
using Cons unfolding ‹ml_c = _› ‹c = _› by simp
thus ?case
using Cons unfolding ‹ml_c = _› ‹c = _› by (auto intro: mk_pat_distinct)
qed simp
ultimately show ?case
using mat by auto
next
case (constr name ts es)
hence "list_all wellformed ts"
by (simp add: wellformed.list_comb)
with ‹list_all2 _ ts es› have "list_all is_cupcake_exp es"
by induction auto
thus ?case
by simp
qed auto
definition related_fun :: "(term × sterm) list ⇒ name ⇒ exp ⇒ bool" where
"related_fun cs n e ⟷
n |∉| ids (Sabs cs) ∧ n |∉| all_consts ∧ (case e of
(Ast.Mat (Ast.Var (Short n')) ml_cs) ⇒
n = Name n' ∧ list_all2 (rel_prod related_pat related_exp) cs ml_cs
| _ ⇒ False)"
lemma related_fun_alt_def:
"related_fun cs n (Ast.Mat (Ast.Var (Short (as_string n))) ml_cs) ⟷
list_all2 (rel_prod related_pat related_exp) cs ml_cs ∧
n |∉| ids (Sabs cs) ∧ n |∉| all_consts"
unfolding related_fun_def
by auto
lemma related_funE:
assumes "related_fun cs n e"
obtains ml_cs
where "e = Ast.Mat (Ast.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 assms unfolding related_fun_def
by (simp split: exp0.splits id0.splits)
lemma related_exp_fun:
"related_fun cs n e ⟷ related_exp (Sabs cs) (Ast.Fun (as_string n) e) ∧ n |∉| ids (Sabs cs) ∧ n |∉| all_consts"
(is "?lhs ⟷ ?rhs")
proof
assume ?rhs
hence "related_exp (Sabs cs) (Ast.Fun (as_string n) e)" by simp
thus ?lhs
by cases (auto simp: related_fun_def dest: name.expand)
next
assume ?lhs
thus ?rhs
by (auto intro: related_exp.fun elim: related_funE)
qed
inductive related_v :: "value ⇒ v ⇒ bool" where
conv:
"list_all2 related_v us vs ⟹
related_v (Vconstr name us) (Conv (Some (as_string name, _)) vs)" |
closure:
"related_fun cs n e ⟹
fmrel_on_fset (ids (Sabs cs)) related_v Γ (fmap_of_ns (sem_env.v env)) ⟹
related_v (Vabs cs Γ) (Closure env (as_string n) e)" |
rec_closure:
"fmrel_on_fset (fbind (fmran css) (ids ∘ Sabs)) related_v Γ (fmap_of_ns (sem_env.v env)) ⟹
fmrel (λcs. λ(n, e). related_fun cs n e) css (fmap_of_list (map (map_prod Name (map_prod Name id)) exps)) ⟹
related_v (Vrecabs css name Γ) (Recclosure env exps (as_string name))"
abbreviation var_env :: "(name, value) fmap ⇒ (string × v) list ⇒ bool" where
"var_env Γ ns ≡ fmrel related_v Γ (fmap_of_list (map (map_prod Name id) ns))"
lemma related_v_ext:
assumes "related_v v ml_v"
assumes "v' ≈⇩e v"
shows "related_v v' ml_v"
using assms proof (induction arbitrary: v')
case (conv us ml_us name)
obtain ts where "v' = Vconstr name ts" "list_all2 erelated ts us"
using ‹v' ≈⇩e Vconstr name us›
by cases auto
have "list_all2 related_v ts ml_us"
by (rule list_all2_trans[OF _ ‹list_all2 erelated ts us› conv(1)]) auto
thus ?case
using conv unfolding ‹v' = _›
by (auto intro: related_v.conv)
next
case (closure cs n e Γ⇩2 env)
obtain Γ⇩1 where "v' = Vabs cs Γ⇩1" "fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩1 Γ⇩2"
using ‹v' ≈⇩e _›
by cases auto
have "fmrel_on_fset (ids (Sabs cs)) related_v Γ⇩1 (fmap_of_ns (sem_env.v env))"
apply rule
subgoal premises prems for x
apply (insert prems)
apply (drule fmrel_on_fsetD)
apply (rule closure)
subgoal
apply (insert prems)
apply (drule fmrel_on_fsetD)
apply (rule ‹fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩1 Γ⇩2›)
apply (metis (mono_tags, lifting) option.rel_sel)
done
done
done
show ?case
unfolding ‹v' = _›
by (rule related_v.closure) fact+
next
case (rec_closure css Γ⇩2 env exps name)
obtain Γ⇩1 where "v' = Vrecabs css name Γ⇩1" "pred_fmap (λcs. fmrel_on_fset (ids (Sabs cs)) erelated Γ⇩1 Γ⇩2) css"
using ‹v' ≈⇩e _›
by cases auto
have "fmrel_on_fset (fbind (fmran css) (ids ∘ Sabs)) related_v Γ⇩1 (fmap_of_ns (sem_env.v env))"
apply (rule fmrel_on_fsetI)
subgoal premises prems for x
apply (insert prems)
apply (drule fmrel_on_fsetD)
apply (rule rec_closure)
subgoal
apply (insert prems)
apply (erule fbindE)
apply (drule pred_fmapD[OF ‹pred_fmap _ css›])
unfolding comp_apply
apply (drule fmrel_on_fsetD)
apply assumption
apply (metis (mono_tags, lifting) option.rel_sel)
done
done
done
show ?case
unfolding ‹v' = _›
by (rule related_v.rec_closure) fact+
qed
context begin
private inductive match_result_related :: "(string × v) list ⇒ (string × v) list match_result ⇒ (name, value) fmap option ⇒ bool" for eenv where
no_match: "match_result_related eenv No_match None" |
error: "match_result_related eenv Match_type_error _" |
match: "var_env Γ eenv_m ⟹ match_result_related eenv (Match (eenv_m @ eenv)) (Some Γ)"
private corollary match_result_related_empty: "match_result_related eenv (Match eenv) (Some fmempty)"
proof -
have "match_result_related eenv (Match ([] @ eenv)) (Some fmempty)"
by (rule match_result_related.match) auto
thus ?thesis
by simp
qed
private fun is_Match :: "'a match_result ⇒ bool" where
"is_Match (Match _) ⟷ True" |
"is_Match _ ⟷ False"
lemma cupcake_pmatch_related:
assumes "related_v v ml_v"
shows "match_result_related eenv (cupcake_pmatch as_static_cenv (mk_ml_pat pat) ml_v eenv) (vmatch pat v)"
using assms proof (induction pat arbitrary: v ml_v eenv)
case (Patvar name)
have "var_env (fmap_of_list [(name, v)]) [(as_string name, ml_v)]"
using Patvar by auto
hence "match_result_related eenv (Match ([(as_string name, ml_v)] @ eenv)) (Some (fmap_of_list [(name, v)]))"
by (rule match_result_related.match)
thus ?case
by simp
next
case (Patconstr name ps v0)
show ?case
using Patconstr.prems
proof (cases rule: related_v.cases)
case (conv us vs name' _)
define f where
"f p v m =
(case m of
Match env ⇒ cupcake_pmatch as_static_cenv p v env
| m ⇒ m)" for p v m
{
assume "name = name'"
assume "length ps = length us"
hence "list_all2 (λ_ _. True) us ps"
by (induct rule: list_induct2) auto
hence "list_all3 (λt p v. related_v t v) us ps vs"
using ‹list_all2 related_v us vs›
by (rule list_all3_from_list_all2s) auto
hence *: "match_result_related eenv
(Matching.fold2 f Match_type_error (map mk_ml_pat ps) vs (Match (eenv_m @ eenv)))
(map_option (foldl (++⇩f) Γ) (those (map2 vmatch ps us)))" (is "?rel")
if "var_env Γ eenv_m"
for eenv_m Γ
using Patconstr.IH ‹related_v v0 ml_v› that
proof (induction us ps vs arbitrary: Γ eenv_m rule: list_all3_induct)
case (Cons t us p ps v vs)
have "match_result_related (eenv_m @ eenv) (cupcake_pmatch as_static_cenv (mk_ml_pat p) v (eenv_m @ eenv)) (vmatch p t)"
using Cons by simp
thus ?case
proof cases
case no_match
thus ?thesis
unfolding f_def
apply (cases "length (map mk_ml_pat ps) = length vs")
by (fastforce intro: match_result_related.intros simp:cup_pmatch_list_nomatch cup_pmatch_list_length_neq)+
next
case error
thus ?thesis
unfolding f_def
apply (cases "length (map mk_ml_pat ps) = length vs")
by (fastforce intro: match_result_related.intros simp:cup_pmatch_list_typerr cup_pmatch_list_length_neq)+
next
case (match Γ' eenv_m')
have "match_result_related eenv
(Matching.fold2 f Match_type_error (map mk_ml_pat ps) vs (Match ((eenv_m' @ eenv_m) @ eenv)))
(map_option (foldl (++⇩f) (Γ ++⇩f Γ')) (those (map2 vmatch ps us)))"
proof (rule Cons, rule Cons)
show "var_env (Γ ++⇩f Γ') (eenv_m' @ eenv_m)"
using ‹var_env Γ eenv_m› match
by force
qed (simp | fact)+
thus ?thesis
using match
unfolding f_def
by (auto simp: map_option.compositionality comp_def)
qed
qed (auto intro: match_result_related.match)
moreover have "var_env fmempty []"
by force
ultimately have "?rel [] fmempty"
by fastforce
hence ?thesis
using conv ‹length ps = length us›
unfolding f_def ‹name = name'›
by (auto intro: match_result_related.intros split: option.splits elim: static_cenv_lookup)
}
moreover
{
assume "name ≠ name'"
with conv have ?thesis
by (auto intro: match_result_related.intros split: option.splits elim: same_ctor.elims simp: name.expand)
}
moreover
{
let ?fold = "Matching.fold2 f Match_type_error (map mk_ml_pat ps) vs (Match eenv)"
assume *: "length ps ≠ length us"
moreover have "length us = length vs"
using ‹list_all2 related_v us vs› by (rule list_all2_lengthD)
ultimately have "length ps ≠ length vs"
by simp
moreover have "¬ is_Match (Matching.fold2 f err xs ys init)"
if "¬ is_Match err" and "length xs ≠ length ys" for init err xs ys
using that f_def
by (induct f err xs ys init rule: fold2.induct) (auto split: match_result.splits)
ultimately have "¬ is_Match ?fold"
by simp
hence "?fold = Match_type_error ∨ ?fold = No_match"
by (cases ?fold) auto
with * have ?thesis
unfolding ‹ml_v = _› ‹v0 = _› f_def
by (auto intro: match_result_related.intros split: option.splits)
}
ultimately show ?thesis
by auto
qed (auto intro: match_result_related.intros)
qed
lemma match_all_related:
assumes "list_all2 (rel_prod related_pat related_exp) cs ml_cs"
assumes "list_all (λ(pat, _). linear pat) cs"
assumes "related_v v ml_v"
assumes "cupcake_match_result as_static_cenv ml_v ml_cs Bindv = Rval (ml_rhs, ml_pat, eenv)"
obtains rhs pat Γ where
"ml_pat = mk_ml_pat (mk_pat pat)"
"related_exp rhs ml_rhs"
"vfind_match cs v = Some (Γ, pat, rhs)"
"var_env Γ eenv"
using assms
proof (induction cs ml_cs arbitrary: thesis ml_pat ml_rhs rule: list_all2_induct)
case (Cons c cs ml_c ml_cs)
moreover obtain pat0 rhs0 where "c = (pat0, rhs0)" by fastforce
moreover obtain ml_pat0 ml_rhs0 where "ml_c = (ml_pat0, ml_rhs0)" by fastforce
ultimately have "ml_pat0 = mk_ml_pat (mk_pat pat0)" "related_exp rhs0 ml_rhs0" by auto
have "linear pat0"
using Cons(5) unfolding ‹c = _› by simp+
have rel: "match_result_related [] (cupcake_pmatch as_static_cenv (mk_ml_pat (mk_pat pat0)) ml_v []) (vmatch (mk_pat pat0) v)"
by (rule cupcake_pmatch_related) fact+
show ?case
proof (cases "cupcake_pmatch as_static_cenv ml_pat0 ml_v []")
case Match_type_error
hence False
using Cons(7) unfolding ‹ml_c = _›
by (simp split: if_splits)
thus thesis ..
next
case No_match
show thesis
proof (rule Cons(3))
show "cupcake_match_result as_static_cenv ml_v ml_cs Bindv = Rval (ml_rhs, ml_pat, eenv)"
using Cons(7) No_match unfolding ‹ml_c = _›
by (simp split: if_splits)
next
fix pat rhs Γ
assume "ml_pat = mk_ml_pat (mk_pat pat)"
assume "related_exp rhs ml_rhs"
assume "vfind_match cs v = Some (Γ, pat, rhs)"
assume "var_env Γ eenv"
from rel have "match_result_related [] No_match (vmatch (mk_pat pat0) v)"
using No_match unfolding ‹ml_pat0 = _›
by simp
hence "vmatch (mk_pat pat0) v = None"
by (cases rule: match_result_related.cases)
show thesis
proof (rule Cons(4))
show "vfind_match (c # cs) v = Some (Γ, pat, rhs)"
unfolding ‹c = _›
using ‹vfind_match cs v = _› ‹vmatch (mk_pat pat0) v = _›
by simp
qed fact+
next
show "list_all (λ(pat, _). linear pat) cs"
using Cons(5) by simp
qed fact+
next
case (Match eenv')
hence "ml_rhs = ml_rhs0" "ml_pat = ml_pat0" "eenv = eenv'"
using Cons(7) unfolding ‹ml_c = _›
by (simp split: if_splits)+
from rel have "match_result_related [] (Match eenv') (vmatch (mk_pat pat0) v) "
using Match unfolding ‹ml_pat0 = _› by simp
then obtain Γ where "vmatch (mk_pat pat0) v = Some Γ" "var_env Γ eenv'"
by (cases rule: match_result_related.cases) auto
show thesis
proof (rule Cons(4))
show "ml_pat = mk_ml_pat (mk_pat pat0)"
unfolding ‹ml_pat = _› by fact
next
show "related_exp rhs0 ml_rhs"
unfolding ‹ml_rhs = _› by fact
next
show "var_env Γ eenv"
unfolding ‹eenv = _› by fact
next
show "vfind_match (c # cs) v = Some (Γ, pat0, rhs0)"
unfolding ‹c = _›
using ‹vmatch (mk_pat pat0) v = Some Γ›
by simp
qed
qed
qed simp
end end
end