Theory Consistency_Property

theory Consistency_Property imports
  "Abstract_Consistency_Property.Abstract_Consistency_Property"
  "Q0_Metatheory.Syntax"
begin

section ‹Consistency Property›

inductive confl_class :: ‹form list ⇒ form list ⇒ bool› (infix ‹↝⇩✗› 50) where
  CFalse: ‹[] ↝⇩✗ [ F⇘o⇙ ]›
| CNot: ‹[ ∼⇧𝒬 A ] ↝⇩✗ [ A ]› if ‹A ∈ wffs⇘o⇙›

inductive alpha_class :: ‹form list ⇒ form list ⇒ bool› (infix ‹↝⇩α› 50) where
  CBool: ‹[ A ] ↝⇩α [ A =⇘o⇙ T⇘o⇙ ]› if ‹A ∈ wffs⇘o⇙›
| CIota: ‹[] ↝⇩α [ ι · (Q⇘i⇙ · A) =⇘i⇙ A ]› if ‹A ∈ wffs⇘i⇙›
| CRefl: ‹[] ↝⇩α [ A =⇘α⇙ A ]› if ‹A ∈ wffs⇘α⇙›
| CTrans: ‹[ A =⇘α⇙ B, B =⇘α⇙ C ] ↝⇩α [ A =⇘α⇙ C ]› if ‹A ∈ wffs⇘α⇙› and ‹B ∈ wffs⇘α⇙› and ‹C ∈ wffs⇘α⇙›
| CCong: ‹[ A =⇘α⇙ B ] ↝⇩α [ C · A =⇘β⇙ C · B ]› if ‹A ∈ wffs⇘α⇙› and ‹B ∈ wffs⇘α⇙› and ‹C ∈ wffs⇘α → β⇙›
| CSubst: ‹[] ↝⇩α [ (λx⇘α⇙. B) · A =⇘β⇙ ❙S {(x, α) ↣ A} B ]› if
  ‹A ∈ wffs⇘α⇙› and ‹B ∈ wffs⇘β⇙› and ‹free_vars A = {}›

inductive beta_class :: ‹form list ⇒ form list ⇒ bool› (infix ‹↝⇩β› 50) where
  CLEM: ‹[] ↝⇩β [ A, ∼⇧𝒬 A ]› if ‹A ∈ wffs⇘o⇙›

inductive gamma_class :: ‹form list ⇒ (form set ⇒ _) × (form ⇒ _) ⇒ bool› (infix ‹↝⇩γ› 50) where
  CExt: ‹[ A =⇘α → β⇙ B ] ↝⇩γ (λ_. wffs⇘α⇙, λC. [ A · C =⇘β⇙ B · C ])› if
  ‹A ∈ wffs⇘α → β⇙› and ‹B ∈ wffs⇘α → β⇙›

subsection ‹Negated Equality›

inductive ineq_match :: ‹form ⇒ type × type × form × form ⇒ bool› where
  ‹ineq_match (∼⇧𝒬 (A =⇘α → β⇙ B)) (α, β, A, B)›

inductive_cases ineq_matchE [elim]: ‹ineq_match (∼⇧𝒬 (A =⇘α → β⇙ B)) (α', β', A', B')›

lemma ineq_match_uniq [dest]:
  assumes ‹ineq_match C (α, β, A, B)›
    and ‹ineq_match C (α', β', A', B')›
  shows ‹α = α' ∧ β = β' ∧ A = A' ∧ B = B'›
  using assms by (auto elim: ineq_match.cases)

lemma THE_ineq_match:
  assumes ‹ineq_match C (α, β, A, B)›
  shows ‹(THE (α, β, A, B). ineq_match C (α, β, A, B)) = (α, β, A, B)›
  using assms by blast

lemma ineq_matchD [dest]:
  assumes ‹ineq_match C (α, β, A, B)›
  shows ‹C = ∼⇧𝒬 (A =⇘α → β⇙ B)›
  using assms by (auto elim!: ineq_match.cases)

lemma ineq_matchI [intro]:
  assumes ‹C = ∼⇧𝒬 (A =⇘α → β⇙ B)›
  shows ‹ineq_match C (α, β, A, B)›
  using assms ineq_match.intros by blast

subsection ‹Delta›

fun delta :: ‹form ⇒ nat ⇒ form list› where
  CDelta: ‹delta C c =
    (if C ∈ wffs⇘o⇙ ∧ (∃α β A B. ineq_match C (α, β, A, B)) then
       case THE (α, β, A, B). ineq_match C (α, β, A, B) of
         (α, β, A, B) ⇒ [ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ]
     else [])›

lemma ineq_match_delta [simp]:
  assumes ‹C ∈ wffs⇘o⇙› ‹ineq_match C (α, β, A, B)›
  shows ‹delta C c = [ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ]›
  unfolding CDelta using assms THE_ineq_match by auto

