author | wenzelm |
Fri, 10 Oct 1997 19:02:28 +0200 | |
changeset 3842 | b55686a7b22c |
parent 3568 | 36ff1ab12021 |
child 3919 | c036caebfc75 |
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*) |
|
12 |
goalw Prod.thy [Prod_def] "Pair_Rep a b : Prod"; |
|
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 |
||
22 |
goal Prod.thy "inj_onto Abs_Prod Prod"; |
|
23 |
by (rtac inj_onto_inverseI 1); |
|
24 |
by (etac Abs_Prod_inverse 1); |
|
25 |
qed "inj_onto_Abs_Prod"; |
|
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"; |
923 | 29 |
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); |
30 |
by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
|
31 |
qed "Pair_inject"; |
|
32 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
33 |
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; |
3429 | 34 |
by (blast_tac (!claset addSEs [Pair_inject]) 1); |
923 | 35 |
qed "Pair_eq"; |
3429 | 36 |
AddIffs [Pair_eq]; |
923 | 37 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
38 |
goalw Prod.thy [fst_def] "fst((a,b)) = a"; |
2935 | 39 |
by (blast_tac (!claset addIs [select_equality]) 1); |
923 | 40 |
qed "fst_conv"; |
41 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
42 |
goalw Prod.thy [snd_def] "snd((a,b)) = b"; |
2935 | 43 |
by (blast_tac (!claset addIs [select_equality]) 1); |
923 | 44 |
qed "snd_conv"; |
45 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
46 |
goalw Prod.thy [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 |
||
1301 | 57 |
(* replace parameters of product type by individual component parameters *) |
58 |
local |
|
59 |
fun is_pair (_,Type("*",_)) = true |
|
60 |
| is_pair _ = false; |
|
61 |
||
1727 | 62 |
fun find_pair_param prem = |
63 |
let val params = Logic.strip_params prem |
|
1301 | 64 |
in if exists is_pair params |
1727 | 65 |
then let val params = rev(rename_wrt_term prem params) |
1301 | 66 |
(*as they are printed*) |
67 |
in apsome fst (find_first is_pair params) end |
|
68 |
else None |
|
69 |
end; |
|
70 |
||
71 |
in |
|
72 |
||
1727 | 73 |
val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) => |
74 |
case find_pair_param prem of |
|
1301 | 75 |
None => no_tac |
1727 | 76 |
| Some x => EVERY[res_inst_tac[("p",x)] PairE i, |
77 |
REPEAT(hyp_subst_tac i), prune_params_tac]); |
|
1301 | 78 |
|
79 |
end; |
|
80 |
||
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
81 |
(* Could be nice, but breaks too many proofs: |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
82 |
claset := !claset addbefore split_all_tac; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
83 |
*) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
84 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
85 |
(*** lemmas for splitting paired `!!' |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
86 |
Does not work with simplifier because it also affects premises in |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
87 |
congrence rules, where is can lead to premises of the form |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
88 |
!!a b. ... = ?P(a,b) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
89 |
which cannot be solved by reflexivity. |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
90 |
|
3842 | 91 |
val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))"; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
92 |
br prem 1; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
93 |
val lemma1 = result(); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
94 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
95 |
local |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
96 |
val psig = sign_of Prod.thy; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
97 |
val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop"; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
98 |
val PeqP = reflexive(read_cterm psig ("P", pT)); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
99 |
val psplit = zero_var_indexes(read_instantiate [("p","x")] |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
100 |
surjective_pairing RS eq_reflection) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
101 |
in |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
102 |
val adhoc = combination PeqP psplit |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
103 |
end; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
104 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
105 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
106 |
val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x"; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
107 |
bw adhoc; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
108 |
br prem 1; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
109 |
val lemma = result(); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
110 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
111 |
val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)"; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
112 |
br lemma 1; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
113 |
br prem 1; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
114 |
val lemma2 = result(); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
115 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
116 |
bind_thm("split_paired_all", equal_intr lemma1 lemma2); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
117 |
Addsimps [split_paired_all]; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
118 |
***) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
119 |
|
1301 | 120 |
goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2089
diff
changeset
|
121 |
by (fast_tac (!claset addbefore split_all_tac) 1); |
1301 | 122 |
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
|
123 |
Addsimps [split_paired_All]; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
124 |
(* 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
|
125 |
|
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
126 |
goal Prod.thy "(? x. P x) = (? a b. P(a,b))"; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
127 |
by (fast_tac (!claset addbefore split_all_tac) 1); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
128 |
qed "split_paired_Ex"; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
129 |
(* Addsimps [split_paired_Ex]; breaks a number of IOA proofs *) |
1301 | 130 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
131 |
goalw Prod.thy [split_def] "split c (a,b) = c a b"; |
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
132 |
by (EVERY1[stac fst_conv, stac snd_conv]); |
923 | 133 |
by (rtac refl 1); |
134 |
qed "split"; |
|
135 |
||
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
136 |
Addsimps [fst_conv, snd_conv, split]; |
923 | 137 |
|
138 |
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
|
139 |
by (res_inst_tac[("p","s")] PairE 1); |
|
140 |
by (res_inst_tac[("p","t")] PairE 1); |
|
1264 | 141 |
by (Asm_simp_tac 1); |
923 | 142 |
qed "Pair_fst_snd_eq"; |
143 |
||
144 |
(*Prevents simplification of c: much faster*) |
|
145 |
qed_goal "split_weak_cong" Prod.thy |
|
146 |
"p=q ==> split c p = split c q" |
|
147 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
148 |
||
149 |
(* Do not add as rewrite rule: invalidates some proofs in IMP *) |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
150 |
goal Prod.thy "p = (fst(p),snd(p))"; |
923 | 151 |
by (res_inst_tac [("p","p")] PairE 1); |
1264 | 152 |
by (Asm_simp_tac 1); |
923 | 153 |
qed "surjective_pairing"; |
154 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
155 |
goal Prod.thy "p = split (%x y.(x,y)) p"; |
923 | 156 |
by (res_inst_tac [("p","p")] PairE 1); |
1264 | 157 |
by (Asm_simp_tac 1); |
923 | 158 |
qed "surjective_pairing2"; |
159 |
||
1655 | 160 |
qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f" |
161 |
(fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]); |
|
162 |
||
923 | 163 |
(*For use with split_tac and the simplifier*) |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
164 |
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))"; |
923 | 165 |
by (stac surjective_pairing 1); |
166 |
by (stac split 1); |
|
2935 | 167 |
by (Blast_tac 1); |
923 | 168 |
qed "expand_split"; |
169 |
||
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
170 |
(* could be done after split_tac has been speeded up significantly: |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
171 |
simpset := (!simpset setloop split_tac[expand_split]); |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
*) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
175 |
|
923 | 176 |
(** split used as a logical connective or set former **) |
177 |
||
2935 | 178 |
(*These rules are for use with blast_tac. |
923 | 179 |
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
180 |
||
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
181 |
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
1552 | 182 |
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
|
183 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
184 |
qed "splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
185 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
186 |
goal Prod.thy "!!a b c. c a b ==> split c (a,b)"; |
1264 | 187 |
by (Asm_simp_tac 1); |
923 | 188 |
qed "splitI"; |
189 |
||
190 |
val prems = goalw Prod.thy [split_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
191 |
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
923 | 192 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
193 |
qed "splitE"; |
|
194 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
195 |
goal Prod.thy "!!R a b. split R (a,b) ==> R a b"; |
923 | 196 |
by (etac (split RS iffD1) 1); |
197 |
qed "splitD"; |
|
198 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
199 |
goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)"; |
1264 | 200 |
by (Asm_simp_tac 1); |
923 | 201 |
qed "mem_splitI"; |
202 |
||
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
203 |
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
1552 | 204 |
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
|
205 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
206 |
qed "mem_splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
207 |
|
923 | 208 |
val prems = goalw Prod.thy [split_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
209 |
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
923 | 210 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
211 |
qed "mem_splitE"; |
|
212 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
213 |
AddSIs [splitI, splitI2, mem_splitI, mem_splitI2]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
214 |
AddSEs [splitE, mem_splitE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
215 |
|
923 | 216 |
(*** prod_fun -- action of the product functor upon functions ***) |
217 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
218 |
goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
923 | 219 |
by (rtac split 1); |
220 |
qed "prod_fun"; |
|
221 |
||
222 |
goal Prod.thy |
|
223 |
"prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
|
224 |
by (rtac ext 1); |
|
225 |
by (res_inst_tac [("p","x")] PairE 1); |
|
1264 | 226 |
by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1); |
923 | 227 |
qed "prod_fun_compose"; |
228 |
||
3842 | 229 |
goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)"; |
923 | 230 |
by (rtac ext 1); |
231 |
by (res_inst_tac [("p","z")] PairE 1); |
|
1264 | 232 |
by (asm_simp_tac (!simpset addsimps [prod_fun]) 1); |
923 | 233 |
qed "prod_fun_ident"; |
234 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
235 |
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; |
923 | 236 |
by (rtac image_eqI 1); |
237 |
by (rtac (prod_fun RS sym) 1); |
|
238 |
by (resolve_tac prems 1); |
|
239 |
qed "prod_fun_imageI"; |
|
240 |
||
241 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
242 |
"[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
923 | 243 |
\ |] ==> P"; |
244 |
by (rtac (major RS imageE) 1); |
|
245 |
by (res_inst_tac [("p","x")] PairE 1); |
|
246 |
by (resolve_tac prems 1); |
|
2935 | 247 |
by (Blast_tac 2); |
248 |
by (blast_tac (!claset addIs [prod_fun]) 1); |
|
923 | 249 |
qed "prod_fun_imageE"; |
250 |
||
251 |
(*** Disjoint union of a family of sets - Sigma ***) |
|
252 |
||
253 |
qed_goalw "SigmaI" Prod.thy [Sigma_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
254 |
"[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
923 | 255 |
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
256 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
257 |
AddSIs [SigmaI]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
258 |
|
923 | 259 |
(*The general elimination rule*) |
260 |
qed_goalw "SigmaE" Prod.thy [Sigma_def] |
|
261 |
"[| c: Sigma A B; \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
262 |
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
923 | 263 |
\ |] ==> P" |
264 |
(fn major::prems=> |
|
265 |
[ (cut_facts_tac [major] 1), |
|
266 |
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
|
267 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
268 |
(** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
269 |
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A" |
923 | 270 |
(fn [major]=> |
271 |
[ (rtac (major RS SigmaE) 1), |
|
272 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
273 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
274 |
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)" |
923 | 275 |
(fn [major]=> |
276 |
[ (rtac (major RS SigmaE) 1), |
|
277 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
278 |
||
279 |
qed_goal "SigmaE2" Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
280 |
"[| (a,b) : Sigma A B; \ |
923 | 281 |
\ [| a:A; b:B(a) |] ==> P \ |
282 |
\ |] ==> P" |
|
283 |
(fn [major,minor]=> |
|
284 |
[ (rtac minor 1), |
|
285 |
(rtac (major RS SigmaD1) 1), |
|
286 |
(rtac (major RS SigmaD2) 1) ]); |
|
287 |
||
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
288 |
AddSEs [SigmaE2, SigmaE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
289 |
|
1515 | 290 |
val prems = goal Prod.thy |
1642 | 291 |
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; |
1515 | 292 |
by (cut_facts_tac prems 1); |
2935 | 293 |
by (blast_tac (!claset addIs (prems RL [subsetD])) 1); |
1515 | 294 |
qed "Sigma_mono"; |
295 |
||
1618 | 296 |
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}" |
2935 | 297 |
(fn _ => [ (Blast_tac 1) ]); |
1618 | 298 |
|
1642 | 299 |
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}" |
2935 | 300 |
(fn _ => [ (Blast_tac 1) ]); |
1618 | 301 |
|
302 |
Addsimps [Sigma_empty1,Sigma_empty2]; |
|
303 |
||
304 |
goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))"; |
|
2935 | 305 |
by (Blast_tac 1); |
1618 | 306 |
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
|
307 |
AddIffs [mem_Sigma_iff]; |
1618 | 308 |
|
1515 | 309 |
|
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
310 |
(*Suggested by Pierre Chartier*) |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
311 |
goal Prod.thy |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
312 |
"(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; |
2935 | 313 |
by (Blast_tac 1); |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
314 |
qed "UNION_Times_distrib"; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
315 |
|
923 | 316 |
(*** Domain of a relation ***) |
317 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
318 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r"; |
923 | 319 |
by (rtac CollectI 1); |
320 |
by (rtac bexI 1); |
|
321 |
by (rtac (fst_conv RS sym) 1); |
|
322 |
by (resolve_tac prems 1); |
|
323 |
qed "fst_imageI"; |
|
324 |
||
325 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
326 |
"[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P"; |
923 | 327 |
by (rtac (major RS imageE) 1); |
328 |
by (resolve_tac prems 1); |
|
329 |
by (etac ssubst 1); |
|
330 |
by (rtac (surjective_pairing RS subst) 1); |
|
331 |
by (assume_tac 1); |
|
332 |
qed "fst_imageE"; |
|
333 |
||
334 |
(*** Range of a relation ***) |
|
335 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
336 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r"; |
923 | 337 |
by (rtac CollectI 1); |
338 |
by (rtac bexI 1); |
|
339 |
by (rtac (snd_conv RS sym) 1); |
|
340 |
by (resolve_tac prems 1); |
|
341 |
qed "snd_imageI"; |
|
342 |
||
343 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
344 |
"[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P"; |
923 | 345 |
by (rtac (major RS imageE) 1); |
346 |
by (resolve_tac prems 1); |
|
347 |
by (etac ssubst 1); |
|
348 |
by (rtac (surjective_pairing RS subst) 1); |
|
349 |
by (assume_tac 1); |
|
350 |
qed "snd_imageE"; |
|
351 |
||
352 |
(** Exhaustion rule for unit -- a degenerate form of induction **) |
|
353 |
||
354 |
goalw Prod.thy [Unity_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
355 |
"u = ()"; |
2886 | 356 |
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); |
2880 | 357 |
by (rtac (Rep_unit_inverse RS sym) 1); |
923 | 358 |
qed "unit_eq"; |
1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset
|
359 |
|
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset
|
360 |
AddIs [fst_imageI, snd_imageI, prod_fun_imageI]; |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
361 |
AddSEs [fst_imageE, snd_imageE, prod_fun_imageE]; |
923 | 362 |
|
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
363 |
structure Prod_Syntax = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
364 |
struct |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
365 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
366 |
val unitT = Type("unit",[]); |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
367 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
368 |
fun mk_prod (T1,T2) = Type("*", [T1,T2]); |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
369 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
370 |
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
371 |
fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2 |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
372 |
| factors T = [T]; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
373 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
374 |
(*Make a correctly typed ordered pair*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
375 |
fun mk_Pair (t1,t2) = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
376 |
let val T1 = fastype_of t1 |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
377 |
and T2 = fastype_of t2 |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
378 |
in Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2 end; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
379 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
380 |
fun split_const(Ta,Tb,Tc) = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
381 |
Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc); |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
382 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
383 |
(*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
|
384 |
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
|
385 |
of type S.*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
386 |
fun ap_split (Type("*", [T1,T2])) T3 u = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
387 |
split_const(T1,T2,T3) $ |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
388 |
Abs("v", T1, |
2031 | 389 |
ap_split T2 T3 |
390 |
((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ |
|
391 |
Bound 0)) |
|
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
392 |
| ap_split T T3 u = u; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
393 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
394 |
(*Makes a nested tuple from a list, following the product type structure*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
395 |
fun mk_tuple (Type("*", [T1,T2])) tms = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
396 |
mk_Pair (mk_tuple T1 tms, |
2031 | 397 |
mk_tuple T2 (drop (length (factors T1), tms))) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
398 |
| mk_tuple T (t::_) = t; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
399 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
400 |
(*Attempts to remove occurrences of split, and pair-valued parameters*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
401 |
val remove_split = rewrite_rule [split RS eq_reflection] o |
2031 | 402 |
rule_by_tactic (ALLGOALS split_all_tac); |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
403 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
404 |
(*Uncurries any Var of function type in the rule*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
405 |
fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) = |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
406 |
let val T' = factors T1 ---> T2 |
2031 | 407 |
val newt = ap_split T1 T2 (Var(v,T')) |
408 |
val cterm = Thm.cterm_of (#sign(rep_thm rl)) |
|
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
409 |
in |
2031 | 410 |
remove_split (instantiate ([], [(cterm t, cterm newt)]) rl) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
411 |
end |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
412 |
| split_rule_var (t,rl) = rl; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
413 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
414 |
(*Uncurries ALL function variables occurring in a rule's conclusion*) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
415 |
fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl) |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
416 |
|> standard; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
417 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
418 |
end; |