Theory Core

section ‹Core Inference system›

text ‹Contains just the stuff necessary for the definition of the Inference system›

theory Core
  imports Main
begin

text ‹Basic types ›
type_synonym name = String.literal
type_synonym indexname = "name × int"

type_synonym "class" = String.literal

type_synonym "sort" = "class set"
abbreviation "full_sort ≡ ({}::sort)"

(* Name duplication with Fv in term, change later*)
datatype variable = Free name | Var indexname

datatype "typ" =
  is_Ty: Ty name "typ list" |
  is_Tv: Tv variable sort

datatype "term" =
  is_Ct: Ct name "typ" |
  is_Fv: Fv variable "typ" |
  is_Bv: Bv nat |
  is_Abs: Abs "typ" "term" |
  is_App: App "term" "term" (infixl ‹$› 100)

abbreviation "mk_fun_typ S T ≡ Ty STR ''fun'' [S,T]" 
notation mk_fun_typ (infixr ‹→› 100)

text ‹Collect variables in a term›

fun fv :: "term ⇒ (variable × typ) set" where
  "fv (Ct _ _) = {}"
| "fv (Fv v T) = {(v, T)}"
| "fv (Bv _) = {}"
| "fv (Abs _ body) = fv body"
| "fv (t $ u) = fv t ∪ fv u"
definition [simp]: "FV S = (⋃s∈S . fv s)"

text ‹Typ/term instantiations›

fun tsubstT :: "typ ⇒ (variable ⇒ sort ⇒ typ) ⇒ typ" where 
  "tsubstT (Tv a s) ρ = ρ a s"
| "tsubstT (Ty κ σs) ρ = Ty κ (map (λσ. tsubstT σ ρ) σs)"
definition "tinstT T1 T2 ≡ ∃ρ. tsubstT T2 ρ = T1"

fun tsubst :: "term ⇒ (variable ⇒ sort ⇒ typ) ⇒ term" where
  "tsubst (Ct s T) ρ = Ct s (tsubstT T ρ)"
| "tsubst (Fv v T) ρ = Fv v (tsubstT T ρ)"
| "tsubst (Bv i) _ = Bv i"
| "tsubst (Abs T t) ρ = Abs (tsubstT T ρ) (tsubst t ρ)"
| "tsubst (t $ u) ρ = tsubst t ρ $ tsubst u ρ"

text ‹Typ of a term›

inductive has_typ1 :: "typ list ⇒ term ⇒ typ ⇒ bool" (‹_ ⊢⇩τ _ : _› [51, 51, 51] 51) where
  "has_typ1 _ (Ct _ T) T"
| "i < length Ts ⟹ has_typ1 Ts (Bv i) (nth Ts i)"
| "has_typ1 _ (Fv _ T) T"
| "has_typ1 (T#Ts) t T' ⟹ has_typ1 Ts (Abs T t) (T → T')"
| "has_typ1 Ts u U ⟹ has_typ1 Ts t (U → T) ⟹
      has_typ1 Ts (t $ u) T"
definition has_typ :: "term ⇒ typ ⇒ bool" (‹⊢⇩τ _ : _› [51, 51] 51) where "has_typ t T = has_typ1 [] t T"

definition "typ_of t = (if ∃T . has_typ t T then Some (THE T . has_typ t T) else None)"

text‹More operations on terms›

fun lift :: "term ⇒ nat ⇒ term" where
  "lift (Bv i) n = (if i ≥ n then Bv (i+1) else Bv i)"
| "lift (Abs T body) n = Abs T (lift body (n+1))"
| "lift (App f t) n = App (lift f n) (lift t n)"
| "lift u n = u"

fun subst_bv2 :: "term ⇒ nat ⇒ term ⇒ term" where
  "subst_bv2 (Bv i) n u = (if i < n then Bv i
    else if i = n then u
    else (Bv (i - 1)))" 
| "subst_bv2 (Abs T body) n u = Abs T (subst_bv2 body (n + 1) (lift u 0))"
| "subst_bv2 (f $ t) n u = subst_bv2 f n u $ subst_bv2 t n u"
| "subst_bv2 t _ _ = t"

definition "subst_bv u t = subst_bv2 t 0 u"

fun bind_fv2 :: "(variable × typ) ⇒ nat ⇒ term ⇒ term" where
  "bind_fv2 vT n (Fv v T) = (if vT = (v,T) then Bv n else Fv v T)"
| "bind_fv2 vT n (Abs T t) = Abs T (bind_fv2 vT (n+1) t)"
| "bind_fv2 vT n (f $ u) = bind_fv2 vT n f $ bind_fv2 vT n u"
| "bind_fv2 _ _ t = t"

