src/HOL/Prod.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2886 fd5645efa43d
child 2935 998cb95fdd43
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 AddSEs [Pair_inject];
    34 
    35 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
    36 by (Fast_tac 1);
    37 qed "Pair_eq";
    38 
    39 goalw Prod.thy [fst_def] "fst((a,b)) = a";
    40 by (fast_tac (!claset addIs [select_equality]) 1);
    41 qed "fst_conv";
    42 
    43 goalw Prod.thy [snd_def] "snd((a,b)) = b";
    44 by (fast_tac (!claset addIs [select_equality]) 1);
    45 qed "snd_conv";
    46 
    47 goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
    48 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
    49 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
    50            rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
    51 qed "PairE_lemma";
    52 
    53 val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
    54 by (rtac (PairE_lemma RS exE) 1);
    55 by (REPEAT (eresolve_tac [prem,exE] 1));
    56 qed "PairE";
    57 
    58 (* replace parameters of product type by individual component parameters *)
    59 local
    60 fun is_pair (_,Type("*",_)) = true
    61   | is_pair _ = false;
    62 
    63 fun find_pair_param prem =
    64   let val params = Logic.strip_params prem
    65   in if exists is_pair params
    66      then let val params = rev(rename_wrt_term prem params)
    67                            (*as they are printed*)
    68           in apsome fst (find_first is_pair params) end
    69      else None
    70   end;
    71 
    72 in
    73 
    74 val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) =>
    75   case find_pair_param prem of
    76     None => no_tac
    77   | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
    78                     REPEAT(hyp_subst_tac i), prune_params_tac]);
    79 
    80 end;
    81 
    82 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
    83 by (fast_tac (!claset addbefore split_all_tac) 1);
    84 qed "split_paired_All";
    85 
    86 goalw Prod.thy [split_def] "split c (a,b) = c a b";
    87 by (EVERY1[stac fst_conv, stac snd_conv]);
    88 by (rtac refl 1);
    89 qed "split";
    90 
    91 Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
    92 
    93 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
    94 by (res_inst_tac[("p","s")] PairE 1);
    95 by (res_inst_tac[("p","t")] PairE 1);
    96 by (Asm_simp_tac 1);
    97 qed "Pair_fst_snd_eq";
    98 
    99 (*Prevents simplification of c: much faster*)
   100 qed_goal "split_weak_cong" Prod.thy
   101   "p=q ==> split c p = split c q"
   102   (fn [prem] => [rtac (prem RS arg_cong) 1]);
   103 
   104 (* Do not add as rewrite rule: invalidates some proofs in IMP *)
   105 goal Prod.thy "p = (fst(p),snd(p))";
   106 by (res_inst_tac [("p","p")] PairE 1);
   107 by (Asm_simp_tac 1);
   108 qed "surjective_pairing";
   109 
   110 goal Prod.thy "p = split (%x y.(x,y)) p";
   111 by (res_inst_tac [("p","p")] PairE 1);
   112 by (Asm_simp_tac 1);
   113 qed "surjective_pairing2";
   114 
   115 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   116   (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]);
   117 
   118 (*For use with split_tac and the simplifier*)
   119 goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
   120 by (stac surjective_pairing 1);
   121 by (stac split 1);
   122 by (Fast_tac 1);
   123 qed "expand_split";
   124 
   125 (** split used as a logical connective or set former **)
   126 
   127 (*These rules are for use with fast_tac.
   128   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   129 
   130 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   131 by (split_all_tac 1);
   132 by (Asm_simp_tac 1);
   133 qed "splitI2";
   134 
   135 goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
   136 by (Asm_simp_tac 1);
   137 qed "splitI";
   138 
   139 val prems = goalw Prod.thy [split_def]
   140     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   141 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   142 qed "splitE";
   143 
   144 goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
   145 by (etac (split RS iffD1) 1);
   146 qed "splitD";
   147 
   148 goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
   149 by (Asm_simp_tac 1);
   150 qed "mem_splitI";
   151 
   152 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   153 by (split_all_tac 1);
   154 by (Asm_simp_tac 1);
   155 qed "mem_splitI2";
   156 
   157 val prems = goalw Prod.thy [split_def]
   158     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   159 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   160 qed "mem_splitE";
   161 
   162 AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
   163 AddSEs [splitE, mem_splitE];
   164 
   165 (*** prod_fun -- action of the product functor upon functions ***)
   166 
   167 goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   168 by (rtac split 1);
   169 qed "prod_fun";
   170 
   171 goal Prod.thy 
   172     "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   173 by (rtac ext 1);
   174 by (res_inst_tac [("p","x")] PairE 1);
   175 by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
   176 qed "prod_fun_compose";
   177 
   178 goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
   179 by (rtac ext 1);
   180 by (res_inst_tac [("p","z")] PairE 1);
   181 by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
   182 qed "prod_fun_ident";
   183 
   184 val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   185 by (rtac image_eqI 1);
   186 by (rtac (prod_fun RS sym) 1);
   187 by (resolve_tac prems 1);
   188 qed "prod_fun_imageI";
   189 
   190 val major::prems = goal Prod.thy
   191     "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   192 \    |] ==> P";
   193 by (rtac (major RS imageE) 1);
   194 by (res_inst_tac [("p","x")] PairE 1);
   195 by (resolve_tac prems 1);
   196 by (Fast_tac 2);
   197 by (fast_tac (!claset addIs [prod_fun]) 1);
   198 qed "prod_fun_imageE";
   199 
   200 (*** Disjoint union of a family of sets - Sigma ***)
   201 
   202 qed_goalw "SigmaI" Prod.thy [Sigma_def]
   203     "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   204  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
   205 
   206 AddSIs [SigmaI];
   207 
   208 (*The general elimination rule*)
   209 qed_goalw "SigmaE" Prod.thy [Sigma_def]
   210     "[| c: Sigma A B;  \
   211 \       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   212 \    |] ==> P"
   213  (fn major::prems=>
   214   [ (cut_facts_tac [major] 1),
   215     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   216 
   217 (** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   218 qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
   219  (fn [major]=>
   220   [ (rtac (major RS SigmaE) 1),
   221     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   222 
   223 qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
   224  (fn [major]=>
   225   [ (rtac (major RS SigmaE) 1),
   226     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   227 
   228 qed_goal "SigmaE2" Prod.thy
   229     "[| (a,b) : Sigma A B;    \
   230 \       [| a:A;  b:B(a) |] ==> P   \
   231 \    |] ==> P"
   232  (fn [major,minor]=>
   233   [ (rtac minor 1),
   234     (rtac (major RS SigmaD1) 1),
   235     (rtac (major RS SigmaD2) 1) ]);
   236 
   237 AddSEs [SigmaE2, SigmaE];
   238 
   239 val prems = goal Prod.thy
   240     "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   241 by (cut_facts_tac prems 1);
   242 by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
   243 qed "Sigma_mono";
   244 
   245 qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
   246  (fn _ => [ (Fast_tac 1) ]);
   247 
   248 qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
   249  (fn _ => [ (Fast_tac 1) ]);
   250 
   251 Addsimps [Sigma_empty1,Sigma_empty2]; 
   252 
   253 goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
   254 by (Fast_tac 1);
   255 qed "mem_Sigma_iff";
   256 Addsimps [mem_Sigma_iff]; 
   257 
   258 
   259 (*Suggested by Pierre Chartier*)
   260 goal Prod.thy
   261      "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
   262 by (Fast_tac 1);
   263 qed "UNION_Times_distrib";
   264 
   265 (*** Domain of a relation ***)
   266 
   267 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
   268 by (rtac CollectI 1);
   269 by (rtac bexI 1);
   270 by (rtac (fst_conv RS sym) 1);
   271 by (resolve_tac prems 1);
   272 qed "fst_imageI";
   273 
   274 val major::prems = goal Prod.thy
   275     "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
   276 by (rtac (major RS imageE) 1);
   277 by (resolve_tac prems 1);
   278 by (etac ssubst 1);
   279 by (rtac (surjective_pairing RS subst) 1);
   280 by (assume_tac 1);
   281 qed "fst_imageE";
   282 
   283 (*** Range of a relation ***)
   284 
   285 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
   286 by (rtac CollectI 1);
   287 by (rtac bexI 1);
   288 by (rtac (snd_conv RS sym) 1);
   289 by (resolve_tac prems 1);
   290 qed "snd_imageI";
   291 
   292 val major::prems = goal Prod.thy
   293     "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
   294 by (rtac (major RS imageE) 1);
   295 by (resolve_tac prems 1);
   296 by (etac ssubst 1);
   297 by (rtac (surjective_pairing RS subst) 1);
   298 by (assume_tac 1);
   299 qed "snd_imageE";
   300 
   301 (** Exhaustion rule for unit -- a degenerate form of induction **)
   302 
   303 goalw Prod.thy [Unity_def]
   304     "u = ()";
   305 by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
   306 by (rtac (Rep_unit_inverse RS sym) 1);
   307 qed "unit_eq";
   308  
   309 AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
   310 AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
   311 
   312 structure Prod_Syntax =
   313 struct
   314 
   315 val unitT = Type("unit",[]);
   316 
   317 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
   318 
   319 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
   320 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
   321   | factors T                    = [T];
   322 
   323 (*Make a correctly typed ordered pair*)
   324 fun mk_Pair (t1,t2) = 
   325   let val T1 = fastype_of t1
   326       and T2 = fastype_of t2
   327   in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
   328    
   329 fun split_const(Ta,Tb,Tc) = 
   330     Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
   331 
   332 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   333   with result type T.  The call creates a new term expecting one argument
   334   of type S.*)
   335 fun ap_split (Type("*", [T1,T2])) T3 u = 
   336       split_const(T1,T2,T3) $ 
   337       Abs("v", T1, 
   338           ap_split T2 T3
   339              ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   340               Bound 0))
   341   | ap_split T T3 u = u;
   342 
   343 (*Makes a nested tuple from a list, following the product type structure*)
   344 fun mk_tuple (Type("*", [T1,T2])) tms = 
   345         mk_Pair (mk_tuple T1 tms, 
   346                  mk_tuple T2 (drop (length (factors T1), tms)))
   347   | mk_tuple T (t::_) = t;
   348 
   349 (*Attempts to remove occurrences of split, and pair-valued parameters*)
   350 val remove_split = rewrite_rule [split RS eq_reflection]  o  
   351                    rule_by_tactic (ALLGOALS split_all_tac);
   352 
   353 (*Uncurries any Var of function type in the rule*)
   354 fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
   355       let val T' = factors T1 ---> T2
   356           val newt = ap_split T1 T2 (Var(v,T'))
   357           val cterm = Thm.cterm_of (#sign(rep_thm rl))
   358       in
   359           remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
   360       end
   361   | split_rule_var (t,rl) = rl;
   362 
   363 (*Uncurries ALL function variables occurring in a rule's conclusion*)
   364 fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
   365                     |> standard;
   366 
   367 end;