Theory TAO_7_Axioms

(*<*)
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 *)
(*<*) unbundle no list_enumeration_syntax and no list_comprehension_syntax(*>*) 

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] ⟶ (∃ o⇩1 . Some o⇩1 = 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] ⟶ (∃ o⇩1 . Some o⇩1 = 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!,x⇧P⦈ ❙& ❙◇❙¬⦇E!,x⇧P⦈) ❙& ❙◇❙¬(❙∃x. ⦇E!,x⇧P⦈ ❙& ❙◇❙¬⦇E!,x⇧P⦈)]]"
     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]:
    "[[x⇧P ❙= (❙ιx. φ x) ❙≡ (❙∀z.(❙𝒜(φ z) ❙≡ z ❙= x))]]"
    unfolding axiom_def
    proof (rule allI, rule EquivI; rule)
      fix v
      assume "[x⇧P ❙= (❙ιx. φ x) in v]"
      moreover hence 1:
        "∃o⇩1 o⇩2. Some o⇩1 = d⇩κ (x⇧P) ∧ Some o⇩2 = d⇩κ (❙ιx. φ x) ∧ o⇩1 = o⇩2"
        apply - unfolding identity_κ_def by meta_solver
      then obtain o⇩1 o⇩2 where 2:
        "Some o⇩1 = d⇩κ (x⇧P) ∧ Some o⇩2 = d⇩κ (❙ιx. φ x) ∧ o⇩1 = o⇩2"
        by auto
      hence 3:
        "(∃ x .((w⇩0 ⊨ φ x) ∧ (∀y. (w⇩0 ⊨ φ y) ⟶ y = x)))
         ∧ d⇩κ (❙ιx. φ x) = Some (THE x. (w⇩0 ⊨ φ x))"
        using D3 by (metis option.distinct(1))
      then obtain X where 4:
        "((w⇩0 ⊨ φ X) ∧ (∀y. (w⇩0 ⊨ φ y) ⟶ y = X))"
        by auto
      moreover have "o⇩1 = (THE x. (w⇩0 ⊨ φ x))"
        using 2 3 by auto
      ultimately have 5: "X = o⇩1"
        by (metis (mono_tags) theI)
      have "∀ z . [❙𝒜φ z in v] = [(z⇧P) ❙= (x⇧P) in v]"
      proof
        fix z
        have "[❙𝒜φ z in v] ⟹ [(z⇧P) ❙= (x⇧P) in v]"
          unfolding identity_κ_def apply meta_solver
          using 4 5 2 d⇩κ_proper w⇩0_def by auto
        moreover have "[(z⇧P) ❙= (x⇧P) in v] ⟹ [❙𝒜φ z in v]"
          unfolding identity_κ_def apply meta_solver
          using 2 4 5 
          by (simp add: d⇩κ_proper w⇩0_def)
        ultimately show "[❙𝒜φ z in v] = [(z⇧P) ❙= (x⇧P) 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) = (∃o⇩1 o⇩2. Some o⇩1 = d⇩κ (z⇧P)
                ∧ Some o⇩2 = d⇩κ (x⇧P) ∧ o⇩1 = o⇩2)"
        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 "x⇧P = (❙ιx. φ x)"
        using D3 d⇩κ_inject d⇩κ_proper w⇩0_def by presburger
      thus "[x⇧P ❙= (❙ι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 . φ (x⇧P), x⇧P⦈ ❙≡ φ (x⇧P)]]"
    apply axiom_meta_solver
    using D5_1[OF assms] d⇩κ_proper propex⇩1
    by metis

  lemma lambda_predicates_2_2[axiom]:
    assumes "IsProperInXY φ"
    shows "[[⦇(❙λ⇧2 (λ x y . φ (x⇧P) (y⇧P))), x⇧P, y⇧P⦈ ❙≡ φ (x⇧P) (y⇧P)]]"
    apply axiom_meta_solver
    using D5_2[OF assms] d⇩κ_proper propex⇩2
    by metis

  lemma lambda_predicates_2_3[axiom]:
    assumes "IsProperInXYZ φ"
    shows "[[⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈ ❙≡ φ (x⇧P) (y⇧P) (z⇧P)]]"
    proof -
      have "[[⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈ ❙→ φ (x⇧P) (y⇧P) (z⇧P)]]"
        apply axiom_meta_solver using D5_3[OF assms] by auto
      moreover have
        "[[φ (x⇧P) (y⇧P) (z⇧P) ❙→ ⦇(❙λ⇧3 (λ x y z . φ (x⇧P) (y⇧P) (z⇧P))),x⇧P,y⇧P,z⇧P⦈]]"
        apply axiom_meta_solver
        using D5_3[OF assms] d⇩κ_proper propex⇩3
        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, x⇧P⦈) ❙= F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π⇩1_def apply (rule Eq⇩1I)
    using D4_1 d⇩1_inject by simp

  lemma lambda_predicates_3_2[axiom]:
    "[[(❙λ⇧2 (λ x y . ⦇F, x⇧P, y⇧P⦈)) ❙= F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π⇩2_def apply (rule Eq⇩2I)
    using D4_2 d⇩2_inject by simp

  lemma lambda_predicates_3_3[axiom]:
    "[[(❙λ⇧3 (λ x y z . ⦇F, x⇧P, y⇧P, z⇧P⦈)) ❙= F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π⇩3_def apply (rule Eq⇩3I)
    using D4_3 d⇩3_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 Eq⇩0I)
    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 Eq⇩1I)
    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 Eq⇩2I)
    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 Eq⇩3I)
    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!,x⇧P⦈ ❙& (❙∀ F . (⦃x⇧P,F⦄ ❙≡ φ F))]]"
    unfolding axiom_def
    proof (rule allI, rule ExIRule)
      fix v
      let ?x = "αν { F . [φ F in v]}"
      have "[⦇A!,?x⇧P⦈ in v]" by (simp add: AbsS d⇩κ_proper)
      moreover have "[(❙∀F. ⦃?x⇧P,F⦄ ❙≡ φ F) in v]"
        apply meta_solver unfolding en_def
        using d⇩1.rep_eq d⇩κ_def d⇩κ_proper evalΠ⇩1_inverse by auto
      ultimately show "[⦇A!,?x⇧P⦈ ❙& (❙∀F. ⦃?x⇧P,F⦄ ❙≡ φ F) in v]"
        by (simp only: ConjS)
    qed

end

(*<*)
end
(*>*)