Theory Rhombus_HOL_Code_API

(* SPDX-License-Identifier: 0BSD *)
(* Original executable API and diagnostic refinement proofs. *)

theory Rhombus_HOL_Code_API
  imports "../verification/Rhombus_HOL_Audit" "../extensions/Rhombus_HOL_Nat_Extension"
begin

section ‹Finite code-generation façade›

type_synonym type_subst_entries = "(hname × htype) list"

definition entries_subst :: "type_subst_entries ⇒ hname ⇒ htype option" where
  "entries_subst entries = map_of entries"

definition valid_type_subst_entries ::
  "htheory ⇒ type_subst_entries ⇒ bool" where
  "valid_type_subst_entries thy entries ⟷
    distinct (map fst entries) ∧ list_all (check_type thy ∘ snd) entries"

lemma valid_type_subst_entries_lookup:
  assumes "valid_type_subst_entries thy entries"
    "entries_subst entries n = Some ty"
  shows "check_type thy ty"
  using assms map_of_SomeD
  by (auto simp: valid_type_subst_entries_def entries_subst_def list_all_iff)

lemma valid_type_subst_entries_preserve_type:
  assumes valid: "valid_type_subst_entries thy entries"
    and checked: "check_type thy ty"
  shows "check_type thy (type_subst (entries_subst entries) ty)"
  using checked
proof (induction ty)
  case (TyVar n)
  then show ?case
    using valid valid_type_subst_entries_lookup
    by (auto split: option.splits)
next
  case (TyApp n args)
  then show ?case by (auto simp: list_all_iff)
qed

definition subst_option_map ::
  "(hname ⇒ htype option) ⇒ (hname ⇒ htype option) ⇒ hname ⇒ htype option" where
  "subst_option_map σ θ n = map_option (type_subst σ) (θ n)"

lemma type_subst_option_map:
  assumes "∀n. type_var_occurs n ty ⟶ θ n ≠ None"
  shows "type_subst (subst_option_map σ θ) ty = type_subst σ (type_subst θ ty)"
  using assms
proof (induction ty)
  case (TyVar n)
  then show ?case by (cases "θ n") (auto simp: subst_option_map_def)
next
  case (TyApp n args)
  have each: "⋀arg. arg ∈ set args ⟹
      ∀v. type_var_occurs v arg ⟶ θ v ≠ None"
    using TyApp.prems by (auto simp: list_ex_iff)
  have args_eq: "map (type_subst (subst_option_map σ θ)) args =
      map (type_subst σ ∘ type_subst θ) args"
  proof (rule map_cong)
    fix arg
    assume arg: "arg ∈ set args"
    show "type_subst (subst_option_map σ θ) arg =
      (type_subst σ ∘ type_subst θ) arg"
      using TyApp.IH[OF arg each[OF arg]] by simp
  qed simp
  then show ?case by (simp only: type_subst.simps map_map o_apply)
qed

lemma fold_type_match_fuel_none [simp]:
  "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
    pairs None = None"
  by (induction pairs) auto

lemma fold_type_match_fuel_subst:
  assumes step: "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹
      type_match_fuel k p (type_subst σ t) (subst_option_map σ acc) =
        Some (subst_option_map σ out)"
    and run: "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
      pairs (Some acc) = Some out"
  shows "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
      (map (λ(p, t). (p, type_subst σ t)) pairs)
      (Some (subst_option_map σ acc)) = Some (subst_option_map σ out)"
  using run step
proof (induction pairs arbitrary: acc out)
  case Nil
  then show ?case by simp
next
  case (Cons pair pairs)
  obtain p t where pair: "pair = (p, t)" by (cases pair)
  show ?case
  proof (cases "type_match_fuel k p t acc")
    case None
    then show ?thesis using Cons.prems pair by simp
  next
    case (Some mid)
    have first: "type_match_fuel k p (type_subst σ t)
        (subst_option_map σ acc) = Some (subst_option_map σ mid)"
      using Cons.prems(2)[of p t acc mid] Some pair by simp
    have rest: "fold (λ(p, t) result.
        case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
        pairs (Some mid) = Some out"
      using Cons.prems(1) Some pair by simp
    have rest_step: "⋀p t acc out. (p, t) ∈ set pairs ⟹
        type_match_fuel k p t acc = Some out ⟹
        type_match_fuel k p (type_subst σ t) (subst_option_map σ acc) =
          Some (subst_option_map σ out)"
      using Cons.prems(2) pair by auto
    show ?thesis using Cons.IH[OF rest rest_step] first pair by simp
  qed
qed

lemma type_match_fuel_subst:
  assumes "type_match_fuel k pat ty acc = Some out"
  shows "type_match_fuel k pat (type_subst σ ty) (subst_option_map σ acc) =
    Some (subst_option_map σ out)"
  using assms
