equal
deleted
inserted
replaced
18 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
18 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
19 (Blast_tac 1) ]); |
19 (Blast_tac 1) ]); |
20 |
20 |
21 qed_goalw "Pair_iff" ZF.thy [Pair_def] |
21 qed_goalw "Pair_iff" ZF.thy [Pair_def] |
22 "<a,b> = <c,d> <-> a=c & b=d" |
22 "<a,b> = <c,d> <-> a=c & b=d" |
23 (fn _=> [ (simp_tac (!simpset addsimps [doubleton_eq_iff]) 1), |
23 (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1), |
24 (Blast_tac 1) ]); |
24 (Blast_tac 1) ]); |
25 |
25 |
26 Addsimps [Pair_iff]; |
26 Addsimps [Pair_iff]; |
27 |
27 |
28 bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE); |
28 bind_thm ("Pair_inject", Pair_iff RS iffD1 RS conjE); |
31 |
31 |
32 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1); |
32 bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1); |
33 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2); |
33 bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2); |
34 |
34 |
35 qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0" |
35 qed_goalw "Pair_not_0" ZF.thy [Pair_def] "<a,b> ~= 0" |
36 (fn _ => [ (blast_tac (!claset addEs [equalityE]) 1) ]); |
36 (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]); |
37 |
37 |
38 bind_thm ("Pair_neq_0", Pair_not_0 RS notE); |
38 bind_thm ("Pair_neq_0", Pair_not_0 RS notE); |
39 |
39 |
40 AddSEs [Pair_neq_0, sym RS Pair_neq_0]; |
40 AddSEs [Pair_neq_0, sym RS Pair_neq_0]; |
41 |
41 |
86 (rtac (major RS SigmaD2) 1) ]); |
86 (rtac (major RS SigmaD2) 1) ]); |
87 |
87 |
88 qed_goalw "Sigma_cong" ZF.thy [Sigma_def] |
88 qed_goalw "Sigma_cong" ZF.thy [Sigma_def] |
89 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
89 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
90 \ Sigma(A,B) = Sigma(A',B')" |
90 \ Sigma(A,B) = Sigma(A',B')" |
91 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]); |
91 (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]); |
92 |
92 |
93 |
93 |
94 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
94 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause |
95 flex-flex pairs and the "Check your prover" error. Most |
95 flex-flex pairs and the "Check your prover" error. Most |
96 Sigmas and Pis are abbreviated as * or -> *) |
96 Sigmas and Pis are abbreviated as * or -> *) |
108 |
108 |
109 |
109 |
110 (*** Projections: fst, snd ***) |
110 (*** Projections: fst, snd ***) |
111 |
111 |
112 qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a" |
112 qed_goalw "fst_conv" ZF.thy [fst_def] "fst(<a,b>) = a" |
113 (fn _=> [ (blast_tac (!claset addIs [the_equality]) 1) ]); |
113 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]); |
114 |
114 |
115 qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b" |
115 qed_goalw "snd_conv" ZF.thy [snd_def] "snd(<a,b>) = b" |
116 (fn _=> [ (blast_tac (!claset addIs [the_equality]) 1) ]); |
116 (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]); |
117 |
117 |
118 Addsimps [fst_conv,snd_conv]; |
118 Addsimps [fst_conv,snd_conv]; |
119 |
119 |
120 qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A" |
120 qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A" |
121 (fn _=> [ Auto_tac() ]); |
121 (fn _=> [ Auto_tac() ]); |
141 "[| p:Sigma(A,B); \ |
141 "[| p:Sigma(A,B); \ |
142 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
142 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
143 \ |] ==> split(%x y. c(x,y), p) : C(p)" |
143 \ |] ==> split(%x y. c(x,y), p) : C(p)" |
144 (fn major::prems=> |
144 (fn major::prems=> |
145 [ (rtac (major RS SigmaE) 1), |
145 [ (rtac (major RS SigmaE) 1), |
146 (asm_simp_tac (!simpset addsimps prems) 1) ]); |
146 (asm_simp_tac (simpset() addsimps prems) 1) ]); |
147 |
147 |
148 goalw ZF.thy [split_def] |
148 goalw ZF.thy [split_def] |
149 "!!u. u: A*B ==> \ |
149 "!!u. u: A*B ==> \ |
150 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
150 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
151 by (Auto_tac()); |
151 by (Auto_tac()); |