11 imports FOLP |
11 imports FOLP |
12 begin |
12 begin |
13 |
13 |
14 subsubsection \<open>Some simple backward proofs\<close> |
14 subsubsection \<open>Some simple backward proofs\<close> |
15 |
15 |
16 schematic_lemma mythm: "?p : P|P --> P" |
16 schematic_goal mythm: "?p : P|P --> P" |
17 apply (rule impI) |
17 apply (rule impI) |
18 apply (rule disjE) |
18 apply (rule disjE) |
19 prefer 3 apply (assumption) |
19 prefer 3 apply (assumption) |
20 prefer 2 apply (assumption) |
20 prefer 2 apply (assumption) |
21 apply assumption |
21 apply assumption |
22 done |
22 done |
23 |
23 |
24 schematic_lemma "?p : (P & Q) | R --> (P | R)" |
24 schematic_goal "?p : (P & Q) | R --> (P | R)" |
25 apply (rule impI) |
25 apply (rule impI) |
26 apply (erule disjE) |
26 apply (erule disjE) |
27 apply (drule conjunct1) |
27 apply (drule conjunct1) |
28 apply (rule disjI1) |
28 apply (rule disjI1) |
29 apply (rule_tac [2] disjI2) |
29 apply (rule_tac [2] disjI2) |
30 apply assumption+ |
30 apply assumption+ |
31 done |
31 done |
32 |
32 |
33 (*Correct version, delaying use of "spec" until last*) |
33 (*Correct version, delaying use of "spec" until last*) |
34 schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))" |
34 schematic_goal "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))" |
35 apply (rule impI) |
35 apply (rule impI) |
36 apply (rule allI) |
36 apply (rule allI) |
37 apply (rule allI) |
37 apply (rule allI) |
38 apply (drule spec) |
38 apply (drule spec) |
39 apply (drule spec) |
39 apply (drule spec) |
41 done |
41 done |
42 |
42 |
43 |
43 |
44 subsubsection \<open>Demonstration of @{text "fast"}\<close> |
44 subsubsection \<open>Demonstration of @{text "fast"}\<close> |
45 |
45 |
46 schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x)) |
46 schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x)) |
47 --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" |
47 --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" |
48 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
48 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
49 done |
49 done |
50 |
50 |
51 |
51 |
52 schematic_lemma "?p : ALL x. P(x,f(x)) <-> |
52 schematic_goal "?p : ALL x. P(x,f(x)) <-> |
53 (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
53 (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
54 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
54 apply (tactic \<open>fast_tac @{context} FOLP_cs 1\<close>) |
55 done |
55 done |
56 |
56 |
57 |
57 |
58 subsubsection \<open>Derivation of conjunction elimination rule\<close> |
58 subsubsection \<open>Derivation of conjunction elimination rule\<close> |
59 |
59 |
60 schematic_lemma |
60 schematic_goal |
61 assumes major: "p : P&Q" |
61 assumes major: "p : P&Q" |
62 and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R" |
62 and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R" |
63 shows "?p : R" |
63 shows "?p : R" |
64 apply (rule minor) |
64 apply (rule minor) |
65 apply (rule major [THEN conjunct1]) |
65 apply (rule major [THEN conjunct1]) |
69 |
69 |
70 subsection \<open>Derived rules involving definitions\<close> |
70 subsection \<open>Derived rules involving definitions\<close> |
71 |
71 |
72 text \<open>Derivation of negation introduction\<close> |
72 text \<open>Derivation of negation introduction\<close> |
73 |
73 |
74 schematic_lemma |
74 schematic_goal |
75 assumes "!!x. x : P ==> f(x) : False" |
75 assumes "!!x. x : P ==> f(x) : False" |
76 shows "?p : ~ P" |
76 shows "?p : ~ P" |
77 apply (unfold not_def) |
77 apply (unfold not_def) |
78 apply (rule impI) |
78 apply (rule impI) |
79 apply (rule assms) |
79 apply (rule assms) |
80 apply assumption |
80 apply assumption |
81 done |
81 done |
82 |
82 |
83 schematic_lemma |
83 schematic_goal |
84 assumes major: "p : ~P" |
84 assumes major: "p : ~P" |
85 and minor: "q : P" |
85 and minor: "q : P" |
86 shows "?p : R" |
86 shows "?p : R" |
87 apply (rule FalseE) |
87 apply (rule FalseE) |
88 apply (rule mp) |
88 apply (rule mp) |
89 apply (rule major [unfolded not_def]) |
89 apply (rule major [unfolded not_def]) |
90 apply (rule minor) |
90 apply (rule minor) |
91 done |
91 done |
92 |
92 |
93 text \<open>Alternative proof of the result above\<close> |
93 text \<open>Alternative proof of the result above\<close> |
94 schematic_lemma |
94 schematic_goal |
95 assumes major: "p : ~P" |
95 assumes major: "p : ~P" |
96 and minor: "q : P" |
96 and minor: "q : P" |
97 shows "?p : R" |
97 shows "?p : R" |
98 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]]) |
98 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]]) |
99 done |
99 done |