proof (induction k pat ty acc arbitrary: out rule: type_match_fuel.induct)
  case (3 k n ps m ts acc)
  show ?case
  proof (cases "n = m ∧ length ps = length ts")
    case False
    have False using 3 False by (auto split: if_splits)
    then show ?thesis by blast
  next
    case True
    have run: "fold (λ(p, t) result.
        case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
        (zip ps ts) (Some acc) = Some out"
      using 3 True by (auto split: if_splits)
    have step: "⋀p t acc out. (p, t) ∈ set (zip ps ts) ⟹
        type_match_fuel k p t acc = Some out ⟹
        type_match_fuel k p (type_subst σ t) (subst_option_map σ acc) =
          Some (subst_option_map σ out)"
    proof -
      fix p t acc' out'
      assume mem: "(p, t) ∈ set (zip ps ts)"
        and subrun: "type_match_fuel k p t acc' = Some out'"
      show "type_match_fuel k p (type_subst σ t) (subst_option_map σ acc') =
        Some (subst_option_map σ out')"
        using 3(1)[OF True mem refl subrun] .
    qed
    have transformed: "fold (λ(p, t) result.
        case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
        (map (λ(p, t). (p, type_subst σ t)) (zip ps ts))
        (Some (subst_option_map σ acc)) = Some (subst_option_map σ out)"
      using fold_type_match_fuel_subst[OF step run] .
    show ?thesis using transformed True
      by (simp add: zip_map2)
  qed
qed (auto simp: subst_option_map_def split: htype.splits option.splits if_splits)


lemma fold_type_match_fuel_invariant:
  fixes pairs :: "(htype × htype) list"
  assumes step_preserves: "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ acc v ≠ None ⟹ out v = acc v"
    and step_covers: "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ type_var_occurs v p ⟹ out v ≠ None"
    and run: "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
      pairs (Some acc) = Some out"
  shows "(acc v ≠ None ⟶ out v = acc v) ∧
    (list_ex (λ(p, t). type_var_occurs v p) pairs ⟶ out v ≠ None)"
  using step_preserves step_covers run
proof (induction pairs arbitrary: acc out)
  case Nil
  then show ?case by simp
next
  case (Cons pair pairs)
  obtain p t where pair: "pair = (p, t)" by (cases pair)
  obtain mid where first: "type_match_fuel k p t acc = Some mid"
    and rest: "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
      pairs (Some mid) = Some out"
    using Cons.prems(3) unfolding pair
    by (cases "type_match_fuel k p t acc") auto
  have head_mem: "(p, t) ∈ set (pair # pairs)" unfolding pair by simp
  have head_preserves: "acc v ≠ None ⟹ mid v = acc v"
    using Cons.prems(1)[OF head_mem first] .
  have head_covers: "type_var_occurs v p ⟹ mid v ≠ None"
    using Cons.prems(2)[OF head_mem first] .
  have tail_preserves: "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ acc v ≠ None ⟹ out v = acc v"
  proof -
    fix p t acc' out'
    assume mem: "(p, t) ∈ set pairs"
      and subrun: "type_match_fuel k p t acc' = Some out'"
      and present: "acc' v ≠ None"
    have "(p, t) ∈ set (pair # pairs)" using mem by simp
    then show "out' v = acc' v"
      using Cons.prems(1) subrun present by blast
  qed
  have tail_covers: "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ type_var_occurs v p ⟹ out v ≠ None"
  proof -
    fix p t acc' out'
    assume mem: "(p, t) ∈ set pairs"
      and subrun: "type_match_fuel k p t acc' = Some out'"
      and occurs: "type_var_occurs v p"
    have "(p, t) ∈ set (pair # pairs)" using mem by simp
    then show "out' v ≠ None"
      using Cons.prems(2) subrun occurs by blast
  qed
  have tail: "(mid v ≠ None ⟶ out v = mid v) ∧
      (list_ex (λ(p, t). type_var_occurs v p) pairs ⟶ out v ≠ None)"
  proof (rule Cons.IH)
    show "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ acc v ≠ None ⟹ out v = acc v"
      by (rule tail_preserves)
    show "⋀p t acc out. (p, t) ∈ set pairs ⟹
      type_match_fuel k p t acc = Some out ⟹ type_var_occurs v p ⟹ out v ≠ None"
      by (rule tail_covers)
    show "fold (λ(p, t) result.
      case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
      pairs (Some mid) = Some out" by (rule rest)
  qed
  show ?case using head_preserves head_covers tail unfolding pair by auto
qed

lemma type_match_fuel_invariant:
  assumes "type_match_fuel k pat ty acc = Some out"
  shows "(acc v ≠ None ⟶ out v = acc v) ∧
    (type_var_occurs v pat ⟶ out v ≠ None)"
  using assms
proof (induction k pat ty acc arbitrary: out rule: type_match_fuel.induct)
  case (3 k n ps m ts acc)
  show ?case
  proof (cases "n = m ∧ length ps = length ts")
    case False
    have False using 3 False by (auto split: if_splits)
    then show ?thesis by blast
  next
    case True
    have run: "fold (λ(p, t) result.
        case result of None ⇒ None | Some acc ⇒ type_match_fuel k p t acc)
        (zip ps ts) (Some acc) = Some out"
      using 3 True by (auto split: if_splits)
    have step_preserves: "⋀p t acc out. (p, t) ∈ set (zip ps ts) ⟹
        type_match_fuel k p t acc = Some out ⟹ acc v ≠ None ⟹ out v = acc v"
      using 3(1)[OF True] by blast
    have step_covers: "⋀p t acc out. (p, t) ∈ set (zip ps ts) ⟹
        type_match_fuel k p t acc = Some out ⟹ type_var_occurs v p ⟹ out v ≠ None"
      using 3(1)[OF True] by blast
    have folded: "(acc v ≠ None ⟶ out v = acc v) ∧
        (list_ex (λ(p, t). type_var_occurs v p) (zip ps ts) ⟶ out v ≠ None)"
      using fold_type_match_fuel_invariant[OF step_preserves step_covers run] .
    have zipped: "list_ex (type_var_occurs v) ps ⟹
        list_ex (λ(p, t). type_var_occurs v p) (zip ps ts)"
      using True
    proof (induction ps arbitrary: ts)
      case Nil
      then show ?case by simp
    next
      case (Cons p ps)
      then obtain t ts' where ts: "ts = t # ts'" by (cases ts) auto
      show ?case
      proof (cases "type_var_occurs v p")
        case True
        then show ?thesis unfolding ts by simp
      next
        case False
        have tail_occurs: "list_ex (type_var_occurs v) ps"
          using Cons.prems(1) False by simp
        have tail_length: "n = m ∧ length ps = length ts'"
          using Cons.prems(2) ts by simp
        have tail_zipped: "list_ex (λ(p, t). type_var_occurs v p) (zip ps ts')"
          using Cons.IH[OF tail_occurs tail_length] .
        then show ?thesis unfolding ts by simp
      qed
    qed
    show ?thesis using folded zipped by auto
  qed
