# HG changeset patch # User oheimb # Date 884279323 -3600 # Node ID 6932c3ae3912534fd898157ec983ec2fc0b020ba # Parent 05ecfa08fefa6aeb7ca9c49fb45bc34e67d7f276 added select_equality to the implicit claset added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset removed split_select renamed Collect_Prod to Collect_split diff -r 05ecfa08fefa -r 6932c3ae3912 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Thu Jan 08 18:07:06 1998 +0100 +++ b/src/HOL/Prod.ML Thu Jan 08 18:08:43 1998 +0100 @@ -36,12 +36,12 @@ AddIffs [Pair_eq]; goalw Prod.thy [fst_def] "fst((a,b)) = a"; -by (blast_tac (claset() addIs [select_equality]) 1); +by (Blast_tac 1); qed "fst_conv"; - goalw Prod.thy [snd_def] "snd((a,b)) = b"; -by (blast_tac (claset() addIs [select_equality]) 1); +by (Blast_tac 1); qed "snd_conv"; +Addsimps [fst_conv, snd_conv]; goalw Prod.thy [Pair_def] "? x y. p = (x,y)"; by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); @@ -128,17 +128,12 @@ goal Prod.thy "(? x. P x) = (? a b. P(a,b))"; by (fast_tac (claset() addbefore split_all_tac) 1); qed "split_paired_Ex"; -(* Addsimps [split_paired_Ex]; breaks a number of IOA proofs *) +Addsimps [split_paired_Ex]; goalw Prod.thy [split_def] "split c (a,b) = c a b"; -by (EVERY1[stac fst_conv, stac snd_conv]); -by (rtac refl 1); +by (Simp_tac 1); qed "split"; - -val split_select = prove_goalw Prod.thy [split_def] - "(@(x,y). P x y) = (@xy. P (fst xy) (snd xy))" (K [rtac refl 1]); - -Addsimps [fst_conv, snd_conv, split]; +Addsimps [split]; goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; by (res_inst_tac[("p","s")] PairE 1); @@ -167,10 +162,10 @@ Addsimps [surj_pair]; qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f" - (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]); + (K [rtac ext 1, split_all_tac 1, rtac split 1]); val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)" - (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]); + (K [stac surjective_pairing 1, stac split 1, rtac refl 1]); (*For use with split_tac and the simplifier*) goal Prod.thy "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; @@ -236,6 +231,30 @@ AddSIs [splitI, splitI2, mem_splitI, mem_splitI2]; AddSEs [splitE, mem_splitE]; +(* allows simplifications of nested splits in case of independent predicates *) +goal Prod.thy "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; +by (rtac ext 1); +by (Blast_tac 1); +qed "split_part"; +Addsimps [split_part]; + +goal Prod.thy "(@(x',y'). x = x' & y = y') = (x,y)"; +by (Blast_tac 1); +qed "Eps_split_eq"; +Addsimps [Eps_split_eq]; +(* +the following would be slightly more general, +but cannot be used as rewrite rule: +### Cannot add premise as rewrite rule because it contains (type) unknowns: +### ?y = .x +goal Prod.thy "!!P. [| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"; +by (rtac select_equality 1); +by ( Simp_tac 1); +by (split_all_tac 1); +by (Asm_full_simp_tac 1); +qed "Eps_split_eq"; +*) + (*** prod_fun -- action of the product functor upon functions ***) goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; @@ -332,9 +351,9 @@ qed "mem_Sigma_iff"; AddIffs [mem_Sigma_iff]; -val Collect_Prod = prove_goal Prod.thy +val Collect_split = prove_goal Prod.thy "{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]); -Addsimps [Collect_Prod]; +Addsimps [Collect_split]; (*Suggested by Pierre Chartier*) goal Prod.thy