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  x1...xn φ{x1...xn}]  (x1...xn φ{x1...xn}]x1...xn  φ{x1...xn})
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": x1...xn [F]x1...xn] = 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  x1x2[F]  x1y [F]yx2] & x2y [F]x1y]
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  x1x2x3[F]  x1y [F]yx2x3] & x2y [F]x1yx3] & x3y [F]x1x2y]
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  x1x2x3x4[F]  x1y [F]yx2x3x4] &
181                 x2y [F]x1yx3x4] &
182                 x3y [F]x1x2yx4] &
183                 x4y [F]x1x2x3y]
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(*>*)