13 begin |
13 begin |
14 |
14 |
15 text "This finds the functions fst and snd!" |
15 text "This finds the functions fst and snd!" |
16 |
16 |
17 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" |
17 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" |
18 apply (tactic {* pc_tac @{context} [] 1 *}) |
18 apply pc |
19 done |
19 done |
20 |
20 |
21 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" |
21 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" |
22 apply (tactic {* pc_tac @{context} [] 1 *}) |
22 apply pc |
23 back |
23 back |
24 done |
24 done |
25 |
25 |
26 text "Double negation of the Excluded Middle" |
26 text "Double negation of the Excluded Middle" |
27 schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F" |
27 schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F" |
28 apply (tactic "intr_tac @{context} []") |
28 apply intr |
29 apply (rule ProdE) |
29 apply (rule ProdE) |
30 apply assumption |
30 apply assumption |
31 apply (tactic "pc_tac @{context} [] 1") |
31 apply pc |
32 done |
32 done |
33 |
33 |
34 schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)" |
34 schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)" |
35 apply (tactic "pc_tac @{context} [] 1") |
35 apply pc |
36 done |
36 done |
37 (*The sequent version (ITT) could produce an interesting alternative |
37 (*The sequent version (ITT) could produce an interesting alternative |
38 by backtracking. No longer.*) |
38 by backtracking. No longer.*) |
39 |
39 |
40 text "Binary sums and products" |
40 text "Binary sums and products" |
41 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)" |
41 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)" |
42 apply (tactic "pc_tac @{context} [] 1") |
42 apply pc |
43 done |
43 done |
44 |
44 |
45 (*A distributive law*) |
45 (*A distributive law*) |
46 schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)" |
46 schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)" |
47 apply (tactic "pc_tac @{context} [] 1") |
47 apply pc |
48 done |
48 done |
49 |
49 |
50 (*more general version, same proof*) |
50 (*more general version, same proof*) |
51 schematic_lemma |
51 schematic_lemma |
52 assumes "A type" |
52 assumes "A type" |
53 and "!!x. x:A ==> B(x) type" |
53 and "!!x. x:A ==> B(x) type" |
54 and "!!x. x:A ==> C(x) type" |
54 and "!!x. x:A ==> C(x) type" |
55 shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" |
55 shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" |
56 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
56 apply (pc assms) |
57 done |
57 done |
58 |
58 |
59 text "Construction of the currying functional" |
59 text "Construction of the currying functional" |
60 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))" |
60 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))" |
61 apply (tactic "pc_tac @{context} [] 1") |
61 apply pc |
62 done |
62 done |
63 |
63 |
64 (*more general goal with same proof*) |
64 (*more general goal with same proof*) |
65 schematic_lemma |
65 schematic_lemma |
66 assumes "A type" |
66 assumes "A type" |
67 and "!!x. x:A ==> B(x) type" |
67 and "!!x. x:A ==> B(x) type" |
68 and "!!z. z: (SUM x:A. B(x)) ==> C(z) type" |
68 and "!!z. z: (SUM x:A. B(x)) ==> C(z) type" |
69 shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). |
69 shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). |
70 (PROD x:A . PROD y:B(x) . C(<x,y>))" |
70 (PROD x:A . PROD y:B(x) . C(<x,y>))" |
71 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
71 apply (pc assms) |
72 done |
72 done |
73 |
73 |
74 text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" |
74 text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" |
75 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)" |
75 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)" |
76 apply (tactic "pc_tac @{context} [] 1") |
76 apply pc |
77 done |
77 done |
78 |
78 |
79 (*more general goal with same proof*) |
79 (*more general goal with same proof*) |
80 schematic_lemma |
80 schematic_lemma |
81 assumes "A type" |
81 assumes "A type" |
82 and "!!x. x:A ==> B(x) type" |
82 and "!!x. x:A ==> B(x) type" |
83 and "!!z. z: (SUM x:A . B(x)) ==> C(z) type" |
83 and "!!z. z: (SUM x:A . B(x)) ==> C(z) type" |
84 shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) |
84 shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) |
85 --> (PROD z : (SUM x:A . B(x)) . C(z))" |
85 --> (PROD z : (SUM x:A . B(x)) . C(z))" |
86 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
86 apply (pc assms) |
87 done |
87 done |
88 |
88 |
89 text "Function application" |
89 text "Function application" |
90 schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B" |
90 schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B" |
91 apply (tactic "pc_tac @{context} [] 1") |
91 apply pc |
92 done |
92 done |
93 |
93 |
94 text "Basic test of quantifier reasoning" |
94 text "Basic test of quantifier reasoning" |
95 schematic_lemma |
95 schematic_lemma |
96 assumes "A type" |
96 assumes "A type" |
97 and "B type" |
97 and "B type" |
98 and "!!x y.[| x:A; y:B |] ==> C(x,y) type" |
98 and "!!x y.[| x:A; y:B |] ==> C(x,y) type" |
99 shows |
99 shows |
100 "?a : (SUM y:B . PROD x:A . C(x,y)) |
100 "?a : (SUM y:B . PROD x:A . C(x,y)) |
101 --> (PROD x:A . SUM y:B . C(x,y))" |
101 --> (PROD x:A . SUM y:B . C(x,y))" |
102 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
102 apply (pc assms) |
103 done |
103 done |
104 |
104 |
105 text "Martin-Lof (1984) pages 36-7: the combinator S" |
105 text "Martin-Lof (1984) pages 36-7: the combinator S" |
106 schematic_lemma |
106 schematic_lemma |
107 assumes "A type" |
107 assumes "A type" |
108 and "!!x. x:A ==> B(x) type" |
108 and "!!x. x:A ==> B(x) type" |
109 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
109 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
110 shows "?a : (PROD x:A. PROD y:B(x). C(x,y)) |
110 shows "?a : (PROD x:A. PROD y:B(x). C(x,y)) |
111 --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
111 --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
112 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
112 apply (pc assms) |
113 done |
113 done |
114 |
114 |
115 text "Martin-Lof (1984) page 58: the axiom of disjunction elimination" |
115 text "Martin-Lof (1984) page 58: the axiom of disjunction elimination" |
116 schematic_lemma |
116 schematic_lemma |
117 assumes "A type" |
117 assumes "A type" |
118 and "B type" |
118 and "B type" |
119 and "!!z. z: A+B ==> C(z) type" |
119 and "!!z. z: A+B ==> C(z) type" |
120 shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) |
120 shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) |
121 --> (PROD z: A+B. C(z))" |
121 --> (PROD z: A+B. C(z))" |
122 apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) |
122 apply (pc assms) |
123 done |
123 done |
124 |
124 |
125 (*towards AXIOM OF CHOICE*) |
125 (*towards AXIOM OF CHOICE*) |
126 schematic_lemma [folded basic_defs]: |
126 schematic_lemma [folded basic_defs]: |
127 "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)" |
127 "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)" |
128 apply (tactic "pc_tac @{context} [] 1") |
128 apply pc |
129 done |
129 done |
130 |
130 |
131 |
131 |
132 (*Martin-Lof (1984) page 50*) |
132 (*Martin-Lof (1984) page 50*) |
133 text "AXIOM OF CHOICE! Delicate use of elimination rules" |
133 text "AXIOM OF CHOICE! Delicate use of elimination rules" |
135 assumes "A type" |
135 assumes "A type" |
136 and "!!x. x:A ==> B(x) type" |
136 and "!!x. x:A ==> B(x) type" |
137 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
137 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
138 shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). |
138 shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). |
139 (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
139 (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
140 apply (tactic {* intr_tac @{context} @{thms assms} *}) |
140 apply (intr assms) |
141 apply (tactic "add_mp_tac @{context} 2") |
141 prefer 2 apply add_mp |
142 apply (tactic "add_mp_tac @{context} 1") |
142 prefer 2 apply add_mp |
143 apply (erule SumE_fst) |
143 apply (erule SumE_fst) |
144 apply (rule replace_type) |
144 apply (rule replace_type) |
145 apply (rule subst_eqtyparg) |
145 apply (rule subst_eqtyparg) |
146 apply (rule comp_rls) |
146 apply (rule comp_rls) |
147 apply (rule_tac [4] SumE_snd) |
147 apply (rule_tac [4] SumE_snd) |
148 apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *}) |
148 apply (typechk SumE_fst assms) |
149 done |
149 done |
150 |
150 |
151 text "Axiom of choice. Proof without fst, snd. Harder still!" |
151 text "Axiom of choice. Proof without fst, snd. Harder still!" |
152 schematic_lemma [folded basic_defs]: |
152 schematic_lemma [folded basic_defs]: |
153 assumes "A type" |
153 assumes "A type" |
154 and "!!x. x:A ==> B(x) type" |
154 and "!!x. x:A ==> B(x) type" |
155 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
155 and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" |
156 shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). |
156 shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). |
157 (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
157 (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" |
158 apply (tactic {* intr_tac @{context} @{thms assms} *}) |
158 apply (intr assms) |
159 (*Must not use add_mp_tac as subst_prodE hides the construction.*) |
159 (*Must not use add_mp as subst_prodE hides the construction.*) |
160 apply (rule ProdE [THEN SumE], assumption) |
160 apply (rule ProdE [THEN SumE]) |
161 apply (tactic "TRYALL (assume_tac @{context})") |
161 apply assumption |
|
162 apply assumption |
|
163 apply assumption |
162 apply (rule replace_type) |
164 apply (rule replace_type) |
163 apply (rule subst_eqtyparg) |
165 apply (rule subst_eqtyparg) |
164 apply (rule comp_rls) |
166 apply (rule comp_rls) |
165 apply (erule_tac [4] ProdE [THEN SumE]) |
167 apply (erule_tac [4] ProdE [THEN SumE]) |
166 apply (tactic {* typechk_tac @{context} @{thms assms} *}) |
168 apply (typechk assms) |
167 apply (rule replace_type) |
169 apply (rule replace_type) |
168 apply (rule subst_eqtyparg) |
170 apply (rule subst_eqtyparg) |
169 apply (rule comp_rls) |
171 apply (rule comp_rls) |
170 apply (tactic {* typechk_tac @{context} @{thms assms} *}) |
172 apply (typechk assms) |
171 apply assumption |
173 apply assumption |
172 done |
174 done |
173 |
175 |
174 text "Example of sequent_style deduction" |
176 text "Example of sequent_style deduction" |
175 (*When splitting z:A*B, the assumption C(z) is affected; ?a becomes |
177 (*When splitting z:A*B, the assumption C(z) is affected; ?a becomes |