author  paulson 
Fri, 18 Feb 2000 15:35:29 +0100  
changeset 8255  38f96394c099 
parent 8157  b1a458416c92 
child 8261  e4726ac0863a 
permissions  rwrr 
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 

5810  6 
Ordered Pairs, the Cartesian product type, the unit type 
923  7 
*) 
8 

9 
(*This counts as a nonemptiness result for admitting 'a * 'b as a type*) 

5069  10 
Goalw [Prod_def] "Pair_Rep a b : Prod"; 
923  11 
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); 
12 
qed "ProdI"; 

13 

14 
val [major] = goalw Prod.thy [Pair_Rep_def] 

15 
"Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; 

16 
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 

1465  17 
rtac conjI, rtac refl, rtac refl]); 
923  18 
qed "Pair_Rep_inject"; 
19 

5069  20 
Goal "inj_on Abs_Prod Prod"; 
4830  21 
by (rtac inj_on_inverseI 1); 
923  22 
by (etac Abs_Prod_inverse 1); 
4830  23 
qed "inj_on_Abs_Prod"; 
923  24 

5316  25 
val prems = Goalw [Pair_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

26 
"[ (a, b) = (a',b'); [ a=a'; b=b' ] ==> R ] ==> R"; 
4830  27 
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); 
923  28 
by (REPEAT (ares_tac (prems@[ProdI]) 1)); 
29 
qed "Pair_inject"; 

30 

5069  31 
Goal "((a,b) = (a',b')) = (a=a' & b=b')"; 
4089  32 
by (blast_tac (claset() addSEs [Pair_inject]) 1); 
923  33 
qed "Pair_eq"; 
3429  34 
AddIffs [Pair_eq]; 
923  35 

7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

36 
Goalw [fst_def] "fst (a,b) = a"; 
4534  37 
by (Blast_tac 1); 
923  38 
qed "fst_conv"; 
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

39 
Goalw [snd_def] "snd (a,b) = b"; 
4534  40 
by (Blast_tac 1); 
923  41 
qed "snd_conv"; 
4534  42 
Addsimps [fst_conv, snd_conv]; 
923  43 

7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

44 
Goal "fst (x, y) = a ==> x = a"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

45 
by (Asm_full_simp_tac 1); 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

46 
qed "fst_eqD"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

47 
Goal "snd (x, y) = a ==> y = a"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

48 
by (Asm_full_simp_tac 1); 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

49 
qed "snd_eqD"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

50 

5069  51 
Goalw [Pair_def] "? x y. p = (x,y)"; 
923  52 
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); 
53 
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, 

1465  54 
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); 
923  55 
qed "PairE_lemma"; 
56 

5316  57 
val [prem] = Goal "[ !!x y. p = (x,y) ==> Q ] ==> Q"; 
923  58 
by (rtac (PairE_lemma RS exE) 1); 
59 
by (REPEAT (eresolve_tac [prem,exE] 1)); 

60 
qed "PairE"; 

61 

4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset

62 
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

63 
K prune_params_tac]; 
4134  64 

4828  65 
(* Do not add as rewrite rule: invalidates some proofs in IMP *) 
5069  66 
Goal "p = (fst(p),snd(p))"; 
4828  67 
by (pair_tac "p" 1); 
68 
by (Asm_simp_tac 1); 

69 
qed "surjective_pairing"; 

70 

7031  71 
Goal "? x y. z = (x, y)"; 
72 
by (rtac exI 1); 

73 
by (rtac exI 1); 

74 
by (rtac surjective_pairing 1); 

75 
qed "surj_pair"; 

4828  76 
Addsimps [surj_pair]; 
77 

78 

5699  79 
bind_thm ("split_paired_all", 
80 
SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection))); 

4828  81 
(* 
82 
Addsimps [split_paired_all] does not work with simplifier 

83 
because it also affects premises in congrence rules, 

84 
where is can lead to premises of the form !!a b. ... = ?P(a,b) 

85 
which cannot be solved by reflexivity. 

86 
*) 

87 