definition "bind_fv vT t = bind_fv2 vT 0 t"

abbreviation "Abs_fv v T t ≡ Abs T (bind_fv (v,T) t)"

text ‹Some typ/term constants›

abbreviation "itselfT ty ≡ Ty STR ''itself'' [ty]"
abbreviation "constT name ≡ Ty name []"
abbreviation "propT ≡ constT STR ''prop''"

abbreviation "mk_eq t1 t2 ≡ Ct STR ''Pure.eq'' 
  (the (typ_of t1) → (the (typ_of t2) → propT)) $ t1 $ t2"
(* Because mk_eq works only with closed terms *)
abbreviation "mk_eq' ty t1 t2 ≡ Ct STR ''Pure.eq'' 
  (ty → (ty → propT)) $ t1 $ t2"
abbreviation mk_imp :: "term ⇒ term ⇒ term"  (infixr ‹⟼› 51) where 
  "A ⟼ B ≡ Ct STR ''Pure.imp'' (propT → (propT → propT)) $ A $ B"
abbreviation "mk_all x ty t ≡
  Ct STR ''Pure.all'' ((ty → propT) → propT) $ Abs_fv x ty t"

text ‹Order sorted signature›

type_synonym osig = "(class rel × (name ⇀ (class ⇀ sort list)))"

fun "subclass" :: "osig ⇒ class rel" where "subclass (cl, _) = cl"
fun tcsigs :: "osig ⇒ (name ⇀ (class ⇀ sort list))" where "tcsigs (_, ars) = ars"

text ‹Relation in sorts›

definition "class_leq sub c1 c2 = ((c1,c2) ∈ sub)"
definition "class_les sub c1 c2 = (class_leq sub c1 c2 ∧ ¬ class_leq sub c2 c1)"
definition "sort_leq sub s1 s2 = (∀c⇩2 ∈ s2 . ∃c⇩1 ∈ s1. class_leq sub c⇩1 c⇩2)"

text ‹Is a class/sort defined›

definition "class_ex rel c = (c ∈ Field rel)"
definition "sort_ex rel S = (S ⊆ Field rel)"

text ‹Normalizing sorts›

definition "normalize_sort sub (S::sort)
  = {c ∈ S. ¬ (∃c' ∈ S. class_les sub c' c)}"
abbreviation "normalized_sort sub S ≡ normalize_sort sub S = S"

definition "wf_sort sub S = (normalized_sort sub S ∧ sort_ex sub S)"

text ‹Wellformedness of osig›

definition [simp]: "wf_subclass rel = (trans rel ∧ antisym rel ∧ Refl rel)"

definition "complete_tcsigs sub tcs ≡ (∀ars ∈ ran tcs . 
  ∀(c⇩1, c⇩2) ∈ sub . c⇩1∈dom ars ⟶ c⇩2∈dom ars)"

definition "coregular_tcsigs sub tcs ≡ (∀ars ∈ ran tcs .
  ∀c⇩1 ∈ dom ars. ∀c⇩2 ∈ dom ars.
    (class_leq sub c⇩1 c⇩2 ⟶ list_all2 (sort_leq sub) (the (ars c⇩1)) (the (ars c⇩2))))" 

definition "consistent_length_tcsigs tcs ≡ (∀ars ∈ ran tcs . 
  ∀ss⇩1 ∈ ran ars. ∀ss⇩2 ∈ ran ars. length ss⇩1 = length ss⇩2)"

definition "all_normalized_and_ex_tcsigs sub tcs ≡
  (∀ars ∈ ran tcs . ∀ss ∈ ran ars . ∀s ∈ set ss. wf_sort sub s)"

definition [simp]: "wf_tcsigs sub tcs ⟷
    coregular_tcsigs sub tcs
  ∧ complete_tcsigs sub tcs
  ∧ consistent_length_tcsigs tcs
  ∧ all_normalized_and_ex_tcsigs sub tcs"

fun wf_osig where "wf_osig (sub, tcs) ⟷ wf_subclass sub ∧ wf_tcsigs sub tcs"

text ‹Embedding typs into terms/Encoding of type classes›

definition "mk_type ty = Ct STR ''Pure.type'' (Core.itselfT ty)"

abbreviation "mk_suffix (str::name) suff ≡ String.implode (String.explode str @ String.explode suff)"

abbreviation "classN ≡ STR ''_class''"
abbreviation "const_of_class name ≡ mk_suffix name classN"

definition "mk_of_class ty c =
  Ct (const_of_class c) (Core.itselfT ty → propT) $ mk_type ty"

text ‹Checking if a typ belongs to a sort›