lemma delta:
  assumes ‹A ∈ wffs⇘α → β⇙› ‹B ∈ wffs⇘α → β⇙›
  shows ‹delta (∼⇧𝒬 (A =⇘α → β⇙ B)) c = [ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ]›
  using assms equality_wff ineq_matchI ineq_match_delta neg_wff by metis

subsection ‹Operations›

definition ‹logical_names ≡ {𝔠⇩Q, 𝔠⇩ι}›
abbreviation ‹is_logical_name c ≡ c ∈ logical_names›

lemma logical_name_simps[simp]:
  shows ‹is_logical_name 𝔠⇩Q›
    and ‹is_logical_name 𝔠⇩ι›
  by (simp_all add: logical_names_def)

definition ‹is_param c ≡ ¬ is_logical_name c›

fun map_con :: ‹(nat ⇒ nat) ⇒ form ⇒ form› where
  ‹map_con _ (x⇘α⇙) = (x⇘α⇙)›
| ‹map_con f (⦃c⦄⇘α⇙) = (if is_logical_name c ∨ is_logical_name (f c) then ⦃c⦄⇘α⇙ else ⦃f c⦄⇘α⇙)›
| ‹map_con f (A · B) = map_con f A · map_con f B›
| ‹map_con f (λx⇘α⇙. A) = λx⇘α⇙. map_con f A›

fun cons_form :: ‹form ⇒ nat set› where
  ‹cons_form (x⇘α⇙) = {}›
| ‹cons_form (⦃c⦄⇘α⇙) = (if is_logical_name c then {} else {c})›
| ‹cons_form (A · B) = cons_form A ∪ cons_form B›
| ‹cons_form (λx⇘α⇙. A) = cons_form A›

subsection ‹Lemmas›

text ‹This property is really what dodging the logical constants is all about.›
proposition ‹map_con f (∼⇧𝒬 A) = ∼⇧𝒬 (map_con f A)›
  by simp

lemma map_con_id [simp]: ‹map_con id = id›
proof
  fix A
  show ‹map_con id A = id A›
    by (induct A) auto
qed

lemma map_con_cong [simp]:
  assumes ‹∀x ∈ cons_form A. f x = g x›
  shows ‹map_con f A = map_con g A›
  using assms by (induct A) auto

lemma wff_map_con [iff]: ‹map_con f A ∈ wffs⇘α⇙ ⟷ A ∈ wffs⇘α⇙›
proof (induct A arbitrary: α)
  case (FVar x)
  then show ?case
    by (metis map_con.simps(1) surj_pair)
next
  case (FCon x)
  then show ?case
    by (induct x) (auto dest: wff_has_unique_type)
next
  case (FApp A B)
  then show ?case
    by (metis map_con.simps(3) wffs_from_app wffs_of_type_intros(3))
next
  case (FAbs x1a A)
  then show ?case
    by (metis map_con.simps(4) surj_pair wffs_from_abs wffs_of_type_intros(4))
qed

lemma finite_cons_form [simp]: ‹finite (cons_form A)›
  by (induct A) auto

lemma map_con_ineq_match [intro]: 
  assumes ‹ineq_match C (α, β, A, B)›
  shows ‹ineq_match (map_con f C) (α, β, map_con f A, map_con f B)›
  using assms
  by (auto elim: ineq_match.cases simp: ineq_match.simps)

lemma free_vars_map_con [simp]: ‹free_vars (map_con f A) = free_vars A›
  by (induct A) (auto split: if_splits)

lemma map_con_substitute [simp]: ‹map_con f (substitute {(x, α) ↣ A} B) 
  = substitute {(x, α) ↣ map_con f A} (map_con f B)›
  using singleton_substitution_simps by (induct B) auto

subsection ‹Parameter Substitution Inversion›

lemma map_con_FVar [dest]: ‹map_con f A = x⇘α⇙ ⟹ A = x⇘α⇙›
  by (induct A) (auto split: if_splits)

lemma map_con_FCon_not_param [dest]: ‹map_con f A = ⦃c⦄⇘α⇙ ⟹ ¬ is_param c ⟹ A = ⦃c⦄⇘α⇙›
  unfolding is_param_def by (induct A) (auto split: if_splits)

lemma map_con_FApp [dest!]: 
  assumes ‹map_con f A = B · C›
  shows ‹∃B' C'. map_con f B' = B ∧ map_con f C' = C ∧ A = B' · C'›
  using assms
  by (induct A) (auto split: if_splits)

lemma map_con_FAbs [dest!]: 
  assumes ‹map_con f A = λx⇘α⇙. B›
  shows ‹∃B'. map_con f B' = B ∧ A = λx⇘α⇙. B'›
  using assms
  by (induct A) (auto split: if_splits)

