src/HOL/Prod.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 4534 6932c3ae3912
child 4650 91af1ef45d68
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
     1 (*  Title:      HOL/prod
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     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), 
    19             rtac conjI, rtac refl, rtac refl]);
    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]
    28     "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    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 
    33 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
    34 by (blast_tac (claset() addSEs [Pair_inject]) 1);
    35 qed "Pair_eq";
    36 AddIffs [Pair_eq];
    37 
    38 goalw Prod.thy [fst_def] "fst((a,b)) = a";
    39 by (Blast_tac 1);
    40 qed "fst_conv";
    41 goalw Prod.thy [snd_def] "snd((a,b)) = b";
    42 by (Blast_tac 1);
    43 qed "snd_conv";
    44 Addsimps [fst_conv, snd_conv];
    45 
    46 goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
    47 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
    48 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
    49            rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
    50 qed "PairE_lemma";
    51 
    52 val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
    53 by (rtac (PairE_lemma RS exE) 1);
    54 by (REPEAT (eresolve_tac [prem,exE] 1));
    55 qed "PairE";
    56 
    57 fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
    58 
    59 (* replace parameters of product type by individual component parameters *)
    60 local
    61 fun is_pair (_,Type("*",_)) = true
    62   | is_pair _ = false;
    63 
    64 fun find_pair_param prem =
    65   let val params = Logic.strip_params prem
    66   in if exists is_pair params
    67      then let val params = rev(rename_wrt_term prem params)
    68                            (*as they are printed*)
    69           in apsome fst (find_first is_pair params) end
    70      else None
    71   end;
    72 
    73 in
    74 
    75 val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) =>
    76   case find_pair_param prem of
    77     None => no_tac
    78   | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
    79                     REPEAT(hyp_subst_tac i), prune_params_tac]);
    80 
    81 end;
    82 
    83 (* Could be nice, but breaks too many proofs:
    84 claset_ref() := claset() addbefore split_all_tac;
    85 *)
    86 
    87 (*** lemmas for splitting paired `!!'
    88 Does not work with simplifier because it also affects premises in
    89 congrence rules, where is can lead to premises of the form
    90 !!a b. ... = ?P(a,b)
    91 which cannot be solved by reflexivity.
    92    
    93 val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
    94 by (rtac prem 1);
    95 val lemma1 = result();
    96 
    97 local
    98     val psig = sign_of Prod.thy;
    99     val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
   100     val PeqP = reflexive(read_cterm psig ("P", pT));
   101     val psplit = zero_var_indexes(read_instantiate [("p","x")]
   102                                   surjective_pairing RS eq_reflection)
   103 in
   104 val adhoc = combination PeqP psplit
   105 end;
   106 
   107 
   108 val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
   109 by (rewtac adhoc);
   110 by (rtac prem 1);
   111 val lemma = result();
   112 
   113 val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
   114 by (rtac lemma 1);
   115 by (rtac prem 1);
   116 val lemma2 = result();
   117 
   118 bind_thm("split_paired_all", equal_intr lemma1 lemma2);
   119 Addsimps [split_paired_all];
   120 ***)
   121 
   122 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
   123 by (fast_tac (claset() addbefore split_all_tac) 1);
   124 qed "split_paired_All";
   125 Addsimps [split_paired_All];
   126 (* AddIffs is not a good idea because it makes Blast_tac loop *)
   127 
   128 goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
   129 by (fast_tac (claset() addbefore split_all_tac) 1);
   130 qed "split_paired_Ex";
   131 Addsimps [split_paired_Ex];
   132 
   133 goalw Prod.thy [split_def] "split c (a,b) = c a b";
   134 by (Simp_tac 1);
   135 qed "split";
   136 Addsimps [split];
   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);
   141 by (Asm_simp_tac 1);
   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 *)
   150 goal Prod.thy "p = (fst(p),snd(p))";
   151 by (res_inst_tac [("p","p")] PairE 1);
   152 by (Asm_simp_tac 1);
   153 qed "surjective_pairing";
   154 
   155 goal Prod.thy "p = split (%x y.(x,y)) p";
   156 by (res_inst_tac [("p","p")] PairE 1);
   157 by (Asm_simp_tac 1);
   158 qed "surjective_pairing2";
   159 
   160 val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
   161 	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
   162 Addsimps [surj_pair];
   163 
   164 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   165   (K [rtac ext 1, split_all_tac 1, rtac split 1]);
   166 
   167 val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
   168 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
   169 
   170 (*For use with split_tac and the simplifier*)
   171 goal Prod.thy "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
   172 by (stac surjective_pairing 1);
   173 by (stac split 1);
   174 by (Blast_tac 1);
   175 qed "expand_split";
   176 
   177 (* could be done after split_tac has been speeded up significantly:
   178 simpset_ref() := (simpset() addsplits [expand_split]);
   179    precompute the constants involved and don't do anything unless
   180    the current goal contains one of those constants
   181 *)
   182 
   183 goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
   184 by (stac expand_split 1);
   185 by (Simp_tac 1);
   186 qed "expand_split_asm";
   187 
   188 (** split used as a logical connective or set former **)
   189 
   190 (*These rules are for use with blast_tac.
   191   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   192 
   193 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   194 by (split_all_tac 1);
   195 by (Asm_simp_tac 1);
   196 qed "splitI2";
   197 
   198 goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
   199 by (Asm_simp_tac 1);
   200 qed "splitI";
   201 
   202 val prems = goalw Prod.thy [split_def]
   203     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   204 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   205 qed "splitE";
   206 
   207 val splitE2 = prove_goal Prod.thy 
   208 "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
   209 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
   210 	rtac (split_beta RS subst) 1,
   211 	rtac (hd prems) 1]);
   212 
   213 goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
   214 by (etac (split RS iffD1) 1);
   215 qed "splitD";
   216 
   217 goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
   218 by (Asm_simp_tac 1);
   219 qed "mem_splitI";
   220 
   221 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   222 by (split_all_tac 1);
   223 by (Asm_simp_tac 1);
   224 qed "mem_splitI2";
   225 
   226 val prems = goalw Prod.thy [split_def]
   227     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   228 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   229 qed "mem_splitE";
   230 
   231 AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
   232 AddSEs [splitE, mem_splitE];
   233 
   234 (* allows simplifications of nested splits in case of independent predicates *)
   235 goal Prod.thy "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
   236 by (rtac ext 1);
   237 by (Blast_tac 1);
   238 qed "split_part";
   239 Addsimps [split_part];
   240 
   241 goal Prod.thy "(@(x',y'). x = x' & y = y') = (x,y)";
   242 by (Blast_tac 1);
   243 qed "Eps_split_eq";
   244 Addsimps [Eps_split_eq];
   245 (*
   246 the following  would be slightly more general, 
   247 but cannot be used as rewrite rule:
   248 ### Cannot add premise as rewrite rule because it contains (type) unknowns:
   249 ### ?y = .x
   250 goal Prod.thy "!!P. [| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   251 by (rtac select_equality 1);
   252 by ( Simp_tac 1);
   253 by (split_all_tac 1);
   254 by (Asm_full_simp_tac 1);
   255 qed "Eps_split_eq";
   256 *)
   257 
   258 (*** prod_fun -- action of the product functor upon functions ***)
   259 
   260 goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   261 by (rtac split 1);
   262 qed "prod_fun";
   263 Addsimps [prod_fun];
   264 
   265 goal Prod.thy 
   266     "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   267 by (rtac ext 1);
   268 by (res_inst_tac [("p","x")] PairE 1);
   269 by (Asm_simp_tac 1);
   270 qed "prod_fun_compose";
   271 
   272 goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
   273 by (rtac ext 1);
   274 by (res_inst_tac [("p","z")] PairE 1);
   275 by (Asm_simp_tac 1);
   276 qed "prod_fun_ident";
   277 Addsimps [prod_fun_ident];
   278 
   279 val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   280 by (rtac image_eqI 1);
   281 by (rtac (prod_fun RS sym) 1);
   282 by (resolve_tac prems 1);
   283 qed "prod_fun_imageI";
   284 
   285 val major::prems = goal Prod.thy
   286     "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   287 \    |] ==> P";
   288 by (rtac (major RS imageE) 1);
   289 by (res_inst_tac [("p","x")] PairE 1);
   290 by (resolve_tac prems 1);
   291 by (Blast_tac 2);
   292 by (blast_tac (claset() addIs [prod_fun]) 1);
   293 qed "prod_fun_imageE";
   294 
   295 
   296 (*** Disjoint union of a family of sets - Sigma ***)
   297 
   298 qed_goalw "SigmaI" Prod.thy [Sigma_def]
   299     "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   300  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
   301 
   302 AddSIs [SigmaI];
   303 
   304 (*The general elimination rule*)
   305 qed_goalw "SigmaE" Prod.thy [Sigma_def]
   306     "[| c: Sigma A B;  \
   307 \       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   308 \    |] ==> P"
   309  (fn major::prems=>
   310   [ (cut_facts_tac [major] 1),
   311     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   312 
   313 (** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   314 qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
   315  (fn [major]=>
   316   [ (rtac (major RS SigmaE) 1),
   317     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   318 
   319 qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
   320  (fn [major]=>
   321   [ (rtac (major RS SigmaE) 1),
   322     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   323 
   324 qed_goal "SigmaE2" Prod.thy
   325     "[| (a,b) : Sigma A B;    \
   326 \       [| a:A;  b:B(a) |] ==> P   \
   327 \    |] ==> P"
   328  (fn [major,minor]=>
   329   [ (rtac minor 1),
   330     (rtac (major RS SigmaD1) 1),
   331     (rtac (major RS SigmaD2) 1) ]);
   332 
   333 AddSEs [SigmaE2, SigmaE];
   334 
   335 val prems = goal Prod.thy
   336     "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   337 by (cut_facts_tac prems 1);
   338 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   339 qed "Sigma_mono";
   340 
   341 qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
   342  (fn _ => [ (Blast_tac 1) ]);
   343 
   344 qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
   345  (fn _ => [ (Blast_tac 1) ]);
   346 
   347 Addsimps [Sigma_empty1,Sigma_empty2]; 
   348 
   349 goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
   350 by (Blast_tac 1);
   351 qed "mem_Sigma_iff";
   352 AddIffs [mem_Sigma_iff]; 
   353 
   354 val Collect_split = prove_goal Prod.thy 
   355 	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
   356 Addsimps [Collect_split];
   357 
   358 (*Suggested by Pierre Chartier*)
   359 goal Prod.thy
   360      "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
   361 by (Blast_tac 1);
   362 qed "UNION_Times_distrib";
   363 
   364 (*** Domain of a relation ***)
   365 
   366 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
   367 by (rtac CollectI 1);
   368 by (rtac bexI 1);
   369 by (rtac (fst_conv RS sym) 1);
   370 by (resolve_tac prems 1);
   371 qed "fst_imageI";
   372 
   373 val major::prems = goal Prod.thy
   374     "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
   375 by (rtac (major RS imageE) 1);
   376 by (resolve_tac prems 1);
   377 by (etac ssubst 1);
   378 by (rtac (surjective_pairing RS subst) 1);
   379 by (assume_tac 1);
   380 qed "fst_imageE";
   381 
   382 (*** Range of a relation ***)
   383 
   384 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
   385 by (rtac CollectI 1);
   386 by (rtac bexI 1);
   387 by (rtac (snd_conv RS sym) 1);
   388 by (resolve_tac prems 1);
   389 qed "snd_imageI";
   390 
   391 val major::prems = goal Prod.thy
   392     "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
   393 by (rtac (major RS imageE) 1);
   394 by (resolve_tac prems 1);
   395 by (etac ssubst 1);
   396 by (rtac (surjective_pairing RS subst) 1);
   397 by (assume_tac 1);
   398 qed "snd_imageE";
   399 
   400 (** Exhaustion rule for unit -- a degenerate form of induction **)
   401 
   402 goalw Prod.thy [Unity_def]
   403     "u = ()";
   404 by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
   405 by (rtac (Rep_unit_inverse RS sym) 1);
   406 qed "unit_eq";
   407  
   408 AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
   409 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
   410 
   411 structure Prod_Syntax =
   412 struct
   413 
   414 val unitT = Type("unit",[]);
   415 
   416 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
   417 
   418 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
   419 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
   420   | factors T                    = [T];
   421 
   422 (*Make a correctly typed ordered pair*)
   423 fun mk_Pair (t1,t2) = 
   424   let val T1 = fastype_of t1
   425       and T2 = fastype_of t2
   426   in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
   427    
   428 fun split_const(Ta,Tb,Tc) = 
   429     Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
   430 
   431 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   432   with result type T.  The call creates a new term expecting one argument
   433   of type S.*)
   434 fun ap_split (Type("*", [T1,T2])) T3 u = 
   435       split_const(T1,T2,T3) $ 
   436       Abs("v", T1, 
   437           ap_split T2 T3
   438              ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   439               Bound 0))
   440   | ap_split T T3 u = u;
   441 
   442 (*Makes a nested tuple from a list, following the product type structure*)
   443 fun mk_tuple (Type("*", [T1,T2])) tms = 
   444         mk_Pair (mk_tuple T1 tms, 
   445                  mk_tuple T2 (drop (length (factors T1), tms)))
   446   | mk_tuple T (t::_) = t;
   447 
   448 (*Attempts to remove occurrences of split, and pair-valued parameters*)
   449 val remove_split = rewrite_rule [split RS eq_reflection]  o  
   450                    rule_by_tactic (ALLGOALS split_all_tac);
   451 
   452 (*Uncurries any Var of function type in the rule*)
   453 fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
   454       let val T' = factors T1 ---> T2
   455           val newt = ap_split T1 T2 (Var(v,T'))
   456           val cterm = Thm.cterm_of (#sign(rep_thm rl))
   457       in
   458           remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
   459       end
   460   | split_rule_var (t,rl) = rl;
   461 
   462 (*Uncurries ALL function variables occurring in a rule's conclusion*)
   463 fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
   464                     |> standard;
   465 
   466 end;