Theory AOT_PLM

1(*<*)
2theory AOT_PLM
3  imports AOT_Axioms
4begin
5(*>*)
6
7sectionThe Deductive System PLM
8text\label{PLM: 9}
9
10(* constrain sledgehammer to the abstraction layer *)
11unbundle AOT_no_atp
12
13subsectionPrimitive Rule of PLM: Modus Ponens
14text\label{PLM: 9.1}
15
16AOT_theorem "modus-ponens":
17  assumes φ and φ  ψ
18  shows ψ
19  (* NOTE: semantics needed *)
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  (* NOTE: semantics needed *)
35  using assms unfolding AOT_model_act_axiom_def by blast
36
37textConvenience 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  (* NOTE: semantics needed *)
47  using assms unfolding AOT_model_axiom_def by blast
48
49textConvenience 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
55textConvenience 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
96subsectionTwo Fundamental Metarules: GEN and RN
97text\label{PLM: 9.3}
98
99AOT_theorem "rule-gen":
100  assumes for arbitrary α: φ{α}
101  shows α φ{α}
102  (* NOTE: semantics needed *)
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) (* NOTE: semantics needed *)
110AOT_theorem RN:
111  assumes  φ
112  shows φ
113  using "RN[prem]" assms by blast
114
115subsectionThe Inferential Role of Definitions
116text\label{PLM: 9.4}
117
118AOT_axiom "df-rules-formulas[1]":
119  assumes φ df ψ
120  shows φ  ψ
121  (* NOTE: semantics needed *)
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 φ df ψ
126  shows ψ  φ
127  (* NOTE: semantics needed *)
128  using assms
129  by (auto simp: AOT_model_axiomI AOT_model_equiv_def AOT_sem_imp)
130(* NOTE: for convenience also state the above as regular theorems *)
131AOT_theorem "df-rules-formulas[3]":
132  assumes φ df ψ
133  shows φ  ψ
134  using "df-rules-formulas[1]"[axiom_inst, OF assms].
135AOT_theorem "df-rules-formulas[4]":
136  assumes φ df ψ
137  shows ψ  φ
138  using "df-rules-formulas[2]"[axiom_inst, OF assms].
139
140
141AOT_axiom "df-rules-terms[1]":
142  assumes τ{α1...αn} =df σ{α1...αn}
143  shows (σ{τ1...τn}  τ{τ1...τn} = σ{τ1...τn}) &
144         (¬σ{τ1...τn}  ¬τ{τ1...τn})
145  (* NOTE: semantics needed *)
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 τ =df σ
151  shows (σ  τ = σ) & (¬σ  ¬τ)
152  by (metis "df-rules-terms[1]" case_unit_Unity assms)
153(* NOTE: for convenience also state the above as regular theorems *)
154AOT_theorem "df-rules-terms[3]":
155  assumes τ{α1...αn} =df σ{α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 τ =df σ
161  shows (σ  τ = σ) & (¬σ  ¬τ)
162  using "df-rules-terms[2]"[axiom_inst, OF assms].
163
164subsectionThe 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  (* NOTE: semantics needed *)
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 φ df ψ
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 φ df ψ and φ
608  shows ψ
609  using "≡Df" "≡E"(1) assms by blast
610lemmas "dfE" = "rule-eq-df:2"
611AOT_theorem "rule-eq-df:3":
612  assumes φ df ψ and ψ
613  shows φ
614  using "≡Df" "≡E"(2) assms by blast
615lemmas "dfI" = "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(* Note: this is a slight variation from PLM *)
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
628subsectionThe 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(* Generalized mechanism for ∀I followed by ∀E *)
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_nameAOT_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_nameAOT_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_nameAOT_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(* Note: rereplace-lem does not apply to the embedding *)
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 "dfI" "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) "dfE" 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(* NOTE: vacuous in the embedding *)
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
912subsectionLogical 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 "dfI"[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(* TODO: replace this mechanism by a "proof by types" command *)
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 "dfE"[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 "dfE"[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 "dfE"[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 "dfE"[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 "dfE"[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 "dfE"[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 "dfE" 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 "dfI" "&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 "dfE" 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 "dfI" "&I" tuple_denotes)
1028    qed
1029  }
1030qed
1031
1032(* This is the end of the "proof by types" and
1033   makes the results available on new theorems *)
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  Π = Π'  x1...∀xn ([Π]x1...xn  [Π']x1...xn)
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 FG (F = G  ((x1...∀xn ([F]x1...xn  [F]x1...xn)) 
1048                                     x1...∀xn ([F]x1...xn  [G]x1...xn)))
1049    apply (rule GEN)+ using "l-identity"[axiom_inst] by force
1050  ultimately AOT_have Π = Π'  ((x1...∀xn ([Π]x1...xn  [Π]x1...xn)) 
1051                                   x1...∀xn ([Π]x1...xn  [Π']x1...xn))
1052    using "∀E"(1) by blast
1053  AOT_hence (x1...∀xn ([Π]x1...xn  [Π]x1...xn)) 
1054             x1...∀xn ([Π]x1...xn  [Π']x1...xn)
1055    using assumption "→E" by blast
1056  moreover AOT_have x1...∀xn ([Π]x1...xn  [Π]x1...xn)
1057    by (simp add: RN "oth-class-taut:3:a" "universal-cor")
1058  ultimately AOT_show x1...∀xn ([Π]x1...xn  [Π']x1...xn)
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 pq (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
1107textpropositions-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
1112textdr-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  y1(x [F]xy1] = x [G]xy1] & x [F]y1x] = x [G]y1x])
1164proof -
1165  AOT_have F = G  F & G &
1166              y1(x [F]xy1] = x [G]xy1] & x [F]y1x] = x [G]y1x])
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  y1y2(x [F]xy1y2] = x [G]xy1y2] &
1177                  x [F]y1xy2] = x [G]y1xy2] &
1178                  x [F]y1y2x] = x [G]y1y2x])
1179proof -
1180  AOT_have F = G  F & G & y1y2(x [F]xy1y2] = x [G]xy1y2] &
1181                                     x [F]y1xy2] = x [G]y1xy2] &
1182                                     x [F]y1y2x] = x [G]y1y2x])
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  y1y2y3(x [F]xy1y2y3] = x [G]xy1y2y3] &
1193                     x [F]y1xy2y3] = x [G]y1xy2y3] &
1194                     x [F]y1y2xy3] = x [G]y1y2xy3] &
1195                     x [F]y1y2y3x] = x [G]y1y2y3x])
1196proof -
1197  AOT_have F = G  F & G & y1y2y3(x [F]xy1y2y3] = x [G]xy1y2y3] &
1198                                        x [F]y1xy2y3] = x [G]y1xy2y3] &
1199                                        x [F]y1y2xy3] = x [G]y1y2xy3] &
1200                                        x [F]y1y2y3x] = x [G]y1y2y3x])
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  x1...∀xn «AOT_sem_proj_id x1xn (λ τ . «[F]τ») (λ τ . «[G]τ»)»
1211proof -
1212  AOT_have F = G  F & G &
1213              x1...∀xn «AOT_sem_proj_id x1xn (λ τ . «[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: x1...xn [F]x1...xn] = F
1265      by (simp add: "lambda-predicates:3"[axiom_inst])
1266    AOT_have x1...xn [F]x1...xn]
1267      by "cqt:2[lambda]"
1268    AOT_hence x1...xn [F]x1...xn] = x1...xn [F]x1...xn]
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 "dfE" "&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 "dfI" "&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} =df σ{α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 τ =df σ 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} =df σ{α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)»} =df σ{«(α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 τ =df σ 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 "=dfE" = "rule-id-df:2:a" "rule-id-df:2:a[zero]"
1411
1412AOT_theorem "rule-id-df:2:b":
1413  assumes τ{α1...αn} =df σ{α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)»} =df σ{«(α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 τ =df σ 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 "=dfI" = "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))