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