Theory TAO_7_Axioms

theory TAO_7_Axioms
imports TAO_6_Identifiable
(*<*)
theory TAO_7_Axioms
imports TAO_6_Identifiable
begin
(*>*)

section‹The Axioms of PLM›
text‹\label{TAO_Axioms}›

text‹
\begin{remark}
  The axioms of PLM can now be derived from the Semantics
  and the model structure.
\end{remark}
›

(* TODO: why is this needed again here? The syntax should already
         have been disabled in TAO_Semantics. *)
(* disable list syntax [] to replace it with truth evaluation *)
(*<*) no_syntax "_list" :: "args ⇒ 'a list" ("[(_)]") (*>*) 
(*<*) no_syntax "__listcompr" :: "args ⇒ 'a list" ("[(_)]") (*>*) 

locale Axioms
begin
  interpretation MetaSolver .
  interpretation Semantics .
  named_theorems axiom

text‹
\begin{remark}
  The special syntax ‹[[_]]› is introduced for stating the axioms.
  Modally-fragile axioms are stated with the syntax for actual validity ‹[_]›.
\end{remark}
›

  definition axiom :: "𝗈⇒bool" ("[[_]]") where "axiom ≡ λ φ . ∀ v . [φ in v]"

  method axiom_meta_solver = ((((unfold axiom_def)?, rule allI) | (unfold actual_validity_def)?), meta_solver,
                              (simp | (auto; fail))?)

subsection‹Closures›
text‹\label{TAO_Axioms_Closures}›

  text‹
\begin{remark}
  Rules resembling the concepts of closures in PLM are derived. Theorem attributes are introduced
  to aid in the instantiation of the axioms.
\end{remark}
›

  lemma axiom_instance[axiom]: "[[φ]] ⟹ [φ in v]"
    unfolding axiom_def by simp
  lemma closures_universal[axiom]: "(⋀x.[[φ x]]) ⟹ [[ x. φ x]]"
    by axiom_meta_solver
  lemma closures_actualization[axiom]: "[[φ]] ⟹ [[𝒜 φ]]"
    by axiom_meta_solver
  lemma closures_necessitation[axiom]: "[[φ]] ⟹ [[ φ]]"
    by axiom_meta_solver
  lemma necessitation_averse_axiom_instance[axiom]: "[φ] ⟹ [φ in dw]"
    by axiom_meta_solver
  lemma necessitation_averse_closures_universal[axiom]: "(⋀x.[φ x]) ⟹ [ x. φ x]"
    by axiom_meta_solver

  attribute_setup axiom_instance = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm axiom_instance}))
›

  attribute_setup necessitation_averse_axiom_instance = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm necessitation_averse_axiom_instance}))
›

  attribute_setup axiom_necessitation = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_necessitation}))
›

  attribute_setup axiom_actualization = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_actualization}))
›

  attribute_setup axiom_universal = ‹
    Scan.succeed (Thm.rule_attribute [] 
      (fn _ => fn thm => thm RS @{thm closures_universal}))
›

subsection‹Axioms for Negations and Conditionals›
text‹\label{TAO_Axioms_NegationsAndConditionals}›

  lemma pl_1[axiom]:
    "[[φ  φ)]]"
    by axiom_meta_solver
  lemma pl_2[axiom]:
    "[[(φ  χ))  ((φ  ψ)  χ))]]"
    by axiom_meta_solver
  lemma pl_3[axiom]:
    "[[(¬φ  ¬ψ)  ((¬φ  ψ)  φ)]]"
    by axiom_meta_solver

subsection‹Axioms of Identity›
text‹\label{TAO_Axioms_Identity}›

  lemma l_identity[axiom]:
    "[[α = β  (φ α  φ β)]]"
    using l_identity apply - by axiom_meta_solver