qed (auto simp: subst_option_map_def split: htype.splits option.splits if_splits)


lemma type_match_subst:
  assumes match: "type_match pat ty (λ_. None) = Some out"
  shows "type_match pat (type_subst σ ty) (λ_. None) =
    Some (subst_option_map σ out)"
proof -
  have run: "type_match_fuel (size pat + 1) pat ty (λ_. None) = Some out"
    using match by (auto simp: type_match_def split: option.splits if_splits)
  have covers: "∀v. type_var_occurs v pat ⟶ out v ≠ None"
    using type_match_fuel_invariant[OF run] by blast
  have composed: "type_subst (subst_option_map σ out) pat = type_subst σ ty"
    using type_subst_option_map[OF covers] type_match_sound[OF match] by simp
  have empty_map: "subst_option_map σ (λ_. None) = (λ_. None)"
    by (rule ext) (simp add: subst_option_map_def)
  have transformed: "type_match_fuel (size pat + 1) pat (type_subst σ ty)
      (λ_. None) = Some (subst_option_map σ out)"
    using type_match_fuel_subst[where σ = σ, OF run] empty_map by simp
  show ?thesis unfolding type_match_def using transformed composed by simp
qed


lemma valid_type_subst_entries_type_subst_ok:
  assumes valid: "valid_type_subst_entries thy entries"
  shows "type_subst_ok thy (entries_subst entries)"
  unfolding type_subst_ok_def
proof (intro conjI)
  show "∀n ty. entries_subst entries n = Some ty ⟶ check_type thy ty"
    using valid valid_type_subst_entries_lookup by blast
  show "∀ty. check_type thy ty ⟶ check_type thy (type_subst (entries_subst entries) ty)"
    using valid valid_type_subst_entries_preserve_type by blast
  show "∀n ty. check_open_term thy [] (Const n ty) ⟶
      check_open_term thy [] (Const n (type_subst (entries_subst entries) ty))"
  proof (intro allI impI)
    fix n ty
    assume checked: "check_open_term thy [] (Const n ty)"
    have checked_type: "check_type thy (type_subst (entries_subst entries) ty)"
      using checked valid valid_type_subst_entries_preserve_type by simp
    obtain generic where generic: "const_tab thy n = Some generic"
      using checked by (cases "const_tab thy n") auto
    obtain out where matched: "type_match generic ty (λ_. None) = Some out"
      using checked generic by (cases "type_match generic ty (λ_. None)") auto
    have substituted: "type_match generic (type_subst (entries_subst entries) ty) (λ_. None) =
        Some (subst_option_map (entries_subst entries) out)"
      using type_match_subst[OF matched] .
    show "check_open_term thy [] (Const n (type_subst (entries_subst entries) ty))"
      using checked_type generic substituted by simp
  qed
qed

