src/HOL/Prod.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1552 6f71b5d46700
child 1618 372880456b5b
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     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 (fast_tac (set_cs addIs [Pair_inject]) 1);
    35 qed "Pair_eq";
    36 
    37 goalw Prod.thy [fst_def] "fst((a,b)) = a";
    38 by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
    39 qed "fst_conv";
    40 
    41 goalw Prod.thy [snd_def] "snd((a,b)) = b";
    42 by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
    43 qed "snd_conv";
    44 
    45 goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
    46 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
    47 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
    48            rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
    49 qed "PairE_lemma";
    50 
    51 val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
    52 by (rtac (PairE_lemma RS exE) 1);
    53 by (REPEAT (eresolve_tac [prem,exE] 1));
    54 qed "PairE";
    55 
    56 (* replace parameters of product type by individual component parameters *)
    57 local
    58 fun is_pair (_,Type("*",_)) = true
    59   | is_pair _ = false;
    60 
    61 fun find_pair_param t =
    62   let val params = Logic.strip_params t
    63   in if exists is_pair params
    64      then let val params = rev(rename_wrt_term t params)
    65                            (*as they are printed*)
    66           in apsome fst (find_first is_pair params) end
    67      else None
    68   end;
    69 
    70 in
    71 
    72 val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
    73   case find_pair_param t of
    74     None => no_tac
    75   | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
    76                     REPEAT(hyp_subst_tac 1), prune_params_tac]);
    77 
    78 end;
    79 
    80 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
    81 by (fast_tac (HOL_cs addbefore split_all_tac 1) 1);
    82 qed "split_paired_All";
    83 
    84 goalw Prod.thy [split_def] "split c (a,b) = c a b";
    85 by (EVERY1[stac fst_conv, stac snd_conv]);
    86 by (rtac refl 1);
    87 qed "split";
    88 
    89 Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
    90 
    91 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
    92 by (res_inst_tac[("p","s")] PairE 1);
    93 by (res_inst_tac[("p","t")] PairE 1);
    94 by (Asm_simp_tac 1);
    95 qed "Pair_fst_snd_eq";
    96 
    97 (*Prevents simplification of c: much faster*)
    98 qed_goal "split_weak_cong" Prod.thy
    99   "p=q ==> split c p = split c q"
   100   (fn [prem] => [rtac (prem RS arg_cong) 1]);
   101 
   102 (* Do not add as rewrite rule: invalidates some proofs in IMP *)
   103 goal Prod.thy "p = (fst(p),snd(p))";
   104 by (res_inst_tac [("p","p")] PairE 1);
   105 by (Asm_simp_tac 1);
   106 qed "surjective_pairing";
   107 
   108 goal Prod.thy "p = split (%x y.(x,y)) p";
   109 by (res_inst_tac [("p","p")] PairE 1);
   110 by (Asm_simp_tac 1);
   111 qed "surjective_pairing2";
   112 
   113 (*For use with split_tac and the simplifier*)
   114 goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
   115 by (stac surjective_pairing 1);
   116 by (stac split 1);
   117 by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
   118 qed "expand_split";
   119 
   120 (** split used as a logical connective or set former **)
   121 
   122 (*These rules are for use with fast_tac.
   123   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   124 
   125 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   126 by (split_all_tac 1);
   127 by (Asm_simp_tac 1);
   128 qed "splitI2";
   129 
   130 goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
   131 by (Asm_simp_tac 1);
   132 qed "splitI";
   133 
   134 val prems = goalw Prod.thy [split_def]
   135     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   136 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   137 qed "splitE";
   138 
   139 goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
   140 by (etac (split RS iffD1) 1);
   141 qed "splitD";
   142 
   143 goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
   144 by (Asm_simp_tac 1);
   145 qed "mem_splitI";
   146 
   147 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   148 by (split_all_tac 1);
   149 by (Asm_simp_tac 1);
   150 qed "mem_splitI2";
   151 
   152 val prems = goalw Prod.thy [split_def]
   153     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   154 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   155 qed "mem_splitE";
   156 
   157 (*** prod_fun -- action of the product functor upon functions ***)
   158 
   159 goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   160 by (rtac split 1);
   161 qed "prod_fun";
   162 
   163 goal Prod.thy 
   164     "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   165 by (rtac ext 1);
   166 by (res_inst_tac [("p","x")] PairE 1);
   167 by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
   168 qed "prod_fun_compose";
   169 
   170 goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
   171 by (rtac ext 1);
   172 by (res_inst_tac [("p","z")] PairE 1);
   173 by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
   174 qed "prod_fun_ident";
   175 
   176 val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   177 by (rtac image_eqI 1);
   178 by (rtac (prod_fun RS sym) 1);
   179 by (resolve_tac prems 1);
   180 qed "prod_fun_imageI";
   181 
   182 val major::prems = goal Prod.thy
   183     "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   184 \    |] ==> P";
   185 by (rtac (major RS imageE) 1);
   186 by (res_inst_tac [("p","x")] PairE 1);
   187 by (resolve_tac prems 1);
   188 by (fast_tac HOL_cs 2);
   189 by (fast_tac (HOL_cs addIs [prod_fun]) 1);
   190 qed "prod_fun_imageE";
   191 
   192 (*** Disjoint union of a family of sets - Sigma ***)
   193 
   194 qed_goalw "SigmaI" Prod.thy [Sigma_def]
   195     "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   196  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
   197 
   198 (*The general elimination rule*)
   199 qed_goalw "SigmaE" Prod.thy [Sigma_def]
   200     "[| c: Sigma A B;  \
   201 \       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   202 \    |] ==> P"
   203  (fn major::prems=>
   204   [ (cut_facts_tac [major] 1),
   205     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   206 
   207 (** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   208 qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
   209  (fn [major]=>
   210   [ (rtac (major RS SigmaE) 1),
   211     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   212 
   213 qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
   214  (fn [major]=>
   215   [ (rtac (major RS SigmaE) 1),
   216     (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
   217 
   218 qed_goal "SigmaE2" Prod.thy
   219     "[| (a,b) : Sigma A B;    \
   220 \       [| a:A;  b:B(a) |] ==> P   \
   221 \    |] ==> P"
   222  (fn [major,minor]=>
   223   [ (rtac minor 1),
   224     (rtac (major RS SigmaD1) 1),
   225     (rtac (major RS SigmaD2) 1) ]);
   226 
   227 val prems = goal Prod.thy
   228     "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
   229 by (cut_facts_tac prems 1);
   230 by (fast_tac (set_cs addIs (prems RL [subsetD]) 
   231                      addSIs [SigmaI] 
   232                      addSEs [SigmaE]) 1);
   233 qed "Sigma_mono";
   234 
   235 
   236 (*** Domain of a relation ***)
   237 
   238 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
   239 by (rtac CollectI 1);
   240 by (rtac bexI 1);
   241 by (rtac (fst_conv RS sym) 1);
   242 by (resolve_tac prems 1);
   243 qed "fst_imageI";
   244 
   245 val major::prems = goal Prod.thy
   246     "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
   247 by (rtac (major RS imageE) 1);
   248 by (resolve_tac prems 1);
   249 by (etac ssubst 1);
   250 by (rtac (surjective_pairing RS subst) 1);
   251 by (assume_tac 1);
   252 qed "fst_imageE";
   253 
   254 (*** Range of a relation ***)
   255 
   256 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
   257 by (rtac CollectI 1);
   258 by (rtac bexI 1);
   259 by (rtac (snd_conv RS sym) 1);
   260 by (resolve_tac prems 1);
   261 qed "snd_imageI";
   262 
   263 val major::prems = goal Prod.thy
   264     "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
   265 by (rtac (major RS imageE) 1);
   266 by (resolve_tac prems 1);
   267 by (etac ssubst 1);
   268 by (rtac (surjective_pairing RS subst) 1);
   269 by (assume_tac 1);
   270 qed "snd_imageE";
   271 
   272 (** Exhaustion rule for unit -- a degenerate form of induction **)
   273 
   274 goalw Prod.thy [Unity_def]
   275     "u = ()";
   276 by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
   277 by (rtac (Rep_Unit_inverse RS sym) 1);
   278 qed "unit_eq";
   279 
   280 val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
   281                      addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
   282                      addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
   283                              fst_imageE, snd_imageE, prod_fun_imageE,
   284                              Pair_inject];