subsection‹Axioms of Quantification›
text‹\label{TAO_Axioms_Quantification}›

  lemma cqt_1[axiom]:
    "[[( α. φ α)  φ α]]"
    by axiom_meta_solver
  lemma cqt_1_κ[axiom]:
    "[[( α. φ (αP))  (( β . (βP) = α)  φ α)]]"
    proof -
      {
        fix v
        assume 1: "[( α. φ (αP)) in v]"
        assume "[( β . (βP) = α) in v]"
        then obtain β where 2:
          "[(βP) = α in v]" by (rule ExERule)
        hence "[φ (βP) in v]" using 1 AllE by fast
        hence "[φ α in v]"
          using l_identity[where φ=φ, axiom_instance]
          ImplS 2 by simp
      }
      thus "[[( α. φ (αP))  (( β . (βP) = α)  φ α)]]"
        unfolding axiom_def using ImplI by blast
    qed
  lemma cqt_3[axiom]:
    "[[(α. φ α  ψ α)  ((α. φ α)  (α. ψ α))]]"
    by axiom_meta_solver
  lemma cqt_4[axiom]:
    "[[φ  (α. φ)]]"
    by axiom_meta_solver

  inductive SimpleExOrEnc
    where "SimpleExOrEnc (λ x . ⦇F,x⦈)"
        | "SimpleExOrEnc (λ x . ⦇F,x,y⦈)"
        | "SimpleExOrEnc (λ x . ⦇F,y,x⦈)"
        | "SimpleExOrEnc (λ x . ⦇F,x,y,z⦈)"
        | "SimpleExOrEnc (λ x . ⦇F,y,x,z⦈)"
        | "SimpleExOrEnc (λ x . ⦇F,y,z,x⦈)"
        | "SimpleExOrEnc (λ x . ⦃x,F⦄)"

  lemma cqt_5[axiom]:
    assumes "SimpleExOrEnc ψ"
    shows "[[(ψ (ιx . φ x))  ( α. (αP) = (ιx . φ x))]]"
    proof -
      have "∀ w . ([(ψ (ιx . φ x)) in w] ⟶ (∃ o1 . Some o1 = dκ (ιx . φ x)))"
        using assms apply induct by (meta_solver;metis)+
     thus ?thesis
      apply - unfolding identity_κ_def
      apply axiom_meta_solver
      using dκ_proper by auto
    qed

  lemma cqt_5_mod[axiom]:
    assumes "SimpleExOrEnc ψ"
    shows "[[ψ τ  ( α . (αP) = τ)]]"
    proof -
      have "∀ w . ([(ψ τ) in w] ⟶ (∃ o1 . Some o1 = dκ τ))"
        using assms apply induct by (meta_solver;metis)+
      thus ?thesis
        apply - unfolding identity_κ_def
        apply axiom_meta_solver
        using dκ_proper by auto
    qed

subsection‹Axioms of Actuality›
text‹\label{TAO_Axioms_Actuality}›

  lemma logic_actual[axiom]: "[(𝒜φ)  φ]"
    by axiom_meta_solver
  lemma "[[(𝒜φ)  φ]]"
    nitpick[user_axioms, expect = genuine, card = 1, card i = 2]
    oops ― ‹Counter-model by nitpick›

  lemma logic_actual_nec_1[axiom]:
    "[[𝒜¬φ  ¬𝒜φ]]"
    by axiom_meta_solver
  lemma logic_actual_nec_2[axiom]:
    "[[(𝒜 ψ))  (𝒜φ  𝒜ψ)]]"
    by axiom_meta_solver
  lemma logic_actual_nec_3[axiom]:
    "[[𝒜(α. φ α)  (α. 𝒜(φ α))]]"
    by axiom_meta_solver
  lemma logic_actual_nec_4[axiom]:
    "[[𝒜φ  𝒜𝒜φ]]"
    by axiom_meta_solver

subsection‹Axioms of Necessity›
text‹\label{TAO_Axioms_Necessity}›

  lemma qml_1[axiom]:
    "[[ ψ)  (φ  ψ)]]"
    by axiom_meta_solver
  lemma qml_2[axiom]:
    "[[φ  φ]]"
    by axiom_meta_solver
  lemma qml_3[axiom]:
    "[[φ  φ]]"
    by axiom_meta_solver
  lemma qml_4[axiom]:
    "[[(x. ⦇E!,xP& ¬⦇E!,xP⦈) & ¬(x. ⦇E!,xP& ¬⦇E!,xP⦈)]]"
     unfolding axiom_def
     using PossiblyContingentObjectExistsAxiom
           PossiblyNoContingentObjectExistsAxiom
     apply (simp add: meta_defs meta_aux conn_defs forall_ν_def
                 split: ν.split υ.split)
     by (metis νυ_ων_is_ωυ υ.distinct(1) υ.inject(1))