definition inst_type_entries ::
  "htheory ⇒ type_subst_entries ⇒ hthm ⇒ hthm option" where
  "inst_type_entries thy entries th =
    (if valid_type_subst_entries thy entries ∧
        descends (thm_stamp th) (thy_stamp thy) then
       checked_thm thy
         (rehash_hyps (map (inst_type (entries_subst entries)) (hyps th)))
         (inst_type (entries_subst entries) (concl th)) (thy_stamp thy)
     else None)"

lemma inst_type_entries_agrees:
  assumes valid: "valid_type_subst_entries thy entries"
  shows "inst_type_entries thy entries th =
    inst_type_rule thy (entries_subst entries) th"
  using valid valid_type_subst_entries_type_subst_ok[OF valid]
  by (simp add: inst_type_entries_def inst_type_rule_def)


section ‹Direct code-generation rule façade›

datatype code_failure =
    CodeUndeclaredType hname
  | CodeTypeArity hname nat nat
  | CodeInvalidType htype
  | CodeUnboundIndex nat nat
  | CodeBinderTypeMismatch nat htype htype
  | CodeUndeclaredConstant hname
  | CodeConstantTypeMismatch hname htype htype
  | CodeOperatorNotFunction hterm
  | CodeIllTypedApplication hterm
  | CodeNotProposition hterm
  | CodeNotEquation hterm
  | CodeMiddleTermsDiffer hterm hterm
  | CodeCombinationTypeMismatch
  | CodeVariableFreeInHypotheses hname
  | CodeNotBetaRedex hterm
  | CodeAntecedentMismatch hterm hterm
  | CodeInvalidInstantiationTarget hterm
  | CodeInstantiationTypeMismatch hterm hterm
  | CodeInvalidTypeSubstitution
  | CodeDuplicateType hname
  | CodeDuplicateConstant hname
  | CodeDefinitionNotEquation
  | CodeDefinitionLeftNotVariable
  | CodeDefinitionOpen hterm
  | CodeDefinitionTypeMismatch
  | CodeDefinitionExtraTypeVariables
  | CodeTypeDefinitionSameConstants
  | CodeTypeDefinitionHasHypotheses
  | CodeTypeDefinitionOpenPredicate
  | CodeTypeDefinitionExtraTypeVariables htype
  | CodeTypeDefinitionBadWitness
  | CodeRuleRejected
  | CodeExtensionRejected

datatype 'a code_result =
    CodeSuccess 'a
  | CodeFailure code_failure

fun erase_code_result :: "'a code_result ⇒ 'a option" where
  "erase_code_result (CodeSuccess value) = Some value"
| "erase_code_result (CodeFailure _) = None"

fun result_of_option :: "code_failure ⇒ 'a option ⇒ 'a code_result" where
  "result_of_option _ (Some value) = CodeSuccess value"
| "result_of_option failure None = CodeFailure failure"

lemma erase_result_of_option [simp]:
  "erase_code_result (result_of_option failure result) = result"
  by (cases result) simp_all

lemma result_of_option_success_iff [simp]:
  "result_of_option failure result = CodeSuccess value ⟷ result = Some value"
  by (cases result) simp_all

lemma result_of_option_failure_iff [simp]:
  "result_of_option failure result = CodeFailure failure ⟷ result = None"
  by (cases result) simp_all

lemma erase_code_result_option_case [simp]:
  "erase_code_result
      (case result of Some value ⇒ CodeSuccess value | None ⇒ CodeFailure failure) =
    result"
  by (cases result) simp_all

fun diagnose_type_failure :: "htheory ⇒ htype ⇒ code_failure option" where
  "diagnose_type_failure thy (TyVar _) = None"
| "diagnose_type_failure thy (TyApp n args) =
    (case tyops thy n of
       None ⇒ Some (CodeUndeclaredType n)
     | Some arity ⇒
         if arity ≠ length args then Some (CodeTypeArity n arity (length args))
         else if list_all (check_type thy) args then None
         else Some (CodeInvalidType (TyApp n args)))"

fun diagnose_open_term_failure ::
  "htheory ⇒ htype list ⇒ hterm ⇒ code_failure option" where
  "diagnose_open_term_failure thy env (FVar _ ty) = diagnose_type_failure thy ty"
| "diagnose_open_term_failure thy env (BVar i ty) =
    (if i ≥ length env then Some (CodeUnboundIndex i (length env))
     else if env ! i ≠ ty then Some (CodeBinderTypeMismatch i (env ! i) ty)
     else diagnose_type_failure thy ty)"
| "diagnose_open_term_failure thy env (Const n ty) =
    (case diagnose_type_failure thy ty of
       Some failure ⇒ Some failure
     | None ⇒ (case const_tab thy n of
         None ⇒ Some (CodeUndeclaredConstant n)
       | Some generic ⇒ if type_match generic ty (λ_. None) = None
           then Some (CodeConstantTypeMismatch n generic ty) else None))"