1301  88 
(* replace parameters of product type by individual component parameters *) 
89 
local 

4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset

90 
fun is_pair (_,Type("*",_)) = true 
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset

91 
 is_pair _ = false; 
4828  92 
fun exists_paired_all prem = exists is_pair (Logic.strip_params prem); 
93 
val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]); 

1301  94 
in 
4828  95 
val split_all_tac = SUBGOAL (fn (prem,i) => 
96 
if exists_paired_all prem then split_tac i else no_tac); 

1301  97 
end; 
98 

4828  99 
claset_ref() := claset() addSWrapper ("split_all_tac", 
100 
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

101 

5069  102 
Goal "(!x. P x) = (!a b. P(a,b))"; 
4650  103 
by (Fast_tac 1); 
1301  104 
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

105 
Addsimps [split_paired_All]; 
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset

106 
(* 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

107 

5715
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset

108 
bind_thm ("prod_induct", 
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset

109 
allI RS (allI RS (split_paired_All RS iffD2)) RS spec); 
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset

110 

5069  111 
Goal "(? x. P x) = (? a b. P(a,b))"; 
4650  112 
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

113 
qed "split_paired_Ex"; 
4534  114 
Addsimps [split_paired_Ex]; 
1301  115 

5069  116 
Goalw [split_def] "split c (a,b) = c a b"; 
4534  117 
by (Simp_tac 1); 
923  118 
qed "split"; 
4534  119 
Addsimps [split]; 
923  120 

7339  121 
(*Subsumes the old split_Pair when f is the identity function*) 
122 
Goal "split (%x y. f(x,y)) = f"; 

123 
by (rtac ext 1); 

124 
by (pair_tac "x" 1); 

4828  125 
by (Simp_tac 1); 
7339  126 
qed "split_Pair_apply"; 
127 

128 
(*Can't be added to simpset: loops!*) 

129 
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))"; 

130 
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1); 

131 
qed "split_paired_Eps"; 

4828  132 

5069  133 
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; 
4828  134 
by (split_all_tac 1); 
1264  135 
by (Asm_simp_tac 1); 
923  136 
qed "Pair_fst_snd_eq"; 
137 

138 
(*Prevents simplification of c: much faster*) 

7031  139 
val [prem] = goal Prod.thy 
140 
"p=q ==> split c p = split c q"; 

141 
by (rtac (prem RS arg_cong) 1); 

142 
qed "split_weak_cong"; 

923  143 

7031  144 
Goal "(%(x,y). f(x,y)) = f"; 
145 
by (rtac ext 1); 

146 
by (split_all_tac 1); 

147 
by (rtac split 1); 

148 
qed "split_eta"; 

1655  149 

7031  150 
val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"; 
151 
by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1); 

152 
qed "cond_split_eta"; 

5294  153 

154 
(*simplification procedure for cond_split_eta. 

155 
using split_eta a rewrite rule is not general enough, and using 

7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

156 
cond_split_eta directly would render some existing proofs very inefficient. 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

157 
similarly for split_beta. *) 
5294  158 
local 
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

159 
fun Pair_pat k 0 (Bound m) = (m = k) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

160 
 Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

161 
m = k+i andalso Pair_pat k (i1) t 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

162 
 Pair_pat _ _ _ = false; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

163 
fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

164 
 no_args k i (t $ u) = no_args k i t andalso no_args k i u 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

165 
 no_args k i (Bound m) = m < k orelse m > k+i 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

166 
 no_args _ _ _ = true; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

167 
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

168 
 split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

169 
 split_pat tp i _ = None; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

170 
fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

171 
(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

172 
(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

173 
fun simproc name patstr = Simplifier.mk_simproc name 
8100  174 
[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termT)]; 
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

175 

affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

176 
val beta_patstr = "split f z"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

177 
val eta_patstr = "split f"; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

178 
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

179 
 beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

180 
(beta_term_pat k i t andalso beta_term_pat k i u) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

181 
 beta_term_pat k i t = no_args k i t; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

182 
fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

183 
 eta_term_pat _ _ _ = false; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

184 
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

185 
 subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

186 
else (subst arg k i t $ subst arg k i u) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

187 
 subst arg k i t = t; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

188 
fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

189 
(case split_pat beta_term_pat 1 t of 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

190 
Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) 
5294  191 
 None => None) 
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

