Theory Rhombus_HOL_Kernel

(* SPDX-FileCopyrightText: 2026 Masaya Taniguchi *)
(* SPDX-FileCopyrightText: 1998 University of Cambridge *)
(* SPDX-FileCopyrightText: 1998-2007 John Harrison *)
(* SPDX-License-Identifier: 0BSD AND BSD-2-Clause *)
(* Adapts the primitive kernel rules in HOL Light fusion.ml; see ../THIRD_PARTY_NOTICES. *)

theory Rhombus_HOL_Kernel
  imports Rhombus_HOL_Substitution
begin

section ‹Executable primitive rules›

text ‹Rhombus correspondence: kernel.rhm's ten primitive inference rules. Each branch mirrors the source; option replaces source exceptions.›

definition checked_thm :: "htheory ⇒ hterm list ⇒ hterm ⇒ stamp ⇒ hthm option" where
  "checked_thm thy hs c st =
    (let th = ⦇hyps = hs, concl = c, thm_stamp = st⦈
     in if wf_thm thy th then Some th else None)"

definition checked_eq_thm ::
  "htheory ⇒ hterm list ⇒ hterm ⇒ hterm ⇒ stamp ⇒ hthm option" where
  "checked_eq_thm thy hs l r st =
    (case mk_eq l r of None ⇒ None | Some eq ⇒ checked_thm thy hs eq st)"

definition refl :: "htheory ⇒ hterm ⇒ hthm option" where
  "refl thy t = checked_eq_thm thy [] t t (thy_stamp thy)"