subsection‹Axioms of Necessity and Actuality›
text‹\label{TAO_Axioms_NecessityAndActuality}›

  lemma qml_act_1[axiom]:
    "[[𝒜φ  𝒜φ]]"
    by axiom_meta_solver
  lemma qml_act_2[axiom]:
    "[[φ  𝒜(φ)]]"
    by axiom_meta_solver

subsection‹Axioms of Descriptions›
text‹\label{TAO_Axioms_Descriptions}›

  lemma descriptions[axiom]:
    "[[xP = (ιx. φ x)  (z.(𝒜(φ z)  z = x))]]"
    unfolding axiom_def
    proof (rule allI, rule EquivI; rule)
      fix v
      assume "[xP = (ιx. φ x) in v]"
      moreover hence 1:
        "∃o1 o2. Some o1 = dκ (xP) ∧ Some o2 = dκ (ιx. φ x) ∧ o1 = o2"
        apply - unfolding identity_κ_def by meta_solver
      then obtain o1 o2 where 2:
        "Some o1 = dκ (xP) ∧ Some o2 = dκ (ιx. φ x) ∧ o1 = o2"
        by auto
      hence 3:
        "(∃ x .((w0 ⊨ φ x) ∧ (∀y. (w0 ⊨ φ y) ⟶ y = x)))
         ∧ dκ (ιx. φ x) = Some (THE x. (w0 ⊨ φ x))"
        using D3 by (metis option.distinct(1))
      then obtain X where 4:
        "((w0 ⊨ φ X) ∧ (∀y. (w0 ⊨ φ y) ⟶ y = X))"
        by auto
      moreover have "o1 = (THE x. (w0 ⊨ φ x))"
        using 2 3 by auto
      ultimately have 5: "X = o1"
        by (metis (mono_tags) theI)
      have "∀ z . [𝒜φ z in v] = [(zP) = (xP) in v]"
      proof
        fix z
        have "[𝒜φ z in v] ⟹ [(zP) = (xP) in v]"
          unfolding identity_κ_def apply meta_solver
          using 4 5 2 dκ_proper w0_def by auto
        moreover have "[(zP) = (xP) in v] ⟹ [𝒜φ z in v]"
          unfolding identity_κ_def apply meta_solver
          using 2 4 5 
          by (simp add: dκ_proper w0_def)
        ultimately show "[𝒜φ z in v] = [(zP) = (xP) in v]"
          by auto
      qed
      thus "[z. 𝒜φ z  (z) = (x) in v]"
        unfolding identity_ν_def
        by (simp add: AllI EquivS)
    next
      fix v
      assume "[z. 𝒜φ z  (z) = (x) in v]"
      hence "⋀z. (dw ⊨ φ z) = (∃o1 o2. Some o1 = dκ (zP)
                ∧ Some o2 = dκ (xP) ∧ o1 = o2)"
        apply - unfolding identity_ν_def identity_κ_def by meta_solver
      hence "∀ z . (dw ⊨ φ z) = (z = x)"
        by (simp add: dκ_proper)
      moreover hence "x = (THE z . (dw ⊨ φ z))" by simp
      ultimately have "xP = (ιx. φ x)"
        using D3 dκ_inject dκ_proper w0_def by presburger
      thus "[xP = (ιx. φ x) in v]"
        using EqκS unfolding identity_κ_def by (metis dκ_proper)
    qed