192 
 beta_proc _ _ _ = None; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

193 
fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

194 
(case split_pat eta_term_pat 1 t of 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

195 
Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

196 
 None => None) 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

197 
 eta_proc _ _ _ = None; 
5294  198 
in 
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

199 
val split_beta_proc = simproc "split_beta" beta_patstr beta_proc; 
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

200 
val split_eta_proc = simproc "split_eta" eta_patstr eta_proc; 
5294  201 
end; 
202 

7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset

203 
Addsimprocs [split_beta_proc,split_eta_proc]; 
5294  204 

7031  205 
Goal "(%(x,y). P x y) z = P (fst z) (snd z)"; 
206 
by (stac surjective_pairing 1 THEN rtac split 1); 

207 
qed "split_beta"; 

4134  208 

923  209 
(*For use with split_tac and the simplifier*) 
5069  210 
Goal "R (split c p) = (! x y. p = (x,y) > R (c x y))"; 
923  211 
by (stac surjective_pairing 1); 
212 
by (stac split 1); 

2935  213 
by (Blast_tac 1); 
4830  214 
qed "split_split"; 
923  215 

3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset

216 
(* could be done after split_tac has been speeded up significantly: 
4830  217 
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

218 
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

219 
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

220 
*) 
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset

221 

5069  222 
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; 
4830  223 
by (stac split_split 1); 
4435  224 
by (Simp_tac 1); 
225 
qed "expand_split_asm"; 

226 

923  227 
(** split used as a logical connective or set former **) 
228 

2935  229 
(*These rules are for use with blast_tac. 
923  230 
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) 
231 

5069  232 
Goal "!!p. [ !!a b. p=(a,b) ==> c a b ] ==> split c p"; 
1552  233 
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

234 
by (Asm_simp_tac 1); 
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset

235 
qed "splitI2"; 
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset

236 

7958  237 
Goal "!!p. [ !!a b. (a,b)=p ==> c a b x ] ==> split c p x"; 
238 
by (split_all_tac 1); 

239 
by (Asm_simp_tac 1); 

240 
qed "splitI2'"; 

241 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

242 
Goal "c a b ==> split c (a,b)"; 
1264  243 
by (Asm_simp_tac 1); 
923  244 
qed "splitI"; 
245 

5316  246 
val prems = Goalw [split_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

247 
"[ split c p; !!x y. [ p = (x,y); c x y ] ==> Q ] ==> Q"; 
923  248 
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); 
249 
qed "splitE"; 

250 

8157  251 
val prems = Goalw [split_def] 
252 
"[ split c p z; !!x y. [ p = (x,y); c x y z ] ==> Q ] ==> Q"; 

253 
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); 

254 
qed "splitE'"; 

255 

7031  256 
val major::prems = goal Prod.thy 
257 
"[ Q (split P z); !!x y. [z = (x, y); Q (P x y)] ==> R \ 

258 
\ ] ==> R"; 

259 
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); 

260 
by (rtac (split_beta RS subst) 1 THEN rtac major 1); 

261 
qed "splitE2"; 

4134  262 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

263 
Goal "split R (a,b) ==> R a b"; 
923  264 
by (etac (split RS iffD1) 1); 
265 
qed "splitD"; 

266 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

267 
Goal "z: c a b ==> z: split c (a,b)"; 
1264  268 
by (Asm_simp_tac 1); 
923  269 
qed "mem_splitI"; 
270 

5069  271 
Goal "!!p. [ !!a b. p=(a,b) ==> z: c a b ] ==> z: split c p"; 
1552  272 
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

273 
by (Asm_simp_tac 1); 
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset

274 
qed "mem_splitI2"; 
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset

275 

