moved to Product_Type_lemmas.ML
authorwenzelm
Thu Feb 01 21:28:23 2001 +0100 (2001-02-01)
changeset 110288cf44cbe22e8
parent 11027 17e9f0ba15ee
child 11029 a221d8a9413c
moved to Product_Type_lemmas.ML
src/HOL/Product_Type.ML
     1.1 --- a/src/HOL/Product_Type.ML	Thu Feb 01 20:56:21 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,645 +0,0 @@
     1.4 -(*  Title:      HOL/Product_Type.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Ordered Pairs, the Cartesian product type, the unit type
    1.10 -*)
    1.11 -
    1.12 -(** unit **)
    1.13 -
    1.14 -Goalw [Unity_def]
    1.15 -    "u = ()";
    1.16 -by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
    1.17 -by (rtac (Rep_unit_inverse RS sym) 1);
    1.18 -qed "unit_eq";
    1.19 -
    1.20 -(*simplification procedure for unit_eq.
    1.21 -  Cannot use this rule directly -- it loops!*)
    1.22 -local
    1.23 -  val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
    1.24 -  val unit_meta_eq = standard (mk_meta_eq unit_eq);
    1.25 -  fun proc _ _ t =
    1.26 -    if HOLogic.is_unit t then None
    1.27 -    else Some unit_meta_eq;
    1.28 -in
    1.29 -  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
    1.30 -end;
    1.31 -
    1.32 -Addsimprocs [unit_eq_proc];
    1.33 -
    1.34 -Goal "(!!x::unit. PROP P x) == PROP P ()";
    1.35 -by (Simp_tac 1);
    1.36 -qed "unit_all_eq1";
    1.37 -
    1.38 -Goal "(!!x::unit. PROP P) == PROP P";
    1.39 -by (rtac triv_forall_equality 1);
    1.40 -qed "unit_all_eq2";
    1.41 -
    1.42 -Goal "P () ==> P x";
    1.43 -by (Simp_tac 1);
    1.44 -qed "unit_induct";
    1.45 -
    1.46 -(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
    1.47 -  replacing it by f rather than by %u.f(). *)
    1.48 -Goal "(%u::unit. f()) = f";
    1.49 -by (rtac ext 1);
    1.50 -by (Simp_tac 1);
    1.51 -qed "unit_abs_eta_conv";
    1.52 -Addsimps [unit_abs_eta_conv];
    1.53 -
    1.54 -
    1.55 -(** prod **)
    1.56 -
    1.57 -Goalw [Prod_def] "Pair_Rep a b : Prod";
    1.58 -by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
    1.59 -qed "ProdI";
    1.60 -
    1.61 -Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
    1.62 -by (dtac (fun_cong RS fun_cong) 1);
    1.63 -by (Blast_tac 1);
    1.64 -qed "Pair_Rep_inject";
    1.65 -
    1.66 -Goal "inj_on Abs_Prod Prod";
    1.67 -by (rtac inj_on_inverseI 1);
    1.68 -by (etac Abs_Prod_inverse 1);
    1.69 -qed "inj_on_Abs_Prod";
    1.70 -
    1.71 -val prems = Goalw [Pair_def]
    1.72 -    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    1.73 -by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
    1.74 -by (REPEAT (ares_tac (prems@[ProdI]) 1));
    1.75 -qed "Pair_inject";
    1.76 -
    1.77 -Goal "((a,b) = (a',b')) = (a=a' & b=b')";
    1.78 -by (blast_tac (claset() addSEs [Pair_inject]) 1);
    1.79 -qed "Pair_eq";
    1.80 -AddIffs [Pair_eq];
    1.81 -
    1.82 -Goalw [fst_def] "fst (a,b) = a";
    1.83 -by (Blast_tac 1);
    1.84 -qed "fst_conv";
    1.85 -Goalw [snd_def] "snd (a,b) = b";
    1.86 -by (Blast_tac 1);
    1.87 -qed "snd_conv";
    1.88 -Addsimps [fst_conv, snd_conv];
    1.89 -
    1.90 -Goal "fst (x, y) = a ==> x = a";
    1.91 -by (Asm_full_simp_tac 1);
    1.92 -qed "fst_eqD";
    1.93 -Goal "snd (x, y) = a ==> y = a";
    1.94 -by (Asm_full_simp_tac 1);
    1.95 -qed "snd_eqD";
    1.96 -
    1.97 -Goalw [Pair_def] "? x y. p = (x,y)";
    1.98 -by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
    1.99 -by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
   1.100 -           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
   1.101 -qed "PairE_lemma";
   1.102 -
   1.103 -val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
   1.104 -by (rtac (PairE_lemma RS exE) 1);
   1.105 -by (REPEAT (eresolve_tac [prem,exE] 1));
   1.106 -qed "PairE";
   1.107 -
   1.108 -fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
   1.109 -                         K prune_params_tac];
   1.110 -
   1.111 -(* Do not add as rewrite rule: invalidates some proofs in IMP *)
   1.112 -Goal "p = (fst(p),snd(p))";
   1.113 -by (pair_tac "p" 1);
   1.114 -by (Asm_simp_tac 1);
   1.115 -qed "surjective_pairing";
   1.116 -Addsimps [surjective_pairing RS sym];
   1.117 -
   1.118 -Goal "? x y. z = (x, y)";
   1.119 -by (rtac exI 1);
   1.120 -by (rtac exI 1);
   1.121 -by (rtac surjective_pairing 1);
   1.122 -qed "surj_pair";
   1.123 -Addsimps [surj_pair];
   1.124 -
   1.125 -
   1.126 -bind_thm ("split_paired_all",
   1.127 -  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
   1.128 -bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
   1.129 -
   1.130 -(*
   1.131 -Addsimps [split_paired_all] does not work with simplifier
   1.132 -because it also affects premises in congrence rules,
   1.133 -where is can lead to premises of the form !!a b. ... = ?P(a,b)
   1.134 -which cannot be solved by reflexivity.
   1.135 -*)
   1.136 -
   1.137 -(* replace parameters of product type by individual component parameters *)
   1.138 -local
   1.139 -  fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
   1.140 -        can HOLogic.dest_prodT T orelse exists_paired_all t
   1.141 -    | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
   1.142 -    | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
   1.143 -    | exists_paired_all _ = false;
   1.144 -  val ss = HOL_basic_ss
   1.145 -    addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
   1.146 -    addsimprocs [unit_eq_proc];
   1.147 -in
   1.148 -  val split_all_tac = SUBGOAL (fn (t, i) =>
   1.149 -    if exists_paired_all t then full_simp_tac ss i else no_tac);
   1.150 -  fun split_all th =
   1.151 -    if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
   1.152 -end;
   1.153 -
   1.154 -claset_ref() := claset()
   1.155 -  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
   1.156 -
   1.157 -Goal "(!x. P x) = (!a b. P(a,b))";
   1.158 -by (Fast_tac 1);
   1.159 -qed "split_paired_All";
   1.160 -Addsimps [split_paired_All];
   1.161 -(* AddIffs is not a good idea because it makes Blast_tac loop *)
   1.162 -
   1.163 -bind_thm ("prod_induct",
   1.164 -  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
   1.165 -
   1.166 -Goal "(? x. P x) = (? a b. P(a,b))";
   1.167 -by (Fast_tac 1);
   1.168 -qed "split_paired_Ex";
   1.169 -Addsimps [split_paired_Ex];
   1.170 -
   1.171 -Goalw [split_def] "split c (a,b) = c a b";
   1.172 -by (Simp_tac 1);
   1.173 -qed "split_conv";
   1.174 -Addsimps [split_conv];
   1.175 -(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
   1.176 -
   1.177 -(*Subsumes the old split_Pair when f is the identity function*)
   1.178 -Goal "split (%x y. f(x,y)) = f";
   1.179 -by (rtac ext 1);
   1.180 -by (pair_tac "x" 1);
   1.181 -by (Simp_tac 1);
   1.182 -qed "split_Pair_apply";
   1.183 -
   1.184 -(*Can't be added to simpset: loops!*)
   1.185 -Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
   1.186 -by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
   1.187 -qed "split_paired_Eps";
   1.188 -
   1.189 -Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
   1.190 -by (split_all_tac 1);
   1.191 -by (Asm_simp_tac 1);
   1.192 -qed "Pair_fst_snd_eq";
   1.193 -
   1.194 -Goal "fst p = fst q ==> snd p = snd q ==> p = q";
   1.195 -by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
   1.196 -qed "prod_eqI";
   1.197 -AddXIs [prod_eqI];
   1.198 -
   1.199 -(*Prevents simplification of c: much faster*)
   1.200 -Goal "p=q ==> split c p = split c q";
   1.201 -by (etac arg_cong 1);
   1.202 -qed "split_weak_cong";
   1.203 -
   1.204 -Goal "(%(x,y). f(x,y)) = f";
   1.205 -by (rtac ext 1);
   1.206 -by (split_all_tac 1);
   1.207 -by (rtac split_conv 1);
   1.208 -qed "split_eta";
   1.209 -
   1.210 -val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
   1.211 -by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
   1.212 -qed "cond_split_eta";
   1.213 -
   1.214 -(*simplification procedure for cond_split_eta.
   1.215 -  using split_eta a rewrite rule is not general enough, and using
   1.216 -  cond_split_eta directly would render some existing proofs very inefficient.
   1.217 -  similarly for split_beta. *)
   1.218 -local
   1.219 -  fun  Pair_pat k 0 (Bound m) = (m = k)
   1.220 -  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
   1.221 -                        m = k+i andalso Pair_pat k (i-1) t
   1.222 -  |    Pair_pat _ _ _ = false;
   1.223 -  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
   1.224 -  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
   1.225 -  |   no_args k i (Bound m) = m < k orelse m > k+i
   1.226 -  |   no_args _ _ _ = true;
   1.227 -  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
   1.228 -  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   1.229 -  |   split_pat tp i _ = None;
   1.230 -  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
   1.231 -        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
   1.232 -        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   1.233 -  val sign = sign_of (the_context ());
   1.234 -  fun simproc name patstr = Simplifier.mk_simproc name
   1.235 -                [Thm.read_cterm sign (patstr, HOLogic.termT)];
   1.236 -
   1.237 -  val beta_patstr = "split f z";
   1.238 -  val  eta_patstr = "split f";
   1.239 -  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   1.240 -  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
   1.241 -                        (beta_term_pat k i t andalso beta_term_pat k i u)
   1.242 -  |   beta_term_pat k i t = no_args k i t;
   1.243 -  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
   1.244 -  |    eta_term_pat _ _ _ = false;
   1.245 -  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
   1.246 -  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
   1.247 -                              else (subst arg k i t $ subst arg k i u)
   1.248 -  |   subst arg k i t = t;
   1.249 -  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
   1.250 -        (case split_pat beta_term_pat 1 t of
   1.251 -        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
   1.252 -        | None => None)
   1.253 -  |   beta_proc _ _ _ = None;
   1.254 -  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
   1.255 -        (case split_pat eta_term_pat 1 t of
   1.256 -          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
   1.257 -        | None => None)
   1.258 -  |   eta_proc _ _ _ = None;
   1.259 -in
   1.260 -  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
   1.261 -  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
   1.262 -end;
   1.263 -
   1.264 -Addsimprocs [split_beta_proc,split_eta_proc];
   1.265 -
   1.266 -Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
   1.267 -by (stac surjective_pairing 1 THEN rtac split_conv 1);
   1.268 -qed "split_beta";
   1.269 -
   1.270 -(*For use with split_tac and the simplifier*)
   1.271 -Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
   1.272 -by (stac surjective_pairing 1);
   1.273 -by (stac split_conv 1);
   1.274 -by (Blast_tac 1);
   1.275 -qed "split_split";
   1.276 -
   1.277 -(* could be done after split_tac has been speeded up significantly:
   1.278 -simpset_ref() := simpset() addsplits [split_split];
   1.279 -   precompute the constants involved and don't do anything unless
   1.280 -   the current goal contains one of those constants
   1.281 -*)
   1.282 -
   1.283 -Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
   1.284 -by (stac split_split 1);
   1.285 -by (Simp_tac 1);
   1.286 -qed "split_split_asm";
   1.287 -
   1.288 -(** split used as a logical connective or set former **)
   1.289 -
   1.290 -(*These rules are for use with blast_tac.
   1.291 -  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   1.292 -
   1.293 -Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   1.294 -by (split_all_tac 1);
   1.295 -by (Asm_simp_tac 1);
   1.296 -qed "splitI2";
   1.297 -
   1.298 -Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
   1.299 -by (split_all_tac 1);
   1.300 -by (Asm_simp_tac 1);
   1.301 -qed "splitI2'";
   1.302 -
   1.303 -Goal "c a b ==> split c (a,b)";
   1.304 -by (Asm_simp_tac 1);
   1.305 -qed "splitI";
   1.306 -
   1.307 -val prems = Goalw [split_def]
   1.308 -    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   1.309 -by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   1.310 -qed "splitE";
   1.311 -
   1.312 -val prems = Goalw [split_def]
   1.313 -    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
   1.314 -by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   1.315 -qed "splitE'";
   1.316 -
   1.317 -val major::prems = Goal
   1.318 -    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
   1.319 -\    |] ==> R";
   1.320 -by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   1.321 -by (rtac (split_beta RS subst) 1 THEN rtac major 1);
   1.322 -qed "splitE2";
   1.323 -
   1.324 -Goal "split R (a,b) ==> R a b";
   1.325 -by (etac (split_conv RS iffD1) 1);
   1.326 -qed "splitD";
   1.327 -
   1.328 -Goal "z: c a b ==> z: split c (a,b)";
   1.329 -by (Asm_simp_tac 1);
   1.330 -qed "mem_splitI";
   1.331 -
   1.332 -Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   1.333 -by (split_all_tac 1);
   1.334 -by (Asm_simp_tac 1);
   1.335 -qed "mem_splitI2";
   1.336 -
   1.337 -val prems = Goalw [split_def]
   1.338 -    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   1.339 -by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   1.340 -qed "mem_splitE";
   1.341 -
   1.342 -AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
   1.343 -AddSEs [splitE, splitE', mem_splitE];
   1.344 -
   1.345 -Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
   1.346 -by (rtac ext 1);
   1.347 -by (Fast_tac 1);
   1.348 -qed "split_eta_SetCompr";
   1.349 -Addsimps [split_eta_SetCompr];
   1.350 -
   1.351 -Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
   1.352 -br ext 1;
   1.353 -by (Fast_tac 1);
   1.354 -qed "split_eta_SetCompr2";
   1.355 -Addsimps [split_eta_SetCompr2];
   1.356 -
   1.357 -(* allows simplifications of nested splits in case of independent predicates *)
   1.358 -Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
   1.359 -by (rtac ext 1);
   1.360 -by (Blast_tac 1);
   1.361 -qed "split_part";
   1.362 -Addsimps [split_part];
   1.363 -
   1.364 -Goal "(@(x',y'). x = x' & y = y') = (x,y)";
   1.365 -by (Blast_tac 1);
   1.366 -qed "Eps_split_eq";
   1.367 -Addsimps [Eps_split_eq];
   1.368 -(*
   1.369 -the following  would be slightly more general,
   1.370 -but cannot be used as rewrite rule:
   1.371 -### Cannot add premise as rewrite rule because it contains (type) unknowns:
   1.372 -### ?y = .x
   1.373 -Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   1.374 -by (rtac some_equality 1);
   1.375 -by ( Simp_tac 1);
   1.376 -by (split_all_tac 1);
   1.377 -by (Asm_full_simp_tac 1);
   1.378 -qed "Eps_split_eq";
   1.379 -*)
   1.380 -
   1.381 -(*** prod_fun -- action of the product functor upon functions ***)
   1.382 -
   1.383 -Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   1.384 -by (rtac split_conv 1);
   1.385 -qed "prod_fun";
   1.386 -Addsimps [prod_fun];
   1.387 -
   1.388 -Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   1.389 -by (rtac ext 1);
   1.390 -by (pair_tac "x" 1);
   1.391 -by (Asm_simp_tac 1);
   1.392 -qed "prod_fun_compose";
   1.393 -
   1.394 -Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
   1.395 -by (rtac ext 1);
   1.396 -by (pair_tac "z" 1);
   1.397 -by (Asm_simp_tac 1);
   1.398 -qed "prod_fun_ident";
   1.399 -Addsimps [prod_fun_ident];
   1.400 -
   1.401 -Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
   1.402 -by (rtac image_eqI 1);
   1.403 -by (rtac (prod_fun RS sym) 1);
   1.404 -by (assume_tac 1);
   1.405 -qed "prod_fun_imageI";
   1.406 -
   1.407 -val major::prems = Goal
   1.408 -    "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   1.409 -\    |] ==> P";
   1.410 -by (rtac (major RS imageE) 1);
   1.411 -by (res_inst_tac [("p","x")] PairE 1);
   1.412 -by (resolve_tac prems 1);
   1.413 -by (Blast_tac 2);
   1.414 -by (blast_tac (claset() addIs [prod_fun]) 1);
   1.415 -qed "prod_fun_imageE";
   1.416 -
   1.417 -AddIs  [prod_fun_imageI];
   1.418 -AddSEs [prod_fun_imageE];
   1.419 -
   1.420 -
   1.421 -(*** Disjoint union of a family of sets - Sigma ***)
   1.422 -
   1.423 -Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
   1.424 -by (REPEAT (ares_tac [singletonI,UN_I] 1));
   1.425 -qed "SigmaI";
   1.426 -
   1.427 -AddSIs [SigmaI];
   1.428 -
   1.429 -(*The general elimination rule*)
   1.430 -val major::prems = Goalw [Sigma_def]
   1.431 -    "[| c: Sigma A B;  \
   1.432 -\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   1.433 -\    |] ==> P";
   1.434 -by (cut_facts_tac [major] 1);
   1.435 -by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
   1.436 -qed "SigmaE";
   1.437 -
   1.438 -(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   1.439 -
   1.440 -Goal "(a,b) : Sigma A B ==> a : A";
   1.441 -by (etac SigmaE 1);
   1.442 -by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
   1.443 -qed "SigmaD1";
   1.444 -
   1.445 -Goal "(a,b) : Sigma A B ==> b : B(a)";
   1.446 -by (etac SigmaE 1);
   1.447 -by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
   1.448 -qed "SigmaD2";
   1.449 -
   1.450 -val [major,minor]= Goal
   1.451 -    "[| (a,b) : Sigma A B;    \
   1.452 -\       [| a:A;  b:B(a) |] ==> P   \
   1.453 -\    |] ==> P";
   1.454 -by (rtac minor 1);
   1.455 -by (rtac (major RS SigmaD1) 1);
   1.456 -by (rtac (major RS SigmaD2) 1) ;
   1.457 -qed "SigmaE2";
   1.458 -
   1.459 -AddSEs [SigmaE2, SigmaE];
   1.460 -
   1.461 -val prems = Goal
   1.462 -    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   1.463 -by (cut_facts_tac prems 1);
   1.464 -by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   1.465 -qed "Sigma_mono";
   1.466 -
   1.467 -Goal "Sigma {} B = {}";
   1.468 -by (Blast_tac 1) ;
   1.469 -qed "Sigma_empty1";
   1.470 -
   1.471 -Goal "A <*> {} = {}";
   1.472 -by (Blast_tac 1) ;
   1.473 -qed "Sigma_empty2";
   1.474 -
   1.475 -Addsimps [Sigma_empty1,Sigma_empty2];
   1.476 -
   1.477 -Goal "UNIV <*> UNIV = UNIV";
   1.478 -by Auto_tac;
   1.479 -qed "UNIV_Times_UNIV";
   1.480 -Addsimps [UNIV_Times_UNIV];
   1.481 -
   1.482 -Goal "- (UNIV <*> A) = UNIV <*> (-A)";
   1.483 -by Auto_tac;
   1.484 -qed "Compl_Times_UNIV1";
   1.485 -
   1.486 -Goal "- (A <*> UNIV) = (-A) <*> UNIV";
   1.487 -by Auto_tac;
   1.488 -qed "Compl_Times_UNIV2";
   1.489 -
   1.490 -Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
   1.491 -
   1.492 -Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
   1.493 -by (Blast_tac 1);
   1.494 -qed "mem_Sigma_iff";
   1.495 -AddIffs [mem_Sigma_iff];
   1.496 -
   1.497 -Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
   1.498 -by (Blast_tac 1);
   1.499 -qed "Times_subset_cancel2";
   1.500 -
   1.501 -Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
   1.502 -by (blast_tac (claset() addEs [equalityE]) 1);
   1.503 -qed "Times_eq_cancel2";
   1.504 -
   1.505 -Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
   1.506 -by (Fast_tac 1);
   1.507 -qed "SetCompr_Sigma_eq";
   1.508 -
   1.509 -(*** Complex rules for Sigma ***)
   1.510 -
   1.511 -Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
   1.512 -by (Blast_tac 1);
   1.513 -qed "Collect_split";
   1.514 -
   1.515 -Addsimps [Collect_split];
   1.516 -
   1.517 -(*Suggested by Pierre Chartier*)
   1.518 -Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
   1.519 -by (Blast_tac 1);
   1.520 -qed "UN_Times_distrib";
   1.521 -
   1.522 -Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
   1.523 -by (Fast_tac 1);
   1.524 -qed "split_paired_Ball_Sigma";
   1.525 -Addsimps [split_paired_Ball_Sigma];
   1.526 -
   1.527 -Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
   1.528 -by (Fast_tac 1);
   1.529 -qed "split_paired_Bex_Sigma";
   1.530 -Addsimps [split_paired_Bex_Sigma];
   1.531 -
   1.532 -Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
   1.533 -by (Blast_tac 1);
   1.534 -qed "Sigma_Un_distrib1";
   1.535 -
   1.536 -Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
   1.537 -by (Blast_tac 1);
   1.538 -qed "Sigma_Un_distrib2";
   1.539 -
   1.540 -Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
   1.541 -by (Blast_tac 1);
   1.542 -qed "Sigma_Int_distrib1";
   1.543 -
   1.544 -Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
   1.545 -by (Blast_tac 1);
   1.546 -qed "Sigma_Int_distrib2";
   1.547 -
   1.548 -Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
   1.549 -by (Blast_tac 1);
   1.550 -qed "Sigma_Diff_distrib1";
   1.551 -
   1.552 -Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
   1.553 -by (Blast_tac 1);
   1.554 -qed "Sigma_Diff_distrib2";
   1.555 -
   1.556 -Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
   1.557 -by (Blast_tac 1);
   1.558 -qed "Sigma_Union";
   1.559 -
   1.560 -(*Non-dependent versions are needed to avoid the need for higher-order
   1.561 -  matching, especially when the rules are re-oriented*)
   1.562 -Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
   1.563 -by (Blast_tac 1);
   1.564 -qed "Times_Un_distrib1";
   1.565 -
   1.566 -Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
   1.567 -by (Blast_tac 1);
   1.568 -qed "Times_Int_distrib1";
   1.569 -
   1.570 -Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
   1.571 -by (Blast_tac 1);
   1.572 -qed "Times_Diff_distrib1";
   1.573 -
   1.574 -
   1.575 -(*Attempts to remove occurrences of split, and pair-valued parameters*)
   1.576 -val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
   1.577 -
   1.578 -local
   1.579 -
   1.580 -(*In ap_split S T u, term u expects separate arguments for the factors of S,
   1.581 -  with result type T.  The call creates a new term expecting one argument
   1.582 -  of type S.*)
   1.583 -fun ap_split (Type ("*", [T1, T2])) T3 u =
   1.584 -      HOLogic.split_const (T1, T2, T3) $
   1.585 -      Abs("v", T1,
   1.586 -          ap_split T2 T3
   1.587 -             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
   1.588 -              Bound 0))
   1.589 -  | ap_split T T3 u = u;
   1.590 -
   1.591 -(*Curries any Var of function type in the rule*)
   1.592 -fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
   1.593 -      let val T' = HOLogic.prodT_factors T1 ---> T2
   1.594 -          val newt = ap_split T1 T2 (Var (v, T'))
   1.595 -          val cterm = Thm.cterm_of (#sign (rep_thm rl))
   1.596 -      in
   1.597 -          instantiate ([], [(cterm t, cterm newt)]) rl
   1.598 -      end
   1.599 -  | split_rule_var' (t, rl) = rl;
   1.600 -
   1.601 -(*** Complete splitting of partially splitted rules ***)
   1.602 -
   1.603 -fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
   1.604 -      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
   1.605 -        (incr_boundvars 1 u) $ Bound 0))
   1.606 -  | ap_split' _ _ u = u;
   1.607 -
   1.608 -fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
   1.609 -      let
   1.610 -        val cterm = Thm.cterm_of (#sign (rep_thm rl))
   1.611 -        val (Us', U') = strip_type T;
   1.612 -        val Us = take (length ts, Us');
   1.613 -        val U = drop (length ts, Us') ---> U';
   1.614 -        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
   1.615 -        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
   1.616 -              let
   1.617 -                val Ts = HOLogic.prodT_factors T;
   1.618 -                val ys = variantlist (replicate (length Ts) a, xs);
   1.619 -              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
   1.620 -                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
   1.621 -              end
   1.622 -          | mk_tuple (x, _) = x;
   1.623 -        val newt = ap_split' Us U (Var (v, T'));
   1.624 -        val cterm = Thm.cterm_of (#sign (rep_thm rl));
   1.625 -        val (vs', insts) = foldl mk_tuple ((vs, []), ts);
   1.626 -      in
   1.627 -        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
   1.628 -      end
   1.629 -  | complete_split_rule_var (_, x) = x;
   1.630 -
   1.631 -fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
   1.632 -  | collect_vars (vs, t) = (case strip_comb t of
   1.633 -        (v as Var _, ts) => (v, ts)::vs
   1.634 -      | (t, ts) => foldl collect_vars (vs, ts));
   1.635 -
   1.636 -in
   1.637 -
   1.638 -val split_rule_var = standard o remove_split o split_rule_var';
   1.639 -
   1.640 -(*Curries ALL function variables occurring in a rule's conclusion*)
   1.641 -fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
   1.642 -
   1.643 -fun complete_split_rule rl =
   1.644 -  standard (remove_split (fst (foldr complete_split_rule_var
   1.645 -    (collect_vars ([], concl_of rl),
   1.646 -     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))));
   1.647 -
   1.648 -end;