author paulson Mon Mar 01 15:57:29 1999 +0100 (1999-03-01) changeset 6291 2c3f72d9f5d1 parent 6290 31483ca40e91 child 6292 e50e1142dd06
simpler proofs of congruence rules
 src/HOL/Set.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Set.ML	Mon Feb 22 10:21:59 1999 +0100
1.2 +++ b/src/HOL/Set.ML	Mon Mar 01 15:57:29 1999 +0100
1.3 @@ -99,22 +99,20 @@
1.4
1.5  (** Congruence rules **)
1.6
1.7 -val prems = Goal
1.8 +val prems = Goalw [Ball_def]
1.9      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
1.10  \    (! x:A. P(x)) = (! x:B. Q(x))";
1.11 -by (resolve_tac (prems RL [ssubst]) 1);
1.12 -by (REPEAT (ares_tac [ballI,iffI] 1
1.13 -     ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
1.14 +by (asm_simp_tac (simpset() addsimps prems) 1);
1.15  qed "ball_cong";
1.16
1.17 -val prems = Goal
1.18 +val prems = Goalw [Bex_def]
1.19      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
1.20  \    (? x:A. P(x)) = (? x:B. Q(x))";
1.21 -by (resolve_tac (prems RL [ssubst]) 1);
1.22 -by (REPEAT (etac bexE 1
1.23 -     ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
1.25  qed "bex_cong";
1.26
1.28 +
1.29  section "Subsets";
1.30
1.31  val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
1.32 @@ -496,12 +494,10 @@
1.35
1.36 -val prems = Goal
1.37 +val prems = Goalw [UNION_def]
1.38      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
1.39  \    (UN x:A. C(x)) = (UN x:B. D(x))";
1.40 -by (REPEAT (etac UN_E 1
1.41 -     ORELSE ares_tac ([UN_I,equalityI,subsetI] @
1.42 -                      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
1.43 +by (asm_simp_tac (simpset() addsimps prems) 1);
1.44  qed "UN_cong";
1.45
1.46
1.47 @@ -532,12 +528,10 @@
1.50
1.51 -val prems = Goal
1.52 +val prems = Goalw [INTER_def]
1.53      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
1.54  \    (INT x:A. C(x)) = (INT x:B. D(x))";
1.55 -by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
1.56 -by (REPEAT (dtac INT_D 1
1.57 -     ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
1.58 +by (asm_simp_tac (simpset() addsimps prems) 1);
1.59  qed "INT_cong";
1.60
1.61
1.62 @@ -676,8 +670,7 @@
1.63
1.64  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
1.65
1.66 -simpset_ref() := simpset() addcongs [ball_cong,bex_cong]
1.67 -                    setmksimps (mksimps mksimps_pairs);
1.68 +simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
1.69