author | paulson |
Tue, 04 Aug 1998 10:46:44 +0200 | |
changeset 5237 | aebc63048f2d |
parent 5144 | 7ac22e5a05d7 |
child 5278 | a903b66822e2 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/prod |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
For prod.thy. Ordered Pairs, the Cartesian product type, the unit type |
|
7 |
*) |
|
8 |
||
9 |
open Prod; |
|
10 |
||
11 |
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*) |
|
5069 | 12 |
Goalw [Prod_def] "Pair_Rep a b : Prod"; |
923 | 13 |
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); |
14 |
qed "ProdI"; |
|
15 |
||
16 |
val [major] = goalw Prod.thy [Pair_Rep_def] |
|
17 |
"Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
|
18 |
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), |
|
1465 | 19 |
rtac conjI, rtac refl, rtac refl]); |
923 | 20 |
qed "Pair_Rep_inject"; |
21 |
||
5069 | 22 |
Goal "inj_on Abs_Prod Prod"; |
4830 | 23 |
by (rtac inj_on_inverseI 1); |
923 | 24 |
by (etac Abs_Prod_inverse 1); |
4830 | 25 |
qed "inj_on_Abs_Prod"; |
923 | 26 |
|
27 |
val prems = goalw Prod.thy [Pair_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
28 |
"[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
4830 | 29 |
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); |
923 | 30 |
by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
31 |
qed "Pair_inject"; |
|
32 |
||
5069 | 33 |
Goal "((a,b) = (a',b')) = (a=a' & b=b')"; |
4089 | 34 |
by (blast_tac (claset() addSEs [Pair_inject]) 1); |
923 | 35 |
qed "Pair_eq"; |
3429 | 36 |
AddIffs [Pair_eq]; |
923 | 37 |
|
5069 | 38 |
Goalw [fst_def] "fst((a,b)) = a"; |
4534 | 39 |
by (Blast_tac 1); |
923 | 40 |
qed "fst_conv"; |
5069 | 41 |
Goalw [snd_def] "snd((a,b)) = b"; |
4534 | 42 |
by (Blast_tac 1); |
923 | 43 |
qed "snd_conv"; |
4534 | 44 |
Addsimps [fst_conv, snd_conv]; |
923 | 45 |
|
5069 | 46 |
Goalw [Pair_def] "? x y. p = (x,y)"; |
923 | 47 |
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); |
48 |
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, |
|
1465 | 49 |
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); |
923 | 50 |
qed "PairE_lemma"; |
51 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
52 |
val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q"; |
923 | 53 |
by (rtac (PairE_lemma RS exE) 1); |
54 |
by (REPEAT (eresolve_tac [prem,exE] 1)); |
|
55 |
qed "PairE"; |
|
56 |
||
4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
57 |
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, |
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
58 |
K prune_params_tac]; |
4134 | 59 |
|
4828 | 60 |
(* Do not add as rewrite rule: invalidates some proofs in IMP *) |
5069 | 61 |
Goal "p = (fst(p),snd(p))"; |
4828 | 62 |
by (pair_tac "p" 1); |
63 |
by (Asm_simp_tac 1); |
|
64 |
qed "surjective_pairing"; |
|
65 |
||
66 |
val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [ |
|
67 |
rtac exI 1, rtac exI 1, rtac surjective_pairing 1]); |
|
68 |
Addsimps [surj_pair]; |
|
69 |
||
70 |
(* lemmas for splitting paired `!!' *) |
|
71 |
local |
|
72 |
val lemma1 = prove_goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))" |
|
73 |
(fn prems => [resolve_tac prems 1]); |
|
74 |
||
75 |
val psig = sign_of Prod.thy; |
|
76 |
val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop"; |
|
77 |
val PeqP = reflexive(read_cterm psig ("P", pT)); |
|
78 |
val psplit = zero_var_indexes(read_instantiate [("p","x")] |
|
79 |
surjective_pairing RS eq_reflection); |
|
80 |
val adhoc = combination PeqP psplit; |
|
81 |
val lemma = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x" |
|
82 |
(fn prems => [rewtac adhoc, resolve_tac prems 1]); |
|
83 |
val lemma2 = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)" |
|
84 |
(fn prems => [rtac lemma 1, resolve_tac prems 1]); |
|
85 |
in |
|
86 |
val split_paired_all = equal_intr lemma1 lemma2 |
|
87 |
end; |
|
88 |
bind_thm("split_paired_all", split_paired_all); |
|
89 |
(* |
|
90 |
Addsimps [split_paired_all] does not work with simplifier |
|
91 |
because it also affects premises in congrence rules, |
|
92 |
where is can lead to premises of the form !!a b. ... = ?P(a,b) |
|
93 |
which cannot be solved by reflexivity. |
|
94 |
*) |
|
95 |
||
1301 | 96 |
(* replace parameters of product type by individual component parameters *) |
97 |
local |
|
4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
98 |
fun is_pair (_,Type("*",_)) = true |
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
99 |
| is_pair _ = false; |
4828 | 100 |
fun exists_paired_all prem = exists is_pair (Logic.strip_params prem); |
101 |
val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]); |
|
1301 | 102 |
in |
4828 | 103 |
val split_all_tac = SUBGOAL (fn (prem,i) => |
104 |
if exists_paired_all prem then split_tac i else no_tac); |
|
1301 | 105 |
end; |
106 |
||
4828 | 107 |
claset_ref() := claset() addSWrapper ("split_all_tac", |
108 |
fn tac2 => split_all_tac ORELSE' tac2); |
|
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
109 |
|
5069 | 110 |
Goal "(!x. P x) = (!a b. P(a,b))"; |
4650 | 111 |
by (Fast_tac 1); |
1301 | 112 |
qed "split_paired_All"; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
113 |
Addsimps [split_paired_All]; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
114 |
(* AddIffs is not a good idea because it makes Blast_tac loop *) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
115 |
|
5069 | 116 |
Goal "(? x. P x) = (? a b. P(a,b))"; |
4650 | 117 |
by (Fast_tac 1); |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
118 |
qed "split_paired_Ex"; |
4534 | 119 |
Addsimps [split_paired_Ex]; |
1301 | 120 |
|
5069 | 121 |
Goalw [split_def] "split c (a,b) = c a b"; |
4534 | 122 |
by (Simp_tac 1); |
923 | 123 |
qed "split"; |
4534 | 124 |
Addsimps [split]; |
923 | 125 |
|
5069 | 126 |
Goal "split Pair p = p"; |
4828 | 127 |
by (pair_tac "p" 1); |
128 |
by (Simp_tac 1); |
|
129 |
qed "split_Pair"; |
|
130 |
(*unused: val surjective_pairing2 = split_Pair RS sym;*) |
|
131 |
||
5069 | 132 |
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
4828 | 133 |
by (split_all_tac 1); |
1264 | 134 |
by (Asm_simp_tac 1); |
923 | 135 |
qed "Pair_fst_snd_eq"; |
136 |
||
137 |
(*Prevents simplification of c: much faster*) |
|
138 |
qed_goal "split_weak_cong" Prod.thy |
|
139 |
"p=q ==> split c p = split c q" |
|
140 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
141 |
||
1655 | 142 |
qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f" |
4534 | 143 |
(K [rtac ext 1, split_all_tac 1, rtac split 1]); |
1655 | 144 |
|
4989 | 145 |
qed_goal "cond_split_eta" Prod.thy |
146 |
"!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g" |
|
147 |
(K [asm_simp_tac (simpset() addsimps [split_eta]) 1]); |
|
148 |
(*Addsimps [cond_split_eta]; with this version of split_eta, the simplifier |
|
149 |
can eta-contract arbitrarily tupled functions. |
|
150 |
Unfortunately, this renders some existing proofs very inefficient. |
|
151 |
stac split_eta does not work in general either. *) |
|
152 |
val split_etas = split_eta::map (fn s => prove_goal Prod.thy s |
|
153 |
(K [simp_tac (simpset() addsimps [cond_split_eta]) 1])) |
|
154 |
["(%(a,b,c ). f(a,b,c )) = f","(%(a,b,c,d ). f(a,b,c,d )) = f", |
|
155 |
"(%(a,b,c,d,e). f(a,b,c,d,e)) = f","(%(a,b,c,d,e,g). f(a,b,c,d,e,g)) = f"]; |
|
156 |
Addsimps split_etas; (* pragmatic solution *) |
|
157 |
||
4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
158 |
qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)" |
4534 | 159 |
(K [stac surjective_pairing 1, stac split 1, rtac refl 1]); |
4134 | 160 |
|
923 | 161 |
(*For use with split_tac and the simplifier*) |
5069 | 162 |
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
923 | 163 |
by (stac surjective_pairing 1); |
164 |
by (stac split 1); |
|
2935 | 165 |
by (Blast_tac 1); |
4830 | 166 |
qed "split_split"; |
923 | 167 |
|
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
168 |
(* could be done after split_tac has been speeded up significantly: |
4830 | 169 |
simpset_ref() := simpset() addsplits [split_split]; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
170 |
precompute the constants involved and don't do anything unless |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
171 |
the current goal contains one of those constants |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
172 |
*) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
173 |
|
5069 | 174 |
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
4830 | 175 |
by (stac split_split 1); |
4435 | 176 |
by (Simp_tac 1); |
177 |
qed "expand_split_asm"; |
|
178 |
||
923 | 179 |
(** split used as a logical connective or set former **) |
180 |
||
2935 | 181 |
(*These rules are for use with blast_tac. |
923 | 182 |
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
183 |
||
5069 | 184 |
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
1552 | 185 |
by (split_all_tac 1); |
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
186 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
187 |
qed "splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
188 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
189 |
Goal "c a b ==> split c (a,b)"; |
1264 | 190 |
by (Asm_simp_tac 1); |
923 | 191 |
qed "splitI"; |
192 |
||
193 |
val prems = goalw Prod.thy [split_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
194 |
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
923 | 195 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
196 |
qed "splitE"; |
|
197 |
||
4134 | 198 |
val splitE2 = prove_goal Prod.thy |
199 |
"[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [ |
|
200 |
REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
|
201 |
rtac (split_beta RS subst) 1, |
|
202 |
rtac (hd prems) 1]); |
|
203 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
204 |
Goal "split R (a,b) ==> R a b"; |
923 | 205 |
by (etac (split RS iffD1) 1); |
206 |
qed "splitD"; |
|
207 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
208 |
Goal "z: c a b ==> z: split c (a,b)"; |
1264 | 209 |
by (Asm_simp_tac 1); |
923 | 210 |
qed "mem_splitI"; |
211 |
||
5069 | 212 |
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
1552 | 213 |
by (split_all_tac 1); |
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
214 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
215 |
qed "mem_splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
216 |
|
923 | 217 |
val prems = goalw Prod.thy [split_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
218 |
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
923 | 219 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
220 |
qed "mem_splitE"; |
|
221 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
222 |
AddSIs [splitI, splitI2, mem_splitI, mem_splitI2]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
223 |
AddSEs [splitE, mem_splitE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
224 |
|
4534 | 225 |
(* allows simplifications of nested splits in case of independent predicates *) |
5069 | 226 |
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; |
4534 | 227 |
by (rtac ext 1); |
228 |
by (Blast_tac 1); |
|
229 |
qed "split_part"; |
|
230 |
Addsimps [split_part]; |
|
231 |
||
5069 | 232 |
Goal "(@(x',y'). x = x' & y = y') = (x,y)"; |
4534 | 233 |
by (Blast_tac 1); |
234 |
qed "Eps_split_eq"; |
|
235 |
Addsimps [Eps_split_eq]; |
|
236 |
(* |
|
237 |
the following would be slightly more general, |
|
238 |
but cannot be used as rewrite rule: |
|
239 |
### Cannot add premise as rewrite rule because it contains (type) unknowns: |
|
240 |
### ?y = .x |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
241 |
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"; |
4534 | 242 |
by (rtac select_equality 1); |
243 |
by ( Simp_tac 1); |
|
244 |
by (split_all_tac 1); |
|
245 |
by (Asm_full_simp_tac 1); |
|
246 |
qed "Eps_split_eq"; |
|
247 |
*) |
|
248 |
||
923 | 249 |
(*** prod_fun -- action of the product functor upon functions ***) |
250 |
||
5069 | 251 |
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
923 | 252 |
by (rtac split 1); |
253 |
qed "prod_fun"; |
|
4521 | 254 |
Addsimps [prod_fun]; |
923 | 255 |
|
5069 | 256 |
Goal |
923 | 257 |
"prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
258 |
by (rtac ext 1); |
|
4828 | 259 |
by (pair_tac "x" 1); |
4521 | 260 |
by (Asm_simp_tac 1); |
923 | 261 |
qed "prod_fun_compose"; |
262 |
||
5069 | 263 |
Goal "prod_fun (%x. x) (%y. y) = (%z. z)"; |
923 | 264 |
by (rtac ext 1); |
4828 | 265 |
by (pair_tac "z" 1); |
4521 | 266 |
by (Asm_simp_tac 1); |
923 | 267 |
qed "prod_fun_ident"; |
4521 | 268 |
Addsimps [prod_fun_ident]; |
923 | 269 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
270 |
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; |
923 | 271 |
by (rtac image_eqI 1); |
272 |
by (rtac (prod_fun RS sym) 1); |
|
273 |
by (resolve_tac prems 1); |
|
274 |
qed "prod_fun_imageI"; |
|
275 |
||
276 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
277 |
"[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
923 | 278 |
\ |] ==> P"; |
279 |
by (rtac (major RS imageE) 1); |
|
280 |
by (res_inst_tac [("p","x")] PairE 1); |
|
281 |
by (resolve_tac prems 1); |
|
2935 | 282 |
by (Blast_tac 2); |
4089 | 283 |
by (blast_tac (claset() addIs [prod_fun]) 1); |
923 | 284 |
qed "prod_fun_imageE"; |
285 |
||
4521 | 286 |
|
923 | 287 |
(*** Disjoint union of a family of sets - Sigma ***) |
288 |
||
289 |
qed_goalw "SigmaI" Prod.thy [Sigma_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
290 |
"[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
923 | 291 |
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
292 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
293 |
AddSIs [SigmaI]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
294 |
|
923 | 295 |
(*The general elimination rule*) |
296 |
qed_goalw "SigmaE" Prod.thy [Sigma_def] |
|
297 |
"[| c: Sigma A B; \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
298 |
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
923 | 299 |
\ |] ==> P" |
300 |
(fn major::prems=> |
|
301 |
[ (cut_facts_tac [major] 1), |
|
302 |
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
|
303 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
304 |
(** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
305 |
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A" |
923 | 306 |
(fn [major]=> |
307 |
[ (rtac (major RS SigmaE) 1), |
|
308 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
309 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
310 |
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)" |
923 | 311 |
(fn [major]=> |
312 |
[ (rtac (major RS SigmaE) 1), |
|
313 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
314 |
||
315 |
qed_goal "SigmaE2" Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
316 |
"[| (a,b) : Sigma A B; \ |
923 | 317 |
\ [| a:A; b:B(a) |] ==> P \ |
318 |
\ |] ==> P" |
|
319 |
(fn [major,minor]=> |
|
320 |
[ (rtac minor 1), |
|
321 |
(rtac (major RS SigmaD1) 1), |
|
322 |
(rtac (major RS SigmaD2) 1) ]); |
|
323 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
324 |
AddSEs [SigmaE2, SigmaE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
325 |
|
1515 | 326 |
val prems = goal Prod.thy |
1642 | 327 |
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; |
1515 | 328 |
by (cut_facts_tac prems 1); |
4089 | 329 |
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
1515 | 330 |
qed "Sigma_mono"; |
331 |
||
1618 | 332 |
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}" |
2935 | 333 |
(fn _ => [ (Blast_tac 1) ]); |
1618 | 334 |
|
1642 | 335 |
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}" |
2935 | 336 |
(fn _ => [ (Blast_tac 1) ]); |
1618 | 337 |
|
338 |
Addsimps [Sigma_empty1,Sigma_empty2]; |
|
339 |
||
5069 | 340 |
Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; |
2935 | 341 |
by (Blast_tac 1); |
1618 | 342 |
qed "mem_Sigma_iff"; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
343 |
AddIffs [mem_Sigma_iff]; |
1618 | 344 |
|
4534 | 345 |
val Collect_split = prove_goal Prod.thy |
4134 | 346 |
"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]); |
4534 | 347 |
Addsimps [Collect_split]; |
1515 | 348 |
|
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
349 |
(*Suggested by Pierre Chartier*) |
5069 | 350 |
Goal |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
351 |
"(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; |
2935 | 352 |
by (Blast_tac 1); |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
353 |
qed "UNION_Times_distrib"; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
354 |
|
923 | 355 |
(*** Domain of a relation ***) |
356 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
357 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r"; |
923 | 358 |
by (rtac CollectI 1); |
359 |
by (rtac bexI 1); |
|
360 |
by (rtac (fst_conv RS sym) 1); |
|
361 |
by (resolve_tac prems 1); |
|
362 |
qed "fst_imageI"; |
|
363 |
||
364 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
365 |
"[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P"; |
923 | 366 |
by (rtac (major RS imageE) 1); |
367 |
by (resolve_tac prems 1); |
|
368 |
by (etac ssubst 1); |
|
369 |
by (rtac (surjective_pairing RS subst) 1); |
|
370 |
by (assume_tac 1); |
|
371 |
qed "fst_imageE"; |
|
372 |
||
373 |
(*** Range of a relation ***) |
|
374 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
375 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r"; |
923 | 376 |
by (rtac CollectI 1); |
377 |
by (rtac bexI 1); |
|
378 |
by (rtac (snd_conv RS sym) 1); |
|
379 |
by (resolve_tac prems 1); |
|
380 |
qed "snd_imageI"; |
|
381 |
||
382 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
383 |
"[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P"; |
923 | 384 |
by (rtac (major RS imageE) 1); |
385 |
by (resolve_tac prems 1); |
|
386 |
by (etac ssubst 1); |
|
387 |
by (rtac (surjective_pairing RS subst) 1); |
|
388 |
by (assume_tac 1); |
|
389 |
qed "snd_imageE"; |
|
390 |
||
5083 | 391 |
|
923 | 392 |
(** Exhaustion rule for unit -- a degenerate form of induction **) |
393 |
||
5069 | 394 |
Goalw [Unity_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
395 |
"u = ()"; |
2886 | 396 |
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); |
2880 | 397 |
by (rtac (Rep_unit_inverse RS sym) 1); |
923 | 398 |
qed "unit_eq"; |
1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset
|
399 |
|
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset
|
400 |
AddIs [fst_imageI, snd_imageI, prod_fun_imageI]; |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
401 |
AddSEs [fst_imageE, snd_imageE, prod_fun_imageE]; |
923 | 402 |
|
5083 | 403 |
|
5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
404 |
(*simplification procedure for unit_eq. |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
405 |
Cannot use this rule directly -- it loops!*) |
5083 | 406 |
local |
407 |
val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT)); |
|
408 |
val unit_meta_eq = standard (mk_meta_eq unit_eq); |
|
409 |
fun proc _ _ t = |
|
410 |
if HOLogic.is_unit t then None |
|
411 |
else Some unit_meta_eq; |
|
412 |
in |
|
413 |
val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
|
414 |
end; |
|
415 |
||
416 |
Addsimprocs [unit_eq_proc]; |
|
417 |
||
418 |
||
5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
419 |
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
420 |
replacing it by f rather than by %u.f(). *) |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
421 |
Goal "(%u::unit. f()) = f"; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
422 |
by (rtac ext 1); |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
423 |
by (Simp_tac 1); |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
424 |
qed "unit_abs_eta_conv"; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
425 |
Addsimps [unit_abs_eta_conv]; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
426 |
|
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
427 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
428 |
(*Attempts to remove occurrences of split, and pair-valued parameters*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
429 |
val remove_split = rewrite_rule [split RS eq_reflection] o |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
430 |
rule_by_tactic (TRYALL split_all_tac); |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
431 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
432 |
local |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
433 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
434 |
(*In ap_split S T u, term u expects separate arguments for the factors of S, |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
435 |
with result type T. The call creates a new term expecting one argument |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
436 |
of type S.*) |
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
437 |
fun ap_split (Type ("*", [T1, T2])) T3 u = |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
438 |
HOLogic.split_const (T1, T2, T3) $ |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
439 |
Abs("v", T1, |
2031 | 440 |
ap_split T2 T3 |
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
441 |
((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
2031 | 442 |
Bound 0)) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
443 |
| ap_split T T3 u = u; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
444 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
445 |
(*Curries any Var of function type in the rule*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
446 |
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
447 |
let val T' = HOLogic.prodT_factors T1 ---> T2 |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
448 |
val newt = ap_split T1 T2 (Var (v, T')) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
449 |
val cterm = Thm.cterm_of (#sign (rep_thm rl)) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
450 |
in |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
451 |
instantiate ([], [(cterm t, cterm newt)]) rl |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
452 |
end |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
453 |
| split_rule_var' (t, rl) = rl; |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
454 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
455 |
in |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
456 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
457 |
val split_rule_var = standard o remove_split o split_rule_var'; |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
458 |
|
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
459 |
(*Curries ALL function variables occurring in a rule's conclusion*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
460 |
fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
461 |
|> standard; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
462 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
463 |
end; |