equal
deleted
inserted
replaced
62 "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"; |
62 "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"; |
63 by (pc_tac prems 1); |
63 by (pc_tac prems 1); |
64 result(); |
64 result(); |
65 |
65 |
66 (*more general goal with same proof*) |
66 (*more general goal with same proof*) |
67 val prems = goal CTT.thy |
67 val prems = goal CTT.thy |
68 "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A. B(x)) ==> C(z) type|] \ |
68 "[| A type; !!x. x:A ==> B(x) type; \ |
69 \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ |
69 \ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ |
70 \ --> (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
70 \ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ |
|
71 \ (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
71 by (pc_tac prems 1); |
72 by (pc_tac prems 1); |
72 result(); |
73 result(); |
73 |
74 |
74 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"; |
75 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"; |
75 val prems = goal CTT.thy |
76 val prems = goal CTT.thy |
128 result(); |
129 result(); |
129 |
130 |
130 (*Martin-Lof (1984) page 50*) |
131 (*Martin-Lof (1984) page 50*) |
131 writeln"AXIOM OF CHOICE!!! Delicate use of elimination rules"; |
132 writeln"AXIOM OF CHOICE!!! Delicate use of elimination rules"; |
132 val prems = goal CTT.thy |
133 val prems = goal CTT.thy |
133 "[| A type; !!x. x:A ==> B(x) type; \ |
134 "[| A type; !!x. x:A ==> B(x) type; \ |
134 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type|] \ |
135 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
135 \ ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ |
136 \ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ |
136 \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
137 \ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
137 by (intr_tac prems); |
138 by (intr_tac prems); |
138 by (add_mp_tac 2); |
139 by (add_mp_tac 2); |
139 by (add_mp_tac 1); |
140 by (add_mp_tac 1); |
140 by (etac SumE_fst 1); |
141 by (etac SumE_fst 1); |
141 by (rtac replace_type 1); |
142 by (rtac replace_type 1); |
145 by (typechk_tac (SumE_fst::prems)); |
146 by (typechk_tac (SumE_fst::prems)); |
146 result(); |
147 result(); |
147 |
148 |
148 writeln"Axiom of choice. Proof without fst, snd. Harder still!"; |
149 writeln"Axiom of choice. Proof without fst, snd. Harder still!"; |
149 val prems = goal CTT.thy |
150 val prems = goal CTT.thy |
150 "[| A type; !!x.x:A ==> B(x) type; \ |
151 "[| A type; !!x.x:A ==> B(x) type; \ |
151 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type|] \ |
152 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
152 \ ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ |
153 \ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ |
153 \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
154 \ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
154 by (intr_tac prems); |
155 by (intr_tac prems); |
155 (*Must not use add_mp_tac as subst_prodE hides the construction.*) |
156 (*Must not use add_mp_tac as subst_prodE hides the construction.*) |
156 by (resolve_tac [ProdE RS SumE] 1 THEN assume_tac 1); |
157 by (resolve_tac [ProdE RS SumE] 1 THEN assume_tac 1); |
157 by (TRYALL assume_tac); |
158 by (TRYALL assume_tac); |
158 by (rtac replace_type 1); |
159 by (rtac replace_type 1); |