(*<*)
theory AOT_Axioms
  imports AOT_Definitions
begin
(*>*)

section‹Axioms of PLM›

AOT_axiom "pl:1": ‹φ → (ψ → φ)›
  by (auto simp: AOT_sem_imp AOT_model_axiomI)
AOT_axiom "pl:2": ‹(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))›
  by (auto simp: AOT_sem_imp AOT_model_axiomI)
AOT_axiom "pl:3": ‹(¬φ → ¬ψ) → ((¬φ → ψ) → φ)›
  by (auto simp: AOT_sem_imp AOT_sem_not AOT_model_axiomI)

AOT_axiom "cqt:1": ‹∀α φ{α} → (τ↓ → φ{τ})›
  by (auto simp: AOT_sem_denotes AOT_sem_forall AOT_sem_imp AOT_model_axiomI)

AOT_axiom "cqt:2[const_var]": ‹α↓›
  using AOT_sem_vars_denote by (rule AOT_model_axiomI)
AOT_axiom "cqt:2[lambda]":
  assumes ‹INSTANCE_OF_CQT_2(φ)›
  shows ‹[λν₁...ν_n φ{ν₁...ν_n}]↓›
  by (auto intro!: AOT_model_axiomI AOT_sem_cqt_2[OF assms])
AOT_axiom "cqt:2[lambda0]":
  shows ‹[λ φ]↓›
  by (auto intro!: AOT_model_axiomI
           simp: AOT_sem_lambda_denotes "existence:3"[unfolded AOT_model_equiv_def])

AOT_axiom "cqt:3": ‹∀α (φ{α} → ψ{α}) → (∀α φ{α} → ∀α ψ{α})›
  by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:4": ‹φ → ∀α φ›
  by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:5:a": ‹[Π]κ₁...κ_n → (Π↓ & κ₁...κ_n↓)›
  by (simp add: AOT_sem_conj AOT_sem_denotes AOT_sem_exe
                AOT_sem_imp AOT_model_axiomI)
AOT_axiom "cqt:5:a[1]": ‹[Π]κ → (Π↓ & κ↓)›
  using "cqt:5:a" AOT_model_axiomI by blast
AOT_axiom "cqt:5:a[2]": ‹[Π]κ₁κ₂ → (Π↓ & κ₁↓ & κ₂↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
            AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:a[3]": ‹[Π]κ₁κ₂κ₃ → (Π↓ & κ₁↓ & κ₂↓ & κ₃↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
            AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:a[4]": ‹[Π]κ₁κ₂κ₃κ₄ → (Π↓ & κ₁↓ & κ₂↓ & κ₃↓ & κ₄↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
            AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b": ‹κ₁...κ_n[Π] → (Π↓ & κ₁...κ_n↓)›
  using AOT_sem_enc_denotes
  by (auto intro!: AOT_model_axiomI simp: AOT_sem_conj AOT_sem_denotes AOT_sem_imp)+
AOT_axiom "cqt:5:b[1]": ‹κ[Π] → (Π↓ & κ↓)›
  using "cqt:5:b" AOT_model_axiomI by blast
AOT_axiom "cqt:5:b[2]": ‹κ₁κ₂[Π] → (Π↓ & κ₁↓ & κ₂↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
            AOT_sem_enc_denotes AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b[3]": ‹κ₁κ₂κ₃[Π] → (Π↓ & κ₁↓ & κ₂↓ & κ₃↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
            AOT_sem_enc_denotes AOT_sem_imp case_prodD)
AOT_axiom "cqt:5:b[4]": ‹κ₁κ₂κ₃κ₄[Π] → (Π↓ & κ₁↓ & κ₂↓ & κ₃↓ & κ₄↓)›
  by (rule AOT_model_axiomI)
     (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
            AOT_sem_enc_denotes AOT_sem_imp case_prodD)

AOT_axiom "l-identity": ‹α = β → (φ{α} → φ{β})›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_eq AOT_sem_imp)

AOT_act_axiom "logic-actual": ‹\Aφ → φ›
  by (rule AOT_model_act_axiomI)
     (simp add: AOT_sem_act AOT_sem_imp)

AOT_axiom "logic-actual-nec:1": ‹\A¬φ ≡ ¬\Aφ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_not)
AOT_axiom "logic-actual-nec:2": ‹\A(φ → ψ) ≡ (\Aφ → \Aψ)›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_imp)

AOT_axiom "logic-actual-nec:3": ‹\A(∀α φ{α}) ≡ ∀α \Aφ{α}›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_forall AOT_sem_denotes)
AOT_axiom "logic-actual-nec:4": ‹\Aφ ≡ \A\Aφ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_equiv)

