Theory Rhombus_HOL_Syntax

(* SPDX-License-Identifier: 0BSD *)
(* HOL systems are design references; this locally nameless formalization is original. *)

theory Rhombus_HOL_Syntax
  imports "HOL-ZF.MainZF"
begin

text ‹Trust boundary: Isabelle/HOL, HOLZF's axiomatized ZFC universe, and the three target-logic base axioms ETA_AX, SELECT_AX, and BOOL_CASES_AX. INFINITY_AX is a proved fact of the HOLZF model, not a target-theory axiom. New axioms are only conditionally model-preserving.›

section ‹Deep syntax and provenance›

text ‹Rhombus correspondence: kernel.rhm's names, types, terms, stamps, theorems, and theories. The final name constructor records both generative identity and display text.›

datatype hname =
    NFun | NBool | NEq | NAlpha | NRepVar
  | NNat | NZero | NSucc | NNatN | NNatM | NNatP
  | NUser nat string

datatype htype = TyVar hname | TyApp hname "htype list"

datatype hterm =
    FVar hname htype
  | BVar nat htype
  | Const hname htype
  | Comb hterm hterm
  | Abs htype hterm
  | NatLit nat

definition nat_ty_name :: hname where "nat_ty_name = NNat"
definition nat_zero_name :: hname where "nat_zero_name = NZero"
definition nat_succ_name :: hname where "nat_succ_name = NSucc"
definition nat_aty :: htype where "nat_aty = TyApp nat_ty_name []"

record stamp =
  sid :: nat
  gen :: nat
  ancestors :: "nat set"

record hthm =
  hyps :: "hterm list"
  concl :: hterm
  thm_stamp :: stamp

record htheory =
  tyops :: "hname ⇒ nat option"
  const_tab :: "hname ⇒ htype option"
  axiom_list :: "hthm list"
  def_tab :: "hname ⇒ hthm option"
  thy_stamp :: stamp

section ‹Names and types›

definition bool_ty :: htype where
  "bool_ty = TyApp NBool []"

definition mk_fun :: "htype ⇒ htype ⇒ htype" where
  "mk_fun a b = TyApp NFun [a, b]"

definition nat_sty :: htype where "nat_sty = mk_fun nat_aty nat_aty"

fun dest_fun :: "htype ⇒ (htype × htype) option" where
  "dest_fun (TyApp NFun [a, b]) = Some (a, b)"
| "dest_fun _ = None"

fun insert_once :: "'a ⇒ 'a list ⇒ 'a list" where
  "insert_once x xs = (if x ∈ set xs then xs else xs @ [x])"

fun type_vars_acc :: "htype ⇒ hname list ⇒ hname list" where
  "type_vars_acc (TyVar n) acc = insert_once n acc"
| "type_vars_acc (TyApp _ args) acc = fold type_vars_acc args acc"

definition type_vars :: "htype ⇒ hname list" where
  "type_vars ty = type_vars_acc ty []"

fun type_var_occurs :: "hname ⇒ htype ⇒ bool" where
  "type_var_occurs v (TyVar n) = (v = n)"
| "type_var_occurs v (TyApp _ args) = list_ex (type_var_occurs v) args"

fun type_operator_occurs :: "hname ⇒ htype ⇒ bool" where
  "type_operator_occurs op (TyVar _) = False"
| "type_operator_occurs op (TyApp n args) =
    (op = n ∨ list_ex (type_operator_occurs op) args)"

fun type_subst :: "(hname ⇒ htype option) ⇒ htype ⇒ htype" where
  "type_subst θ (TyVar n) = (case θ n of None ⇒ TyVar n | Some ty ⇒ ty)"
| "type_subst θ (TyApp n args) = TyApp n (map (type_subst θ) args)"

lemma type_subst_nat_aty [simp]: "type_subst θ nat_aty = nat_aty"
  by (simp add: nat_aty_def)

lemma type_subst_component_avoids_operator:
  assumes occurs: "type_var_occurs v generic"
    and avoids: "¬ type_operator_occurs op (type_subst θ generic)"
  shows "case θ v of None ⇒ True | Some ty ⇒ ¬ type_operator_occurs op ty"
  using occurs avoids