definition trans :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm option" where
  "trans thy a b =
    (case (dest_eq (concl a), dest_eq (concl b),
           combine_stamps (thm_stamp a) (thm_stamp b)) of
       (Some (l, m), Some (m', r), Some st) ⇒
          if m = m' then checked_eq_thm thy (hyp_union (hyps a) (hyps b)) l r st
          else None
     | _ ⇒ None)"

definition mk_comb_rule :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm option" where
  "mk_comb_rule thy fth xth =
    (case (dest_eq (concl fth), dest_eq (concl xth),
           combine_stamps (thm_stamp fth) (thm_stamp xth)) of
       (Some (f, g), Some (x, y), Some st) ⇒
          checked_eq_thm thy (hyp_union (hyps fth) (hyps xth))
            (Comb f x) (Comb g y) st
     | _ ⇒ None)"

definition abs_rule :: "htheory ⇒ hname ⇒ htype ⇒ hthm ⇒ hthm option" where
  "abs_rule thy n ty th =
    (case dest_eq (concl th) of
       None ⇒ None
     | Some (l, r) ⇒
         if descends (thm_stamp th) (thy_stamp thy) ∧
            check_term thy (FVar n ty) ∧
            (∀h∈set (hyps th). ¬ vfree_in n ty h)
         then checked_eq_thm thy (hyps th)
           (Abs ty (abstract_fvar n ty l)) (Abs ty (abstract_fvar n ty r))
           (thy_stamp thy)
         else None)"

definition beta :: "htheory ⇒ hterm ⇒ hthm option" where
  "beta thy t =
    (case t of Comb (Abs aty body) arg ⇒
       if check_term thy t then checked_eq_thm thy [] t (subst_bvar arg body)
         (thy_stamp thy)
       else None
     | _ ⇒ None)"

definition assume_rule :: "htheory ⇒ hterm ⇒ hthm option" where
  "assume_rule thy p =
    (if check_prop thy p then checked_thm thy [p] p (thy_stamp thy) else None)"

definition eq_mp :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm option" where
  "eq_mp thy eqth th =
    (case (dest_eq (concl eqth),
           combine_stamps (thm_stamp eqth) (thm_stamp th)) of
       (Some (p, q), Some st) ⇒
          if p = concl th then
            checked_thm thy (hyp_union (hyps eqth) (hyps th)) q st
          else None
     | _ ⇒ None)"

definition deduct_antisym_rule :: "htheory ⇒ hthm ⇒ hthm ⇒ hthm option" where
  "deduct_antisym_rule thy a b =
    (case combine_stamps (thm_stamp a) (thm_stamp b) of
       None ⇒ None
     | Some st ⇒ checked_eq_thm thy
         (hyp_union (hyp_remove (concl b) (hyps a))
                    (hyp_remove (concl a) (hyps b)))
         (concl a) (concl b) st)"

fun decode_term_subst ::
  "(hterm × hterm) list ⇒ (hterm × (hname × htype)) list option" where
  "decode_term_subst [] = Some []"
| "decode_term_subst ((rep, FVar n ty) # rest) =
    map_option ((#) (rep, (n, ty))) (decode_term_subst rest)"
| "decode_term_subst ((_ , _) # _) = None"

definition inst :: "htheory ⇒ (hterm × hterm) list ⇒ hthm ⇒ hthm option" where
  "inst thy raw th =
    (case decode_term_subst raw of
       None ⇒ None
     | Some θ ⇒
         if descends (thm_stamp th) (thy_stamp thy) ∧ wf_term_subst thy θ then
           checked_thm thy (rehash_hyps (map (inst_fvar θ) (hyps th)))
             (inst_fvar θ (concl th)) (thy_stamp thy)
         else None)"

definition inst_type_rule ::
  "htheory ⇒ (hname ⇒ htype option) ⇒ hthm ⇒ hthm option" where
  "inst_type_rule thy θ th =
    (if descends (thm_stamp th) (thy_stamp thy) ∧ type_subst_ok thy θ then
       checked_thm thy (rehash_hyps (map (inst_type θ) (hyps th)))
         (inst_type θ (concl th)) (thy_stamp thy)
     else None)"

lemma type_subst_empty [simp]: "type_subst (λ_. None) ty = ty"
proof (induction ty)
  case (TyApp n args)
  then have "map (type_subst (λ_. None)) args = map id args"
    by (intro map_cong) auto
  then show ?case by simp
qed simp

lemma type_subst_ok_empty [simp]: "type_subst_ok thy (λ_. None)"
  by (simp add: type_subst_ok_def)

section ‹Rule requests and declarative results›

datatype inference =
    IRefl htheory hterm
  | ITrans htheory hthm hthm
  | IMkComb htheory hthm hthm
  | IAbs htheory hname htype hthm
  | IBeta htheory hterm
  | IAssume htheory hterm
  | IEqMp htheory hthm hthm
  | IDeductAntisym htheory hthm hthm
  | IInst htheory "(hterm × hterm) list" hthm
  | IInstType htheory "hname ⇒ htype option" hthm

fun ambient_theory :: "inference ⇒ htheory" where
  "ambient_theory (IRefl thy _) = thy"
| "ambient_theory (ITrans thy _ _) = thy"
| "ambient_theory (IMkComb thy _ _) = thy"
| "ambient_theory (IAbs thy _ _ _) = thy"
| "ambient_theory (IBeta thy _) = thy"
| "ambient_theory (IAssume thy _) = thy"
| "ambient_theory (IEqMp thy _ _) = thy"
| "ambient_theory (IDeductAntisym thy _ _) = thy"
| "ambient_theory (IInst thy _ _) = thy"
| "ambient_theory (IInstType thy _ _) = thy"

fun run_rule :: "inference ⇒ hthm option" where
  "run_rule (IRefl thy t) = refl thy t"
| "run_rule (ITrans thy a b) = trans thy a b"
| "run_rule (IMkComb thy a b) = mk_comb_rule thy a b"
| "run_rule (IAbs thy n ty th) = abs_rule thy n ty th"
| "run_rule (IBeta thy t) = beta thy t"
| "run_rule (IAssume thy p) = assume_rule thy p"
| "run_rule (IEqMp thy a b) = eq_mp thy a b"
| "run_rule (IDeductAntisym thy a b) = deduct_antisym_rule thy a b"
| "run_rule (IInst thy θ th) = inst thy θ th"
| "run_rule (IInstType thy θ th) = inst_type_rule thy θ th"

fun wf_inputs :: "inference ⇒ bool" where
  "wf_inputs (IRefl thy t) = check_term thy t"
| "wf_inputs (ITrans thy a b) = (wf_thm thy a ∧ wf_thm thy b)"
| "wf_inputs (IMkComb thy a b) = (wf_thm thy a ∧ wf_thm thy b)"
| "wf_inputs (IAbs thy n ty th) =
    (wf_thm thy th ∧ check_term thy (FVar n ty) ∧
      (∀h∈set (hyps th). ¬ vfree_in n ty h))"
| "wf_inputs (IBeta thy t) = check_term thy t"
| "wf_inputs (IAssume thy p) = check_prop thy p"
| "wf_inputs (IEqMp thy a b) = (wf_thm thy a ∧ wf_thm thy b)"
| "wf_inputs (IDeductAntisym thy a b) = (wf_thm thy a ∧ wf_thm thy b)"
| "wf_inputs (IInst thy raw th) =
    (wf_thm thy th ∧ (∃θ. decode_term_subst raw = Some θ ∧ wf_term_subst thy θ))"
| "wf_inputs (IInstType thy θ th) = (wf_thm thy th ∧ type_subst_ok thy θ)"

definition thm_shape ::
  "htheory ⇒ hterm list ⇒ hterm ⇒ stamp ⇒ hthm ⇒ bool" where
  "thm_shape thy hs c st th ⟷
    th = ⦇hyps = hs, concl = c, thm_stamp = st⦈ ∧ wf_thm thy th"

definition eq_shape ::
  "htheory ⇒ hterm list ⇒ hterm ⇒ hterm ⇒ stamp ⇒ hthm ⇒ bool" where
  "eq_shape thy hs l r st th ⟷
    (∃ty. type_of l = Some ty ∧ type_of r = Some ty ∧
      thm_shape thy hs (eq_term ty l r) st th)"

lemma checked_thm_iff [simp]:
  "checked_thm thy hs c st = Some th ⟷ thm_shape thy hs c st th"
  by (auto simp: checked_thm_def thm_shape_def Let_def split: if_splits)

lemma checked_eq_thm_iff [simp]:
  "checked_eq_thm thy hs l r st = Some th ⟷ eq_shape thy hs l r st th"
  by (auto simp: checked_eq_thm_def eq_shape_def mk_eq_def
      split: option.splits if_splits prod.splits)

text ‹The specification below is phrased only with sequents, equality shapes, lineage, and side conditions; no premise mentions an executable rule.›

inductive rule_spec :: "inference ⇒ hthm ⇒ bool" where
  Refl_spec:
    "eq_shape thy [] t t (thy_stamp thy) th ⟹ rule_spec (IRefl thy t) th"
| Trans_spec:
    "⟦dest_eq (concl a) = Some (l, m); dest_eq (concl b) = Some (m, r);
      combine_stamps (thm_stamp a) (thm_stamp b) = Some st;
      eq_shape thy (hyp_union (hyps a) (hyps b)) l r st th⟧
     ⟹ rule_spec (ITrans thy a b) th"
| MkComb_spec:
    "⟦dest_eq (concl a) = Some (f, g); dest_eq (concl b) = Some (x, y);
      combine_stamps (thm_stamp a) (thm_stamp b) = Some st;
      eq_shape thy (hyp_union (hyps a) (hyps b)) (Comb f x) (Comb g y) st th⟧
     ⟹ rule_spec (IMkComb thy a b) th"
| Abs_spec:
    "⟦dest_eq (concl old) = Some (l, r);
      descends (thm_stamp old) (thy_stamp thy); check_term thy (FVar n ty);
      ∀h∈set (hyps old). ¬ vfree_in n ty h;
      eq_shape thy (hyps old) (Abs ty (abstract_fvar n ty l))
        (Abs ty (abstract_fvar n ty r)) (thy_stamp thy) th⟧
     ⟹ rule_spec (IAbs thy n ty old) th"
| Beta_spec:
    "⟦check_term thy (Comb (Abs aty body) arg);
      eq_shape thy [] (Comb (Abs aty body) arg) (subst_bvar arg body)
        (thy_stamp thy) th⟧
     ⟹ rule_spec (IBeta thy (Comb (Abs aty body) arg)) th"
| Assume_spec:
    "⟦check_prop thy p; thm_shape thy [p] p (thy_stamp thy) th⟧
     ⟹ rule_spec (IAssume thy p) th"
| EqMp_spec:
    "⟦dest_eq (concl eqth) = Some (p, q); p = concl old;
      combine_stamps (thm_stamp eqth) (thm_stamp old) = Some st;
      thm_shape thy (hyp_union (hyps eqth) (hyps old)) q st th⟧
     ⟹ rule_spec (IEqMp thy eqth old) th"
| DeductAntisym_spec:
    "⟦combine_stamps (thm_stamp a) (thm_stamp b) = Some st;
      eq_shape thy
        (hyp_union (hyp_remove (concl b) (hyps a))
                   (hyp_remove (concl a) (hyps b)))
        (concl a) (concl b) st th⟧
     ⟹ rule_spec (IDeductAntisym thy a b) th"
| Inst_spec:
    "⟦decode_term_subst raw = Some θ;
      descends (thm_stamp old) (thy_stamp thy); wf_term_subst thy θ;
      thm_shape thy (rehash_hyps (map (inst_fvar θ) (hyps old)))
        (inst_fvar θ (concl old)) (thy_stamp thy) th⟧
     ⟹ rule_spec (IInst thy raw old) th"
| InstType_spec:
    "⟦descends (thm_stamp old) (thy_stamp thy); type_subst_ok thy θ;
      thm_shape thy (rehash_hyps (map (inst_type θ) (hyps old)))
        (inst_type θ (concl old)) (thy_stamp thy) th⟧
     ⟹ rule_spec (IInstType thy θ old) th"

lemma thm_shape_wf: "thm_shape thy hs c st th ⟹ wf_thm thy th"
  by (auto simp: thm_shape_def)

lemma eq_shape_wf: "eq_shape thy hs l r st th ⟹ wf_thm thy th"
  by (auto simp: eq_shape_def thm_shape_def)

theorem run_rule_preserves_wf:
  assumes "run_rule i = Some th" "wf_inputs i"
  shows "wf_thm (ambient_theory i) th"
  using assms
  by (cases i)
     (auto simp: refl_def trans_def mk_comb_rule_def abs_rule_def beta_def
       assume_rule_def eq_mp_def deduct_antisym_rule_def inst_def inst_type_rule_def
       split: option.splits prod.splits hterm.splits if_splits
       dest: thm_shape_wf eq_shape_wf)

theorem run_rule_sound:
  assumes "run_rule i = Some th"
  shows "rule_spec i th"
  using assms
  by (cases i)
     (auto simp: refl_def trans_def mk_comb_rule_def abs_rule_def beta_def
       assume_rule_def eq_mp_def deduct_antisym_rule_def inst_def inst_type_rule_def
       split: option.splits prod.splits hterm.splits if_splits
       intro: rule_spec.intros)

theorem run_rule_complete:
  assumes "rule_spec i th"
  shows "run_rule i = Some th"
  using assms
  by cases
     (auto simp: refl_def trans_def mk_comb_rule_def abs_rule_def beta_def
       assume_rule_def eq_mp_def deduct_antisym_rule_def inst_def inst_type_rule_def
       split: option.splits prod.splits hterm.splits if_splits)

section ‹Finite derivations and lineage›

fun input_thms :: "inference ⇒ hthm list" where
  "input_thms (IRefl _ _) = []"
| "input_thms (ITrans _ a b) = [a, b]"
| "input_thms (IMkComb _ a b) = [a, b]"
| "input_thms (IAbs _ _ _ th) = [th]"
| "input_thms (IBeta _ _) = []"
| "input_thms (IAssume _ _) = []"
| "input_thms (IEqMp _ a b) = [a, b]"
| "input_thms (IDeductAntisym _ a b) = [a, b]"
| "input_thms (IInst _ _ th) = [th]"
| "input_thms (IInstType _ _ th) = [th]"

inductive derives :: "htheory ⇒ hthm ⇒ bool" where
  Axiom: "⟦th ∈ set (axiom_list thy); wf_thm thy th⟧ ⟹ derives thy th"
| Primitive: "⟦ambient_theory i = thy; rule_spec i th;
    list_all (derives thy) (input_thms i)⟧ ⟹ derives thy th"

lemma rule_spec_wf:
  "rule_spec i th ⟹ wf_thm (ambient_theory i) th"
  by (induction rule: rule_spec.induct)
     (auto dest: thm_shape_wf eq_shape_wf)

theorem derives_wf: "derives thy th ⟹ wf_thm thy th"
  by (induction rule: derives.induct)
     (auto dest: rule_spec_wf)

lemma combine_stamps_returns_later:
  "combine_stamps a b = Some st ⟹
    (descends a b ∧ st = b) ∨ (¬ descends a b ∧ descends b a ∧ st = a)"
  by (auto simp: combine_stamps_def split: if_splits)

lemma trans_rejects_siblings:
  assumes "¬ descends (thm_stamp a) (thm_stamp b)"
    "¬ descends (thm_stamp b) (thm_stamp a)"
  shows "trans thy a b = None"
  using assms by (simp add: trans_def combine_stamps_def split: option.splits prod.splits)

lemma abs_rule_current_stamp:
  "abs_rule thy n ty old = Some th ⟹ thm_stamp th = thy_stamp thy"
  by (auto simp: abs_rule_def eq_shape_def thm_shape_def
      split: option.splits if_splits)

lemma inst_rule_current_stamp:
  "inst thy θ old = Some th ⟹ thm_stamp th = thy_stamp thy"
  by (auto simp: inst_def thm_shape_def split: option.splits if_splits)

lemma inst_type_rule_current_stamp:
  "inst_type_rule thy θ old = Some th ⟹ thm_stamp th = thy_stamp thy"
  by (auto simp: inst_type_rule_def thm_shape_def split: if_splits)

section ‹Concrete executable checks›

lemma ill_typed_binder_rejected:
  "¬ check_term (initial_theory 0)
    (Abs (TyVar NAlpha)
      (Comb (FVar (NUser 10 ''not'') (mk_fun bool_ty bool_ty))
        (BVar 0 bool_ty)))"
  by eval

lemma well_typed_beta_succeeds:
  "∃th. beta (initial_theory 0)
      (Comb (Abs bool_ty (BVar 0 bool_ty))
        (FVar (NUser 11 ''p'') bool_ty)) = Some th ∧
    wf_thm (initial_theory 0) th"
proof -
  let ?t = "Comb (Abs bool_ty (BVar 0 bool_ty))
    (FVar (NUser 11 ''p'') bool_ty)"
  have present: "beta (initial_theory 0) ?t ≠ None" by eval
  then obtain th where run: "beta (initial_theory 0) ?t = Some th"
    by (cases "beta (initial_theory 0) ?t") auto
  have checked: "check_term (initial_theory 0) ?t"
    using run by (auto simp: beta_def split: hterm.splits if_splits)
  have input: "wf_inputs (IBeta (initial_theory 0) ?t)"
    using checked by simp
  have "wf_thm (initial_theory 0) th"
    using run_rule_preserves_wf[of "IBeta (initial_theory 0) ?t" th]
      run input by simp
  with run show ?thesis by blast
qed

lemma sibling_extensions_do_not_combine:
  "combine_stamps (next_stamp 1 (fresh_stamp 0))
      (next_stamp 2 (fresh_stamp 0)) = None"
  by eval

end