inductive has_sort :: "osig ⇒ typ ⇒ sort ⇒ bool" where
  has_sort_Tv[intro]: "sort_leq sub S S' ⟹ has_sort (sub, tcs) (Tv a S) S'"
| has_sort_Ty: 
  "tcs κ = Some dm ⟹ ∀c ∈ S. ∃Ss . dm c = Some Ss ∧ list_all2 (has_sort (sub, tcs)) Ts Ss
    ⟹ has_sort (sub, tcs) (Ty κ Ts) S"

text ‹Signatures ›

type_synonym signature = "(name ⇀ typ) × (name ⇀ nat) × osig"

fun const_type :: "signature ⇒ (name ⇀ typ)" where "const_type (ctf, _, _) = ctf"
fun type_arity :: "signature ⇒ (name ⇀ nat)" where "type_arity (_, arf, _) = arf"
fun osig :: "signature ⇒ osig" where "osig (_, _, oss) = oss"

(* Which typs and consts must be defined in a signature*)
fun is_std_sig where "is_std_sig (ctf, arf, _) ⟷
    arf STR ''fun'' = Some 2 ∧ arf STR ''prop'' = Some 0 
  ∧ arf STR ''itself'' = Some 1
  ∧ ctf STR ''Pure.eq'' 
    = Some ((Tv (Var (STR '''a'', 0)) full_sort) → ((Tv (Var (STR '''a'', 0)) full_sort) → propT))
  ∧ ctf STR ''Pure.all'' = Some ((Tv (Var  (STR '''a'', 0)) full_sort → propT) → propT)
  ∧ ctf STR ''Pure.imp'' = Some (propT → (propT → propT))
  ∧ ctf STR ''Pure.type'' = Some (itselfT (Tv (Var (STR '''a'', 0)) full_sort))"

text ‹Wellformedness checks›

definition [simp]: "class_ok_sig Σ c ≡ class_ex (subclass (osig Σ)) c"

inductive wf_type :: "signature ⇒ typ ⇒ bool" where
  typ_ok_Ty: "type_arity Σ κ = Some (length Ts) ⟹ ∀T∈set Ts . wf_type Σ T
    ⟹ wf_type Σ (Ty κ Ts)"
| typ_ok_Tv[intro]: "wf_sort (subclass (osig Σ)) S ⟹ wf_type Σ (Tv a S)"

inductive wf_term :: "signature ⇒ term ⇒ bool" where
  "wf_type Σ T ⟹ wf_term Σ (Fv v T)"
| "wf_term Σ (Bv n)"
| "const_type Σ s = Some ty ⟹ wf_type Σ T ⟹ tinstT T ty ⟹ wf_term Σ (Ct s T)"
| "wf_term Σ t ⟹ wf_term Σ u ⟹ wf_term Σ (t $ u)"
| "wf_type Σ T ⟹ wf_term Σ t ⟹ wf_term Σ (Abs T t)"

definition "wt_term Σ t ≡ wf_term Σ t ∧ (∃T. has_typ t T)"

fun wf_sig :: "signature ⇒ bool" where                
  "wf_sig (ctf, arf, oss) = (wf_osig oss
  ∧ dom (tcsigs oss) = dom arf
  ∧ (∀type ∈ dom (tcsigs oss). (∀ars ∈ ran (the (tcsigs oss type)) . the (arf type) = length ars))
  ∧ (∀ty ∈ Map.ran ctf . wf_type (ctf, arf, oss) ty))"

text ‹Theories›

type_synonym "theory" = "signature × term set"

fun sig :: "theory ⇒ signature" where "sig (Σ, _) = Σ"
fun axioms :: "theory ⇒ term set" where "axioms (_, axs) = axs"

text ‹Equality axioms, stated directly›

abbreviation "tvariable a ≡ (Tv (Var (a, 0)) full_sort)"
abbreviation "variable x T ≡ Fv (Var (x, 0)) T"

abbreviation "aT ≡ tvariable STR '''a''"
abbreviation "bT ≡ tvariable STR '''b''"
abbreviation "x ≡ variable STR ''x'' aT"
abbreviation "y ≡ variable STR ''y'' aT"
abbreviation "z ≡ variable STR ''z'' aT"
abbreviation "f ≡ variable STR ''f'' (aT → bT)"
abbreviation "g ≡ variable STR ''g'' (aT → bT)"
abbreviation "P ≡ variable STR ''P'' (aT → propT)"
abbreviation "Q ≡ variable STR ''Q'' (aT → propT)"
abbreviation "A ≡ variable STR ''A'' propT"
abbreviation "B ≡ variable STR ''B'' propT"