AOT_axiom "qml:1": ‹◻(φ → ψ) → (◻φ → ◻ψ)›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_box AOT_sem_imp)
AOT_axiom "qml:2": ‹◻φ → φ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_box AOT_sem_imp)
AOT_axiom "qml:3": ‹♢φ → ◻♢φ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_box AOT_sem_dia AOT_sem_imp)

AOT_axiom "qml:4": ‹♢∃x (E!x & ¬\AE!x)›
  using AOT_sem_concrete AOT_model_contingent
  by (auto intro!: AOT_model_axiomI
             simp: AOT_sem_box AOT_sem_dia AOT_sem_imp AOT_sem_exists
                   AOT_sem_denotes AOT_sem_conj AOT_sem_not AOT_sem_act
                   AOT_sem_exe)+

AOT_axiom "qml-act:1": ‹\Aφ → ◻\Aφ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_box AOT_sem_imp)
AOT_axiom "qml-act:2": ‹◻φ ≡ \A◻φ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_box AOT_sem_equiv)

AOT_axiom descriptions: ‹x = \ιx(φ{x}) ≡ ∀z(\Aφ{z} ≡ z = x)›
proof (rule AOT_model_axiomI)
  AOT_modally_strict {
    AOT_show ‹x = \ιx(φ{x}) ≡ ∀z(\Aφ{z} ≡ z = x)›
      by (induct; simp add: AOT_sem_equiv AOT_sem_forall AOT_sem_act AOT_sem_eq)
         (metis (no_types, opaque_lifting) AOT_sem_desc_denotes AOT_sem_desc_prop
                                           AOT_sem_denotes)
  }
qed

AOT_axiom "lambda-predicates:1":
  ‹[λν₁...ν_n φ{ν₁...ν_n}]↓ → [λν₁...ν_n φ{ν₁...ν_n}] = [λμ₁...μ_n φ{μ₁...μ_n}]›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
AOT_axiom "lambda-predicates:1[zero]": ‹[λ p]↓ → [λ p] = [λ p]›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
AOT_axiom "lambda-predicates:2":
  ‹[λx₁...x_n φ{x₁...x_n}]↓ → ([λx₁...x_n φ{x₁...x_n}]x₁...x_n ≡ φ{x₁...x_n})›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_equiv AOT_sem_imp AOT_sem_lambda_beta AOT_sem_vars_denote)
AOT_axiom "lambda-predicates:3": ‹[λx₁...x_n [F]x₁...x_n] = F›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_lambda_eta AOT_sem_vars_denote)
AOT_axiom "lambda-predicates:3[zero]": ‹[λ p] = p›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_eq AOT_sem_lambda0 AOT_sem_vars_denote)

AOT_axiom "safe-ext":
  ‹([λν₁...ν_n φ{ν₁...ν_n}]↓ & ◻∀ν₁...∀ν_n (φ{ν₁...ν_n} ≡ ψ{ν₁...ν_n})) →
 [λν₁...ν_n ψ{ν₁...ν_n}]↓›
  using AOT_sem_lambda_coex
  by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_denotes AOT_sem_conj
                   AOT_sem_equiv AOT_sem_box AOT_sem_forall)
AOT_axiom "safe-ext[2]":
  ‹([λν₁ν₂ φ{ν₁,ν₂}]↓ & ◻∀ν₁∀ν₂ (φ{ν₁, ν₂} ≡ ψ{ν₁, ν₂})) →
 [λν₁ν₂ ψ{ν₁,ν₂}]↓›
  using "safe-ext"[where φ="λ(x,y). φ x y"]
  by (simp add: AOT_model_axiom_def AOT_sem_denotes AOT_model_denotes_prod_def
                AOT_sem_forall AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
AOT_axiom "safe-ext[3]":
  ‹([λν₁ν₂ν₃ φ{ν₁,ν₂,ν₃}]↓ & ◻∀ν₁∀ν₂∀ν₃ (φ{ν₁, ν₂, ν₃} ≡ ψ{ν₁, ν₂, ν₃})) →
 [λν₁ν₂ν₃ ψ{ν₁,ν₂,ν₃}]↓›
  using "safe-ext"[where φ="λ(x,y,z). φ x y z"]
  by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
                AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
AOT_axiom "safe-ext[4]":
  ‹([λν₁ν₂ν₃ν₄ φ{ν₁,ν₂,ν₃,ν₄}]↓ &
 ◻∀ν₁∀ν₂∀ν₃∀ν₄ (φ{ν₁, ν₂, ν₃, ν₄} ≡ ψ{ν₁, ν₂, ν₃, ν₄})) →
 [λν₁ν₂ν₃ν₄ ψ{ν₁,ν₂,ν₃,ν₄}]↓›
  using "safe-ext"[where φ="λ(x,y,z,w). φ x y z w"]
  by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
                AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)

