(*<*)
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 :: "o→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]]) ==> [[\<forall> x. φ x]]"
    by axiom_meta_solver
  lemma closures_actualization[axiom]: "[[φ]] ==> [[\<A> φ]]"
    by axiom_meta_solver
  lemma closures_necessitation[axiom]: "[[φ]] ==> [[\<box> φ]]"
    by axiom_meta_solver
  lemma necessitation_averse_axiom_instance[axiom]: "[φ] ==> [φ in dw]"
    by axiom_meta_solver
  lemma necessitation_averse_closures_universal[axiom]: "(∧x.[φ x]) ==> [\<forall> 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]:
    "[[φ \<rightarrow> (ψ \<rightarrow> φ)]]"
    by axiom_meta_solver
  lemma pl_2[axiom]:
    "[[(φ \<rightarrow> (ψ \<rightarrow> χ)) \<rightarrow> ((φ \<rightarrow> ψ) \<rightarrow> (φ \<rightarrow> χ))]]"
    by axiom_meta_solver
  lemma pl_3[axiom]:
    "[[(\<not>φ \<rightarrow> \<not>ψ) \<rightarrow> ((\<not>φ \<rightarrow> ψ) \<rightarrow> φ)]]"
    by axiom_meta_solver

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

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

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

  lemma cqt_1[axiom]:
    "[[(\<forall> α. φ α) \<rightarrow> φ α]]"
    by axiom_meta_solver
  lemma cqt_1_κ[axiom]:
    "[[(\<forall> α. φ (α^P)) \<rightarrow> ((\<exists> β . (β^P) = α) \<rightarrow> φ α)]]"
    proof -
      {
        fix v
        assume 1: "[(\<forall> α. φ (α^P)) in v]"
        assume "[(\<exists> β . (β^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 "[[(\<forall> α. φ (α^P)) \<rightarrow> ((\<exists> β . (β^P) = α) \<rightarrow> φ α)]]"
        unfolding axiom_def using ImplI by blast
    qed
  lemma cqt_3[axiom]:
    "[[(\<forall>α. φ α \<rightarrow> ψ α) \<rightarrow> ((\<forall>α. φ α) \<rightarrow> (\<forall>α. ψ α))]]"
    by axiom_meta_solver
  lemma cqt_4[axiom]:
    "[[φ \<rightarrow> (\<forall>α. φ)]]"
    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 "[[(ψ (\<iota>x . φ x)) \<rightarrow> (\<exists> α. (α^P) = (\<iota>x . φ x))]]"
    proof -
      have "∀ w . ([(ψ (\<iota>x . φ x)) in w] ⟶ (∃ o₁ . Some o₁ = d_\<kappa> (\<iota>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 "[[ψ τ \<rightarrow> (\<exists> α . (α^P) = τ)]]"
    proof -
      have "∀ w . ([(ψ τ) in w] ⟶ (∃ o₁ . Some o₁ = d_\<kappa> τ))"
        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]: "[(\<A>φ) \<equiv> φ]"
    by axiom_meta_solver
  lemma "[[(\<A>φ) \<equiv> φ]]"
    nitpick[user_axioms, expect = genuine, card = 1, card i = 2]
    oops ― ‹Counter-model by nitpick›

  lemma logic_actual_nec_1[axiom]:
    "[[\<A>\<not>φ \<equiv> \<not>\<A>φ]]"
    by axiom_meta_solver
  lemma logic_actual_nec_2[axiom]:
    "[[(\<A>(φ \<rightarrow> ψ)) \<equiv> (\<A>φ \<rightarrow> \<A>ψ)]]"
    by axiom_meta_solver
  lemma logic_actual_nec_3[axiom]:
    "[[\<A>(\<forall>α. φ α) \<equiv> (\<forall>α. \<A>(φ α))]]"
    by axiom_meta_solver
  lemma logic_actual_nec_4[axiom]:
    "[[\<A>φ \<equiv> \<A>\<A>φ]]"
    by axiom_meta_solver

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

  lemma qml_1[axiom]:
    "[[\<box>(φ \<rightarrow> ψ) \<rightarrow> (\<box>φ \<rightarrow> \<box>ψ)]]"
    by axiom_meta_solver
  lemma qml_2[axiom]:
    "[[\<box>φ \<rightarrow> φ]]"
    by axiom_meta_solver
  lemma qml_3[axiom]:
    "[[\<diamond>φ \<rightarrow> \<box>\<diamond>φ]]"
    by axiom_meta_solver
  lemma qml_4[axiom]:
    "[[\<diamond>(\<exists>x. (E!,x^P) & \<diamond>\<not>(E!,x^P)) & \<diamond>\<not>(\<exists>x. (E!,x^P) & \<diamond>\<not>(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]:
    "[[\<A>φ \<rightarrow> \<box>\<A>φ]]"
    by axiom_meta_solver
  lemma qml_act_2[axiom]:
    "[[\<box>φ \<equiv> \<A>(\<box>φ)]]"
    by axiom_meta_solver

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

  lemma descriptions[axiom]:
    "[[x^P = (\<iota>x. φ x) \<equiv> (\<forall>z.(\<A>(φ z) \<equiv> z = x))]]"
    unfolding axiom_def
    proof (rule allI, rule EquivI; rule)
      fix v
      assume "[x^P = (\<iota>x. φ x) in v]"
      moreover hence 1:
        "∃o₁ o₂. Some o₁ = d_\<kappa> (x^P) ∧ Some o₂ = d_\<kappa> (\<iota>x. φ x) ∧ o₁ = o₂"
        apply - unfolding identity_κ_def by meta_solver
      then obtain o₁ o₂ where 2:
        "Some o₁ = d_\<kappa> (x^P) ∧ Some o₂ = d_\<kappa> (\<iota>x. φ x) ∧ o₁ = o₂"
        by auto
      hence 3:
        "(∃ x .((w₀ ⊨ φ x) ∧ (∀y. (w₀ ⊨ φ y) ⟶ y = x)))
         ∧ d_\<kappa> (\<iota>x. φ x) = Some (THE x. (w₀ ⊨ φ x))"
        using D3 by (metis option.distinct(1))
      then obtain X where 4:
        "((w₀ ⊨ φ X) ∧ (∀y. (w₀ ⊨ φ y) ⟶ y = X))"
        by auto
      moreover have "o₁ = (THE x. (w₀ ⊨ φ x))"
        using 2 3 by auto
      ultimately have 5: "X = o₁"
        by (metis (mono_tags) theI)
      have "∀ z . [\<A>φ z in v] = [(z^P) = (x^P) in v]"
      proof
        fix z
        have "[\<A>φ z in v] ==> [(z^P) = (x^P) in v]"
          unfolding identity_κ_def apply meta_solver
          using 4 5 2 d_\κ_proper w₀_def by auto
        moreover have "[(z^P) = (x^P) in v] ==> [\<A>φ z in v]"
          unfolding identity_κ_def apply meta_solver
          using 2 4 5 
          by (simp add: d_\κ_proper w₀_def)
        ultimately show "[\<A>φ z in v] = [(z^P) = (x^P) in v]"
          by auto
      qed
      thus "[\<forall>z. \<A>φ z \<equiv> (z) = (x) in v]"
        unfolding identity_ν_def
        by (simp add: AllI EquivS)
    next
      fix v
      assume "[\<forall>z. \<A>φ z \<equiv> (z) = (x) in v]"
      hence "∧z. (dw ⊨ φ z) = (∃o₁ o₂. Some o₁ = d_\<kappa> (z^P)
                ∧ Some o₂ = d_\<kappa> (x^P) ∧ o₁ = o₂)"
        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 = (\<iota>x. φ x)"
        using D3 d_\κ_inject d_\κ_proper w₀_def by presburger
      thus "[x^P = (\<iota>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]:
    "(\<lambda> x . φ x) = (\<lambda> y . φ y)" ..

  lemma lambda_predicates_2_1[axiom]:
    assumes "IsProperInX φ"
    shows "[[(\<lambda> x . φ (x^P), x^P) \<equiv> φ (x^P)]]"
    apply axiom_meta_solver
    using D5_1[OF assms] d_\κ_proper propex₁
    by metis

  lemma lambda_predicates_2_2[axiom]:
    assumes "IsProperInXY φ"
    shows "[[((\<lambda>² (λ x y . φ (x^P) (y^P))), x^P, y^P) \<equiv> φ (x^P) (y^P)]]"
    apply axiom_meta_solver
    using D5_2[OF assms] d_\κ_proper propex₂
    by metis

  lemma lambda_predicates_2_3[axiom]:
    assumes "IsProperInXYZ φ"
    shows "[[((\<lambda>³ (λ x y z . φ (x^P) (y^P) (z^P))),x^P,y^P,z^P) \<equiv> φ (x^P) (y^P) (z^P)]]"
    proof -
      have "[[((\<lambda>³ (λ x y z . φ (x^P) (y^P) (z^P))),x^P,y^P,z^P) \<rightarrow> φ (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) \<rightarrow> ((\<lambda>³ (λ 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₃
        by (metis (no_types, lifting))
      ultimately show ?thesis unfolding axiom_def equiv_def ConjS by blast
    qed

  lemma lambda_predicates_3_0[axiom]:
    "[[(\<lambda>⁰ φ) = φ]]"
    unfolding identity_defs
    apply axiom_meta_solver
    by (simp add: meta_defs meta_aux)

  lemma lambda_predicates_3_1[axiom]:
    "[[(\<lambda> x . (F, x^P)) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π₁_def apply (rule Eq₁I)
    using D4_1 d₁_inject by simp

  lemma lambda_predicates_3_2[axiom]:
    "[[(\<lambda>² (λ x y . (F, x^P, y^P))) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π₂_def apply (rule Eq₂I)
    using D4_2 d₂_inject by simp

  lemma lambda_predicates_3_3[axiom]:
    "[[(\<lambda>³ (λ x y z . (F, x^P, y^P, z^P))) = F]]"
    unfolding axiom_def
    apply (rule allI)
    unfolding identity_Π₃_def apply (rule Eq₃I)
    using D4_3 d₃_inject by simp

  lemma lambda_predicates_4_0[axiom]:
    assumes "∧x.[(\<A>(φ x \<equiv> ψ x)) in v]"
    shows "[[(\<lambda>⁰ (χ (\<iota>x. φ x)) = \<lambda>⁰ (χ (\<iota>x. ψ x)))]]"
    unfolding axiom_def identity_o_def apply - apply (rule allI; rule Eq₀I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_1[axiom]:
    assumes "∧x.[(\<A>(φ x \<equiv> ψ x)) in v]"
    shows "[[((\<lambda> x . χ (\<iota>x. φ x) x) = (\<lambda> x . χ (\<iota>x. ψ x) x))]]"
    unfolding axiom_def identity_Π₁_def apply - apply (rule allI; rule Eq₁I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_2[axiom]:
    assumes "∧x.[(\<A>(φ x \<equiv> ψ x)) in v]"
    shows "[[((\<lambda>² (λ x y . χ (\<iota>x. φ x) x y)) = (\<lambda>² (λ x y . χ (\<iota>x. ψ x) x y)))]]"
    unfolding axiom_def identity_Π₂_def apply - apply (rule allI; rule Eq₂I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

  lemma lambda_predicates_4_3[axiom]:
    assumes "∧x.[(\<A>(φ x \<equiv> ψ x)) in v]"
    shows "[[(\<lambda>³ (λ x y z . χ (\<iota>x. φ x) x y z)) = (\<lambda>³ (λ x y z . χ (\<iota>x. ψ x) x y z))]]"
    unfolding axiom_def identity_Π₃_def apply - apply (rule allI; rule Eq₃I)
    using TheEqI[OF assms[THEN ActualE, THEN EquivE]] by auto

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

  lemma encoding[axiom]:
    "[[{x,F} \<rightarrow> \<box>{x,F}]]"
    by axiom_meta_solver
  lemma nocoder[axiom]:
    "[[(O!,x) \<rightarrow> \<not>(\<exists> 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]:
    "[[\<exists>x. (A!,x^P) & (\<forall> F . ({x^P,F} \<equiv> φ 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 "[(\<forall>F. {?x^P,F} \<equiv> φ F) in v]"
        apply meta_solver unfolding en_def
        using d₁.rep_eq d_\κ_def d_\κ_proper evalΠ₁_inverse by auto
      ultimately show "[(A!,?x^P) & (\<forall>F. {?x^P,F} \<equiv> φ F) in v]"
        by (simp only: ConjS)
    qed

end

(*<*)
end
(*>*)