equal
deleted
inserted
replaced
17 (fn prems => |
17 (fn prems => |
18 [ |
18 [ |
19 (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]) |
19 (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]) |
20 ]); |
20 ]); |
21 |
21 |
22 qed_goal "inj_onto_Abs_Sprod" Sprod0.thy |
22 qed_goal "inj_on_Abs_Sprod" Sprod0.thy |
23 "inj_onto Abs_Sprod Sprod" |
23 "inj_on Abs_Sprod Sprod" |
24 (fn prems => |
24 (fn prems => |
25 [ |
25 [ |
26 (rtac inj_onto_inverseI 1), |
26 (rtac inj_on_inverseI 1), |
27 (etac Abs_Sprod_inverse 1) |
27 (etac Abs_Sprod_inverse 1) |
28 ]); |
28 ]); |
29 |
29 |
30 (* ------------------------------------------------------------------------ *) |
30 (* ------------------------------------------------------------------------ *) |
31 (* Strictness and definedness of Spair_Rep *) |
31 (* Strictness and definedness of Spair_Rep *) |
78 (fn prems => |
78 (fn prems => |
79 [ |
79 [ |
80 (cut_facts_tac prems 1), |
80 (cut_facts_tac prems 1), |
81 (etac inject_Spair_Rep 1), |
81 (etac inject_Spair_Rep 1), |
82 (atac 1), |
82 (atac 1), |
83 (etac (inj_onto_Abs_Sprod RS inj_ontoD) 1), |
83 (etac (inj_on_Abs_Sprod RS inj_onD) 1), |
84 (rtac SprodI 1), |
84 (rtac SprodI 1), |
85 (rtac SprodI 1) |
85 (rtac SprodI 1) |
86 ]); |
86 ]); |
87 |
87 |
88 |
88 |
130 "Ispair a b = Ispair UU UU ==> (a = UU | b = UU)" |
130 "Ispair a b = Ispair UU UU ==> (a = UU | b = UU)" |
131 (fn prems => |
131 (fn prems => |
132 [ |
132 [ |
133 (cut_facts_tac prems 1), |
133 (cut_facts_tac prems 1), |
134 (rtac defined_Spair_Rep_rev 1), |
134 (rtac defined_Spair_Rep_rev 1), |
135 (rtac (inj_onto_Abs_Sprod RS inj_ontoD) 1), |
135 (rtac (inj_on_Abs_Sprod RS inj_onD) 1), |
136 (atac 1), |
136 (atac 1), |
137 (rtac SprodI 1), |
137 (rtac SprodI 1), |
138 (rtac SprodI 1) |
138 (rtac SprodI 1) |
139 ]); |
139 ]); |
140 |
140 |