proof (induction generic)
  case (TyVar n)
  then show ?case by (cases "θ n") auto
next
  case (TyApp n args)
  then obtain arg where arg: "arg ∈ set args" "type_var_occurs v arg"
    by (auto simp: list_ex_iff)
  have "¬ type_operator_occurs op (type_subst θ arg)"
    using TyApp.prems(2) arg(1) by (auto simp: list_ex_iff)
  then show ?case using TyApp.IH[OF arg(1) arg(2)] by blast
qed

fun type_match_fuel :: "nat ⇒ htype ⇒ htype ⇒ (hname ⇒ htype option) ⇒ (hname ⇒ htype option) option" where
  "type_match_fuel 0 _ _ _ = None"
| "type_match_fuel (Suc k) (TyVar n) ty acc =
     (case acc n of None ⇒ Some (acc(n := Some ty))
      | Some old ⇒ if old = ty then Some acc else None)"
| "type_match_fuel (Suc k) (TyApp n ps) (TyApp m ts) acc =
     (if n = m ∧ length ps = length ts then
        fold (λ(p, t) r. case r of None ⇒ None | Some a ⇒ type_match_fuel k p t a)
          (zip ps ts) (Some acc)
      else None)"
| "type_match_fuel (Suc k) (TyApp _ _) (TyVar _) _ = None"

definition type_match :: "htype ⇒ htype ⇒ (hname ⇒ htype option) ⇒ (hname ⇒ htype option) option" where
  "type_match pat ty acc =
    (case type_match_fuel (size pat + 1) pat ty acc of
       None ⇒ None
     | Some θ ⇒ if type_subst θ pat = ty then Some θ else None)"

lemma type_match_sound:
  "type_match pat ty acc = Some θ ⟹ type_subst θ pat = ty"
  by (auto simp: type_match_def split: option.splits if_splits)

section ‹Executable term inspection›

text ‹Rhombus correspondence: typeOf, freeVars, and termTypeVars; failures that raise source exceptions are represented by option or bool.›

fun type_of :: "hterm ⇒ htype option" where
  "type_of (FVar _ ty) = Some ty"
| "type_of (BVar _ ty) = Some ty"
| "type_of (Const _ ty) = Some ty"
| "type_of (NatLit _) = Some nat_aty"
| "type_of (Abs aty body) = map_option (mk_fun aty) (type_of body)"
| "type_of (Comb f x) =
    (case (type_of f, type_of x) of
       (Some (TyApp NFun [dty, rty]), Some aty) ⇒ if dty = aty then Some rty else None
     | _ ⇒ None)"

fun free_vars_acc :: "hterm ⇒ (hname × htype) list ⇒ (hname × htype) list" where
  "free_vars_acc (FVar n ty) acc = insert_once (n, ty) acc"
| "free_vars_acc (Comb f x) acc = free_vars_acc x (free_vars_acc f acc)"
| "free_vars_acc (Abs _ b) acc = free_vars_acc b acc"
| "free_vars_acc _ acc = acc"

definition free_vars :: "hterm ⇒ (hname × htype) list" where
  "free_vars t = free_vars_acc t []"

fun term_type_vars_acc :: "hterm ⇒ hname list ⇒ hname list" where
  "term_type_vars_acc (FVar _ ty) acc = type_vars_acc ty acc"
| "term_type_vars_acc (BVar _ ty) acc = type_vars_acc ty acc"
| "term_type_vars_acc (Const _ ty) acc = type_vars_acc ty acc"
| "term_type_vars_acc (NatLit _) acc = acc"
| "term_type_vars_acc (Comb f x) acc = term_type_vars_acc x (term_type_vars_acc f acc)"
| "term_type_vars_acc (Abs aty b) acc = term_type_vars_acc b (type_vars_acc aty acc)"

definition term_type_vars :: "hterm ⇒ hname list" where
  "term_type_vars t = term_type_vars_acc t []"