definition "eq_reflexive_ax ≡ mk_eq x x"
definition "eq_symmetric_ax ≡ mk_eq x y ⟼ mk_eq y x"
definition "eq_transitive_ax ≡ mk_eq x y ⟼ mk_eq y z ⟼ mk_eq x z"
definition "eq_intr_ax ≡ (A ⟼ B) ⟼ (B ⟼ A) ⟼ mk_eq A B"
definition "eq_elim_ax ≡ mk_eq A B ⟼ A ⟼ B"
definition "eq_combination_ax ≡ mk_eq f g ⟼ mk_eq x y ⟼ mk_eq (f $ x) (g $ y)"
definition "eq_abstract_rule_ax ≡ 
      (Ct STR ''Pure.all'' ((aT → propT) → propT) $ Abs aT (mk_eq' bT (f $ Bv 0) (g $ Bv 0)))
  ⟼ mk_eq (Abs aT (f $ Bv 0)) (Abs aT (g $ Bv 0))"

hide_const (open) x y z f g P Q A B

abbreviation "eq_axs ≡ {eq_reflexive_ax, eq_symmetric_ax, eq_transitive_ax, eq_intr_ax, eq_elim_ax,
  eq_combination_ax, eq_abstract_rule_ax}"

text‹Wellformedness of theories›

fun wf_theory where "wf_theory (Σ, axs) ⟷
    (∀p ∈ axs . wt_term Σ p ∧ has_typ p propT)
  ∧ is_std_sig Σ 
  ∧ wf_sig Σ
  ∧ eq_axs ⊆ axs"

text‹Wellformedness of typ antiations›

definition [simp]: "wf_inst Θ ρ ≡ 
  (∀v S . ρ v S ≠ Tv v S ⟶
    (has_sort (osig (sig Θ)) (ρ v S) S) ∧ wf_type (sig Θ) (ρ v S))"

text‹Inference system›

inductive proves :: "theory ⇒ term set ⇒ term ⇒ bool" (‹(_,_) ⊢ (_)› 50) for Θ where
  axiom: "wf_theory Θ ⟹ A∈axioms Θ ⟹ wf_inst Θ ρ
  ⟹ Θ, Γ ⊢ tsubst A ρ"
| "assume": "wf_term (sig Θ) A ⟹ has_typ A propT ⟹ A ∈ Γ ⟹ Θ,Γ ⊢ A"
| forall_intro: "wf_theory Θ ⟹ Θ, Γ ⊢ B ⟹ (x,τ) ∉ FV Γ ⟹ wf_type (sig Θ)  τ
  ⟹ Θ, Γ ⊢ mk_all x τ B"
| forall_elim: "Θ, Γ ⊢ Ct STR ''Pure.all'' ((τ → propT) → propT) $ Abs τ B
  ⟹ has_typ a τ ⟹ wf_term (sig Θ) a
  ⟹ Θ, Γ ⊢ subst_bv a B"
| implies_intro: "wf_theory Θ ⟹ Θ, Γ ⊢ B ⟹ wf_term (sig Θ) A ⟹ has_typ A propT 
  ⟹ Θ, Γ - {A} ⊢ A ⟼ B"
| implies_elim: "Θ, Γ⇩1 ⊢ A ⟼ B ⟹ Θ, Γ⇩2 ⊢ A ⟹ Θ, Γ⇩1∪Γ⇩2 ⊢ B"
| of_class: "wf_theory Θ
  ⟹ const_type (sig Θ) (const_of_class c) = Some (Core.itselfT aT → propT)
  ⟹ wf_type (sig Θ) T
  ⟹ has_sort (osig (sig Θ)) T {c}
  ⟹ Θ, Γ ⊢ mk_of_class T c"
(* Stuff about equality that cannot be expressed as an axiom*)
| β_conversion: "wf_theory Θ ⟹ wt_term (sig Θ) (Abs T t) ⟹ wf_term (sig Θ) u ⟹ has_typ u T 
  ⟹ Θ, Γ ⊢ mk_eq (Abs T t $ u) (subst_bv u t)"
| eta: "wf_theory Θ ⟹ wf_term (sig Θ) t ⟹ has_typ t (τ → τ')
  ⟹ Θ, Γ ⊢ mk_eq (Abs τ (t $ Bv 0)) t"

text‹Ensure no garbage in ‹Θ,Γ››

definition proves' :: "theory ⇒ term set ⇒ term ⇒ bool" (‹(_,_) ⊩ (_)› 51) where
  "proves' Θ Γ t ≡ wf_theory Θ ∧ (∀h ∈ Γ . wf_term (sig Θ) h ∧ has_typ h propT) ∧ Θ, Γ ⊢ t"

hide_const (open) aT bT

end