Theory AOT_Axioms

(*<*)
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 ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩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": ‹[Π]κ⇩1...κ⇩n → (Π↓ & κ⇩1...κ⇩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]": ‹[Π]κ⇩1κ⇩2 → (Π↓ & κ⇩1↓ & κ⇩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]": ‹[Π]κ⇩1κ⇩2κ⇩3 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩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]": ‹[Π]κ⇩1κ⇩2κ⇩3κ⇩4 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩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": ‹κ⇩1...κ⇩n[Π] → (Π↓ & κ⇩1...κ⇩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]": ‹κ⇩1κ⇩2[Π] → (Π↓ & κ⇩1↓ & κ⇩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]": ‹κ⇩1κ⇩2κ⇩3[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩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]": ‹κ⇩1κ⇩2κ⇩3κ⇩4[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩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": ‹❙𝒜φ → φ›
  by (rule AOT_model_act_axiomI)
     (simp add: AOT_sem_act AOT_sem_imp)

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

AOT_axiom "logic-actual-nec:3": ‹❙𝒜(∀α φ{α}) ≡ ∀α ❙𝒜φ{α}›
  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": ‹❙𝒜φ ≡ ❙𝒜❙𝒜φ›
  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 & ¬❙𝒜E!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": ‹❙𝒜φ → □❙𝒜φ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_box AOT_sem_imp)
AOT_axiom "qml-act:2": ‹□φ ≡ ❙𝒜□φ›
  by (rule AOT_model_axiomI)
     (simp add: AOT_sem_act AOT_sem_box AOT_sem_equiv)

AOT_axiom descriptions: ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{z} ≡ z = x)›
proof (rule AOT_model_axiomI)
  AOT_modally_strict {
    AOT_show ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{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":
  ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ → [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λμ⇩1...μ⇩n φ{μ⇩1...μ⇩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⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → ([λx⇩1...x⇩n φ{x⇩1...x⇩n}]x⇩1...x⇩n ≡ φ{x⇩1...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⇩1...x⇩n [F]x⇩1...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":
  ‹([λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ & □∀ν⇩1...∀ν⇩n (φ{ν⇩1...ν⇩n} ≡ ψ{ν⇩1...ν⇩n})) →
   [λν⇩1...ν⇩n ψ{ν⇩1...ν⇩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]":
  ‹([λν⇩1ν⇩2 φ{ν⇩1,ν⇩2}]↓ & □∀ν⇩1∀ν⇩2 (φ{ν⇩1, ν⇩2} ≡ ψ{ν⇩1, ν⇩2})) →
   [λν⇩1ν⇩2 ψ{ν⇩1,ν⇩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]":
  ‹([λν⇩1ν⇩2ν⇩3 φ{ν⇩1,ν⇩2,ν⇩3}]↓ & □∀ν⇩1∀ν⇩2∀ν⇩3 (φ{ν⇩1, ν⇩2, ν⇩3} ≡ ψ{ν⇩1, ν⇩2, ν⇩3})) →
   [λν⇩1ν⇩2ν⇩3 ψ{ν⇩1,ν⇩2,ν⇩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]":
  ‹([λν⇩1ν⇩2ν⇩3ν⇩4 φ{ν⇩1,ν⇩2,ν⇩3,ν⇩4}]↓ &
    □∀ν⇩1∀ν⇩2∀ν⇩3∀ν⇩4 (φ{ν⇩1, ν⇩2, ν⇩3, ν⇩4} ≡ ψ{ν⇩1, ν⇩2, ν⇩3, ν⇩4})) →
   [λν⇩1ν⇩2ν⇩3ν⇩4 ψ{ν⇩1,ν⇩2,ν⇩3,ν⇩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⇩1x⇩2[F] ≡ x⇩1[λy [F]yx⇩2] & x⇩2[λy [F]x⇩1y]›
  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⇩1x⇩2x⇩3[F] ≡ x⇩1[λy [F]yx⇩2x⇩3] & x⇩2[λy [F]x⇩1yx⇩3] & x⇩3[λy [F]x⇩1x⇩2y]›
  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⇩1x⇩2x⇩3x⇩4[F] ≡ x⇩1[λy [F]yx⇩2x⇩3x⇩4] &
                 x⇩2[λy [F]x⇩1yx⇩3x⇩4] &
                 x⇩3[λy [F]x⇩1x⇩2yx⇩4] &
                 x⇩4[λy [F]x⇩1x⇩2x⇩3y]›
  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 ‹❙𝒜φ ∈ Λ⇩□›
  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
(*>*)