fun vfree_in :: "hname ⇒ htype ⇒ hterm ⇒ bool" where
  "vfree_in n ty (FVar m u) = (n = m ∧ ty = u)"
| "vfree_in n ty (Comb f x) = (vfree_in n ty f ∨ vfree_in n ty x)"
| "vfree_in n ty (Abs _ b) = vfree_in n ty b"
| "vfree_in _ _ _ = False"

section ‹Theory provenance›

text ‹Rhombus correspondence: freshStamp, nextStamp, descends, combineStamps, and initialTheory. Callers provide fresh natural identities; generation is diagnostic only.›

definition wf_stamp :: "stamp ⇒ bool" where
  "wf_stamp st ⟷ sid st ∈ ancestors st"

definition fresh_stamp :: "nat ⇒ stamp" where
  "fresh_stamp fresh = ⦇sid = fresh, gen = 0, ancestors = {fresh}⦈"

definition next_stamp :: "nat ⇒ stamp ⇒ stamp" where
  "next_stamp fresh prev =
    ⦇sid = fresh, gen = Suc (gen prev), ancestors = insert fresh (ancestors prev)⦈"

definition descends :: "stamp ⇒ stamp ⇒ bool" where
  "descends old new ⟷ sid old ∈ ancestors new"

definition combine_stamps :: "stamp ⇒ stamp ⇒ stamp option" where
  "combine_stamps a b =
    (if descends a b then Some b else if descends b a then Some a else None)"

definition initial_theory :: "nat ⇒ htheory" where
  "initial_theory fresh =
    ⦇tyops = (λ_. None)(NFun := Some 2, NBool := Some 0),
     const_tab = (λ_. None)(NEq := Some (mk_fun (TyVar NAlpha)
       (mk_fun (TyVar NAlpha) bool_ty))),
     axiom_list = [], def_tab = (λ_. None), thy_stamp = fresh_stamp fresh⦈"

lemma fresh_stamp_wf [simp]: "wf_stamp (fresh_stamp fresh)"
  by (simp add: wf_stamp_def fresh_stamp_def)

lemma next_stamp_wf [simp]: "wf_stamp (next_stamp fresh st)"
  by (simp add: wf_stamp_def next_stamp_def)

lemma next_stamp_descends: "wf_stamp st ⟹ descends st (next_stamp fresh st)"
  by (simp add: wf_stamp_def descends_def next_stamp_def)

lemma combine_stamps_later:
  "combine_stamps a b = Some st ⟹ st = a ∨ st = b"
  by (auto simp: combine_stamps_def split: if_splits)

lemma combine_stamps_siblings:
  "¬ descends a b ⟹ ¬ descends b a ⟹ combine_stamps a b = None"
  by (simp add: combine_stamps_def)

section ‹Executable checks and sequents›

text ‹Rhombus correspondence: checkType, checkOpenTerm, checkTerm, isBool, mkEq, destEq, and duplicate-free hypothesis operations.›

fun check_type :: "htheory ⇒ htype ⇒ bool" where
  "check_type thy (TyVar _) = True"
| "check_type thy (TyApp n args) =
    (tyops thy n = Some (length args) ∧ list_all (check_type thy) args)"

lemma checked_type_avoids_fresh_operator:
  assumes "tyops thy op = None" "check_type thy ty"
  shows "¬ type_operator_occurs op ty"
  using assms by (induction ty) (auto simp: list_all_iff list_ex_iff)

fun check_open_term :: "htheory ⇒ htype list ⇒ hterm ⇒ bool" where
  "check_open_term thy env (FVar _ ty) = check_type thy ty"
| "check_open_term thy env (BVar i ty) =
    (i < length env ∧ env ! i = ty ∧ check_type thy ty)"
| "check_open_term thy env (Const n ty) =
    (check_type thy ty ∧
      (case const_tab thy n of None ⇒ False
       | Some generic ⇒ type_match generic ty (λ_. None) ≠ None))"