5316  276 
val prems = Goalw [split_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

277 
"[ z: split c p; !!x y. [ p = (x,y); z: c x y ] ==> Q ] ==> Q"; 
923  278 
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); 
279 
qed "mem_splitE"; 

280 

7958  281 
AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2]; 
8157  282 
AddSEs [splitE, splitE', mem_splitE]; 
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

283 

4534  284 
(* allows simplifications of nested splits in case of independent predicates *) 
5069  285 
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; 
4534  286 
by (rtac ext 1); 
287 
by (Blast_tac 1); 

288 
qed "split_part"; 

289 
Addsimps [split_part]; 

290 

5069  291 
Goal "(@(x',y'). x = x' & y = y') = (x,y)"; 
4534  292 
by (Blast_tac 1); 
293 
qed "Eps_split_eq"; 

294 
Addsimps [Eps_split_eq]; 

295 
(* 

296 
the following would be slightly more general, 

297 
but cannot be used as rewrite rule: 

298 
### Cannot add premise as rewrite rule because it contains (type) unknowns: 

299 
### ?y = .x 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

300 
Goal "[ P y; !!x. P x ==> x = y ] ==> (@(x',y). x = x' & P y) = (x,y)"; 
4534  301 
by (rtac select_equality 1); 
302 
by ( Simp_tac 1); 

303 
by (split_all_tac 1); 

304 
by (Asm_full_simp_tac 1); 

305 
qed "Eps_split_eq"; 

306 
*) 

307 

923  308 
(*** prod_fun  action of the product functor upon functions ***) 
309 

5069  310 
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; 
923  311 
by (rtac split 1); 
312 
qed "prod_fun"; 

4521  313 
Addsimps [prod_fun]; 
923  314 

5278  315 
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; 
923  316 
by (rtac ext 1); 
4828  317 
by (pair_tac "x" 1); 
4521  318 
by (Asm_simp_tac 1); 
923  319 
qed "prod_fun_compose"; 
320 

5069  321 
Goal "prod_fun (%x. x) (%y. y) = (%z. z)"; 
923  322 
by (rtac ext 1); 
4828  323 
by (pair_tac "z" 1); 
4521  324 
by (Asm_simp_tac 1); 
923  325 
qed "prod_fun_ident"; 
4521  326 
Addsimps [prod_fun_ident]; 
923  327 

5316  328 
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; 
923  329 
by (rtac image_eqI 1); 
330 
by (rtac (prod_fun RS sym) 1); 

5316  331 
by (assume_tac 1); 
923  332 
qed "prod_fun_imageI"; 
333 

5316  334 
val major::prems = Goal 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

335 
"[ c: (prod_fun f g)``r; !!x y. [ c=(f(x),g(y)); (x,y):r ] ==> P \ 
923  336 
\ ] ==> P"; 
337 
by (rtac (major RS imageE) 1); 

338 
by (res_inst_tac [("p","x")] PairE 1); 

339 
by (resolve_tac prems 1); 

2935  340 
by (Blast_tac 2); 
4089  341 
by (blast_tac (claset() addIs [prod_fun]) 1); 
923  342 
qed "prod_fun_imageE"; 
343 

5788  344 
AddIs [prod_fun_imageI]; 
345 
AddSEs [prod_fun_imageE]; 

346 

4521  347 

923  348 
(*** Disjoint union of a family of sets  Sigma ***) 
349 

7031  350 
Goalw [Sigma_def] "[ a:A; b:B(a) ] ==> (a,b) : Sigma A B"; 
351 
by (REPEAT (ares_tac [singletonI,UN_I] 1)); 

352 
qed "SigmaI"; 

923  353 

2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

354 
AddSIs [SigmaI]; 
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

355 

923  356 
(*The general elimination rule*) 
7031  357 
val major::prems = Goalw [Sigma_def] 
923  358 
"[ c: Sigma A B; \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

359 
\ !!x y.[ x:A; y:B(x); c=(x,y) ] ==> P \ 
7031  360 
\ ] ==> P"; 
361 
by (cut_facts_tac [major] 1); 

