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