| "check_open_term thy env (NatLit _) =
    (check_type thy nat_aty ∧
      check_type thy nat_sty ∧
      const_tab thy nat_zero_name = Some nat_aty ∧
      const_tab thy nat_succ_name = Some nat_sty)"
| "check_open_term thy env (Comb f x) =
    (check_open_term thy env f ∧ check_open_term thy env x ∧ type_of (Comb f x) ≠ None)"
| "check_open_term thy env (Abs aty body) =
    (check_type thy aty ∧ check_open_term thy (aty # env) body)"

definition check_term :: "htheory ⇒ hterm ⇒ bool" where
  "check_term thy t ⟷ check_open_term thy [] t"

definition is_bool :: "hterm ⇒ bool" where
  "is_bool t ⟷ type_of t = Some bool_ty"

definition check_prop :: "htheory ⇒ hterm ⇒ bool" where
  "check_prop thy p ⟷ check_term thy p ∧ is_bool p"

definition eq_const :: "htype ⇒ hterm" where
  "eq_const ty = Const NEq (mk_fun ty (mk_fun ty bool_ty))"

definition eq_term :: "htype ⇒ hterm ⇒ hterm ⇒ hterm" where
  "eq_term ty l r = Comb (Comb (eq_const ty) l) r"

definition mk_eq :: "hterm ⇒ hterm ⇒ hterm option" where
  "mk_eq l r =
    (case (type_of l, type_of r) of
       (Some lty, Some rty) ⇒ if lty = rty then Some (eq_term lty l r) else None
     | _ ⇒ None)"

fun dest_eq :: "hterm ⇒ (hterm × hterm) option" where
  "dest_eq (Comb (Comb (Const NEq _) l) r) = Some (l, r)"
| "dest_eq _ = None"

definition hyp_insert :: "hterm ⇒ hterm list ⇒ hterm list" where
  "hyp_insert t hs = insert_once t hs"

definition hyp_union :: "hterm list ⇒ hterm list ⇒ hterm list" where
  "hyp_union a b = fold hyp_insert b a"

definition hyp_remove :: "hterm ⇒ hterm list ⇒ hterm list" where
  "hyp_remove t hs = filter (λh. h ≠ t) hs"

definition rehash_hyps :: "hterm list ⇒ hterm list" where
  "rehash_hyps hs = fold hyp_insert hs []"

definition wf_theory :: "htheory ⇒ bool" where
  "wf_theory thy ⟷
    wf_stamp (thy_stamp thy) ∧
    tyops thy NFun = Some 2 ∧ tyops thy NBool = Some 0 ∧
    const_tab thy NEq = Some (mk_fun (TyVar NAlpha) (mk_fun (TyVar NAlpha) bool_ty)) ∧
    (∀n ty. const_tab thy n = Some ty ⟶ check_type thy ty)"

definition wf_thm :: "htheory ⇒ hthm ⇒ bool" where
  "wf_thm thy th ⟷
    distinct (hyps th) ∧ check_prop thy (concl th) ∧
    list_all (check_prop thy) (hyps th) ∧ descends (thm_stamp th) (thy_stamp thy)"

lemma hyp_insert_distinct:
  "distinct hs ⟹ distinct (hyp_insert t hs)"
  by (simp add: hyp_insert_def)

lemma hyp_union_distinct:
  "distinct a ⟹ distinct b ⟹ distinct (hyp_union a b)"
  by (induction b arbitrary: a) (auto simp: hyp_union_def hyp_insert_def)

lemma fold_hyp_insert_distinct:
  "distinct acc ⟹ distinct (fold hyp_insert xs acc)"
  by (induction xs arbitrary: acc) (auto simp: hyp_insert_def)

lemma rehash_hyps_distinct [simp]: "distinct (rehash_hyps hs)"
  by (simp add: rehash_hyps_def fold_hyp_insert_distinct)

lemma same_printing_symbols_remain_distinct:
  "length (hyp_insert (FVar (NUser 1 ''x'') bool_ty)
     (hyp_insert (FVar (NUser 0 ''x'') bool_ty) [])) = 2"
  by (simp add: hyp_insert_def bool_ty_def)

lemma initial_theory_wf [simp]: "wf_theory (initial_theory fresh)"
  by (auto simp: wf_theory_def initial_theory_def mk_fun_def bool_ty_def
      type_match_def split: hname.splits option.splits)

lemma set_fold_acc_union:
  assumes step: "⋀x acc. x ∈ set xs ⟹ set (F x acc) = G x ∪ set acc"
  shows "set (fold F xs acc) = (⋃x∈set xs. G x) ∪ set acc"
  using step
proof (induction xs arbitrary: acc)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  have head: "set (F x acc) = G x ∪ set acc"
    using Cons.prems by auto
  have tail_step: "⋀y rest. y ∈ set xs ⟹
      set (F y rest) = G y ∪ set rest"
    using Cons.prems by auto
  have tail: "set (fold F xs (F x acc)) =
      (⋃y∈set xs. G y) ∪ set (F x acc)"
    using Cons.IH[OF tail_step] .
  show ?case using head tail by auto
qed

lemma set_type_vars_acc:
  "set (type_vars_acc ty acc) = {v. type_var_occurs v ty} ∪ set acc"
proof (induction ty arbitrary: acc)
  case (TyVar n)
  then show ?case by auto
next
  case (TyApp n args)
  have step: "⋀ty rest. ty ∈ set args ⟹
      set (type_vars_acc ty rest) =
        {v. type_var_occurs v ty} ∪ set rest"
    using TyApp.IH .
  have fold: "set (fold type_vars_acc args acc) =
      (⋃ty∈set args. {v. type_var_occurs v ty}) ∪ set acc"
    using set_fold_acc_union[OF step] .
  show ?case using fold by (auto simp: list_ex_iff)
qed

lemma set_type_vars:
  "set (type_vars ty) = {v. type_var_occurs v ty}"
  by (simp add: type_vars_def set_type_vars_acc)

lemma set_term_type_vars_acc:
  "set (term_type_vars_acc t acc) =
    set (term_type_vars t) ∪ set acc"
proof (induction t arbitrary: acc)
  case (FVar n ty)
  then show ?case by (simp add: term_type_vars_def set_type_vars_acc)
next
  case (BVar i ty)
  then show ?case by (simp add: term_type_vars_def set_type_vars_acc)
next
  case (Const n ty)
  then show ?case by (simp add: term_type_vars_def set_type_vars_acc)
next
  case (NatLit n)
  then show ?case by (simp add: term_type_vars_def)
next
  case (Comb f x)
  have first: "set (term_type_vars_acc f acc) =
      set (term_type_vars f) ∪ set acc"
    using Comb.IH(1) .
  have second: "set (term_type_vars_acc x (term_type_vars_acc f acc)) =
      set (term_type_vars x) ∪ set (term_type_vars_acc f acc)"
    using Comb.IH(2) .
  have empty: "set (term_type_vars_acc x (term_type_vars_acc f [])) =
      set (term_type_vars x) ∪ set (term_type_vars f)"
    using Comb.IH by auto
  show ?case using first second empty by (simp add: term_type_vars_def) auto
next
  case (Abs ty body)
  have body: "set (term_type_vars_acc body (type_vars_acc ty acc)) =
      set (term_type_vars body) ∪ set (type_vars_acc ty acc)"
    using Abs.IH .
  have empty: "set (term_type_vars_acc body (type_vars_acc ty [])) =
      set (term_type_vars body) ∪ set (type_vars ty)"
    using Abs.IH by (simp add: type_vars_def)
  have ty_set: "set (type_vars ty) = {v. type_var_occurs v ty}"
    by (rule set_type_vars)
  show ?case using body empty ty_set
    by (simp add: term_type_vars_def set_type_vars_acc) auto
qed
lemma set_term_type_vars_FVar [simp]:
  "set (term_type_vars (FVar n ty)) = set (type_vars ty)"
  by (simp add: term_type_vars_def type_vars_def)

lemma set_term_type_vars_BVar [simp]:
  "set (term_type_vars (BVar i ty)) = set (type_vars ty)"
  by (simp add: term_type_vars_def type_vars_def)

lemma set_term_type_vars_Const [simp]:
  "set (term_type_vars (Const n ty)) = set (type_vars ty)"
  by (simp add: term_type_vars_def type_vars_def)

lemma set_term_type_vars_NatLit [simp]:
  "set (term_type_vars (NatLit n)) = {}"
  by (simp add: term_type_vars_def)

lemma set_term_type_vars_Comb [simp]:
  "set (term_type_vars (Comb f x)) =
    set (term_type_vars f) ∪ set (term_type_vars x)"
  using set_term_type_vars_acc[of x "term_type_vars_acc f []"]
  by (auto simp: term_type_vars_def)
lemma set_term_type_vars_Abs [simp]:
  "set (term_type_vars (Abs ty body)) =
    set (type_vars ty) ∪ set (term_type_vars body)"
  using set_term_type_vars_acc[of body "type_vars_acc ty []"]
  by (auto simp: term_type_vars_def type_vars_def)

lemma type_subst_component_occurs:
  assumes source: "type_var_occurs v generic"
    and component: "case θ v of None ⇒ w = v
      | Some ty ⇒ type_var_occurs w ty"
  shows "type_var_occurs w (type_subst θ generic)"
  using source component
proof (induction generic)
  case (TyVar n)
  then show ?case by (cases "θ n") auto
next
  case (TyApp n args)
  then obtain arg where member: "arg ∈ set args"
    and occurs: "type_var_occurs v arg"
    by (auto simp: list_ex_iff)
  have "type_var_occurs w (type_subst θ arg)"
    using TyApp.IH[OF member occurs TyApp.prems(2)] .
  then show ?case using member by (auto simp: list_ex_iff)
qed

lemma set_free_vars_acc:
  "set (free_vars_acc t acc) = set (free_vars t) ∪ set acc"
proof (induction t arbitrary: acc)
  case (FVar n ty)
  then show ?case by (auto simp: free_vars_def)
next
  case (BVar i ty)
  then show ?case by (simp add: free_vars_def)
next
  case (Const n ty)
  then show ?case by (simp add: free_vars_def)
next
  case (NatLit n)
  then show ?case by (simp add: free_vars_def)
next
  case (Comb f x)
  have first: "set (free_vars_acc f acc) =
      set (free_vars f) ∪ set acc" using Comb.IH(1) .
  have second: "set (free_vars_acc x (free_vars_acc f acc)) =
      set (free_vars x) ∪ set (free_vars_acc f acc)"
    using Comb.IH(2) .
  have empty: "set (free_vars_acc x (free_vars_acc f [])) =
      set (free_vars x) ∪ set (free_vars f)"
    using Comb.IH by auto
  show ?case using first second empty by (auto simp: free_vars_def)
next
  case (Abs ty body)
  have collected: "set (free_vars_acc body acc) =
      set (free_vars body) ∪ set acc"
    using Abs.IH .
  have same: "free_vars (Abs ty body) = free_vars body"
    unfolding free_vars_def by simp
  show ?case using collected same by simp
qed

lemma set_free_vars_FVar [simp]:
  "set (free_vars (FVar n ty)) = {(n, ty)}"
  by (auto simp: free_vars_def)

lemma set_free_vars_BVar [simp]: "set (free_vars (BVar i ty)) = {}"
  by (simp add: free_vars_def)

lemma set_free_vars_Const [simp]: "set (free_vars (Const n ty)) = {}"
  by (simp add: free_vars_def)

lemma set_free_vars_NatLit [simp]: "set (free_vars (NatLit n)) = {}"
  by (simp add: free_vars_def)

lemma set_free_vars_Comb [simp]:
  "set (free_vars (Comb f x)) = set (free_vars f) ∪ set (free_vars x)"
  using set_free_vars_acc[of x "free_vars_acc f []"]
  by (auto simp: free_vars_def)

lemma set_free_vars_Abs [simp]:
  "set (free_vars (Abs ty body)) = set (free_vars body)"
  by (simp add: free_vars_def)

end