AOT_axiom "nary-encoding[2]":
  ‹x₁x₂[F] ≡ x₁[λy [F]yx₂] & x₂[λy [F]x₁y]›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
                AOT_sem_unary_proj_enc AOT_sem_vars_denote)
AOT_axiom "nary-encoding[3]":
  ‹x₁x₂x₃[F] ≡ x₁[λy [F]yx₂x₃] & x₂[λy [F]x₁yx₃] & x₃[λy [F]x₁x₂y]›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
                AOT_sem_unary_proj_enc AOT_sem_vars_denote)
AOT_axiom "nary-encoding[4]":
  ‹x₁x₂x₃x₄[F] ≡ x₁[λy [F]yx₂x₃x₄] &
 x₂[λy [F]x₁yx₃x₄] &
 x₃[λy [F]x₁x₂yx₄] &
 x₄[λy [F]x₁x₂x₃y]›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
                AOT_sem_unary_proj_enc AOT_sem_vars_denote)

AOT_axiom encoding: ‹x[F] → ◻x[F]›
  using AOT_sem_enc_nec 
  by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_box)

AOT_axiom nocoder: ‹O!x → ¬∃F x[F]›
  by (auto intro!: AOT_model_axiomI
           simp: AOT_sem_imp AOT_sem_not AOT_sem_exists AOT_sem_ordinary
                 AOT_sem_dia
                AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes,
                                    OF AOT_sem_vars_denote])
     (metis AOT_sem_nocoder)

AOT_axiom "A-objects": ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
proof(rule AOT_model_axiomI)
  AOT_modally_strict {
    AOT_obtain κ where ‹κ↓ & ◻¬E!κ & ∀F (κ[F] ≡ φ{F})›
      using AOT_sem_A_objects[of _ φ]
      by (auto simp: AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_exists
                     AOT_sem_conj AOT_sem_not AOT_sem_dia AOT_sem_denotes
                     AOT_sem_equiv) blast
    AOT_thus ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
      unfolding AOT_sem_exists
      by (auto intro!: exI[where x=κ]
               simp: AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes]
                     AOT_sem_box AOT_sem_dia AOT_sem_not AOT_sem_denotes
                     AOT_var_of_term_inverse AOT_sem_conj
                     AOT_sem_equiv AOT_sem_forall AOT_sem_abstract)
  }
qed

AOT_theorem universal_closure:
  assumes ‹for arbitrary α: φ{α} ∈ Λ_\◻›
  shows ‹∀α φ{α} ∈ Λ_\◻›
  using assms
  by (metis AOT_term_of_var_cases AOT_model_axiom_def AOT_sem_denotes AOT_sem_forall)

AOT_theorem act_closure:
  assumes ‹φ ∈ Λ_\◻›
  shows ‹\Aφ ∈ Λ_\◻›
  using assms by (simp add: AOT_model_axiom_def AOT_sem_act)

AOT_theorem nec_closure:
  assumes ‹φ ∈ Λ_\◻›
  shows ‹◻φ ∈ Λ_\◻›
  using assms by (simp add: AOT_model_axiom_def AOT_sem_box)

AOT_theorem universal_closure_act:
  assumes ‹for arbitrary α: φ{α} ∈ Λ›
  shows ‹∀α φ{α} ∈ Λ›
  using assms
  by (metis AOT_term_of_var_cases AOT_model_act_axiom_def AOT_sem_denotes
            AOT_sem_forall)

text‹The following are not part of PLM and only hold in the extended models.
 They are a generalization of the predecessor axiom.›
context AOT_ExtendedModel
begin
AOT_axiom indistinguishable_ord_enc_all:
  ‹Π↓ & A!x & A!y & ∀F ◻([F]x ≡ [F]y) →
 ((∀G(∀z(O!z → ◻([G]z ≡ [Π]z)) → x[G])) ≡
 ∀G(∀z(O!z → ◻([G]z ≡ [Π]z)) → y[G]))›
  by (rule AOT_model_axiomI)
     (auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj
                 AOT_sem_indistinguishable_ord_enc_all)
AOT_axiom indistinguishable_ord_enc_ex:
  ‹Π↓ & A!x & A!y & ∀F ◻([F]x ≡ [F]y) →
 ((∃G(∀z(O!z → ◻([G]z ≡ [Π]z)) & x[G])) ≡
 ∃G(∀z(O!z → ◻([G]z ≡ [Π]z)) & y[G]))›
  by (rule AOT_model_axiomI)
     (auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj 
                 AOT_sem_indistinguishable_ord_enc_ex)
end

(*<*)
end
(*>*)