Theory AOT_PLM
1
2theory AOT_PLM
3 imports AOT_Axioms
4begin
5
6
7section‹The Deductive System PLM›
8text‹\label{PLM: 9}›
9
10
11unbundle AOT_no_atp
12
13subsection‹Primitive Rule of PLM: Modus Ponens›
14text‹\label{PLM: 9.1}›
15
16AOT_theorem "modus-ponens":
17 assumes ‹φ› and ‹φ → ψ›
18 shows ‹ψ›
19
20 using assms by (simp add: AOT_sem_imp)
21lemmas MP = "modus-ponens"
22
23subsection‹(Modally Strict) Proofs and Derivations›
24text‹\label{PLM: 9.2}›
25
26AOT_theorem "non-con-thm-thm":
27 assumes ‹❙⊢⇩□ φ›
28 shows ‹❙⊢ φ›
29 using assms by simp
30
31AOT_theorem "vdash-properties:1[1]":
32 assumes ‹φ ∈ Λ›
33 shows ‹❙⊢ φ›
34
35 using assms unfolding AOT_model_act_axiom_def by blast
36
37text‹Convenience attribute for instantiating modally-fragile axioms.›
38attribute_setup act_axiom_inst =
39 ‹Scan.succeed (Thm.rule_attribute []
40 (K (fn thm => thm RS @{thm "vdash-properties:1[1]"})))›
41 "Instantiate modally fragile axiom as modally fragile theorem."
42
43AOT_theorem "vdash-properties:1[2]":
44 assumes ‹φ ∈ Λ⇩□›
45 shows ‹❙⊢⇩□ φ›
46
47 using assms unfolding AOT_model_axiom_def by blast
48
49text‹Convenience attribute for instantiating modally-strict axioms.›
50attribute_setup axiom_inst =
51 ‹Scan.succeed (Thm.rule_attribute []
52 (K (fn thm => thm RS @{thm "vdash-properties:1[2]"})))›
53 "Instantiate axiom as theorem."
54
55text‹Convenience methods and theorem sets for applying "cqt:2".›
56method cqt_2_lambda_inst_prover =
57 (fast intro: AOT_instance_of_cqt_2_intro)
58method "cqt:2[lambda]" =
59 (rule "cqt:2[lambda]"[axiom_inst]; cqt_2_lambda_inst_prover)
60lemmas "cqt:2" =
61 "cqt:2[const_var]"[axiom_inst] "cqt:2[lambda]"[axiom_inst]
62 AOT_instance_of_cqt_2_intro
63method "cqt:2" = (safe intro!: "cqt:2")
64
65AOT_theorem "vdash-properties:3":
66 assumes ‹❙⊢⇩□ φ›
67 shows ‹Γ ❙⊢ φ›
68 using assms by blast
69
70AOT_theorem "vdash-properties:5":
71 assumes ‹Γ⇩1 ❙⊢ φ› and ‹Γ⇩2 ❙⊢ φ → ψ›
72 shows ‹Γ⇩1, Γ⇩2 ❙⊢ ψ›
73 using MP assms by blast
74
75AOT_theorem "vdash-properties:6":
76 assumes ‹φ› and ‹φ → ψ›
77 shows ‹ψ›
78 using MP assms by blast
79
80AOT_theorem "vdash-properties:8":
81 assumes ‹Γ ❙⊢ φ› and ‹φ ❙⊢ ψ›
82 shows ‹Γ ❙⊢ ψ›
83 using assms by argo
84
85AOT_theorem "vdash-properties:9":
86 assumes ‹φ›
87 shows ‹ψ → φ›
88 using MP "pl:1"[axiom_inst] assms by blast
89
90AOT_theorem "vdash-properties:10":
91 assumes ‹φ → ψ› and ‹φ›
92 shows ‹ψ›
93 using MP assms by blast
94lemmas "→E" = "vdash-properties:10"
95
96subsection‹Two Fundamental Metarules: GEN and RN›
97text‹\label{PLM: 9.3}›
98
99AOT_theorem "rule-gen":
100 assumes ‹for arbitrary α: φ{α}›
101 shows ‹∀α φ{α}›
102
103 using assms by (metis AOT_var_of_term_inverse AOT_sem_denotes AOT_sem_forall)
104lemmas GEN = "rule-gen"
105
106AOT_theorem "RN[prem]":
107 assumes ‹Γ ❙⊢⇩□ φ›
108 shows ‹□Γ ❙⊢⇩□ □φ›
109 by (meson AOT_sem_box assms image_iff)
110AOT_theorem RN:
111 assumes ‹❙⊢⇩□ φ›
112 shows ‹□φ›
113 using "RN[prem]" assms by blast
114
115subsection‹The Inferential Role of Definitions›
116text‹\label{PLM: 9.4}›
117
118AOT_axiom "df-rules-formulas[1]":
119 assumes ‹φ ≡⇩d⇩f ψ›
120 shows ‹φ → ψ›
121
122 using assms
123 by (auto simp: assms AOT_model_axiomI AOT_model_equiv_def AOT_sem_imp)
124AOT_axiom "df-rules-formulas[2]":
125 assumes ‹φ ≡⇩d⇩f ψ›
126 shows ‹ψ → φ›
127
128 using assms
129 by (auto simp: AOT_model_axiomI AOT_model_equiv_def AOT_sem_imp)
130
131AOT_theorem "df-rules-formulas[3]":
132 assumes ‹φ ≡⇩d⇩f ψ›
133 shows ‹φ → ψ›
134 using "df-rules-formulas[1]"[axiom_inst, OF assms].
135AOT_theorem "df-rules-formulas[4]":
136 assumes ‹φ ≡⇩d⇩f ψ›
137 shows ‹ψ → φ›
138 using "df-rules-formulas[2]"[axiom_inst, OF assms].
139
140
141AOT_axiom "df-rules-terms[1]":
142 assumes ‹τ{α⇩1...α⇩n} =⇩d⇩f σ{α⇩1...α⇩n}›
143 shows ‹(σ{τ⇩1...τ⇩n}↓ → τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}) &
144 (¬σ{τ⇩1...τ⇩n}↓ → ¬τ{τ⇩1...τ⇩n}↓)›
145
146 using assms
147 by (simp add: AOT_model_axiomI AOT_sem_conj AOT_sem_imp AOT_sem_eq
148 AOT_sem_not AOT_sem_denotes AOT_model_id_def)
149AOT_axiom "df-rules-terms[2]":
150 assumes ‹τ =⇩d⇩f σ›
151 shows ‹(σ↓ → τ = σ) & (¬σ↓ → ¬τ↓)›
152 by (metis "df-rules-terms[1]" case_unit_Unity assms)
153
154AOT_theorem "df-rules-terms[3]":
155 assumes ‹τ{α⇩1...α⇩n} =⇩d⇩f σ{α⇩1...α⇩n}›
156 shows ‹(σ{τ⇩1...τ⇩n}↓ → τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}) &
157 (¬σ{τ⇩1...τ⇩n}↓ → ¬τ{τ⇩1...τ⇩n}↓)›
158 using "df-rules-terms[1]"[axiom_inst, OF assms].
159AOT_theorem "df-rules-terms[4]":
160 assumes ‹τ =⇩d⇩f σ›
161 shows ‹(σ↓ → τ = σ) & (¬σ↓ → ¬τ↓)›
162 using "df-rules-terms[2]"[axiom_inst, OF assms].
163
164subsection‹The Theory of Negations and Conditionals›
165text‹\label{PLM: 9.5}›
166
167AOT_theorem "if-p-then-p": ‹φ → φ›
168 by (meson "pl:1"[axiom_inst] "pl:2"[axiom_inst] MP)
169
170AOT_theorem "deduction-theorem":
171 assumes ‹φ ❙⊢ ψ›
172 shows ‹φ → ψ›
173
174 using assms by (simp add: AOT_sem_imp)
175lemmas CP = "deduction-theorem"
176lemmas "→I" = "deduction-theorem"
177
178AOT_theorem "ded-thm-cor:1":
179 assumes ‹Γ⇩1 ❙⊢ φ → ψ› and ‹Γ⇩2 ❙⊢ ψ → χ›
180 shows ‹Γ⇩1, Γ⇩2 ❙⊢ φ → χ›
181 using "→E" "→I" assms by blast
182AOT_theorem "ded-thm-cor:2":
183 assumes ‹Γ⇩1 ❙⊢ φ → (ψ → χ)› and ‹Γ⇩2 ❙⊢ ψ›
184 shows ‹Γ⇩1, Γ⇩2 ❙⊢ φ → χ›
185 using "→E" "→I" assms by blast
186
187AOT_theorem "ded-thm-cor:3":
188 assumes ‹φ → ψ› and ‹ψ → χ›
189 shows ‹φ → χ›
190 using "→E" "→I" assms by blast
191declare "ded-thm-cor:3"[trans]
192AOT_theorem "ded-thm-cor:4":
193 assumes ‹φ → (ψ → χ)› and ‹ψ›
194 shows ‹φ → χ›
195 using "→E" "→I" assms by blast
196
197lemmas "Hypothetical Syllogism" = "ded-thm-cor:3"
198
199AOT_theorem "useful-tautologies:1": ‹¬¬φ → φ›
200 by (metis "pl:3"[axiom_inst] "→I" "Hypothetical Syllogism")
201AOT_theorem "useful-tautologies:2": ‹φ → ¬¬φ›
202 by (metis "pl:3"[axiom_inst] "→I" "ded-thm-cor:4")
203AOT_theorem "useful-tautologies:3": ‹¬φ → (φ → ψ)›
204 by (meson "ded-thm-cor:4" "pl:3"[axiom_inst] "→I")
205AOT_theorem "useful-tautologies:4": ‹(¬ψ → ¬φ) → (φ → ψ)›
206 by (meson "pl:3"[axiom_inst] "Hypothetical Syllogism" "→I")
207AOT_theorem "useful-tautologies:5": ‹(φ → ψ) → (¬ψ → ¬φ)›
208 by (metis "useful-tautologies:4" "Hypothetical Syllogism" "→I")
209
210AOT_theorem "useful-tautologies:6": ‹(φ → ¬ψ) → (ψ → ¬φ)›
211 by (metis "→I" MP "useful-tautologies:4")
212
213AOT_theorem "useful-tautologies:7": ‹(¬φ → ψ) → (¬ψ → φ)›
214 by (metis "→I" MP "useful-tautologies:3" "useful-tautologies:5")
215
216AOT_theorem "useful-tautologies:8": ‹φ → (¬ψ → ¬(φ → ψ))›
217 by (metis "→I" MP "useful-tautologies:5")
218
219AOT_theorem "useful-tautologies:9": ‹(φ → ψ) → ((¬φ → ψ) → ψ)›
220 by (metis "→I" MP "useful-tautologies:6")
221
222AOT_theorem "useful-tautologies:10": ‹(φ → ¬ψ) → ((φ → ψ) → ¬φ)›
223 by (metis "→I" MP "pl:3"[axiom_inst])
224
225AOT_theorem "dn-i-e:1":
226 assumes ‹φ›
227 shows ‹¬¬φ›
228 using MP "useful-tautologies:2" assms by blast
229lemmas "¬¬I" = "dn-i-e:1"
230AOT_theorem "dn-i-e:2":
231 assumes ‹¬¬φ›
232 shows ‹φ›
233 using MP "useful-tautologies:1" assms by blast
234lemmas "¬¬E" = "dn-i-e:2"
235
236AOT_theorem "modus-tollens:1":
237 assumes ‹φ → ψ› and ‹¬ψ›
238 shows ‹¬φ›
239 using MP "useful-tautologies:5" assms by blast
240AOT_theorem "modus-tollens:2":
241 assumes ‹φ → ¬ψ› and ‹ψ›
242 shows ‹¬φ›
243 using "¬¬I" "modus-tollens:1" assms by blast
244lemmas MT = "modus-tollens:1" "modus-tollens:2"
245
246AOT_theorem "contraposition:1[1]":
247 assumes ‹φ → ψ›
248 shows ‹¬ψ → ¬φ›
249 using "→I" MT(1) assms by blast
250AOT_theorem "contraposition:1[2]":
251 assumes ‹¬ψ → ¬φ›
252 shows ‹φ → ψ›
253 using "→I" "¬¬E" MT(2) assms by blast
254
255AOT_theorem "contraposition:2":
256 assumes ‹φ → ¬ψ›
257 shows ‹ψ → ¬φ›
258 using "→I" MT(2) assms by blast
259
260AOT_theorem "reductio-aa:1":
261 assumes ‹¬φ ❙⊢ ¬ψ› and ‹¬φ ❙⊢ ψ›
262 shows ‹φ›
263 using "→I" "¬¬E" MT(2) assms by blast
264AOT_theorem "reductio-aa:2":
265 assumes ‹φ ❙⊢ ¬ψ› and ‹φ ❙⊢ ψ›
266 shows ‹¬φ›
267 using "reductio-aa:1" assms by blast
268lemmas "RAA" = "reductio-aa:1" "reductio-aa:2"
269
270AOT_theorem "exc-mid": ‹φ ∨ ¬φ›
271 using "df-rules-formulas[4]" "if-p-then-p" MP
272 "conventions:2" by blast
273
274AOT_theorem "non-contradiction": ‹¬(φ & ¬φ)›
275 using "df-rules-formulas[3]" MT(2) "useful-tautologies:2"
276 "conventions:1" by blast
277
278AOT_theorem "con-dis-taut:1": ‹(φ & ψ) → φ›
279 by (meson "→I" "df-rules-formulas[3]" MP RAA(1) "conventions:1")
280AOT_theorem "con-dis-taut:2": ‹(φ & ψ) → ψ›
281 by (metis "→I" "df-rules-formulas[3]" MT(2) RAA(2)
282 "¬¬E" "conventions:1")
283lemmas "Conjunction Simplification" = "con-dis-taut:1" "con-dis-taut:2"
284
285AOT_theorem "con-dis-taut:3": ‹φ → (φ ∨ ψ)›
286 by (meson "contraposition:1[2]" "df-rules-formulas[4]"
287 MP "→I" "conventions:2")
288AOT_theorem "con-dis-taut:4": ‹ψ → (φ ∨ ψ)›
289 using "Hypothetical Syllogism" "df-rules-formulas[4]"
290 "pl:1"[axiom_inst] "conventions:2" by blast
291lemmas "Disjunction Addition" = "con-dis-taut:3" "con-dis-taut:4"
292
293AOT_theorem "con-dis-taut:5": ‹φ → (ψ → (φ & ψ))›
294 by (metis "contraposition:2" "Hypothetical Syllogism" "→I"
295 "df-rules-formulas[4]" "conventions:1")
296lemmas Adjunction = "con-dis-taut:5"
297
298AOT_theorem "con-dis-taut:6": ‹(φ & φ) ≡ φ›
299 by (metis Adjunction "→I" "df-rules-formulas[4]" MP
300 "Conjunction Simplification"(1) "conventions:3")
301lemmas "Idempotence of &" = "con-dis-taut:6"
302
303AOT_theorem "con-dis-taut:7": ‹(φ ∨ φ) ≡ φ›
304proof -
305 {
306 AOT_assume ‹φ ∨ φ›
307 AOT_hence ‹¬φ → φ›
308 using "conventions:2"[THEN "df-rules-formulas[3]"] MP by blast
309 AOT_hence ‹φ› using "if-p-then-p" RAA(1) MP by blast
310 }
311 moreover {
312 AOT_assume ‹φ›
313 AOT_hence ‹φ ∨ φ› using "Disjunction Addition"(1) MP by blast
314 }
315 ultimately AOT_show ‹(φ ∨ φ) ≡ φ›
316 using "conventions:3"[THEN "df-rules-formulas[4]"] MP
317 by (metis Adjunction "→I")
318qed
319lemmas "Idempotence of ∨" = "con-dis-taut:7"
320
321
322AOT_theorem "con-dis-i-e:1":
323 assumes ‹φ› and ‹ψ›
324 shows ‹φ & ψ›
325 using Adjunction MP assms by blast
326lemmas "&I" = "con-dis-i-e:1"
327
328AOT_theorem "con-dis-i-e:2:a":
329 assumes ‹φ & ψ›
330 shows ‹φ›
331 using "Conjunction Simplification"(1) MP assms by blast
332AOT_theorem "con-dis-i-e:2:b":
333 assumes ‹φ & ψ›
334 shows ‹ψ›
335 using "Conjunction Simplification"(2) MP assms by blast
336lemmas "&E" = "con-dis-i-e:2:a" "con-dis-i-e:2:b"
337
338AOT_theorem "con-dis-i-e:3:a":
339 assumes ‹φ›
340 shows ‹φ ∨ ψ›
341 using "Disjunction Addition"(1) MP assms by blast
342AOT_theorem "con-dis-i-e:3:b":
343 assumes ‹ψ›
344 shows ‹φ ∨ ψ›
345 using "Disjunction Addition"(2) MP assms by blast
346AOT_theorem "con-dis-i-e:3:c":
347 assumes ‹φ ∨ ψ› and ‹φ → χ› and ‹ψ → Θ›
348 shows ‹χ ∨ Θ›
349 by (metis "con-dis-i-e:3:a" "Disjunction Addition"(2)
350 "df-rules-formulas[3]" MT(1) RAA(1)
351 "conventions:2" assms)
352lemmas "∨I" = "con-dis-i-e:3:a" "con-dis-i-e:3:b" "con-dis-i-e:3:c"
353
354AOT_theorem "con-dis-i-e:4:a":
355 assumes ‹φ ∨ ψ› and ‹φ → χ› and ‹ψ → χ›
356 shows ‹χ›
357 by (metis MP RAA(2) "df-rules-formulas[3]" "conventions:2" assms)
358AOT_theorem "con-dis-i-e:4:b":
359 assumes ‹φ ∨ ψ› and ‹¬φ›
360 shows ‹ψ›
361 using "con-dis-i-e:4:a" RAA(1) "→I" assms by blast
362AOT_theorem "con-dis-i-e:4:c":
363 assumes ‹φ ∨ ψ› and ‹¬ψ›
364 shows ‹φ›
365 using "con-dis-i-e:4:a" RAA(1) "→I" assms by blast
366lemmas "∨E" = "con-dis-i-e:4:a" "con-dis-i-e:4:b" "con-dis-i-e:4:c"
367
368AOT_theorem "raa-cor:1":
369 assumes ‹¬φ ❙⊢ ψ & ¬ψ›
370 shows ‹φ›
371 using "&E" "∨E"(3) "∨I"(2) RAA(2) assms by blast
372AOT_theorem "raa-cor:2":
373 assumes ‹φ ❙⊢ ψ & ¬ψ›
374 shows ‹¬φ›
375 using "raa-cor:1" assms by blast
376AOT_theorem "raa-cor:3":
377 assumes ‹φ› and ‹¬ψ ❙⊢ ¬φ›
378 shows ‹ψ›
379 using RAA assms by blast
380AOT_theorem "raa-cor:4":
381 assumes ‹¬φ› and ‹¬ψ ❙⊢ φ›
382 shows ‹ψ›
383 using RAA assms by blast
384AOT_theorem "raa-cor:5":
385 assumes ‹φ› and ‹ψ ❙⊢ ¬φ›
386 shows ‹¬ψ›
387 using RAA assms by blast
388AOT_theorem "raa-cor:6":
389 assumes ‹¬φ› and ‹ψ ❙⊢ φ›
390 shows ‹¬ψ›
391 using RAA assms by blast
392
393AOT_theorem "oth-class-taut:1:a": ‹(φ → ψ) ≡ ¬(φ & ¬ψ)›
394 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
395 (metis "&E" "&I" "raa-cor:3" "→I" MP)
396AOT_theorem "oth-class-taut:1:b": ‹¬(φ → ψ) ≡ (φ & ¬ψ)›
397 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
398 (metis "&E" "&I" "raa-cor:3" "→I" MP)
399AOT_theorem "oth-class-taut:1:c": ‹(φ → ψ) ≡ (¬φ ∨ ψ)›
400 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
401 (metis "&I" "∨I"(1, 2) "∨E"(3) "→I" MP "raa-cor:1")
402
403AOT_theorem "oth-class-taut:2:a": ‹(φ & ψ) ≡ (ψ & φ)›
404 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
405 (meson "&I" "&E" "→I")
406lemmas "Commutativity of &" = "oth-class-taut:2:a"
407AOT_theorem "oth-class-taut:2:b": ‹(φ & (ψ & χ)) ≡ ((φ & ψ) & χ)›
408 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
409 (metis "&I" "&E" "→I")
410lemmas "Associativity of &" = "oth-class-taut:2:b"
411AOT_theorem "oth-class-taut:2:c": ‹(φ ∨ ψ) ≡ (ψ ∨ φ)›
412 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
413 (metis "&I" "∨I"(1, 2) "∨E"(1) "→I")
414lemmas "Commutativity of ∨" = "oth-class-taut:2:c"
415AOT_theorem "oth-class-taut:2:d": ‹(φ ∨ (ψ ∨ χ)) ≡ ((φ ∨ ψ) ∨ χ)›
416 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
417 (metis "&I" "∨I"(1, 2) "∨E"(1) "→I")
418lemmas "Associativity of ∨" = "oth-class-taut:2:d"
419AOT_theorem "oth-class-taut:2:e": ‹(φ ≡ ψ) ≡ (ψ ≡ φ)›
420 by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]; rule "&I";
421 metis "&I" "df-rules-formulas[4]" "conventions:3" "&E"
422 "Hypothetical Syllogism" "→I" "df-rules-formulas[3]")
423lemmas "Commutativity of ≡" = "oth-class-taut:2:e"
424AOT_theorem "oth-class-taut:2:f": ‹(φ ≡ (ψ ≡ χ)) ≡ ((φ ≡ ψ) ≡ χ)›
425 using "conventions:3"[THEN "df-rules-formulas[4]"]
426 "conventions:3"[THEN "df-rules-formulas[3]"]
427 "→I" "→E" "&E" "&I"
428 by metis
429lemmas "Associativity of ≡" = "oth-class-taut:2:f"
430
431AOT_theorem "oth-class-taut:3:a": ‹φ ≡ φ›
432 using "&I" "vdash-properties:6" "if-p-then-p"
433 "df-rules-formulas[4]" "conventions:3" by blast
434AOT_theorem "oth-class-taut:3:b": ‹φ ≡ ¬¬φ›
435 using "&I" "useful-tautologies:1" "useful-tautologies:2" "→E"
436 "df-rules-formulas[4]" "conventions:3" by blast
437AOT_theorem "oth-class-taut:3:c": ‹¬(φ ≡ ¬φ)›
438 by (metis "&E" "→E" RAA "df-rules-formulas[3]" "conventions:3")
439
440AOT_theorem "oth-class-taut:4:a": ‹(φ → ψ) → ((ψ → χ) → (φ → χ))›
441 by (metis "→E" "→I")
442AOT_theorem "oth-class-taut:4:b": ‹(φ ≡ ψ) ≡ (¬φ ≡ ¬ψ)›
443 using "conventions:3"[THEN "df-rules-formulas[4]"]
444 "conventions:3"[THEN "df-rules-formulas[3]"]
445 "→I" "→E" "&E" "&I" RAA by metis
446AOT_theorem "oth-class-taut:4:c": ‹(φ ≡ ψ) → ((φ → χ) ≡ (ψ → χ))›
447 using "conventions:3"[THEN "df-rules-formulas[4]"]
448 "conventions:3"[THEN "df-rules-formulas[3]"]
449 "→I" "→E" "&E" "&I" by metis
450AOT_theorem "oth-class-taut:4:d": ‹(φ ≡ ψ) → ((χ → φ) ≡ (χ → ψ))›
451 using "conventions:3"[THEN "df-rules-formulas[4]"]
452 "conventions:3"[THEN "df-rules-formulas[3]"]
453 "→I" "→E" "&E" "&I" by metis
454AOT_theorem "oth-class-taut:4:e": ‹(φ ≡ ψ) → ((φ & χ) ≡ (ψ & χ))›
455 using "conventions:3"[THEN "df-rules-formulas[4]"]
456 "conventions:3"[THEN "df-rules-formulas[3]"]
457 "→I" "→E" "&E" "&I" by metis
458AOT_theorem "oth-class-taut:4:f": ‹(φ ≡ ψ) → ((χ & φ) ≡ (χ & ψ))›
459 using "conventions:3"[THEN "df-rules-formulas[4]"]
460 "conventions:3"[THEN "df-rules-formulas[3]"]
461 "→I" "→E" "&E" "&I" by metis
462AOT_theorem "oth-class-taut:4:g": ‹(φ ≡ ψ) ≡ ((φ & ψ) ∨ (¬φ & ¬ψ))›
463proof(safe intro!: "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]
464 "&I" "→I"
465 dest!: "conventions:3"[THEN "df-rules-formulas[3]", THEN "→E"])
466 AOT_show ‹φ & ψ ∨ (¬φ & ¬ψ)› if ‹(φ → ψ) & (ψ → φ)›
467 using "&E" "∨I" "→E" "&I" "raa-cor:1" "→I" "∨E" that by metis
468next
469 AOT_show ‹ψ› if ‹φ & ψ ∨ (¬φ & ¬ψ)› and ‹φ›
470 using that "∨E" "&E" "raa-cor:3" by blast
471next
472 AOT_show ‹φ› if ‹φ & ψ ∨ (¬φ & ¬ψ)› and ‹ψ›
473 using that "∨E" "&E" "raa-cor:3" by blast
474qed
475AOT_theorem "oth-class-taut:4:h": ‹¬(φ ≡ ψ) ≡ ((φ & ¬ψ) ∨ (¬φ & ψ))›
476proof (safe intro!: "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]
477 "&I" "→I")
478 AOT_show ‹φ & ¬ψ ∨ (¬φ & ψ)› if ‹¬(φ ≡ ψ)›
479 by (metis that "&I" "∨I"(1, 2) "→I" MT(1) "df-rules-formulas[4]"
480 "raa-cor:3" "conventions:3")
481next
482 AOT_show ‹¬(φ ≡ ψ)› if ‹φ & ¬ψ ∨ (¬φ & ψ)›
483 by (metis that "&E" "∨E"(2) "→E" "df-rules-formulas[3]"
484 "raa-cor:3" "conventions:3")
485qed
486AOT_theorem "oth-class-taut:5:a": ‹(φ & ψ) ≡ ¬(¬φ ∨ ¬ψ)›
487 using "conventions:3"[THEN "df-rules-formulas[4]"]
488 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
489AOT_theorem "oth-class-taut:5:b": ‹(φ ∨ ψ) ≡ ¬(¬φ & ¬ψ)›
490 using "conventions:3"[THEN "df-rules-formulas[4]"]
491 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
492AOT_theorem "oth-class-taut:5:c": ‹¬(φ & ψ) ≡ (¬φ ∨ ¬ψ)›
493 using "conventions:3"[THEN "df-rules-formulas[4]"]
494 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
495AOT_theorem "oth-class-taut:5:d": ‹¬(φ ∨ ψ) ≡ (¬φ & ¬ψ)›
496 using "conventions:3"[THEN "df-rules-formulas[4]"]
497 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
498
499lemmas DeMorgan = "oth-class-taut:5:c" "oth-class-taut:5:d"
500
501AOT_theorem "oth-class-taut:6:a":
502 ‹(φ & (ψ ∨ χ)) ≡ ((φ & ψ) ∨ (φ & χ))›
503 using "conventions:3"[THEN "df-rules-formulas[4]"]
504 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
505AOT_theorem "oth-class-taut:6:b":
506 ‹(φ ∨ (ψ & χ)) ≡ ((φ ∨ ψ) & (φ ∨ χ))›
507 using "conventions:3"[THEN "df-rules-formulas[4]"]
508 "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
509
510AOT_theorem "oth-class-taut:7:a": ‹((φ & ψ) → χ) → (φ → (ψ → χ))›
511 by (metis "&I" "→E" "→I")
512lemmas Exportation = "oth-class-taut:7:a"
513AOT_theorem "oth-class-taut:7:b": ‹(φ → (ψ →χ)) → ((φ & ψ) → χ)›
514 by (metis "&E" "→E" "→I")
515lemmas Importation = "oth-class-taut:7:b"
516
517AOT_theorem "oth-class-taut:8:a":
518 ‹(φ → (ψ → χ)) ≡ (ψ → (φ → χ))›
519 using "conventions:3"[THEN "df-rules-formulas[4]"] "→I" "→E" "&E" "&I"
520 by metis
521lemmas Permutation = "oth-class-taut:8:a"
522AOT_theorem "oth-class-taut:8:b":
523 ‹(φ → ψ) → ((φ → χ) → (φ → (ψ & χ)))›
524 by (metis "&I" "→E" "→I")
525lemmas Composition = "oth-class-taut:8:b"
526AOT_theorem "oth-class-taut:8:c":
527 ‹(φ → χ) → ((ψ → χ) → ((φ ∨ ψ) → χ))›
528 by (metis "∨E"(2) "→E" "→I" RAA(1))
529AOT_theorem "oth-class-taut:8:d":
530 ‹((φ → ψ) & (χ → Θ)) → ((φ & χ) → (ψ & Θ))›
531 by (metis "&E" "&I" "→E" "→I")
532lemmas "Double Composition" = "oth-class-taut:8:d"
533AOT_theorem "oth-class-taut:8:e":
534 ‹((φ & ψ) ≡ (φ & χ)) ≡ (φ → (ψ ≡ χ))›
535 by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
536 "conventions:3"[THEN "df-rules-formulas[3]"]
537 "→I" "→E" "&E" "&I")
538AOT_theorem "oth-class-taut:8:f":
539 ‹((φ & ψ) ≡ (χ & ψ)) ≡ (ψ → (φ ≡ χ))›
540 by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
541 "conventions:3"[THEN "df-rules-formulas[3]"]
542 "→I" "→E" "&E" "&I")
543AOT_theorem "oth-class-taut:8:g":
544 ‹(ψ ≡ χ) → ((φ ∨ ψ) ≡ (φ ∨ χ))›
545 by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
546 "conventions:3"[THEN "df-rules-formulas[3]"]
547 "→I" "→E" "&E" "&I" "∨I" "∨E"(1))
548AOT_theorem "oth-class-taut:8:h":
549 ‹(ψ ≡ χ) → ((ψ ∨ φ) ≡ (χ ∨ φ))›
550 by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
551 "conventions:3"[THEN "df-rules-formulas[3]"]
552 "→I" "→E" "&E" "&I" "∨I" "∨E"(1))
553AOT_theorem "oth-class-taut:8:i":
554 ‹(φ ≡ (ψ & χ)) → (ψ → (φ ≡ χ))›
555 by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
556 "conventions:3"[THEN "df-rules-formulas[3]"]
557 "→I" "→E" "&E" "&I")
558
559AOT_theorem "intro-elim:1":
560 assumes ‹φ ∨ ψ› and ‹φ ≡ χ› and ‹ψ ≡ Θ›
561 shows ‹χ ∨ Θ›
562 by (metis assms "∨I"(1, 2) "∨E"(1) "→I" "→E" "&E"(1)
563 "conventions:3"[THEN "df-rules-formulas[3]"])
564
565AOT_theorem "intro-elim:2":
566 assumes ‹φ → ψ› and ‹ψ → φ›
567 shows ‹φ ≡ ψ›
568 by (meson "&I" "conventions:3" "df-rules-formulas[4]" MP assms)
569lemmas "≡I" = "intro-elim:2"
570
571AOT_theorem "intro-elim:3:a":
572 assumes ‹φ ≡ ψ› and ‹φ›
573 shows ‹ψ›
574 by (metis "∨I"(1) "→I" "∨E"(1) "intro-elim:1" assms)
575AOT_theorem "intro-elim:3:b":
576 assumes ‹φ ≡ ψ› and ‹ψ›
577 shows ‹φ›
578 using "intro-elim:3:a" "Commutativity of ≡" assms by blast
579AOT_theorem "intro-elim:3:c":
580 assumes ‹φ ≡ ψ› and ‹¬φ›
581 shows ‹¬ψ›
582 using "intro-elim:3:b" "raa-cor:3" assms by blast
583AOT_theorem "intro-elim:3:d":
584 assumes ‹φ ≡ ψ› and ‹¬ψ›
585 shows ‹¬φ›
586 using "intro-elim:3:a" "raa-cor:3" assms by blast
587AOT_theorem "intro-elim:3:e":
588 assumes ‹φ ≡ ψ› and ‹ψ ≡ χ›
589 shows ‹φ ≡ χ›
590 by (metis "≡I" "→I" "intro-elim:3:a" "intro-elim:3:b" assms)
591declare "intro-elim:3:e"[trans]
592AOT_theorem "intro-elim:3:f":
593 assumes ‹φ ≡ ψ› and ‹φ ≡ χ›
594 shows ‹χ ≡ ψ›
595 by (metis "≡I" "→I" "intro-elim:3:a" "intro-elim:3:b" assms)
596lemmas "≡E" = "intro-elim:3:a" "intro-elim:3:b" "intro-elim:3:c"
597 "intro-elim:3:d" "intro-elim:3:e" "intro-elim:3:f"
598
599declare "Commutativity of ≡"[THEN "≡E"(1), sym]
600
601AOT_theorem "rule-eq-df:1":
602 assumes ‹φ ≡⇩d⇩f ψ›
603 shows ‹φ ≡ ψ›
604 by (simp add: "≡I" "df-rules-formulas[3]" "df-rules-formulas[4]" assms)
605lemmas "≡Df" = "rule-eq-df:1"
606AOT_theorem "rule-eq-df:2":
607 assumes ‹φ ≡⇩d⇩f ψ› and ‹φ›
608 shows ‹ψ›
609 using "≡Df" "≡E"(1) assms by blast
610lemmas "≡⇩d⇩fE" = "rule-eq-df:2"
611AOT_theorem "rule-eq-df:3":
612 assumes ‹φ ≡⇩d⇩f ψ› and ‹ψ›
613 shows ‹φ›
614 using "≡Df" "≡E"(2) assms by blast
615lemmas "≡⇩d⇩fI" = "rule-eq-df:3"
616
617AOT_theorem "df-simplify:1":
618 assumes ‹φ ≡ (ψ & χ)› and ‹ψ›
619 shows ‹φ ≡ χ›
620 by (metis "&E"(2) "&I" "≡E"(1, 2) "≡I" "→I" assms)
621
622AOT_theorem "df-simplify:2":
623 assumes ‹φ ≡ (ψ & χ)› and ‹χ›
624 shows ‹φ ≡ ψ›
625 by (metis "&E"(1) "&I" "≡E"(1, 2) "≡I" "→I" assms)
626lemmas "≡S" = "df-simplify:1" "df-simplify:2"
627
628subsection‹The Theory of Quantification›
629text‹\label{PLM: 9.6}›
630
631AOT_theorem "rule-ui:1":
632 assumes ‹∀α φ{α}› and ‹τ↓›
633 shows ‹φ{τ}›
634 using "→E" "cqt:1"[axiom_inst] assms by blast
635AOT_theorem "rule-ui:2[const_var]":
636 assumes ‹∀α φ{α}›
637 shows ‹φ{β}›
638 by (simp add: "rule-ui:1" "cqt:2[const_var]"[axiom_inst] assms)
639AOT_theorem "rule-ui:2[lambda]":
640 assumes ‹∀F φ{F}› and ‹INSTANCE_OF_CQT_2(ψ)›
641 shows ‹φ{[λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]}›
642 by (simp add: "rule-ui:1" "cqt:2[lambda]"[axiom_inst] assms)
643AOT_theorem "rule-ui:3":
644 assumes ‹∀α φ{α}›
645 shows ‹φ{α}›
646 by (simp add: "rule-ui:2[const_var]" assms)
647lemmas "∀E" = "rule-ui:1" "rule-ui:2[const_var]"
648 "rule-ui:2[lambda]" "rule-ui:3"
649
650AOT_theorem "cqt-orig:1[const_var]": ‹∀α φ{α} → φ{β}›
651 by (simp add: "∀E"(2) "→I")
652AOT_theorem "cqt-orig:1[lambda]":
653 assumes ‹INSTANCE_OF_CQT_2(ψ)›
654 shows ‹∀F φ{F} → φ{[λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]}›
655 by (simp add: "∀E"(3) "→I" assms)
656AOT_theorem "cqt-orig:2": ‹∀α (φ → ψ{α}) → (φ → ∀α ψ{α})›
657 by (metis "→I" GEN "vdash-properties:6" "∀E"(4))
658AOT_theorem "cqt-orig:3": ‹∀α φ{α} → φ{α}›
659 using "cqt-orig:1[const_var]".
660
661AOT_theorem universal:
662 assumes ‹for arbitrary β: φ{β}›
663 shows ‹∀α φ{α}›
664 using GEN assms .
665lemmas "∀I" = universal
666
667
668ML‹
669fun get_instantiated_allI ctxt varname thm = let
670val trm = Thm.concl_of thm
671val trm =
672 case trm of (@{const Trueprop} $ (@{const AOT_model_valid_in} $ _ $ x)) => x
673 | _ => raise Term.TERM ("Expected simple theorem.", [trm])
674fun extractVars (Const (\<^const_name>‹AOT_term_of_var›, _) $ Var v) =
675 (if fst (fst v) = fst varname then [Var v] else [])
676 | extractVars (t1 $ t2) = extractVars t1 @ extractVars t2
677 | extractVars (Abs (_, _, t)) = extractVars t
678 | extractVars _ = []
679val vars = extractVars trm
680val vars = fold Term.add_vars vars []
681val var = hd vars
682val trmty =
683 case (snd var) of (Type (\<^type_name>‹AOT_var›, [t])) => (t)
684 | _ => raise Term.TYPE ("Expected variable type.", [snd var], [Var var])
685val trm = Abs (Term.string_of_vname (fst var), trmty, Term.abstract_over (
686 Const (\<^const_name>‹AOT_term_of_var›, Type ("fun", [snd var, trmty]))
687 $ Var var, trm))
688val trm = Thm.cterm_of (Context.proof_of ctxt) trm
689val ty = hd (Term.add_tvars (Thm.prop_of @{thm "∀I"}) [])
690val typ = Thm.ctyp_of (Context.proof_of ctxt) trmty
691val allthm = Drule.instantiate_normalize (TVars.make [(ty, typ)], Vars.empty) @{thm "∀I"}
692val phi = hd (Term.add_vars (Thm.prop_of allthm) [])
693val allthm = Drule.instantiate_normalize (TVars.empty, Vars.make [(phi,trm)]) allthm
694in
695allthm
696end
697›
698
699attribute_setup "∀I" =
700 ‹Scan.lift (Scan.repeat1 Args.var) >> (fn args => Thm.rule_attribute []
701 (fn ctxt => fn thm => fold (fn arg => fn thm =>
702 thm RS get_instantiated_allI ctxt arg thm) args thm))›
703 "Quantify over a variable in a theorem using GEN."
704
705attribute_setup "unvarify" =
706 ‹Scan.lift (Scan.repeat1 Args.var) >> (fn args => Thm.rule_attribute []
707 (fn ctxt => fn thm =>
708 let
709 fun get_inst_allI arg thm = thm RS get_instantiated_allI ctxt arg thm
710 val thm = fold get_inst_allI args thm
711 val thm = fold (K (fn thm => thm RS @{thm "∀E"(1)})) args thm
712 in
713 thm
714 end))›
715 "Generalize a statement about variables to a statement about denoting terms."
716
717
718
719AOT_theorem "cqt-basic:1": ‹∀α∀β φ{α,β} ≡ ∀β∀α φ{α,β}›
720 by (metis "≡I" "∀E"(2) "∀I" "→I")
721
722AOT_theorem "cqt-basic:2":
723 ‹∀α(φ{α} ≡ ψ{α}) ≡ (∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α}))›
724proof (rule "≡I"; rule "→I")
725 AOT_assume ‹∀α(φ{α} ≡ ψ{α})›
726 AOT_hence ‹φ{α} ≡ ψ{α}› for α using "∀E"(2) by blast
727 AOT_hence ‹φ{α} → ψ{α}› and ‹ψ{α} → φ{α}› for α
728 using "≡E"(1,2) "→I" by blast+
729 AOT_thus ‹∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α})›
730 by (auto intro: "&I" "∀I")
731next
732 AOT_assume ‹∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α})›
733 AOT_hence ‹φ{α} → ψ{α}› and ‹ψ{α} → φ{α}› for α
734 using "∀E"(2) "&E" by blast+
735 AOT_hence ‹φ{α} ≡ ψ{α}› for α
736 using "≡I" by blast
737 AOT_thus ‹∀α(φ{α} ≡ ψ{α})› by (auto intro: "∀I")
738qed
739
740AOT_theorem "cqt-basic:3": ‹∀α(φ{α} ≡ ψ{α}) → (∀α φ{α} ≡ ∀α ψ{α})›
741proof(rule "→I")
742 AOT_assume ‹∀α(φ{α} ≡ ψ{α})›
743 AOT_hence 1: ‹φ{α} ≡ ψ{α}› for α using "∀E"(2) by blast
744 {
745 AOT_assume ‹∀α φ{α}›
746 AOT_hence ‹∀α ψ{α}› using 1 "∀I" "∀E"(4) "≡E" by metis
747 }
748 moreover {
749 AOT_assume ‹∀α ψ{α}›
750 AOT_hence ‹∀α φ{α}› using 1 "∀I" "∀E"(4) "≡E" by metis
751 }
752 ultimately AOT_show ‹∀α φ{α} ≡ ∀α ψ{α}›
753 using "≡I" "→I" by auto
754qed
755
756AOT_theorem "cqt-basic:4": ‹∀α(φ{α} & ψ{α}) → (∀α φ{α} & ∀α ψ{α})›
757proof(rule "→I")
758 AOT_assume 0: ‹∀α(φ{α} & ψ{α})›
759 AOT_have ‹φ{α}› and ‹ψ{α}› for α using "∀E"(2) 0 "&E" by blast+
760 AOT_thus ‹∀α φ{α} & ∀α ψ{α}›
761 by (auto intro: "∀I" "&I")
762qed
763
764AOT_theorem "cqt-basic:5": ‹(∀α⇩1...∀α⇩n(φ{α⇩1...α⇩n})) → φ{α⇩1...α⇩n}›
765 using "cqt-orig:3" by blast
766
767AOT_theorem "cqt-basic:6": ‹∀α∀α φ{α} ≡ ∀α φ{α}›
768 by (meson "≡I" "→I" GEN "cqt-orig:1[const_var]")
769
770AOT_theorem "cqt-basic:7": ‹(φ → ∀α ψ{α}) ≡ ∀α(φ → ψ{α})›
771 by (metis "→I" "vdash-properties:6" "rule-ui:3" "≡I" GEN)
772
773AOT_theorem "cqt-basic:8": ‹(∀α φ{α} ∨ ∀α ψ{α}) → ∀α (φ{α} ∨ ψ{α})›
774 by (simp add: "∨I"(3) "→I" GEN "cqt-orig:1[const_var]")
775
776AOT_theorem "cqt-basic:9":
777 ‹(∀α (φ{α} → ψ{α}) & ∀α (ψ{α} → χ{α})) → ∀α(φ{α} → χ{α})›
778proof -
779 {
780 AOT_assume ‹∀α (φ{α} → ψ{α})›
781 moreover AOT_assume ‹∀α (ψ{α} → χ{α})›
782 ultimately AOT_have ‹φ{α} → ψ{α}› and ‹ψ{α} → χ{α}› for α
783 using "∀E" by blast+
784 AOT_hence ‹φ{α} → χ{α}› for α by (metis "→E" "→I")
785 AOT_hence ‹∀α(φ{α} → χ{α})› using "∀I" by fast
786 }
787 thus ?thesis using "&I" "→I" "&E" by meson
788qed
789
790AOT_theorem "cqt-basic:10":
791 ‹(∀α(φ{α} ≡ ψ{α}) & ∀α(ψ{α} ≡ χ{α})) → ∀α (φ{α} ≡ χ{α})›
792proof(rule "→I"; rule "∀I")
793 fix β
794 AOT_assume ‹∀α(φ{α} ≡ ψ{α}) & ∀α(ψ{α} ≡ χ{α})›
795 AOT_hence ‹φ{β} ≡ ψ{β}› and ‹ψ{β} ≡ χ{β}› using "&E" "∀E" by blast+
796 AOT_thus ‹φ{β} ≡ χ{β}› using "≡I" "≡E" by blast
797qed
798
799AOT_theorem "cqt-basic:11": ‹∀α(φ{α} ≡ ψ{α}) ≡ ∀α (ψ{α} ≡ φ{α})›
800proof (rule "≡I"; rule "→I")
801 AOT_assume 0: ‹∀α(φ{α} ≡ ψ{α})›
802 {
803 fix α
804 AOT_have ‹φ{α} ≡ ψ{α}› using 0 "∀E" by blast
805 AOT_hence ‹ψ{α} ≡ φ{α}› using "≡I" "≡E" "→I" "→E" by metis
806 }
807 AOT_thus ‹∀α(ψ{α} ≡ φ{α})› using "∀I" by fast
808next
809 AOT_assume 0: ‹∀α(ψ{α} ≡ φ{α})›
810 {
811 fix α
812 AOT_have ‹ψ{α} ≡ φ{α}› using 0 "∀E" by blast
813 AOT_hence ‹φ{α} ≡ ψ{α}› using "≡I" "≡E" "→I" "→E" by metis
814 }
815 AOT_thus ‹∀α(φ{α} ≡ ψ{α})› using "∀I" by fast
816qed
817
818AOT_theorem "cqt-basic:12": ‹∀α φ{α} → ∀α (ψ{α} → φ{α})›
819 by (simp add: "∀E"(2) "→I" GEN)
820
821AOT_theorem "cqt-basic:13": ‹∀α φ{α} ≡ ∀β φ{β}›
822 using "≡I" "→I" by blast
823
824AOT_theorem "cqt-basic:14":
825 ‹(∀α⇩1...∀α⇩n (φ{α⇩1...α⇩n} → ψ{α⇩1...α⇩n})) →
826 ((∀α⇩1...∀α⇩n φ{α⇩1...α⇩n}) → (∀α⇩1...∀α⇩n ψ{α⇩1...α⇩n}))›
827 using "cqt:3"[axiom_inst] by auto
828
829AOT_theorem "cqt-basic:15":
830 ‹(∀α⇩1...∀α⇩n (φ → ψ{α⇩1...α⇩n})) → (φ → (∀α⇩1...∀α⇩n ψ{α⇩1...α⇩n}))›
831 using "cqt-orig:2" by auto
832
833AOT_theorem "universal-cor":
834 assumes ‹for arbitrary β: φ{β}›
835 shows ‹∀α φ{α}›
836 using GEN assms .
837
838AOT_theorem "existential:1":
839 assumes ‹φ{τ}› and ‹τ↓›
840 shows ‹∃α φ{α}›
841proof(rule "raa-cor:1")
842 AOT_assume ‹¬∃α φ{α}›
843 AOT_hence ‹∀α ¬φ{α}›
844 using "≡⇩d⇩fI" "conventions:4" RAA "&I" by blast
845 AOT_hence ‹¬φ{τ}› using assms(2) "∀E"(1) "→E" by blast
846 AOT_thus ‹φ{τ} & ¬φ{τ}› using assms(1) "&I" by blast
847qed
848
849AOT_theorem "existential:2[const_var]":
850 assumes ‹φ{β}›
851 shows ‹∃α φ{α}›
852 using "existential:1" "cqt:2[const_var]"[axiom_inst] assms by blast
853
854AOT_theorem "existential:2[lambda]":
855 assumes ‹φ{[λν⇩1...ν⇩n ψ{ν⇩1...ν⇩n}]}› and ‹INSTANCE_OF_CQT_2(ψ)›
856 shows ‹∃α φ{α}›
857 using "existential:1" "cqt:2[lambda]"[axiom_inst] assms by blast
858lemmas "∃I" = "existential:1" "existential:2[const_var]"
859 "existential:2[lambda]"
860
861AOT_theorem "instantiation":
862 assumes ‹for arbitrary β: φ{β} ❙⊢ ψ› and ‹∃α φ{α}›
863 shows ‹ψ›
864 by (metis (no_types, lifting) "≡⇩d⇩fE" GEN "raa-cor:3" "conventions:4" assms)
865lemmas "∃E" = "instantiation"
866
867AOT_theorem "cqt-further:1": ‹∀α φ{α} → ∃α φ{α}›
868 using "∀E"(4) "∃I"(2) "→I" by metis
869
870AOT_theorem "cqt-further:2": ‹¬∀α φ{α} → ∃α ¬φ{α}›
871 using "∀I" "∃I"(2) "→I" RAA by metis
872
873AOT_theorem "cqt-further:3": ‹∀α φ{α} ≡ ¬∃α ¬φ{α}›
874 using "∀E"(4) "∃E" "→I" RAA
875 by (metis "cqt-further:2" "≡I" "modus-tollens:1")
876
877AOT_theorem "cqt-further:4": ‹¬∃α φ{α} → ∀α ¬φ{α}›
878 using "∀I" "∃I"(2)"→I" RAA by metis
879
880AOT_theorem "cqt-further:5": ‹∃α (φ{α} & ψ{α}) → (∃α φ{α} & ∃α ψ{α})›
881 by (metis (no_types, lifting) "&E" "&I" "∃E" "∃I"(2) "→I")
882
883AOT_theorem "cqt-further:6": ‹∃α (φ{α} ∨ ψ{α}) → (∃α φ{α} ∨ ∃α ψ{α})›
884 by (metis (mono_tags, lifting) "∃E" "∃I"(2) "∨E"(3) "∨I"(1, 2) "→I" RAA(2))
885
886
887AOT_theorem "cqt-further:7": ‹∃α φ{α} ≡ ∃β φ{β}›
888 by (simp add: "oth-class-taut:3:a")
889
890AOT_theorem "cqt-further:8":
891 ‹(∀α φ{α} & ∀α ψ{α}) → ∀α (φ{α} ≡ ψ{α})›
892 by (metis (mono_tags, lifting) "&E" "≡I" "∀E"(2) "→I" GEN)
893
894AOT_theorem "cqt-further:9":
895 ‹(¬∃α φ{α} & ¬∃α ψ{α}) → ∀α (φ{α} ≡ ψ{α})›
896 by (metis (mono_tags, lifting) "&E" "≡I" "∃I"(2) "→I" GEN "raa-cor:4")
897
898AOT_theorem "cqt-further:10":
899 ‹(∃α φ{α} & ¬∃α ψ{α}) → ¬∀α (φ{α} ≡ ψ{α})›
900proof(rule "→I"; rule "raa-cor:2")
901 AOT_assume 0: ‹∃α φ{α} & ¬∃α ψ{α}›
902 then AOT_obtain α where ‹φ{α}› using "∃E" "&E"(1) by metis
903 moreover AOT_assume ‹∀α (φ{α} ≡ ψ{α})›
904 ultimately AOT_have ‹ψ{α}› using "∀E"(4) "≡E"(1) by blast
905 AOT_hence ‹∃α ψ{α}› using "∃I" by blast
906 AOT_thus ‹∃α ψ{α} & ¬∃α ψ{α}› using 0 "&E"(2) "&I" by blast
907qed
908
909AOT_theorem "cqt-further:11": ‹∃α∃β φ{α,β} ≡ ∃β∃α φ{α,β}›
910 using "≡I" "→I" "∃I"(2) "∃E" by metis
911
912subsection‹Logical Existence, Identity, and Truth›
913text‹\label{PLM: 9.7}›
914
915AOT_theorem "log-prop-prop:1": ‹[λ φ]↓›
916 using "cqt:2[lambda0]"[axiom_inst] by auto
917
918AOT_theorem "log-prop-prop:2": ‹φ↓›
919 by (rule "≡⇩d⇩fI"[OF "existence:3"]) "cqt:2[lambda]"
920
921AOT_theorem "exist-nec": ‹τ↓ → □τ↓›
922proof -
923 AOT_have ‹∀β □β↓›
924 by (simp add: GEN RN "cqt:2[const_var]"[axiom_inst])
925 AOT_thus ‹τ↓ → □τ↓›
926 using "cqt:1"[axiom_inst] "→E" by blast
927qed
928
929
930class AOT_Term_id = AOT_Term +
931 assumes "t=t-proper:1"[AOT]: ‹[v ⊨ τ = τ' → τ↓]›
932 and "t=t-proper:2"[AOT]: ‹[v ⊨ τ = τ' → τ'↓]›
933
934instance κ :: AOT_Term_id
935proof
936 AOT_modally_strict {
937 AOT_show ‹κ = κ' → κ↓› for κ κ'
938 proof(rule "→I")
939 AOT_assume ‹κ = κ'›
940 AOT_hence ‹O!κ ∨ A!κ›
941 by (rule "∨I"(3)[OF "≡⇩d⇩fE"[OF "identity:1"]])
942 (meson "→I" "∨I"(1) "&E"(1))+
943 AOT_thus ‹κ↓›
944 by (rule "∨E"(1))
945 (metis "cqt:5:a"[axiom_inst] "→I" "→E" "&E"(2))+
946 qed
947 }
948next
949 AOT_modally_strict {
950 AOT_show ‹κ = κ' → κ'↓› for κ κ'
951 proof(rule "→I")
952 AOT_assume ‹κ = κ'›
953 AOT_hence ‹O!κ' ∨ A!κ'›
954 by (rule "∨I"(3)[OF "≡⇩d⇩fE"[OF "identity:1"]])
955 (meson "→I" "∨I" "&E")+
956 AOT_thus ‹κ'↓›
957 by (rule "∨E"(1))
958 (metis "cqt:5:a"[axiom_inst] "→I" "→E" "&E"(2))+
959 qed
960 }
961qed
962
963instance rel :: (AOT_κs) AOT_Term_id
964proof
965 AOT_modally_strict {
966 AOT_show ‹Π = Π' → Π↓› for Π Π' :: ‹<'a>›
967 proof(rule "→I")
968 AOT_assume ‹Π = Π'›
969 AOT_thus ‹Π↓› using "≡⇩d⇩fE"[OF "identity:3"[of Π Π']] "&E" by blast
970 qed
971 }
972next
973 AOT_modally_strict {
974 AOT_show ‹Π = Π' → Π'↓› for Π Π' :: ‹<'a>›
975 proof(rule "→I")
976 AOT_assume ‹Π = Π'›
977 AOT_thus ‹Π'↓› using "≡⇩d⇩fE"[OF "identity:3"[of Π Π']] "&E" by blast
978 qed
979 }
980qed
981
982instance 𝗈 :: AOT_Term_id
983proof
984 AOT_modally_strict {
985 fix φ ψ
986 AOT_show ‹φ = ψ → φ↓›
987 proof(rule "→I")
988 AOT_assume ‹φ = ψ›
989 AOT_thus ‹φ↓› using "≡⇩d⇩fE"[OF "identity:4"[of φ ψ]] "&E" by blast
990 qed
991 }
992next
993 AOT_modally_strict {
994 fix φ ψ
995 AOT_show ‹φ = ψ → ψ↓›
996 proof(rule "→I")
997 AOT_assume ‹φ = ψ›
998 AOT_thus ‹ψ↓› using "≡⇩d⇩fE"[OF "identity:4"[of φ ψ]] "&E" by blast
999 qed
1000 }
1001qed
1002
1003instance prod :: (AOT_Term_id, AOT_Term_id) AOT_Term_id
1004proof
1005 AOT_modally_strict {
1006 fix τ τ' :: ‹'a×'b›
1007 AOT_show ‹τ = τ' → τ↓›
1008 proof (induct τ; induct τ'; rule "→I")
1009 fix τ⇩1 τ⇩1' :: 'a and τ⇩2 τ⇩2' :: 'b
1010 AOT_assume ‹«(τ⇩1, τ⇩2)» = «(τ⇩1', τ⇩2')»›
1011 AOT_hence ‹(τ⇩1 = τ⇩1') & (τ⇩2 = τ⇩2')› by (metis "≡⇩d⇩fE" tuple_identity_1)
1012 AOT_hence ‹τ⇩1↓› and ‹τ⇩2↓›
1013 using "t=t-proper:1" "&E" "vdash-properties:10" by blast+
1014 AOT_thus ‹«(τ⇩1, τ⇩2)»↓› by (metis "≡⇩d⇩fI" "&I" tuple_denotes)
1015 qed
1016 }
1017next
1018 AOT_modally_strict {
1019 fix τ τ' :: ‹'a×'b›
1020 AOT_show ‹τ = τ' → τ'↓›
1021 proof (induct τ; induct τ'; rule "→I")
1022 fix τ⇩1 τ⇩1' :: 'a and τ⇩2 τ⇩2' :: 'b
1023 AOT_assume ‹«(τ⇩1, τ⇩2)» = «(τ⇩1', τ⇩2')»›
1024 AOT_hence ‹(τ⇩1 = τ⇩1') & (τ⇩2 = τ⇩2')› by (metis "≡⇩d⇩fE" tuple_identity_1)
1025 AOT_hence ‹τ⇩1'↓› and ‹τ⇩2'↓›
1026 using "t=t-proper:2" "&E" "vdash-properties:10" by blast+
1027 AOT_thus ‹«(τ⇩1', τ⇩2')»↓› by (metis "≡⇩d⇩fI" "&I" tuple_denotes)
1028 qed
1029 }
1030qed
1031
1032
1034AOT_register_type_constraints
1035 Term: ‹_::AOT_Term_id› ‹_::AOT_Term_id›
1036AOT_register_type_constraints
1037 Individual: ‹κ› ‹_::{AOT_κs, AOT_Term_id}›
1038AOT_register_type_constraints
1039 Relation: ‹<_::{AOT_κs, AOT_Term_id}>›
1040
1041AOT_theorem "id-rel-nec-equiv:1":
1042 ‹Π = Π' → □∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π']x⇩1...x⇩n)›
1043proof(rule "→I")
1044 AOT_assume assumption: ‹Π = Π'›
1045 AOT_hence ‹Π↓› and ‹Π'↓›
1046 using "t=t-proper:1" "t=t-proper:2" MP by blast+
1047 moreover AOT_have ‹∀F∀G (F = G → ((□∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n ≡ [F]x⇩1...x⇩n)) →
1048 □∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n ≡ [G]x⇩1...x⇩n)))›
1049 apply (rule GEN)+ using "l-identity"[axiom_inst] by force
1050 ultimately AOT_have ‹Π = Π' → ((□∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π]x⇩1...x⇩n)) →
1051 □∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π']x⇩1...x⇩n))›
1052 using "∀E"(1) by blast
1053 AOT_hence ‹(□∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π]x⇩1...x⇩n)) →
1054 □∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π']x⇩1...x⇩n)›
1055 using assumption "→E" by blast
1056 moreover AOT_have ‹□∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π]x⇩1...x⇩n)›
1057 by (simp add: RN "oth-class-taut:3:a" "universal-cor")
1058 ultimately AOT_show ‹□∀x⇩1...∀x⇩n ([Π]x⇩1...x⇩n ≡ [Π']x⇩1...x⇩n)›
1059 using "→E" by blast
1060qed
1061
1062AOT_theorem "id-rel-nec-equiv:2": ‹φ = ψ → □(φ ≡ ψ)›
1063proof(rule "→I")
1064 AOT_assume assumption: ‹φ = ψ›
1065 AOT_hence ‹φ↓› and ‹ψ↓›
1066 using "t=t-proper:1" "t=t-proper:2" MP by blast+
1067 moreover AOT_have ‹∀p∀q (p = q → ((□(p ≡ p) → □(p ≡ q))))›
1068 apply (rule GEN)+ using "l-identity"[axiom_inst] by force
1069 ultimately AOT_have ‹φ = ψ → (□(φ ≡ φ) → □(φ ≡ ψ))›
1070 using "∀E"(1) by blast
1071 AOT_hence ‹□(φ ≡ φ) → □(φ ≡ ψ)›
1072 using assumption "→E" by blast
1073 moreover AOT_have ‹□(φ ≡ φ)›
1074 by (simp add: RN "oth-class-taut:3:a" "universal-cor")
1075 ultimately AOT_show ‹□(φ ≡ ψ)›
1076 using "→E" by blast
1077qed
1078
1079AOT_theorem "rule=E":
1080 assumes ‹φ{τ}› and ‹τ = σ›
1081 shows ‹φ{σ}›
1082proof -
1083 AOT_have ‹τ↓› and ‹σ↓›
1084 using assms(2) "t=t-proper:1" "t=t-proper:2" "→E" by blast+
1085 moreover AOT_have ‹∀α∀β(α = β → (φ{α} → φ{β}))›
1086 apply (rule GEN)+ using "l-identity"[axiom_inst] by blast
1087 ultimately AOT_have ‹τ = σ → (φ{τ} → φ{σ})›
1088 using "∀E"(1) by blast
1089 AOT_thus ‹φ{σ}› using assms "→E" by blast
1090qed
1091
1092AOT_theorem "propositions-lemma:1": ‹[λ φ] = φ›
1093proof -
1094 AOT_have ‹φ↓› by (simp add: "log-prop-prop:2")
1095 moreover AOT_have ‹∀p [λ p] = p›
1096 using "lambda-predicates:3[zero]"[axiom_inst] "∀I" by fast
1097 ultimately AOT_show ‹[λ φ] = φ›
1098 using "∀E" by blast
1099qed
1100
1101AOT_theorem "propositions-lemma:2": ‹[λ φ] ≡ φ›
1102proof -
1103 AOT_have ‹[λ φ] ≡ [λ φ]› by (simp add: "oth-class-taut:3:a")
1104 AOT_thus ‹[λ φ] ≡ φ› using "propositions-lemma:1" "rule=E" by blast
1105qed
1106
1107text‹propositions-lemma:3 through propositions-lemma:5 hold implicitly›
1108
1109AOT_theorem "propositions-lemma:6": ‹(φ ≡ ψ) ≡ ([λ φ] ≡ [λ ψ])›
1110 by (metis "≡E"(1) "≡E"(5) "Associativity of ≡" "propositions-lemma:2")
1111
1112text‹dr-alphabetic-rules holds implicitly›
1113
1114AOT_theorem "oa-exist:1": ‹O!↓›
1115proof -
1116 AOT_have ‹[λx ◇[E!]x]↓› by "cqt:2[lambda]"
1117 AOT_hence 1: ‹O! = [λx ◇[E!]x]›
1118 using "df-rules-terms[4]"[OF "oa:1", THEN "&E"(1)] "→E" by blast
1119 AOT_show ‹O!↓› using "t=t-proper:1"[THEN "→E", OF 1] by simp
1120qed
1121
1122AOT_theorem "oa-exist:2": ‹A!↓›
1123proof -
1124 AOT_have ‹[λx ¬◇[E!]x]↓› by "cqt:2[lambda]"
1125 AOT_hence 1: ‹A! = [λx ¬◇[E!]x]›
1126 using "df-rules-terms[4]"[OF "oa:2", THEN "&E"(1)] "→E" by blast
1127 AOT_show ‹A!↓› using "t=t-proper:1"[THEN "→E", OF 1] by simp
1128qed
1129
1130AOT_theorem "oa-exist:3": ‹O!x ∨ A!x›
1131proof(rule "raa-cor:1")
1132 AOT_assume ‹¬(O!x ∨ A!x)›
1133 AOT_hence A: ‹¬O!x› and B: ‹¬A!x›
1134 using "Disjunction Addition"(1) "modus-tollens:1"
1135 "∨I"(2) "raa-cor:5" by blast+
1136 AOT_have C: ‹O! = [λx ◇[E!]x]›
1137 by (rule "df-rules-terms[4]"[OF "oa:1", THEN "&E"(1), THEN "→E"]) "cqt:2"
1138 AOT_have D: ‹A! = [λx ¬◇[E!]x]›
1139 by (rule "df-rules-terms[4]"[OF "oa:2", THEN "&E"(1), THEN "→E"]) "cqt:2"
1140 AOT_have E: ‹¬[λx ◇[E!]x]x›
1141 using A C "rule=E" by fast
1142 AOT_have F: ‹¬[λx ¬◇[E!]x]x›
1143 using B D "rule=E" by fast
1144 AOT_have G: ‹[λx ◇[E!]x]x ≡ ◇[E!]x›
1145 by (rule "lambda-predicates:2"[axiom_inst, THEN "→E"]) "cqt:2"
1146 AOT_have H: ‹[λx ¬◇[E!]x]x ≡ ¬◇[E!]x›
1147 by (rule "lambda-predicates:2"[axiom_inst, THEN "→E"]) "cqt:2"
1148 AOT_show ‹¬◇[E!]x & ¬¬◇[E!]x› using G E "≡E" H F "≡E" "&I" by metis
1149qed
1150
1151AOT_theorem "p-identity-thm2:1": ‹F = G ≡ □∀x(x[F] ≡ x[G])›
1152proof -
1153 AOT_have ‹F = G ≡ F↓ & G↓ & □∀x(x[F] ≡ x[G])›
1154 using "identity:2" "df-rules-formulas[3]" "df-rules-formulas[4]"
1155 "→E" "&E" "≡I" "→I" by blast
1156 moreover AOT_have ‹F↓› and ‹G↓›
1157 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1158 ultimately AOT_show ‹F = G ≡ □∀x(x[F] ≡ x[G])›
1159 using "≡S"(1) "&I" by blast
1160qed
1161
1162AOT_theorem "p-identity-thm2:2[2]":
1163 ‹F = G ≡ ∀y⇩1([λx [F]xy⇩1] = [λx [G]xy⇩1] & [λx [F]y⇩1x] = [λx [G]y⇩1x])›
1164proof -
1165 AOT_have ‹F = G ≡ F↓ & G↓ &
1166 ∀y⇩1([λx [F]xy⇩1] = [λx [G]xy⇩1] & [λx [F]y⇩1x] = [λx [G]y⇩1x])›
1167 using "identity:3[2]" "df-rules-formulas[3]" "df-rules-formulas[4]"
1168 "→E" "&E" "≡I" "→I" by blast
1169 moreover AOT_have ‹F↓› and ‹G↓›
1170 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1171 ultimately show ?thesis
1172 using "≡S"(1) "&I" by blast
1173qed
1174
1175AOT_theorem "p-identity-thm2:2[3]":
1176 ‹F = G ≡ ∀y⇩1∀y⇩2([λx [F]xy⇩1y⇩2] = [λx [G]xy⇩1y⇩2] &
1177 [λx [F]y⇩1xy⇩2] = [λx [G]y⇩1xy⇩2] &
1178 [λx [F]y⇩1y⇩2x] = [λx [G]y⇩1y⇩2x])›
1179proof -
1180 AOT_have ‹F = G ≡ F↓ & G↓ & ∀y⇩1∀y⇩2([λx [F]xy⇩1y⇩2] = [λx [G]xy⇩1y⇩2] &
1181 [λx [F]y⇩1xy⇩2] = [λx [G]y⇩1xy⇩2] &
1182 [λx [F]y⇩1y⇩2x] = [λx [G]y⇩1y⇩2x])›
1183 using "identity:3[3]" "df-rules-formulas[3]" "df-rules-formulas[4]"
1184 "→E" "&E" "≡I" "→I" by blast
1185 moreover AOT_have ‹F↓› and ‹G↓›
1186 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1187 ultimately show ?thesis
1188 using "≡S"(1) "&I" by blast
1189qed
1190
1191AOT_theorem "p-identity-thm2:2[4]":
1192 ‹F = G ≡ ∀y⇩1∀y⇩2∀y⇩3([λx [F]xy⇩1y⇩2y⇩3] = [λx [G]xy⇩1y⇩2y⇩3] &
1193 [λx [F]y⇩1xy⇩2y⇩3] = [λx [G]y⇩1xy⇩2y⇩3] &
1194 [λx [F]y⇩1y⇩2xy⇩3] = [λx [G]y⇩1y⇩2xy⇩3] &
1195 [λx [F]y⇩1y⇩2y⇩3x] = [λx [G]y⇩1y⇩2y⇩3x])›
1196proof -
1197 AOT_have ‹F = G ≡ F↓ & G↓ & ∀y⇩1∀y⇩2∀y⇩3([λx [F]xy⇩1y⇩2y⇩3] = [λx [G]xy⇩1y⇩2y⇩3] &
1198 [λx [F]y⇩1xy⇩2y⇩3] = [λx [G]y⇩1xy⇩2y⇩3] &
1199 [λx [F]y⇩1y⇩2xy⇩3] = [λx [G]y⇩1y⇩2xy⇩3] &
1200 [λx [F]y⇩1y⇩2y⇩3x] = [λx [G]y⇩1y⇩2y⇩3x])›
1201 using "identity:3[4]" "df-rules-formulas[3]" "df-rules-formulas[4]"
1202 "→E" "&E" "≡I" "→I" by blast
1203 moreover AOT_have ‹F↓› and ‹G↓›
1204 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1205 ultimately show ?thesis
1206 using "≡S"(1) "&I" by blast
1207qed
1208
1209AOT_theorem "p-identity-thm2:2":
1210 ‹F = G ≡ ∀x⇩1...∀x⇩n «AOT_sem_proj_id x⇩1x⇩n (λ τ . «[F]τ») (λ τ . «[G]τ»)»›
1211proof -
1212 AOT_have ‹F = G ≡ F↓ & G↓ &
1213 ∀x⇩1...∀x⇩n «AOT_sem_proj_id x⇩1x⇩n (λ τ . «[F]τ») (λ τ . «[G]τ»)»›
1214 using "identity:3" "df-rules-formulas[3]" "df-rules-formulas[4]"
1215 "→E" "&E" "≡I" "→I" by blast
1216 moreover AOT_have ‹F↓› and ‹G↓›
1217 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1218 ultimately show ?thesis
1219 using "≡S"(1) "&I" by blast
1220qed
1221
1222AOT_theorem "p-identity-thm2:3":
1223 ‹p = q ≡ [λx p] = [λx q]›
1224proof -
1225 AOT_have ‹p = q ≡ p↓ & q↓ & [λx p] = [λx q]›
1226 using "identity:4" "df-rules-formulas[3]" "df-rules-formulas[4]"
1227 "→E" "&E" "≡I" "→I" by blast
1228 moreover AOT_have ‹p↓› and ‹q↓›
1229 by (auto simp: "cqt:2[const_var]"[axiom_inst])
1230 ultimately show ?thesis
1231 using "≡S"(1) "&I" by blast
1232qed
1233
1234class AOT_Term_id_2 = AOT_Term_id + assumes "id-eq:1": ‹[v ⊨ α = α]›
1235
1236instance κ :: AOT_Term_id_2
1237proof
1238 AOT_modally_strict {
1239 fix x
1240 {
1241 AOT_assume ‹O!x›
1242 moreover AOT_have ‹□∀F([F]x ≡ [F]x)›
1243 using RN GEN "oth-class-taut:3:a" by fast
1244 ultimately AOT_have ‹O!x & O!x & □∀F([F]x ≡ [F]x)› using "&I" by simp
1245 }
1246 moreover {
1247 AOT_assume ‹A!x›
1248 moreover AOT_have ‹□∀F(x[F] ≡ x[F])›
1249 using RN GEN "oth-class-taut:3:a" by fast
1250 ultimately AOT_have ‹A!x & A!x & □∀F(x[F] ≡ x[F])› using "&I" by simp
1251 }
1252 ultimately AOT_have ‹(O!x & O!x & □∀F([F]x ≡ [F]x)) ∨
1253 (A!x & A!x & □∀F(x[F] ≡ x[F]))›
1254 using "oa-exist:3" "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:1" by blast
1255 AOT_thus ‹x = x›
1256 using "identity:1"[THEN "df-rules-formulas[4]"] "→E" by blast
1257 }
1258qed
1259
1260instance rel :: ("{AOT_κs,AOT_Term_id_2}") AOT_Term_id_2
1261proof
1262 AOT_modally_strict {
1263 fix F :: "<'a> AOT_var"
1264 AOT_have 0: ‹[λx⇩1...x⇩n [F]x⇩1...x⇩n] = F›
1265 by (simp add: "lambda-predicates:3"[axiom_inst])
1266 AOT_have ‹[λx⇩1...x⇩n [F]x⇩1...x⇩n]↓›
1267 by "cqt:2[lambda]"
1268 AOT_hence ‹[λx⇩1...x⇩n [F]x⇩1...x⇩n] = [λx⇩1...x⇩n [F]x⇩1...x⇩n]›
1269 using "lambda-predicates:1"[axiom_inst] "→E" by blast
1270 AOT_show ‹F = F› using "rule=E" 0 by force
1271 }
1272qed
1273
1274instance 𝗈 :: AOT_Term_id_2
1275proof
1276 AOT_modally_strict {
1277 fix p
1278 AOT_have 0: ‹[λ p] = p›
1279 by (simp add: "lambda-predicates:3[zero]"[axiom_inst])
1280 AOT_have ‹[λ p]↓›
1281 by (rule "cqt:2[lambda0]"[axiom_inst])
1282 AOT_hence ‹[λ p] = [λ p]›
1283 using "lambda-predicates:1[zero]"[axiom_inst] "→E" by blast
1284 AOT_show ‹p = p› using "rule=E" 0 by force
1285 }
1286qed
1287
1288instance prod :: (AOT_Term_id_2, AOT_Term_id_2) AOT_Term_id_2
1289proof
1290 AOT_modally_strict {
1291 fix α :: ‹('a×'b) AOT_var›
1292 AOT_show ‹α = α›
1293 proof (induct)
1294 AOT_show ‹τ = τ› if ‹τ↓› for τ :: ‹'a×'b›
1295 using that
1296 proof (induct τ)
1297 fix τ⇩1 :: 'a and τ⇩2 :: 'b
1298 AOT_assume ‹«(τ⇩1,τ⇩2)»↓›
1299 AOT_hence ‹τ⇩1↓› and ‹τ⇩2↓›
1300 using "≡⇩d⇩fE" "&E" tuple_denotes by blast+
1301 AOT_hence ‹τ⇩1 = τ⇩1› and ‹τ⇩2 = τ⇩2›
1302 using "id-eq:1"[unvarify α] by blast+
1303 AOT_thus ‹«(τ⇩1, τ⇩2)» = «(τ⇩1, τ⇩2)»›
1304 by (metis "≡⇩d⇩fI" "&I" tuple_identity_1)
1305 qed
1306 qed
1307 }
1308qed
1309
1310AOT_register_type_constraints
1311 Term: ‹_::AOT_Term_id_2› ‹_::AOT_Term_id_2›
1312AOT_register_type_constraints
1313 Individual: ‹κ› ‹_::{AOT_κs, AOT_Term_id_2}›
1314AOT_register_type_constraints
1315 Relation: ‹<_::{AOT_κs, AOT_Term_id_2}>›
1316
1317AOT_theorem "id-eq:2": ‹α = β → β = α›
1318 by (meson "rule=E" "deduction-theorem")
1319
1320AOT_theorem "id-eq:3": ‹α = β & β = γ → α = γ›
1321 using "rule=E" "→I" "&E" by blast
1322
1323AOT_theorem "id-eq:4": ‹α = β ≡ ∀γ (α = γ ≡ β = γ)›
1324proof (rule "≡I"; rule "→I")
1325 AOT_assume 0: ‹α = β›
1326 AOT_hence 1: ‹β = α› using "id-eq:2" "→E" by blast
1327 AOT_show ‹∀γ (α = γ ≡ β = γ)›
1328 by (rule GEN) (metis "≡I" "→I" 0 "1" "rule=E")
1329next
1330 AOT_assume ‹∀γ (α = γ ≡ β = γ)›
1331 AOT_hence ‹α = α ≡ β = α› using "∀E"(2) by blast
1332 AOT_hence ‹α = α → β = α› using "≡E"(1) "→I" by blast
1333 AOT_hence ‹β = α› using "id-eq:1" "→E" by blast
1334 AOT_thus ‹α = β› using "id-eq:2" "→E" by blast
1335qed
1336
1337AOT_theorem "rule=I:1":
1338 assumes ‹τ↓›
1339 shows ‹τ = τ›
1340proof -
1341 AOT_have ‹∀α (α = α)›
1342 by (rule GEN) (metis "id-eq:1")
1343 AOT_thus ‹τ = τ› using assms "∀E" by blast
1344qed
1345
1346AOT_theorem "rule=I:2[const_var]": "α = α"
1347 using "id-eq:1".
1348
1349AOT_theorem "rule=I:2[lambda]":
1350 assumes ‹INSTANCE_OF_CQT_2(φ)›
1351 shows "[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]"
1352proof -
1353 AOT_have ‹∀α (α = α)›
1354 by (rule GEN) (metis "id-eq:1")
1355 moreover AOT_have ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]↓›
1356 using assms by (rule "cqt:2[lambda]"[axiom_inst])
1357 ultimately AOT_show ‹[λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}] = [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}]›
1358 using assms "∀E" by blast
1359qed
1360
1361lemmas "=I" = "rule=I:1" "rule=I:2[const_var]" "rule=I:2[lambda]"
1362
1363AOT_theorem "rule-id-df:1":
1364 assumes ‹τ{α⇩1...α⇩n} =⇩d⇩f σ{α⇩1...α⇩n}› and ‹σ{τ⇩1...τ⇩n}↓›
1365 shows ‹τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}›
1366proof -
1367 AOT_have ‹σ{τ⇩1...τ⇩n}↓ → τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}›
1368 using "df-rules-terms[3]" assms(1) "&E" by blast
1369 AOT_thus ‹τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}›
1370 using assms(2) "→E" by blast
1371qed
1372
1373AOT_theorem "rule-id-df:1[zero]":
1374 assumes ‹τ =⇩d⇩f σ› and ‹σ↓›
1375 shows ‹τ = σ›
1376proof -
1377 AOT_have ‹σ↓ → τ = σ›
1378 using "df-rules-terms[4]" assms(1) "&E" by blast
1379 AOT_thus ‹τ = σ›
1380 using assms(2) "→E" by blast
1381qed
1382
1383AOT_theorem "rule-id-df:2:a":
1384 assumes ‹τ{α⇩1...α⇩n} =⇩d⇩f σ{α⇩1...α⇩n}› and ‹σ{τ⇩1...τ⇩n}↓› and ‹φ{τ{τ⇩1...τ⇩n}}›
1385 shows ‹φ{σ{τ⇩1...τ⇩n}}›
1386proof -
1387 AOT_have ‹τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}› using "rule-id-df:1" assms(1,2) by blast
1388 AOT_thus ‹φ{σ{τ⇩1...τ⇩n}}› using assms(3) "rule=E" by blast
1389qed
1390
1391AOT_theorem "rule-id-df:2:a[2]":
1392 assumes ‹τ{«(α⇩1,α⇩2)»} =⇩d⇩f σ{«(α⇩1,α⇩2)»}›
1393 and ‹σ{«(τ⇩1,τ⇩2)»}↓›
1394 and ‹φ{τ{«(τ⇩1,τ⇩2)»}}›
1395 shows ‹φ{σ{«(τ⇩1::'a::AOT_Term_id_2,τ⇩2::'b::AOT_Term_id_2)»}}›
1396proof -
1397 AOT_have ‹τ{«(τ⇩1,τ⇩2)»} = σ{«(τ⇩1,τ⇩2)»}›
1398 using "rule-id-df:1" assms(1,2) by auto
1399 AOT_thus ‹φ{σ{«(τ⇩1,τ⇩2)»}}› using assms(3) "rule=E" by blast
1400qed
1401
1402AOT_theorem "rule-id-df:2:a[zero]":
1403 assumes ‹τ =⇩d⇩f σ› and ‹σ↓› and ‹φ{τ}›
1404 shows ‹φ{σ}›
1405proof -
1406 AOT_have ‹τ = σ› using "rule-id-df:1[zero]" assms(1,2) by blast
1407 AOT_thus ‹φ{σ}› using assms(3) "rule=E" by blast
1408qed
1409
1410lemmas "=⇩d⇩fE" = "rule-id-df:2:a" "rule-id-df:2:a[zero]"
1411
1412AOT_theorem "rule-id-df:2:b":
1413 assumes ‹τ{α⇩1...α⇩n} =⇩d⇩f σ{α⇩1...α⇩n}› and ‹σ{τ⇩1...τ⇩n}↓› and ‹φ{σ{τ⇩1...τ⇩n}}›
1414 shows ‹φ{τ{τ⇩1...τ⇩n}}›
1415proof -
1416 AOT_have ‹τ{τ⇩1...τ⇩n} = σ{τ⇩1...τ⇩n}›
1417 using "rule-id-df:1" assms(1,2) by blast
1418 AOT_hence ‹σ{τ⇩1...τ⇩n} = τ{τ⇩1...τ⇩n}›
1419 using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
1420 AOT_thus ‹φ{τ{τ⇩1...τ⇩n}}› using assms(3) "rule=E" by blast
1421qed
1422
1423AOT_theorem "rule-id-df:2:b[2]":
1424 assumes ‹τ{«(α⇩1,α⇩2)»} =⇩d⇩f σ{«(α⇩1,α⇩2)»}›
1425 and ‹σ{«(τ⇩1,τ⇩2)»}↓›
1426 and ‹φ{σ{«(τ⇩1,τ⇩2)»}}›
1427 shows ‹φ{τ{«(τ⇩1::'a::AOT_Term_id_2,τ⇩2::'b::AOT_Term_id_2)»}}›
1428proof -
1429 AOT_have ‹τ{«(τ⇩1,τ⇩2)»} = σ{«(τ⇩1,τ⇩2)»}›
1430 using "=I"(1) "rule-id-df:2:a[2]" RAA(1) assms(1,2) "→I" by metis
1431 AOT_hence ‹σ{«(τ⇩1,τ⇩2)»} = τ{«(τ⇩1,τ⇩2)»}›
1432 using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
1433 AOT_thus ‹φ{τ{«(τ⇩1,τ⇩2)»}}› using assms(3) "rule=E" by blast
1434qed
1435
1436AOT_theorem "rule-id-df:2:b[zero]":
1437 assumes ‹τ =⇩d⇩f σ› and ‹σ↓› and ‹φ{σ}›
1438 shows ‹φ{τ}›
1439proof -
1440 AOT_have ‹τ = σ› using "rule-id-df:1[zero]" assms(1,2) by blast
1441 AOT_hence ‹σ = τ›
1442 using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
1443 AOT_thus ‹φ{τ}› using assms(3) "rule=E" by blast
1444qed
1445
1446lemmas "=⇩d⇩fI" = "rule-id-df:2:b" "rule-id-df:2:b[zero]"
1447
1448AOT_theorem "free-thms:1": ‹τ↓ ≡ ∃β (β = τ)›
1449 by (metis "∃E" "rule=I:1" "t=t-proper:2" "→I" "∃I"(1) "≡I" "→E")
1450
1451AOT_theorem "free-thms:2": ‹∀α φ{α} → (∃β (β = τ) → φ{τ})›
1452 by (metis "∃E" "rule=E" "cqt:2[const_var]"[axiom_inst] "→I" "∀E"(1))
1453
1454AOT_theorem "free-thms:3[const_var]": ‹∃β (β = α)›
1455 by (meson "∃I"(2) "id-eq:1")
1456
1457AOT_theorem "free-thms:3[lambda]":
1458 assumes ‹INSTANCE_OF_CQT_2(φ)›
1459 shows ‹∃β (β = [λν⇩1...ν⇩n φ{ν⇩1...ν⇩n}])›
1460 by (meson "=I"(3) assms "cqt:2[lambda]"[axiom_inst] "existential:1")
1461
1462AOT_theorem "free-thms:4[rel]":
1463 ‹([Π]κ⇩1...κ⇩n ∨ κ⇩1...κ⇩n[Π]) → ∃β (β = Π)›
1464 by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
1465 "cqt:5:b"[axiom_inst] "→I" "∃I"(1))
1466
1467AOT_theorem "free-thms:4[vars]":
1468 ‹([Π]κ⇩1...κ⇩n ∨ κ⇩1...κ⇩n[Π]) → ∃β⇩1...∃β⇩n (β⇩1...β⇩n = κ⇩1...κ⇩n)›
1469 by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
1470 "cqt:5:b"[axiom_inst] "→I" "∃I"(1))
1471
1472AOT_theorem "free-thms:4[1,rel]":
1473 ‹([Π]κ ∨ κ[Π]) → ∃β (β = Π)›
1474 by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
1475 "cqt:5:b"[axiom_inst] "→I" "∃I"(1))
1476AOT_theorem "free-thms:4[1,1]":
1477 ‹([Π]κ ∨ κ[Π]) → ∃β (β = κ)›
1478 by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
1479 "cqt:5:b"[axiom_inst] "→I" "∃I"(1))
1480
1481AOT_theorem "free-thms:4[2,rel]":
1482 ‹([Π]κ⇩1κ⇩2 ∨ κ⇩1κ⇩2[Π]) → ∃β (β = Π)›
1483 by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
1484 "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
1485AOT_theorem "free-thms:4[2,1]":
1486 ‹([Π]κ⇩1κ⇩2 ∨ κ⇩1κ⇩2[Π]) → ∃β (β = κ⇩1)›
1487 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[2]"[axiom_inst]
1488 "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
1489AOT_theorem "free-thms:4[2,2]":
1490 ‹([Π]κ⇩1κ⇩2 ∨ κ⇩1κ⇩2[Π]) → ∃β (β = κ⇩2)›
1491 by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
1492 "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
1493AOT_theorem "free-thms:4[3,rel]":
1494 ‹([Π]κ⇩1κ⇩2κ⇩3 ∨ κ⇩1κ⇩2κ⇩3[Π]) → ∃β (β = Π)›
1495 by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[3]"[axiom_inst]
1496 "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
1497AOT_theorem "free-thms:4[3,1]":
1498 ‹([Π]κ⇩1κ⇩2κ⇩3 ∨ κ⇩1κ⇩2κ⇩3[Π]) → ∃β (β = κ⇩1)›
1499 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axiom_inst]
1500 "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
1501AOT_theorem "free-thms:4[3,2]":
1502 ‹([Π]κ⇩1κ⇩2κ⇩3 ∨ κ⇩1κ⇩2κ⇩3[Π]) → ∃β (β = κ⇩2)›
1503 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axiom_inst]
1504 "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
1505AOT_theorem "free-thms:4[3,3]":
1506 ‹([Π]κ⇩1κ⇩2κ⇩3 ∨ κ⇩1κ⇩2κ⇩3[Π]) → ∃β (β = κ⇩3)›
1507 by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[3]"[axiom_inst]
1508 "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
1509AOT_theorem "free-thms:4[4,rel]":
1510 ‹([Π]κ⇩1κ⇩2κ⇩3κ⇩4 ∨ κ⇩1κ⇩2κ⇩3κ⇩4[Π]) → ∃β (β = Π)›
1511 by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[4]"[axiom_inst]
1512 "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
1513AOT_theorem "free-thms:4[4,1]":
1514 ‹([Π]κ⇩1κ⇩2κ⇩3κ⇩4 ∨ κ⇩1κ⇩2κ⇩3κ⇩4[Π]) → ∃β (β = κ⇩1)›
1515 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
1516 "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
1517AOT_theorem "free-thms:4[4,2]":
1518 ‹([Π]κ⇩1κ⇩2κ⇩3κ⇩4 ∨ κ⇩1κ⇩2κ⇩3κ⇩4[Π]) → ∃β (β = κ⇩2)›
1519 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
1520 "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
1521AOT_theorem "free-thms:4[4,3]":
1522 ‹([Π]κ⇩1κ⇩2κ⇩3κ⇩4 ∨ κ⇩1κ⇩2κ⇩3κ⇩4[Π]) → ∃β (β = κ⇩3)›
1523 by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
1524 "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))