subsection‹Axioms for Complex Relation Terms›
text‹\label{TAO_Axioms_ComplexRelationTerms}›

  lemma lambda_predicates_1[axiom]:
    "(λ x . φ x) = (λ y . φ y)" ..

  lemma lambda_predicates_2_1[axiom]:
    assumes "IsProperInX φ"
    shows "[[⦇λ x . φ (xP), xP φ (xP)]]"
    apply axiom_meta_solver
    using D5_1[OF assms] dκ_proper propex1
    by metis

  lemma lambda_predicates_2_2[axiom]:
    assumes "IsProperInXY φ"
    shows "[[⦇(λ2 (λ x y . φ (xP) (yP))), xP, yP φ (xP) (yP)]]"
    apply axiom_meta_solver
    using D5_2[OF assms] dκ_proper propex2
    by metis

  lemma lambda_predicates_2_3[axiom]:
    assumes "IsProperInXYZ φ"
    shows "[[⦇(λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP φ (xP) (yP) (zP)]]"
    proof -
      have "[[⦇(λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP φ (xP) (yP) (zP)]]"
        apply axiom_meta_solver using D5_3[OF assms] by auto
      moreover have
        "[[φ (xP) (yP) (zP)  ⦇(λ3 (λ x y z . φ (xP) (yP) (zP))),xP,yP,zP⦈]]"
        apply axiom_meta_solver
        using D5_3[OF assms] dκ_proper propex3
        by (metis (no_types, lifting))
      ultimately show ?thesis unfolding axiom_def equiv_def ConjS by blast
    qed

  lemma lambda_predicates_3_0[axiom]:
    "[[(λ0 φ) = φ]]"
    unfolding identity_defs
    apply axiom_meta_solver
    by (simp add: meta_defs meta_aux)

  lemma lambda_predicates_3_1[axiom]:
    "[[(λ x . ⦇F, xP⦈) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π1_def apply (rule Eq1I)
    using D4_1 d1_inject by simp

  lemma lambda_predicates_3_2[axiom]:
    "[[(λ2 (λ x y . ⦇F, xP, yP⦈)) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π2_def apply (rule Eq2I)
    using D4_2 d2_inject by simp

  lemma lambda_predicates_3_3[axiom]:
    "[[(λ3 (λ x y z . ⦇F, xP, yP, zP⦈)) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π3_def apply (rule Eq3I)
    using D4_3 d3_inject by simp

  lemma lambda_predicates_4_0[axiom]:
    assumes "⋀x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[(λ0 (χ (ιx. φ x)) = λ0 (χ (ιx. ψ x)))]]"
    unfolding axiom_def identity_𝗈_def apply - apply (rule allI; rule Eq0I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_1[axiom]:
    assumes "⋀x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[((λ x . χ (ιx. φ x) x) = (λ x . χ (ιx. ψ x) x))]]"
    unfolding axiom_def identity_Π1_def apply - apply (rule allI; rule Eq1I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_2[axiom]:
    assumes "⋀x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[((λ2 (λ x y . χ (ιx. φ x) x y)) = (λ2 (λ x y . χ (ιx. ψ x) x y)))]]"
    unfolding axiom_def identity_Π2_def apply - apply (rule allI; rule Eq2I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_3[axiom]:
    assumes "⋀x.[(𝒜(φ x  ψ x)) in v]"
    shows "[[(λ3 (λ x y z . χ (ιx. φ x) x y z)) = (λ3 (λ x y z . χ (ιx. ψ x) x y z))]]"
    unfolding axiom_def identity_Π3_def apply - apply (rule allI; rule Eq3I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

subsection‹Axioms of Encoding›
text‹\label{TAO_Axioms_Encoding}›

  lemma encoding[axiom]:
    "[[⦃x,F⦄  ⦃x,F⦄]]"
    by axiom_meta_solver
  lemma nocoder[axiom]:
    "[[⦇O!,x⦈  ¬( F . ⦃x,F⦄)]]"
    unfolding axiom_def
    apply (rule allI, rule ImplI, subst (asm) OrdS)
    apply meta_solver unfolding en_def
    by (metis ν.simps(5) mem_Collect_eq option.sel)
  lemma A_objects[axiom]:
    "[[x. ⦇A!,xP& ( F . (⦃xP,F⦄  φ F))]]"
    unfolding axiom_def
    proof (rule allI, rule ExIRule)
      fix v
      let ?x = "αν { F . [φ F in v]}"
      have "[⦇A!,?xP⦈ in v]" by (simp add: AbsS dκ_proper)
      moreover have "[(F. ⦃?xP,F⦄  φ F) in v]"
        apply meta_solver unfolding en_def
        using d1.rep_eq dκ_def dκ_proper evalΠ1_inverse by auto
      ultimately show "[⦇A!,?xP& (F. ⦃?xP,F⦄  φ F) in v]"
        by (simp only: ConjS)
    qed

end

(*<*)
end
(*>*)