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