Theory AOT_Axioms
1
2theory AOT_Axioms
3 imports AOT_Definitions
4begin
5
6
7section‹Axioms of PLM›
8
9AOT_axiom "pl:1": ‹φ → (ψ → φ)›
10 by (auto simp: AOT_sem_imp AOT_model_axiomI)
11AOT_axiom "pl:2": ‹(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))›
12 by (auto simp: AOT_sem_imp AOT_model_axiomI)
13AOT_axiom "pl:3": ‹(¬φ → ¬ψ) → ((¬φ → ψ) → φ)›
14 by (auto simp: AOT_sem_imp AOT_sem_not AOT_model_axiomI)
15
16AOT_axiom "cqt:1": ‹∀α φ{α} → (τ↓ → φ{τ})›
17 by (auto simp: AOT_sem_denotes AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
18
19AOT_axiom "cqt:2[const_var]": ‹α↓›
20 using AOT_sem_vars_denote by (rule AOT_model_axiomI)
21AOT_axiom "cqt:2[lambda]":
22 assumes ‹INSTANCE_OF_CQT_2(φ)›
23 shows ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓›
24 by (auto intro!: AOT_model_axiomI AOT_sem_cqt_2[OF assms])
25AOT_axiom "cqt:2[lambda0]":
26 shows ‹[λ φ]↓›
27 by (auto intro!: AOT_model_axiomI
28 simp: AOT_sem_lambda_denotes "existence:3"[unfolded AOT_model_equiv_def])
29
30AOT_axiom "cqt:3": ‹∀α (φ{α} → ψ{α}) → (∀α φ{α} → ∀α ψ{α})›
31 by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
32AOT_axiom "cqt:4": ‹φ → ∀α φ›
33 by (simp add: AOT_sem_forall AOT_sem_imp AOT_model_axiomI)
34AOT_axiom "cqt:5:a": ‹[Π]κ⇩1...κ⇩n → (Π↓ & κ⇩1...κ⇩n↓)›
35 by (simp add: AOT_sem_conj AOT_sem_denotes AOT_sem_exe
36 AOT_sem_imp AOT_model_axiomI)
37AOT_axiom "cqt:5:a[1]": ‹[Π]κ → (Π↓ & κ↓)›
38 using "cqt:5:a" AOT_model_axiomI by blast
39AOT_axiom "cqt:5:a[2]": ‹[Π]κ⇩1κ⇩2 → (Π↓ & κ⇩1↓ & κ⇩2↓)›
40 by (rule AOT_model_axiomI)
41 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
42 AOT_sem_imp case_prodD)
43AOT_axiom "cqt:5:a[3]": ‹[Π]κ⇩1κ⇩2κ⇩3 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓)›
44 by (rule AOT_model_axiomI)
45 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
46 AOT_sem_imp case_prodD)
47AOT_axiom "cqt:5:a[4]": ‹[Π]κ⇩1κ⇩2κ⇩3κ⇩4 → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩4↓)›
48 by (rule AOT_model_axiomI)
49 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes AOT_sem_exe
50 AOT_sem_imp case_prodD)
51AOT_axiom "cqt:5:b": ‹κ⇩1...κ⇩n[Π] → (Π↓ & κ⇩1...κ⇩n↓)›
52 using AOT_sem_enc_denotes
53 by (auto intro!: AOT_model_axiomI simp: AOT_sem_conj AOT_sem_denotes AOT_sem_imp)+
54AOT_axiom "cqt:5:b[1]": ‹κ[Π] → (Π↓ & κ↓)›
55 using "cqt:5:b" AOT_model_axiomI by blast
56AOT_axiom "cqt:5:b[2]": ‹κ⇩1κ⇩2[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓)›
57 by (rule AOT_model_axiomI)
58 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
59 AOT_sem_enc_denotes AOT_sem_imp case_prodD)
60AOT_axiom "cqt:5:b[3]": ‹κ⇩1κ⇩2κ⇩3[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓)›
61 by (rule AOT_model_axiomI)
62 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
63 AOT_sem_enc_denotes AOT_sem_imp case_prodD)
64AOT_axiom "cqt:5:b[4]": ‹κ⇩1κ⇩2κ⇩3κ⇩4[Π] → (Π↓ & κ⇩1↓ & κ⇩2↓ & κ⇩3↓ & κ⇩4↓)›
65 by (rule AOT_model_axiomI)
66 (metis AOT_model_denotes_prod_def AOT_sem_conj AOT_sem_denotes
67 AOT_sem_enc_denotes AOT_sem_imp case_prodD)
68
69AOT_axiom "l-identity": ‹α = β → (φ{α} → φ{β})›
70 by (rule AOT_model_axiomI)
71 (simp add: AOT_sem_eq AOT_sem_imp)
72
73AOT_act_axiom "logic-actual": ‹❙𝒜φ → φ›
74 by (rule AOT_model_act_axiomI)
75 (simp add: AOT_sem_act AOT_sem_imp)
76
77AOT_axiom "logic-actual-nec:1": ‹❙𝒜¬φ ≡ ¬❙𝒜φ›
78 by (rule AOT_model_axiomI)
79 (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_not)
80AOT_axiom "logic-actual-nec:2": ‹❙𝒜(φ → ψ) ≡ (❙𝒜φ → ❙𝒜ψ)›
81 by (rule AOT_model_axiomI)
82 (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_imp)
83
84AOT_axiom "logic-actual-nec:3": ‹❙𝒜(∀α φ{α}) ≡ ∀α ❙𝒜φ{α}›
85 by (rule AOT_model_axiomI)
86 (simp add: AOT_sem_act AOT_sem_equiv AOT_sem_forall AOT_sem_denotes)
87AOT_axiom "logic-actual-nec:4": ‹❙𝒜φ ≡ ❙𝒜❙𝒜φ›
88 by (rule AOT_model_axiomI)
89 (simp add: AOT_sem_act AOT_sem_equiv)
90
91AOT_axiom "qml:1": ‹□(φ → ψ) → (□φ → □ψ)›
92 by (rule AOT_model_axiomI)
93 (simp add: AOT_sem_box AOT_sem_imp)
94AOT_axiom "qml:2": ‹□φ → φ›
95 by (rule AOT_model_axiomI)
96 (simp add: AOT_sem_box AOT_sem_imp)
97AOT_axiom "qml:3": ‹◇φ → □◇φ›
98 by (rule AOT_model_axiomI)
99 (simp add: AOT_sem_box AOT_sem_dia AOT_sem_imp)
100
101AOT_axiom "qml:4": ‹◇∃x (E!x & ¬❙𝒜E!x)›
102 using AOT_sem_concrete AOT_model_contingent
103 by (auto intro!: AOT_model_axiomI
104 simp: AOT_sem_box AOT_sem_dia AOT_sem_imp AOT_sem_exists
105 AOT_sem_denotes AOT_sem_conj AOT_sem_not AOT_sem_act
106 AOT_sem_exe)+
107
108AOT_axiom "qml-act:1": ‹❙𝒜φ → □❙𝒜φ›
109 by (rule AOT_model_axiomI)
110 (simp add: AOT_sem_act AOT_sem_box AOT_sem_imp)
111AOT_axiom "qml-act:2": ‹□φ ≡ ❙𝒜□φ›
112 by (rule AOT_model_axiomI)
113 (simp add: AOT_sem_act AOT_sem_box AOT_sem_equiv)
114
115AOT_axiom descriptions: ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{z} ≡ z = x)›
116proof (rule AOT_model_axiomI)
117 AOT_modally_strict {
118 AOT_show ‹x = ❙ιx(φ{x}) ≡ ∀z(❙𝒜φ{z} ≡ z = x)›
119 by (induct; simp add: AOT_sem_equiv AOT_sem_forall AOT_sem_act AOT_sem_eq)
120 (metis (no_types, opaque_lifting) AOT_sem_desc_denotes AOT_sem_desc_prop
121 AOT_sem_denotes)
122 }
123qed
124
125AOT_axiom "lambda-predicates:1":
126 ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ → [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λμ⇩1...μ⇩n φ{μ⇩1...μ⇩n}]›
127 by (rule AOT_model_axiomI)
128 (simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
129AOT_axiom "lambda-predicates:1[zero]": ‹[λ p]↓ → [λ p] = [λ p]›
130 by (rule AOT_model_axiomI)
131 (simp add: AOT_sem_denotes AOT_sem_eq AOT_sem_imp)
132AOT_axiom "lambda-predicates:2":
133 ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → ([λx⇩1...x⇩n φ{x⇩1...x⇩n}]x⇩1...x⇩n ≡ φ{x⇩1...x⇩n})›
134 by (rule AOT_model_axiomI)
135 (simp add: AOT_sem_equiv AOT_sem_imp AOT_sem_lambda_beta AOT_sem_vars_denote)
136AOT_axiom "lambda-predicates:3": ‹[λx⇩1...x⇩n [F]x⇩1...x⇩n] = F›
137 by (rule AOT_model_axiomI)
138 (simp add: AOT_sem_lambda_eta AOT_sem_vars_denote)
139AOT_axiom "lambda-predicates:3[zero]": ‹[λ p] = p›
140 by (rule AOT_model_axiomI)
141 (simp add: AOT_sem_eq AOT_sem_lambda0 AOT_sem_vars_denote)
142
143AOT_axiom "safe-ext":
144 ‹([λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓ & □∀ν⇩1...∀ν⇩n (φ{ν⇩1...ν⇩n} ≡ ψ{ν⇩1...ν⇩n})) →
145 [λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]↓›
146 using AOT_sem_lambda_coex
147 by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_denotes AOT_sem_conj
148 AOT_sem_equiv AOT_sem_box AOT_sem_forall)
149AOT_axiom "safe-ext[2]":
150 ‹([λν⇩1ν⇩2 φ{ν⇩1,ν⇩2}]↓ & □∀ν⇩1∀ν⇩2 (φ{ν⇩1, ν⇩2} ≡ ψ{ν⇩1, ν⇩2})) →
151 [λν⇩1ν⇩2 ψ{ν⇩1,ν⇩2}]↓›
152 using "safe-ext"[where φ="λ(x,y). φ x y"]
153 by (simp add: AOT_model_axiom_def AOT_sem_denotes AOT_model_denotes_prod_def
154 AOT_sem_forall AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
155AOT_axiom "safe-ext[3]":
156 ‹([λν⇩1ν⇩2ν⇩3 φ{ν⇩1,ν⇩2,ν⇩3}]↓ & □∀ν⇩1∀ν⇩2∀ν⇩3 (φ{ν⇩1, ν⇩2, ν⇩3} ≡ ψ{ν⇩1, ν⇩2, ν⇩3})) →
157 [λν⇩1ν⇩2ν⇩3 ψ{ν⇩1,ν⇩2,ν⇩3}]↓›
158 using "safe-ext"[where φ="λ(x,y,z). φ x y z"]
159 by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
160 AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
161AOT_axiom "safe-ext[4]":
162 ‹([λν⇩1ν⇩2ν⇩3ν⇩4 φ{ν⇩1,ν⇩2,ν⇩3,ν⇩4}]↓ &
163 □∀ν⇩1∀ν⇩2∀ν⇩3∀ν⇩4 (φ{ν⇩1, ν⇩2, ν⇩3, ν⇩4} ≡ ψ{ν⇩1, ν⇩2, ν⇩3, ν⇩4})) →
164 [λν⇩1ν⇩2ν⇩3ν⇩4 ψ{ν⇩1,ν⇩2,ν⇩3,ν⇩4}]↓›
165 using "safe-ext"[where φ="λ(x,y,z,w). φ x y z w"]
166 by (simp add: AOT_model_axiom_def AOT_model_denotes_prod_def AOT_sem_forall
167 AOT_sem_denotes AOT_sem_imp AOT_sem_conj AOT_sem_equiv AOT_sem_box)
168
169AOT_axiom "nary-encoding[2]":
170 ‹x⇩1x⇩2[F] ≡ x⇩1[λy [F]yx⇩2] & x⇩2[λy [F]x⇩1y]›
171 by (rule AOT_model_axiomI)
172 (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
173 AOT_sem_unary_proj_enc AOT_sem_vars_denote)
174AOT_axiom "nary-encoding[3]":
175 ‹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]›
176 by (rule AOT_model_axiomI)
177 (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
178 AOT_sem_unary_proj_enc AOT_sem_vars_denote)
179AOT_axiom "nary-encoding[4]":
180 ‹x⇩1x⇩2x⇩3x⇩4[F] ≡ x⇩1[λy [F]yx⇩2x⇩3x⇩4] &
181 x⇩2[λy [F]x⇩1yx⇩3x⇩4] &
182 x⇩3[λy [F]x⇩1x⇩2yx⇩4] &
183 x⇩4[λy [F]x⇩1x⇩2x⇩3y]›
184 by (rule AOT_model_axiomI)
185 (simp add: AOT_sem_conj AOT_sem_equiv AOT_enc_prod_def AOT_proj_enc_prod_def
186 AOT_sem_unary_proj_enc AOT_sem_vars_denote)
187
188AOT_axiom encoding: ‹x[F] → □x[F]›
189 using AOT_sem_enc_nec
190 by (auto intro!: AOT_model_axiomI simp: AOT_sem_imp AOT_sem_box)
191
192AOT_axiom nocoder: ‹O!x → ¬∃F x[F]›
193 by (auto intro!: AOT_model_axiomI
194 simp: AOT_sem_imp AOT_sem_not AOT_sem_exists AOT_sem_ordinary
195 AOT_sem_dia
196 AOT_sem_lambda_beta[OF AOT_sem_ordinary_def_denotes,
197 OF AOT_sem_vars_denote])
198 (metis AOT_sem_nocoder)
199
200AOT_axiom "A-objects": ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
201proof(rule AOT_model_axiomI)
202 AOT_modally_strict {
203 AOT_obtain κ where ‹κ↓ & □¬E!κ & ∀F (κ[F] ≡ φ{F})›
204 using AOT_sem_A_objects[of _ φ]
205 by (auto simp: AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_exists
206 AOT_sem_conj AOT_sem_not AOT_sem_dia AOT_sem_denotes
207 AOT_sem_equiv) blast
208 AOT_thus ‹∃x (A!x & ∀F(x[F] ≡ φ{F}))›
209 unfolding AOT_sem_exists
210 by (auto intro!: exI[where x=κ]
211 simp: AOT_sem_lambda_beta[OF AOT_sem_abstract_def_denotes]
212 AOT_sem_box AOT_sem_dia AOT_sem_not AOT_sem_denotes
213 AOT_var_of_term_inverse AOT_sem_conj
214 AOT_sem_equiv AOT_sem_forall AOT_sem_abstract)
215 }
216qed
217
218AOT_theorem universal_closure:
219 assumes ‹for arbitrary α: φ{α} ∈ Λ⇩□›
220 shows ‹∀α φ{α} ∈ Λ⇩□›
221 using assms
222 by (metis AOT_term_of_var_cases AOT_model_axiom_def AOT_sem_denotes AOT_sem_forall)
223
224AOT_theorem act_closure:
225 assumes ‹φ ∈ Λ⇩□›
226 shows ‹❙𝒜φ ∈ Λ⇩□›
227 using assms by (simp add: AOT_model_axiom_def AOT_sem_act)
228
229AOT_theorem nec_closure:
230 assumes ‹φ ∈ Λ⇩□›
231 shows ‹□φ ∈ Λ⇩□›
232 using assms by (simp add: AOT_model_axiom_def AOT_sem_box)
233
234AOT_theorem universal_closure_act:
235 assumes ‹for arbitrary α: φ{α} ∈ Λ›
236 shows ‹∀α φ{α} ∈ Λ›
237 using assms
238 by (metis AOT_term_of_var_cases AOT_model_act_axiom_def AOT_sem_denotes
239 AOT_sem_forall)
240
241text‹The following are not part of PLM and only hold in the extended models.
242 They are a generalization of the predecessor axiom.›
243context AOT_ExtendedModel
244begin
245AOT_axiom indistinguishable_ord_enc_all:
246 ‹Π↓ & A!x & A!y & ∀F □([F]x ≡ [F]y) →
247 ((∀G(∀z(O!z → □([G]z ≡ [Π]z)) → x[G])) ≡
248 ∀G(∀z(O!z → □([G]z ≡ [Π]z)) → y[G]))›
249 by (rule AOT_model_axiomI)
250 (auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj
251 AOT_sem_indistinguishable_ord_enc_all)
252AOT_axiom indistinguishable_ord_enc_ex:
253 ‹Π↓ & A!x & A!y & ∀F □([F]x ≡ [F]y) →
254 ((∃G(∀z(O!z → □([G]z ≡ [Π]z)) & x[G])) ≡
255 ∃G(∀z(O!z → □([G]z ≡ [Π]z)) & y[G]))›
256 by (rule AOT_model_axiomI)
257 (auto simp: AOT_sem_equiv AOT_sem_imp AOT_sem_conj
258 AOT_sem_indistinguishable_ord_enc_ex)
259end
260
261
262end
263