lemma map_con_cQ [dest]: ‹map_con f A = ⦃𝔠⇩Q⦄⇘α⇙ ⟹ A = ⦃𝔠⇩Q⦄⇘α⇙›
  by (auto simp: is_param_def)

lemma map_con_equality_of_type [dest]: 
  assumes ‹map_con f A = B =⇘α⇙ C›
  shows ‹∃B' C'. map_con f B' = B ∧ map_con f C' = C ∧ A = B' =⇘α⇙ C'›
  using assms
  by fastforce

lemma map_con_neg [dest]: ‹map_con f A = ∼⇧𝒬 B ⟹ ∃B'. map_con f B' = B ∧ A = ∼⇧𝒬 B'›
  by (induct A) auto

lemma ineq_match_map_con [dest]:
  assumes ‹ineq_match (map_con f C) (α, β, A, B)›
  shows ‹∃A' B'. map_con f A' = A ∧ map_con f B' = B ∧ ineq_match C (α, β, A', B')›
  using assms
  by fast

subsection ‹Interpretations›

interpretation P: Params map_con cons_form is_param
  by unfold_locales simp_all

interpretation C: Confl map_con cons_form is_param confl_class
  by unfold_locales (fastforce elim!: confl_class.cases simp: confl_class.simps)

interpretation A: Alpha map_con cons_form is_param alpha_class
proof (unfold_locales, safe?)
  fix ps qs f
  assume ‹ps ↝⇩α qs›
  then show ‹map (map_con f) ps ↝⇩α map (map_con f) qs›
    by (elim alpha_class.cases) (auto simp: alpha_class.simps)
qed

interpretation B: Beta map_con cons_form is_param beta_class
  by unfold_locales (auto elim!: beta_class.cases simp: beta_class.simps)

interpretation G: Gamma map_con map_con cons_form is_param gamma_class
  by unfold_locales (elim gamma_class.cases, auto simp: gamma_class.simps)

interpretation D: Delta map_con cons_form is_param delta
proof
  fix p x f
  assume ‹is_param x› ‹P.is_subst f›
  then show ‹delta (map_con f p) (f x) = map (map_con f) (delta p x)›
  proof (induct p x rule: delta.induct)
    case (1 C c)
    then have c: ‹¬ is_logical_name (f c)›
      unfolding P.is_subst_def by (auto simp: is_param_def)

    from 1 show ?case
    proof (cases ‹C ∈ wffs⇘o⇙ ∧ (∃α β A B. ineq_match C (α, β, A, B))›)
      case True
      then obtain α β A B where C: ‹C = ∼⇧𝒬 (A =⇘α → β⇙ B)›
        by fast
      then have *: ‹delta C c = [ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ]›
        using True CDelta ineq_match_delta by blast
      then have *: ‹map (map_con f) (delta C c) = [ ∼⇧𝒬 (map_con f A · ⦃f c⦄⇘α⇙ =⇘β⇙ map_con f B · ⦃f c⦄⇘α⇙) ]›
        using 1 c by (auto simp: is_param_def)
      have ‹ineq_match (map_con f C) (α, β, map_con f A, map_con f B)›
        using C map_con_ineq_match by blast
      moreover have ‹map_con f C ∈ wffs⇘o⇙›
        using True wff_map_con by blast
      ultimately have ‹delta (map_con f C) (f c) = [ ∼⇧𝒬 (map_con f A · ⦃f c⦄⇘α⇙ =⇘β⇙ map_con f B · ⦃f c⦄⇘α⇙) ]›
        unfolding CDelta using ineq_match_delta by auto
      then show ?thesis
        using * by simp
    next
      case False
      then show ?thesis
        by auto
    qed
  qed
qed

abbreviation Kinds :: ‹(nat, form) kind list› where
  ‹Kinds ≡ [C.kind, A.kind, B.kind, G.kind, D.kind]›

lemma prop⇩E_Kinds:
  assumes ‹P.sat⇩E C.kind C› ‹P.sat⇩E A.kind C›  ‹P.sat⇩E B.kind C› ‹P.sat⇩E G.kind C› ‹P.sat⇩E D.kind C›
  shows ‹P.prop⇩E Kinds C›
  unfolding P.prop⇩E_def using assms by simp

interpretation Consistency_Kinds map_con cons_form is_param Kinds
  using P.Params_axioms C.Consistency_Kind_axioms A.Consistency_Kind_axioms B.Consistency_Kind_axioms
    G.Consistency_Kind_axioms D.Consistency_Kind_axioms
  by (auto intro: Consistency_Kinds.intro simp: Consistency_Kinds_axioms_def)

interpretation Maximal_Consistency map_con cons_form is_param Kinds
proof
  have ‹infinite (UNIV :: form set)›
    using infinite_UNIV_size[of ‹λA. A · A›] by simp
  then show ‹infinite (UNIV :: form set)›
    using finite_prod by blast
qed simp

end