| "diagnose_open_term_failure thy env (NatLit _) =
    (case diagnose_type_failure thy nat_aty of
       Some failure ⇒ Some failure
     | None ⇒ (case diagnose_type_failure thy nat_sty of
         Some failure ⇒ Some failure
       | None ⇒ (case const_tab thy nat_zero_name of
           None ⇒ Some (CodeUndeclaredConstant nat_zero_name)
         | Some zero_ty ⇒ if zero_ty ≠ nat_aty
             then Some (CodeConstantTypeMismatch nat_zero_name zero_ty nat_aty)
             else (case const_tab thy nat_succ_name of
               None ⇒ Some (CodeUndeclaredConstant nat_succ_name)
             | Some succ_ty ⇒ if succ_ty = nat_sty then None
                 else Some (CodeConstantTypeMismatch nat_succ_name succ_ty nat_sty)))))"
| "diagnose_open_term_failure thy env (Comb f x) =
    (case diagnose_open_term_failure thy env f of
       Some failure ⇒ Some failure
     | None ⇒ (case diagnose_open_term_failure thy env x of
         Some failure ⇒ Some failure
       | None ⇒ (case type_of f of
           Some (TyApp NFun [arg_ty, result_ty]) ⇒
             if type_of x = Some arg_ty then None
             else Some (CodeIllTypedApplication (Comb f x))
         | _ ⇒ Some (CodeOperatorNotFunction (Comb f x)))))"
| "diagnose_open_term_failure thy env (Abs aty body) =
    (case diagnose_type_failure thy aty of
       Some failure ⇒ Some failure
     | None ⇒ diagnose_open_term_failure thy (aty # env) body)"

definition diagnose_term_failure :: "htheory ⇒ hterm ⇒ code_failure" where
  "diagnose_term_failure thy t =
    (case diagnose_open_term_failure thy [] t of
       Some failure ⇒ failure
     | None ⇒ CodeRuleRejected)"

definition diagnose_prop_failure :: "htheory ⇒ hterm ⇒ code_failure" where
  "diagnose_prop_failure thy p =
    (case diagnose_open_term_failure thy [] p of
       Some failure ⇒ failure
     | None ⇒ CodeNotProposition p)"

definition diagnose_trans_failure :: "hthm ⇒ hthm ⇒ code_failure" where
  "diagnose_trans_failure a b =
    (case dest_eq (concl a) of
       None ⇒ CodeNotEquation (concl a)
     | Some (_, middle) ⇒ (case dest_eq (concl b) of
         None ⇒ CodeNotEquation (concl b)
       | Some (middle', _) ⇒ if middle = middle' then CodeRuleRejected
           else CodeMiddleTermsDiffer middle middle'))"

definition diagnose_mk_comb_failure :: "hthm ⇒ hthm ⇒ code_failure" where
  "diagnose_mk_comb_failure fth xth =
    (case dest_eq (concl fth) of
       None ⇒ CodeNotEquation (concl fth)
     | Some (f, _) ⇒ (case dest_eq (concl xth) of
         None ⇒ CodeNotEquation (concl xth)
       | Some (x, _) ⇒ (case type_of f of
           Some (TyApp NFun [arg_ty, result_ty]) ⇒
             if type_of x = Some arg_ty then CodeRuleRejected
             else CodeCombinationTypeMismatch
         | _ ⇒ CodeOperatorNotFunction f)))"

definition diagnose_abs_failure ::
  "htheory ⇒ hname ⇒ htype ⇒ hthm ⇒ code_failure" where
  "diagnose_abs_failure thy n ty th =
    (case diagnose_open_term_failure thy [] (FVar n ty) of
       Some failure ⇒ failure
     | None ⇒ if list_ex (vfree_in n ty) (hyps th)
         then CodeVariableFreeInHypotheses n
         else if dest_eq (concl th) = None then CodeNotEquation (concl th)
         else CodeRuleRejected)"

definition diagnose_beta_failure :: "htheory ⇒ hterm ⇒ code_failure" where
  "diagnose_beta_failure thy t =
    (case diagnose_open_term_failure thy [] t of
       Some failure ⇒ failure
     | None ⇒ CodeNotBetaRedex t)"

definition diagnose_eq_mp_failure :: "hthm ⇒ hthm ⇒ code_failure" where
  "diagnose_eq_mp_failure eqth th =
    (case dest_eq (concl eqth) of
       None ⇒ CodeNotEquation (concl eqth)
     | Some (expected, _) ⇒ if expected = concl th then CodeRuleRejected
         else CodeAntecedentMismatch expected (concl th))"

fun diagnose_inst_entries ::
  "htheory ⇒ (hterm × hterm) list ⇒ code_failure option" where
  "diagnose_inst_entries thy [] = None"
| "diagnose_inst_entries thy ((replacement, target) # rest) =
    (case target of
       FVar _ ty ⇒ (case diagnose_open_term_failure thy [] replacement of
         Some failure ⇒ Some failure
       | None ⇒ if type_of replacement ≠ Some ty
           then Some (CodeInstantiationTypeMismatch target replacement)
           else diagnose_inst_entries thy rest)
     | _ ⇒ Some (CodeInvalidInstantiationTarget target))"

definition diagnose_inst_failure ::
  "htheory ⇒ (hterm × hterm) list ⇒ code_failure" where
  "diagnose_inst_failure thy entries =
    (case diagnose_inst_entries thy entries of
       Some failure ⇒ failure
     | None ⇒ CodeRuleRejected)"

fun diagnose_type_entries ::
  "htheory ⇒ type_subst_entries ⇒ code_failure option" where
  "diagnose_type_entries thy [] = None"
| "diagnose_type_entries thy ((_, ty) # rest) =
    (case diagnose_type_failure thy ty of
       Some failure ⇒ Some failure
     | None ⇒ diagnose_type_entries thy rest)"

definition code_check_type :: "htheory ⇒ htype ⇒ unit code_result" where
  "code_check_type thy ty =
    (if check_type thy ty then CodeSuccess ()
     else case diagnose_type_failure thy ty of
       Some failure ⇒ CodeFailure failure
     | None ⇒ CodeFailure CodeRuleRejected)"

definition code_check_term :: "htheory ⇒ hterm ⇒ unit code_result" where
  "code_check_term thy t =
    (if check_term thy t then CodeSuccess ()
     else case diagnose_open_term_failure thy [] t of
       Some failure ⇒ CodeFailure failure
     | None ⇒ CodeFailure CodeRuleRejected)"
definition code_refl :: "htheory ⇒ hterm ⇒ hthm code_result" where
  "code_refl thy t =
    (case refl thy t of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_term_failure thy t))"

definition code_trans :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm code_result" where
  "code_trans thy a b =
    (case trans thy a b of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_trans_failure a b))"

definition code_mk_comb :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm code_result" where
  "code_mk_comb thy fth xth =
    (case mk_comb_rule thy fth xth of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_mk_comb_failure fth xth))"

definition code_abs ::
  "htheory ⇒ hname ⇒ htype ⇒ hthm ⇒ hthm code_result" where
  "code_abs thy n ty th =
    (case abs_rule thy n ty th of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_abs_failure thy n ty th))"

definition code_beta :: "htheory ⇒ hterm ⇒ hthm code_result" where
  "code_beta thy t =
    (case beta thy t of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_beta_failure thy t))"

