101 (*** Eliminator - split ***) |
101 (*** Eliminator - split ***) |
102 |
102 |
103 val split = prove_goalw ZF.thy [split_def] |
103 val split = prove_goalw ZF.thy [split_def] |
104 "split(%x y.c(x,y), <a,b>) = c(a,b)" |
104 "split(%x y.c(x,y), <a,b>) = c(a,b)" |
105 (fn _ => |
105 (fn _ => |
106 [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]); |
106 [ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]); |
107 |
107 |
108 val split_type = prove_goal ZF.thy |
108 val split_type = prove_goal ZF.thy |
109 "[| p:Sigma(A,B); \ |
109 "[| p:Sigma(A,B); \ |
110 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
110 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
111 \ |] ==> split(%x y.c(x,y), p) : C(p)" |
111 \ |] ==> split(%x y.c(x,y), p) : C(p)" |
112 (fn major::prems=> |
112 (fn major::prems=> |
113 [ (rtac (major RS SigmaE) 1), |
113 [ (rtac (major RS SigmaE) 1), |
114 (etac ssubst 1), |
114 (etac ssubst 1), |
115 (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]); |
115 (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]); |
|
116 |
|
117 |
|
118 goal ZF.thy |
|
119 "!!u. u: A*B ==> \ |
|
120 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
|
121 by (etac SigmaE 1); |
|
122 by (asm_simp_tac (FOL_ss addsimps [split]) 1); |
|
123 by (fast_tac (upair_cs addSEs [Pair_inject]) 1); |
|
124 val expand_split = result(); |
|
125 |
116 |
126 |
117 (*** conversions for fst and snd ***) |
127 (*** conversions for fst and snd ***) |
118 |
128 |
119 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a" |
129 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a" |
120 (fn _=> [ (rtac split 1) ]); |
130 (fn _=> [ (rtac split 1) ]); |