362 
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; 

363 
qed "SigmaE"; 

923  364 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

365 
(** Elimination of (a,b):A*B  introduces no eigenvariables **) 
7007  366 

367 
Goal "(a,b) : Sigma A B ==> a : A"; 

368 
by (etac SigmaE 1); 

369 
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; 

370 
qed "SigmaD1"; 

923  371 

7007  372 
Goal "(a,b) : Sigma A B ==> b : B(a)"; 
373 
by (etac SigmaE 1); 

374 
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; 

375 
qed "SigmaD2"; 

923  376 

7007  377 
val [major,minor]= goal Prod.thy 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

378 
"[ (a,b) : Sigma A B; \ 
923  379 
\ [ a:A; b:B(a) ] ==> P \ 
7007  380 
\ ] ==> P"; 
381 
by (rtac minor 1); 

382 
by (rtac (major RS SigmaD1) 1); 

383 
by (rtac (major RS SigmaD2) 1) ; 

384 
qed "SigmaE2"; 

923  385 

2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

386 
AddSEs [SigmaE2, SigmaE]; 
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

387 

5316  388 
val prems = Goal 
1642  389 
"[ A<=C; !!x. x:A ==> B x <= D x ] ==> Sigma A B <= Sigma C D"; 
1515  390 
by (cut_facts_tac prems 1); 
4089  391 
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); 
1515  392 
qed "Sigma_mono"; 
393 

7007  394 
Goal "Sigma {} B = {}"; 
395 
by (Blast_tac 1) ; 

396 
qed "Sigma_empty1"; 

1618  397 

7007  398 
Goal "A Times {} = {}"; 
399 
by (Blast_tac 1) ; 

400 
qed "Sigma_empty2"; 

1618  401 

402 
Addsimps [Sigma_empty1,Sigma_empty2]; 

403 

5069  404 
Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; 
2935  405 
by (Blast_tac 1); 
1618  406 
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

407 
AddIffs [mem_Sigma_iff]; 
1618  408 

6016  409 
Goal "x:C ==> (A Times C <= B Times C) = (A <= B)"; 
410 
by (Blast_tac 1); 

411 
qed "Times_subset_cancel2"; 

412 

413 
Goal "x:C ==> (A Times C = B Times C) = (A = B)"; 

414 
by (blast_tac (claset() addEs [equalityE]) 1); 

415 
qed "Times_eq_cancel2"; 

416 

5810  417 

418 
(*** Complex rules for Sigma ***) 

419 

7031  420 
Goal "{(a,b). P a & Q b} = Collect P Times Collect Q"; 
421 
by (Blast_tac 1); 

422 
qed "Collect_split"; 

423 

4534  424 
Addsimps [Collect_split]; 
1515  425 

2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

426 
(*Suggested by Pierre Chartier*) 
5278  427 
Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; 
2935  428 
by (Blast_tac 1); 
6830
f8aed3706af7
renamed UNION_... to UN_... (to fit the convention)
paulson
parents:
6394
diff
changeset

429 
qed "UN_Times_distrib"; 
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset

430 

6016  431 
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"; 
5810  432 
by (Fast_tac 1); 
6016  433 
qed "split_paired_Ball_Sigma"; 
434 
Addsimps [split_paired_Ball_Sigma]; 

5810  435 

6016  436 
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"; 
5810  437 
by (Fast_tac 1); 
6016  438 
qed "split_paired_Bex_Sigma"; 
439 
Addsimps [split_paired_Bex_Sigma]; 

5810  440 

441 
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"; 

442 
by (Blast_tac 1); 

443 
qed "Sigma_Un_distrib1"; 

444 

445 
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"; 

446 
by (Blast_tac 1); 

447 
qed "Sigma_Un_distrib2"; 

448 

449 
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"; 

450 
by (Blast_tac 1); 

451 
qed "Sigma_Int_distrib1"; 

452 

453 
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"; 

454 
by (Blast_tac 1); 

455 
qed "Sigma_Int_distrib2"; 

456 