definition code_assume :: "htheory ⇒ hterm ⇒ hthm code_result" where
  "code_assume thy p =
    (case assume_rule thy p of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_prop_failure thy p))"

definition code_eq_mp :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm code_result" where
  "code_eq_mp thy eqth th =
    (case eq_mp thy eqth th of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_eq_mp_failure eqth th))"

definition code_deduct_antisym ::
  "htheory ⇒ hthm ⇒ hthm ⇒ hthm code_result" where
  "code_deduct_antisym thy a b =
    result_of_option CodeRuleRejected (deduct_antisym_rule thy a b)"

definition code_inst ::
  "htheory ⇒ (hterm × hterm) list ⇒ hthm ⇒ hthm code_result" where
  "code_inst thy entries th =
    (case inst thy entries th of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_inst_failure thy entries))"

definition code_inst_type ::
  "htheory ⇒ type_subst_entries ⇒ hthm ⇒ hthm code_result" where
  "code_inst_type thy entries th =
    (if valid_type_subst_entries thy entries then
       result_of_option CodeRuleRejected (inst_type_entries thy entries th)
     else (case diagnose_type_entries thy entries of
       Some failure ⇒ CodeFailure failure
     | None ⇒ CodeFailure CodeInvalidTypeSubstitution))"
lemma code_refl_erasure [simp]:
  "erase_code_result (code_refl thy t) = refl thy t"
  by (simp add: code_refl_def)

lemma code_trans_erasure [simp]:
  "erase_code_result (code_trans thy a b) = trans thy a b"
  by (simp add: code_trans_def)

lemma code_mk_comb_erasure [simp]:
  "erase_code_result (code_mk_comb thy fth xth) = mk_comb_rule thy fth xth"
  by (simp add: code_mk_comb_def)

lemma code_abs_erasure [simp]:
  "erase_code_result (code_abs thy n ty th) = abs_rule thy n ty th"
  by (simp add: code_abs_def)

lemma code_beta_erasure [simp]:
  "erase_code_result (code_beta thy t) = beta thy t"
  by (simp add: code_beta_def)

lemma code_assume_erasure [simp]:
  "erase_code_result (code_assume thy p) = assume_rule thy p"
  by (simp add: code_assume_def)

lemma code_eq_mp_erasure [simp]:
  "erase_code_result (code_eq_mp thy eqth th) = eq_mp thy eqth th"
  by (simp add: code_eq_mp_def)

lemma code_deduct_antisym_erasure [simp]:
  "erase_code_result (code_deduct_antisym thy a b) = deduct_antisym_rule thy a b"
  by (simp add: code_deduct_antisym_def)

