src/HOL/Prod.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6016 797c76d6ff04
child 6394 3d9fd50fcc43
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (*  Title:      HOL/prod
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Ordered Pairs, the Cartesian product type, the unit type
     7 *)
     8 
     9 (*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
    10 Goalw [Prod_def] "Pair_Rep a b : Prod";
    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), 
    17             rtac conjI, rtac refl, rtac refl]);
    18 qed "Pair_Rep_inject";
    19 
    20 Goal "inj_on Abs_Prod Prod";
    21 by (rtac inj_on_inverseI 1);
    22 by (etac Abs_Prod_inverse 1);
    23 qed "inj_on_Abs_Prod";
    24 
    25 val prems = Goalw [Pair_def]
    26     "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    27 by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
    28 by (REPEAT (ares_tac (prems@[ProdI]) 1));
    29 qed "Pair_inject";
    30 
    31 Goal "((a,b) = (a',b')) = (a=a' & b=b')";
    32 by (blast_tac (claset() addSEs [Pair_inject]) 1);
    33 qed "Pair_eq";
    34 AddIffs [Pair_eq];
    35 
    36 Goalw [fst_def] "fst((a,b)) = a";
    37 by (Blast_tac 1);
    38 qed "fst_conv";
    39 Goalw [snd_def] "snd((a,b)) = b";
    40 by (Blast_tac 1);
    41 qed "snd_conv";
    42 Addsimps [fst_conv, snd_conv];
    43 
    44 Goalw [Pair_def] "? x y. p = (x,y)";
    45 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
    46 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
    47            rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
    48 qed "PairE_lemma";
    49 
    50 val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
    51 by (rtac (PairE_lemma RS exE) 1);
    52 by (REPEAT (eresolve_tac [prem,exE] 1));
    53 qed "PairE";
    54 
    55 fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
    56 			 K prune_params_tac];
    57 
    58 (* Do not add as rewrite rule: invalidates some proofs in IMP *)
    59 Goal "p = (fst(p),snd(p))";
    60 by (pair_tac "p" 1);
    61 by (Asm_simp_tac 1);
    62 qed "surjective_pairing";
    63 
    64 val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
    65 	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
    66 Addsimps [surj_pair];
    67 
    68 
    69 bind_thm ("split_paired_all",
    70   SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
    71 (*
    72 Addsimps [split_paired_all] does not work with simplifier 
    73 because it also affects premises in congrence rules, 
    74 where is can lead to premises of the form !!a b. ... = ?P(a,b)
    75 which cannot be solved by reflexivity.
    76 *)
    77 
    78 (* replace parameters of product type by individual component parameters *)
    79 local
    80   fun is_pair (_,Type("*",_)) = true
    81     | is_pair  _              = false;
    82   fun exists_paired_all prem  = exists is_pair (Logic.strip_params prem);
    83   val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]);
    84 in
    85 val split_all_tac = SUBGOAL (fn (prem,i) => 
    86     if exists_paired_all prem then split_tac i else no_tac);  
    87 end;
    88 
    89 claset_ref() := claset() addSWrapper ("split_all_tac", 
    90 				      fn tac2 => split_all_tac ORELSE' tac2);
    91 
    92 Goal "(!x. P x) = (!a b. P(a,b))";
    93 by (Fast_tac 1);
    94 qed "split_paired_All";
    95 Addsimps [split_paired_All];
    96 (* AddIffs is not a good idea because it makes Blast_tac loop *)
    97 
    98 bind_thm ("prod_induct",
    99   allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
   100 
   101 Goal "(? x. P x) = (? a b. P(a,b))";
   102 by (Fast_tac 1);
   103 qed "split_paired_Ex";
   104 Addsimps [split_paired_Ex];
   105 
   106 Goalw [split_def] "split c (a,b) = c a b";
   107 by (Simp_tac 1);
   108 qed "split";
   109 Addsimps [split];
   110 
   111 Goal "split Pair p = p";
   112 by (pair_tac "p" 1);
   113 by (Simp_tac 1);
   114 qed "split_Pair";
   115 (*unused: val surjective_pairing2 = split_Pair RS sym;*)
   116 
   117 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
   118 by (split_all_tac 1);
   119 by (Asm_simp_tac 1);
   120 qed "Pair_fst_snd_eq";
   121 
   122 (*Prevents simplification of c: much faster*)
   123 qed_goal "split_weak_cong" Prod.thy
   124   "p=q ==> split c p = split c q"
   125   (fn [prem] => [rtac (prem RS arg_cong) 1]);
   126 
   127 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   128   (K [rtac ext 1, split_all_tac 1, rtac split 1]);
   129 
   130 qed_goal "cond_split_eta" Prod.thy 
   131 	"!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"
   132   (K [asm_simp_tac (simpset() addsimps [split_eta]) 1]);
   133 
   134 
   135 (*simplification procedure for cond_split_eta. 
   136   using split_eta a rewrite rule is not general enough, and using 
   137   cond_split_eta directly would render some existing proofs very inefficient*)
   138 local
   139   val split_eta_pat = Thm.read_cterm (sign_of thy) 
   140 		("split (%x. split (%y. f x y))", HOLogic.termTVar);
   141   val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
   142   fun  Pair_pat 0      (Bound 0) = true
   143   |    Pair_pat k      (Const ("Pair",  _) $ Bound m $ t) = 
   144 			m = k andalso Pair_pat (k-1) t
   145   |    Pair_pat _ _ = false;
   146   fun split_pat k (Abs  (_, _, f $ 
   147 			(Const ("Pair",_) $ Bound m $ 
   148 			(Const ("Pair",_) $ Bound n $ t)))) =
   149 			if m = k andalso n = k-1 andalso Pair_pat (k-2) t
   150 			then Some f else None
   151   |   split_pat k (Const ("split", _) $ Abs (_, _, t)) = split_pat (k+1) t
   152   |   split_pat k _ = None;
   153   fun proc sg _	(s as
   154 	(Const ("split", _) $ Abs (_, _, 
   155 	(Const ("split", _) $ Abs (_, _, t))))) = (case split_pat 2 t of
   156 	  Some f => (let val fvar = Free ("f", fastype_of f);
   157 			 fun atom_fun t = if t = f then fvar else atom t
   158 			 and atom     (Abs (x, T, t)) = Abs (x, T,atom_fun t)
   159 			   | atom     (t $ u)         = atom_fun t $ atom_fun u
   160 			   | atom     x               = x;
   161 			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
   162 				   (HOLogic.mk_eq (atom_fun s,fvar)));
   163 			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
   164          in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
   165 	| None => None)
   166   |   proc _ _ _ = None;
   167 
   168 in
   169   val split_eta_proc = Simplifier.mk_simproc "split_eta" [split_eta_pat] proc;
   170 end;
   171 
   172 Addsimprocs [split_eta_proc];
   173 
   174 
   175 qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
   176 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
   177 
   178 (*For use with split_tac and the simplifier*)
   179 Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
   180 by (stac surjective_pairing 1);
   181 by (stac split 1);
   182 by (Blast_tac 1);
   183 qed "split_split";
   184 
   185 (* could be done after split_tac has been speeded up significantly:
   186 simpset_ref() := simpset() addsplits [split_split];
   187    precompute the constants involved and don't do anything unless
   188    the current goal contains one of those constants
   189 *)
   190 
   191 Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
   192 by (stac split_split 1);
   193 by (Simp_tac 1);
   194 qed "expand_split_asm";
   195 
   196 (** split used as a logical connective or set former **)
   197 
   198 (*These rules are for use with blast_tac.
   199   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   200 
   201 Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   202 by (split_all_tac 1);
   203 by (Asm_simp_tac 1);
   204 qed "splitI2";
   205 
   206 Goal "c a b ==> split c (a,b)";
   207 by (Asm_simp_tac 1);
   208 qed "splitI";
   209 
   210 val prems = Goalw [split_def]
   211     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   212 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   213 qed "splitE";
   214 
   215 val splitE2 = prove_goal Prod.thy 
   216 "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
   217 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
   218 	rtac (split_beta RS subst) 1,
   219 	rtac (hd prems) 1]);
   220 
   221 Goal "split R (a,b) ==> R a b";
   222 by (etac (split RS iffD1) 1);
   223 qed "splitD";
   224 
   225 Goal "z: c a b ==> z: split c (a,b)";
   226 by (Asm_simp_tac 1);
   227 qed "mem_splitI";
   228 
   229 Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   230 by (split_all_tac 1);
   231 by (Asm_simp_tac 1);
   232 qed "mem_splitI2";
   233 
   234 val prems = Goalw [split_def]
   235     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   236 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   237 qed "mem_splitE";
   238 
   239 AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
   240 AddSEs [splitE, mem_splitE];
   241 
   242 (* allows simplifications of nested splits in case of independent predicates *)
   243 Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
   244 by (rtac ext 1);
   245 by (Blast_tac 1);
   246 qed "split_part";
   247 Addsimps [split_part];
   248 
   249 Goal "(@(x',y'). x = x' & y = y') = (x,y)";
   250 by (Blast_tac 1);
   251 qed "Eps_split_eq";
   252 Addsimps [Eps_split_eq];
   253 (*
   254 the following  would be slightly more general, 
   255 but cannot be used as rewrite rule:
   256 ### Cannot add premise as rewrite rule because it contains (type) unknowns:
   257 ### ?y = .x
   258 Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   259 by (rtac select_equality 1);
   260 by ( Simp_tac 1);
   261 by (split_all_tac 1);
   262 by (Asm_full_simp_tac 1);
   263 qed "Eps_split_eq";
   264 *)
   265 
   266 (*** prod_fun -- action of the product functor upon functions ***)
   267 
   268 Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   269 by (rtac split 1);
   270 qed "prod_fun";
   271 Addsimps [prod_fun];
   272 
   273 Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   274 by (rtac ext 1);
   275 by (pair_tac "x" 1);
   276 by (Asm_simp_tac 1);
   277 qed "prod_fun_compose";
   278 
   279 Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
   280 by (rtac ext 1);
   281 by (pair_tac "z" 1);
   282 by (Asm_simp_tac 1);
   283 qed "prod_fun_ident";
   284 Addsimps [prod_fun_ident];
   285 
   286 Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   287 by (rtac image_eqI 1);
   288 by (rtac (prod_fun RS sym) 1);
   289 by (assume_tac 1);
   290 qed "prod_fun_imageI";
   291 
   292 val major::prems = Goal
   293     "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   294 \    |] ==> P";
   295 by (rtac (major RS imageE) 1);
   296 by (res_inst_tac [("p","x")] PairE 1);
   297 by (resolve_tac prems 1);
   298 by (Blast_tac 2);
   299 by (blast_tac (claset() addIs [prod_fun]) 1);
   300 qed "prod_fun_imageE";
   301 
   302 AddIs  [prod_fun_imageI];
   303 AddSEs [prod_fun_imageE];
   304 
   305 
   306 (*** Disjoint union of a family of sets - Sigma ***)
   307 
   308 qed_goalw "SigmaI" Prod.thy [Sigma_def]
   309     "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   310  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
   311 
   312 AddSIs [SigmaI];
   313 
   314 (*The general elimination rule*)
   315 qed_goalw "SigmaE" Prod.thy [Sigma_def]
   316     "[| c: Sigma A B;  \
   317 \       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   318 \    |] ==> P"
   319  (fn major::prems=>
   320   [ (cut_facts_tac [major] 1),
   321     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   322 
   323 (** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   324 qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
   325  (fn [major]=>
   326   [ (rtac (major RS SigmaE) 1),
   327     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   328 
   329 qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
   330  (fn [major]=>
   331   [ (rtac (major RS SigmaE) 1),
   332     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   333 
   334 qed_goal "SigmaE2" Prod.thy
   335     "[| (a,b) : Sigma A B;    \
   336 \       [| a:A;  b:B(a) |] ==> P   \
   337 \    |] ==> P"
   338  (fn [major,minor]=>
   339   [ (rtac minor 1),
   340     (rtac (major RS SigmaD1) 1),
   341     (rtac (major RS SigmaD2) 1) ]);
   342 
   343 AddSEs [SigmaE2, SigmaE];
   344 
   345 val prems = Goal
   346     "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   347 by (cut_facts_tac prems 1);
   348 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   349 qed "Sigma_mono";
   350 
   351 qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
   352  (fn _ => [ (Blast_tac 1) ]);
   353 
   354 qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
   355  (fn _ => [ (Blast_tac 1) ]);
   356 
   357 Addsimps [Sigma_empty1,Sigma_empty2]; 
   358 
   359 Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
   360 by (Blast_tac 1);
   361 qed "mem_Sigma_iff";
   362 AddIffs [mem_Sigma_iff]; 
   363 
   364 Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
   365 by (Blast_tac 1);
   366 qed "Times_subset_cancel2";
   367 
   368 Goal "x:C ==> (A Times C = B Times C) = (A = B)";
   369 by (blast_tac (claset() addEs [equalityE]) 1);
   370 qed "Times_eq_cancel2";
   371 
   372 
   373 (*** Complex rules for Sigma ***)
   374 
   375 val Collect_split = prove_goal Prod.thy 
   376 	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
   377 Addsimps [Collect_split];
   378 
   379 (*Suggested by Pierre Chartier*)
   380 Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
   381 by (Blast_tac 1);
   382 qed "UNION_Times_distrib";
   383 
   384 Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
   385 by (Fast_tac 1);
   386 qed "split_paired_Ball_Sigma";
   387 Addsimps [split_paired_Ball_Sigma];
   388 
   389 Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
   390 by (Fast_tac 1);
   391 qed "split_paired_Bex_Sigma";
   392 Addsimps [split_paired_Bex_Sigma];
   393 
   394 Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
   395 by (Blast_tac 1);
   396 qed "Sigma_Un_distrib1";
   397 
   398 Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
   399 by (Blast_tac 1);
   400 qed "Sigma_Un_distrib2";
   401 
   402 Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
   403 by (Blast_tac 1);
   404 qed "Sigma_Int_distrib1";
   405 
   406 Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
   407 by (Blast_tac 1);
   408 qed "Sigma_Int_distrib2";
   409 
   410 Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
   411 by (Blast_tac 1);
   412 qed "Sigma_Diff_distrib1";
   413 
   414 Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
   415 by (Blast_tac 1);
   416 qed "Sigma_Diff_distrib2";
   417 
   418 Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
   419 by (Blast_tac 1);
   420 qed "Sigma_Union";
   421 
   422 
   423 (** Exhaustion rule for unit -- a degenerate form of induction **)
   424 
   425 Goalw [Unity_def]
   426     "u = ()";
   427 by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
   428 by (rtac (Rep_unit_inverse RS sym) 1);
   429 qed "unit_eq";
   430  
   431 (*simplification procedure for unit_eq.
   432   Cannot use this rule directly -- it loops!*)
   433 local
   434   val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
   435   val unit_meta_eq = standard (mk_meta_eq unit_eq);
   436   fun proc _ _ t =
   437     if HOLogic.is_unit t then None
   438     else Some unit_meta_eq;
   439 in
   440   val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
   441 end;
   442 
   443 Addsimprocs [unit_eq_proc];
   444 
   445 
   446 Goal "P () ==> P x";
   447 by (Simp_tac 1);
   448 qed "unit_induct";
   449 
   450 
   451 (*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
   452   replacing it by f rather than by %u.f(). *)
   453 Goal "(%u::unit. f()) = f";
   454 by (rtac ext 1);
   455 by (Simp_tac 1);
   456 qed "unit_abs_eta_conv";
   457 Addsimps [unit_abs_eta_conv];
   458 
   459 
   460 (*Attempts to remove occurrences of split, and pair-valued parameters*)
   461 val remove_split = rewrite_rule [split RS eq_reflection] o  
   462                    rule_by_tactic (TRYALL split_all_tac);
   463 
   464 local
   465 
   466 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   467   with result type T.  The call creates a new term expecting one argument
   468   of type S.*)
   469 fun ap_split (Type ("*", [T1, T2])) T3 u = 
   470       HOLogic.split_const (T1, T2, T3) $ 
   471       Abs("v", T1, 
   472           ap_split T2 T3
   473              ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   474               Bound 0))
   475   | ap_split T T3 u = u;
   476 
   477 (*Curries any Var of function type in the rule*)
   478 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
   479       let val T' = HOLogic.prodT_factors T1 ---> T2
   480           val newt = ap_split T1 T2 (Var (v, T'))
   481           val cterm = Thm.cterm_of (#sign (rep_thm rl))
   482       in
   483           instantiate ([], [(cterm t, cterm newt)]) rl
   484       end
   485   | split_rule_var' (t, rl) = rl;
   486 
   487 in
   488 
   489 val split_rule_var = standard o remove_split o split_rule_var';
   490 
   491 (*Curries ALL function variables occurring in a rule's conclusion*)
   492 fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
   493                     |> standard;
   494 
   495 end;
   496 
   497