457 
Goal "(SIGMA i:I  J. C(i)) = (SIGMA i:I. C(i))  (SIGMA j:J. C(j))"; 

458 
by (Blast_tac 1); 

459 
qed "Sigma_Diff_distrib1"; 

460 

461 
Goal "(SIGMA i:I. A(i)  B(i)) = (SIGMA i:I. A(i))  (SIGMA i:I. B(i))"; 

462 
by (Blast_tac 1); 

463 
qed "Sigma_Diff_distrib2"; 

464 

6016  465 
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)"; 
466 
by (Blast_tac 1); 

467 
qed "Sigma_Union"; 

468 

8255  469 
(*Nondependent versions are needed to avoid the need for higherorder 
470 
matching, especially when the rules are reoriented*) 

471 
Goal "(A Un B) Times C = (A Times C) Un (B Times C)"; 

472 
by (Blast_tac 1); 

473 
qed "Times_Un_distrib1"; 

474 

475 
Goal "(A Int B) Times C = (A Times C) Int (B Times C)"; 

476 
by (Blast_tac 1); 

477 
qed "Times_Int_distrib1"; 

478 

479 
Goal "(A  B) Times C = (A Times C)  (B Times C)"; 

480 
by (Blast_tac 1); 

481 
qed "Times_Diff_distrib1"; 

5810  482 

923  483 
(** Exhaustion rule for unit  a degenerate form of induction **) 
484 

5069  485 
Goalw [Unity_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

486 
"u = ()"; 
2886  487 
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); 
2880  488 
by (rtac (Rep_unit_inverse RS sym) 1); 
923  489 
qed "unit_eq"; 
1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset

490 

5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

491 
(*simplification procedure for unit_eq. 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

492 
Cannot use this rule directly  it loops!*) 
5083  493 
local 
6394  494 
val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT)); 
5553  495 
val unit_meta_eq = standard (mk_meta_eq unit_eq); 
5083  496 
fun proc _ _ t = 
497 
if HOLogic.is_unit t then None 

498 
else Some unit_meta_eq; 

499 
in 

500 
val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; 

501 
end; 

502 

503 
Addsimprocs [unit_eq_proc]; 

504 

505 

5761  506 
Goal "P () ==> P x"; 
507 
by (Simp_tac 1); 

508 
qed "unit_induct"; 

509 

510 

5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

511 
(*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

512 
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

513 
Goal "(%u::unit. f()) = f"; 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

514 
by (rtac ext 1); 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

515 
by (Simp_tac 1); 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

516 
qed "unit_abs_eta_conv"; 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

517 
Addsimps [unit_abs_eta_conv]; 
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

518 

e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset

519 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

520 
(*Attempts to remove occurrences of split, and pairvalued parameters*) 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

521 
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

522 
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

523 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

524 
local 
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

525 

f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

526 
(*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

527 
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

528 
of type S.*) 
5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

529 
fun ap_split (Type ("*", [T1, T2])) T3 u = 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

530 
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

531 
Abs("v", T1, 
2031  532 
ap_split T2 T3 
5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

533 
((ap_split T1 (HOLogic.prodT_factors T2 > T3) (incr_boundvars 1 u)) $ 
2031  534 
Bound 0)) 
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

535 
 ap_split T T3 u = u; 
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

536 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

537 
(*Curries any Var of function type in the rule*) 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

538 
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

539 
let val T' = HOLogic.prodT_factors T1 > T2 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

540 
val newt = ap_split T1 T2 (Var (v, T')) 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

541 
val cterm = Thm.cterm_of (#sign (rep_thm rl)) 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

542 
in 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

543 
instantiate ([], [(cterm t, cterm newt)]) rl 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

544 
end 
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

545 
 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

546 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

547 
in 
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

548 

5096
84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

549 
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

550 

84b00be693b4
Moved most of the Prod_Syntax  stuff to HOLogic.
berghofe
parents:
5088
diff
changeset

551 
(*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

552 
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

553 
> standard; 
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

554 

f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset

555 
end; 
5810  556 

557 