lemma code_inst_erasure [simp]:
  "erase_code_result (code_inst thy entries th) = inst thy entries th"
  by (simp add: code_inst_def)

lemma code_inst_type_erasure [simp]:
  "erase_code_result (code_inst_type thy entries th) = inst_type_entries thy entries th"
  by (cases "valid_type_subst_entries thy entries";
      cases "diagnose_type_entries thy entries")
     (simp_all add: code_inst_type_def inst_type_entries_def)

lemma code_result_success_iff [simp]:
  "result = CodeSuccess value ⟷ erase_code_result result = Some value"
  by (cases result) simp_all

lemma code_result_failure_iff [simp]:
  "(∃failure. result = CodeFailure failure) ⟷ erase_code_result result = None"
  by (cases result) auto

section ‹Direct code-generation extension façade›

definition diagnose_new_type_failure :: "htheory ⇒ hname ⇒ code_failure" where
  "diagnose_new_type_failure thy n =
    (if tyops thy n = None then CodeExtensionRejected else CodeDuplicateType n)"

definition diagnose_new_constant_failure ::
  "htheory ⇒ hname ⇒ htype ⇒ code_failure" where
  "diagnose_new_constant_failure thy n ty =
    (if const_tab thy n ≠ None then CodeDuplicateConstant n
     else case diagnose_type_failure thy ty of
       Some failure ⇒ failure
     | None ⇒ CodeExtensionRejected)"

definition diagnose_definition_failure ::
  "htheory ⇒ hterm ⇒ code_failure" where
  "diagnose_definition_failure thy tm =
    (case dest_eq tm of
       None ⇒ CodeDefinitionNotEquation
     | Some (lhs, rhs) ⇒ (case lhs of
         FVar n ty ⇒
           if const_tab thy n ≠ None then CodeDuplicateConstant n
           else (case diagnose_open_term_failure thy [] rhs of
             Some failure ⇒ failure
           | None ⇒ (case free_vars rhs of
               free # _ ⇒ CodeDefinitionOpen (case free of (v, vty) ⇒ FVar v vty)
             | [] ⇒ if type_of rhs ≠ Some ty then CodeDefinitionTypeMismatch
                 else if ¬ set (term_type_vars rhs) ⊆ set (type_vars ty)
                   then CodeDefinitionExtraTypeVariables
                 else CodeExtensionRejected))
       | _ ⇒ CodeDefinitionLeftNotVariable))"

definition diagnose_type_definition_failure ::
  "htheory ⇒ hname ⇒ hname ⇒ hname ⇒ hthm ⇒ code_failure" where
  "diagnose_type_definition_failure thy tyname absname repname wit =
    (if ¬ wf_thm thy wit then CodeTypeDefinitionBadWitness
     else if hyps wit ≠ [] then CodeTypeDefinitionHasHypotheses
     else if tyops thy tyname ≠ None then CodeDuplicateType tyname
     else if const_tab thy absname ≠ None then CodeDuplicateConstant absname
     else if const_tab thy repname ≠ None then CodeDuplicateConstant repname
     else if absname = repname then CodeTypeDefinitionSameConstants
     else case concl wit of
       Comb pred witness ⇒ (case type_of witness of
         None ⇒ CodeTypeDefinitionBadWitness
       | Some rty ⇒ if free_vars pred ≠ [] then CodeTypeDefinitionOpenPredicate
           else if ¬ set (type_vars rty) ⊆ set (term_type_vars pred)
             then CodeTypeDefinitionExtraTypeVariables rty
           else CodeExtensionRejected)
     | _ ⇒ CodeTypeDefinitionBadWitness)"

definition code_new_type ::
  "nat ⇒ htheory ⇒ hname ⇒ nat ⇒ htheory code_result" where
  "code_new_type fresh thy n arity =
    (case new_type fresh thy n arity of
       Some thy' ⇒ CodeSuccess thy'
     | None ⇒ CodeFailure (diagnose_new_type_failure thy n))"

definition code_new_constant ::
  "nat ⇒ htheory ⇒ hname ⇒ htype ⇒ htheory code_result" where
  "code_new_constant fresh thy n ty =
    (case new_constant fresh thy n ty of
       Some thy' ⇒ CodeSuccess thy'
     | None ⇒ CodeFailure (diagnose_new_constant_failure thy n ty))"

definition code_new_axiom ::
  "nat ⇒ htheory ⇒ hterm ⇒ (htheory × hthm) code_result" where
  "code_new_axiom fresh thy p =
    (case new_axiom fresh thy p of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_prop_failure thy p))"

definition code_new_basic_definition ::
  "nat ⇒ htheory ⇒ hterm ⇒ (htheory × hthm) code_result" where
  "code_new_basic_definition fresh thy tm =
    (case new_basic_definition fresh thy tm of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure (diagnose_definition_failure thy tm))"

