# HG changeset patch # User paulson # Date 859972786 -7200 # Node ID cdb908486a967d3781f4e97a322e6d3e3e6f6a63 # Parent 36f75c4a0047e5e8273b2312700383105421f646 Reorganization of how classical rules are installed diff -r 36f75c4a0047 -r cdb908486a96 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Wed Apr 02 11:16:40 1997 +0200 +++ b/src/HOL/Prod.ML Wed Apr 02 11:19:46 1997 +0200 @@ -30,16 +30,18 @@ by (REPEAT (ares_tac (prems@[ProdI]) 1)); qed "Pair_inject"; +AddSEs [Pair_inject]; + goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; -by (fast_tac (!claset addIs [Pair_inject]) 1); +by (Fast_tac 1); qed "Pair_eq"; goalw Prod.thy [fst_def] "fst((a,b)) = a"; -by (fast_tac (!claset addIs [select_equality] addSEs [Pair_inject]) 1); +by (fast_tac (!claset addIs [select_equality]) 1); qed "fst_conv"; goalw Prod.thy [snd_def] "snd((a,b)) = b"; -by (fast_tac (!claset addIs [select_equality] addSEs [Pair_inject]) 1); +by (fast_tac (!claset addIs [select_equality]) 1); qed "snd_conv"; goalw Prod.thy [Pair_def] "? x y. p = (x,y)"; @@ -117,7 +119,7 @@ goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))"; by (stac surjective_pairing 1); by (stac split 1); -by (fast_tac (!claset addSEs [Pair_inject]) 1); +by (Fast_tac 1); qed "expand_split"; (** split used as a logical connective or set former **) @@ -157,6 +159,9 @@ by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); qed "mem_splitE"; +AddSIs [splitI, splitI2, mem_splitI, mem_splitI2]; +AddSEs [splitE, mem_splitE]; + (*** 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))"; @@ -198,6 +203,8 @@ "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); +AddSIs [SigmaI]; + (*The general elimination rule*) qed_goalw "SigmaE" Prod.thy [Sigma_def] "[| c: Sigma A B; \ @@ -227,28 +234,34 @@ (rtac (major RS SigmaD1) 1), (rtac (major RS SigmaD2) 1) ]); +AddSEs [SigmaE2, SigmaE]; + val prems = goal Prod.thy "[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; by (cut_facts_tac prems 1); -by (fast_tac (!claset addIs (prems RL [subsetD]) - addSIs [SigmaI] - addSEs [SigmaE]) 1); +by (fast_tac (!claset addIs (prems RL [subsetD])) 1); qed "Sigma_mono"; qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}" - (fn _ => [ (fast_tac (!claset addSEs [SigmaE]) 1) ]); + (fn _ => [ (Fast_tac 1) ]); qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}" - (fn _ => [ (fast_tac (!claset addSEs [SigmaE]) 1) ]); + (fn _ => [ (Fast_tac 1) ]); Addsimps [Sigma_empty1,Sigma_empty2]; goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))"; -by (fast_tac (!claset addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1); +by (Fast_tac 1); qed "mem_Sigma_iff"; Addsimps [mem_Sigma_iff]; +(*Suggested by Pierre Chartier*) +goal Prod.thy + "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; +by (Fast_tac 1); +qed "UNION_Times_distrib"; + (*** Domain of a relation ***) val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r"; @@ -293,11 +306,8 @@ by (rtac (Rep_Unit_inverse RS sym) 1); qed "unit_eq"; -AddSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2]; AddIs [fst_imageI, snd_imageI, prod_fun_imageI]; -AddSEs [SigmaE2, SigmaE, splitE, mem_splitE, - fst_imageE, snd_imageE, prod_fun_imageE, - Pair_inject]; +AddSEs [fst_imageE, snd_imageE, prod_fun_imageE]; structure Prod_Syntax = struct