definition code_new_basic_type_definition ::
  "nat ⇒ htheory ⇒ hname ⇒ hname ⇒ hname ⇒ hthm ⇒
    (htheory × hthm × hthm) code_result" where
  "code_new_basic_type_definition fresh thy tyname absname repname witness =
    (case new_basic_type_definition fresh thy tyname absname repname witness of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure
         (diagnose_type_definition_failure thy tyname absname repname witness))"

definition code_nat_lit_conv :: "htheory ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_conv thy n =
    (case nat_lit_conv thy n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

lemma code_nat_lit_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_conv thy n) = nat_lit_conv thy n"
  by (simp add: code_nat_lit_conv_def)

definition code_nat_lit_eq_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_eq_conv thy zero_not_succ succ_injective m n =
    (case nat_lit_eq_conv thy zero_not_succ succ_injective m n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

lemma code_nat_lit_eq_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_eq_conv thy zns si m n) =
    nat_lit_eq_conv thy zns si m n"
  by (simp add: code_nat_lit_eq_conv_def)

definition code_nat_lit_add_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_add_conv thy add_zero add_succ m n =
    (case nat_lit_add_conv thy add_zero add_succ m n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

definition code_nat_lit_mul_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_mul_conv thy add_zero add_succ mul_zero mul_succ m n =
    (case nat_lit_mul_conv thy add_zero add_succ mul_zero mul_succ m n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

definition code_nat_lit_le_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_le_conv thy le_zero le_succ_zero le_succ_succ m n =
    (case nat_lit_le_conv thy le_zero le_succ_zero le_succ_succ m n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

definition code_nat_lit_sub_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_sub_conv thy sub_zero sub_succ_zero sub_succ_succ m n =
    (case nat_lit_sub_conv thy sub_zero sub_succ_zero sub_succ_succ m n of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

definition code_nat_lit_pow_conv ::
  "htheory ⇒ hthm ⇒ hthm ⇒ hthm ⇒ hthm ⇒ hthm ⇒ hthm ⇒ nat ⇒ nat ⇒ hthm code_result" where
  "code_nat_lit_pow_conv thy add_zero add_succ mul_zero mul_succ pow_zero pow_succ
      base exponent =
    (case nat_lit_pow_conv thy add_zero add_succ mul_zero mul_succ pow_zero pow_succ
        base exponent of
       Some th ⇒ CodeSuccess th
     | None ⇒ CodeFailure CodeExtensionRejected)"

lemma code_nat_lit_add_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_add_conv thy az ass m n) =
    nat_lit_add_conv thy az ass m n"
  by (simp add: code_nat_lit_add_conv_def)

lemma code_nat_lit_mul_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_mul_conv thy az ass mz ms m n) =
    nat_lit_mul_conv thy az ass mz ms m n"
  by (simp add: code_nat_lit_mul_conv_def)

lemma code_nat_lit_le_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_le_conv thy lz lsz lss m n) =
    nat_lit_le_conv thy lz lsz lss m n"
  by (simp add: code_nat_lit_le_conv_def)

lemma code_nat_lit_sub_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_sub_conv thy sz ssz sss m n) =
    nat_lit_sub_conv thy sz ssz sss m n"
  by (simp add: code_nat_lit_sub_conv_def)

lemma code_nat_lit_pow_conv_erasure [simp]:
  "erase_code_result (code_nat_lit_pow_conv thy az ass mz ms pz ps b e) =
    nat_lit_pow_conv thy az ass mz ms pz ps b e"
  by (simp add: code_nat_lit_pow_conv_def)

definition code_new_nat_type ::
  "nat ⇒ htheory ⇒ (htheory × hthm × hthm × hthm) code_result" where
  "code_new_nat_type fresh thy =
    (case new_nat_type fresh thy of
       Some result ⇒ CodeSuccess result
     | None ⇒ CodeFailure CodeExtensionRejected)"

lemma code_new_nat_type_erasure [simp]:
  "erase_code_result (code_new_nat_type fresh thy) = new_nat_type fresh thy"
  by (simp add: code_new_nat_type_def)

lemma code_new_type_erasure [simp]:
  "erase_code_result (code_new_type fresh thy n arity) =
    new_type fresh thy n arity"
  by (simp add: code_new_type_def)

lemma code_new_constant_erasure [simp]:
  "erase_code_result (code_new_constant fresh thy n ty) =
    new_constant fresh thy n ty"
  by (simp add: code_new_constant_def)

lemma code_new_axiom_erasure [simp]:
  "erase_code_result (code_new_axiom fresh thy p) = new_axiom fresh thy p"
  by (simp add: code_new_axiom_def)

lemma code_new_basic_definition_erasure [simp]:
  "erase_code_result (code_new_basic_definition fresh thy tm) =
    new_basic_definition fresh thy tm"
  by (simp add: code_new_basic_definition_def)

lemma code_new_basic_type_definition_erasure [simp]:
  "erase_code_result
      (code_new_basic_type_definition fresh thy tn an rn witness) =
    new_basic_type_definition fresh thy tn an rn witness"
  by (simp add: code_new_basic_type_definition_def)

end