author paulson Mon, 01 Mar 1999 15:57:29 +0100 changeset 6291 2c3f72d9f5d1 parent 6290 31483ca40e91 child 6292 e50e1142dd06
simpler proofs of congruence rules
 src/HOL/Set.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Set.ML	Mon Feb 22 10:21:59 1999 +0100
+++ b/src/HOL/Set.ML	Mon Mar 01 15:57:29 1999 +0100
@@ -99,22 +99,20 @@

(** Congruence rules **)

-val prems = Goal
+val prems = Goalw [Ball_def]
"[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
\    (! x:A. P(x)) = (! x:B. Q(x))";
-by (resolve_tac (prems RL [ssubst]) 1);
-by (REPEAT (ares_tac [ballI,iffI] 1
-     ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
+by (asm_simp_tac (simpset() addsimps prems) 1);
qed "ball_cong";

-val prems = Goal
+val prems = Goalw [Bex_def]
"[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
\    (? x:A. P(x)) = (? x:B. Q(x))";
-by (resolve_tac (prems RL [ssubst]) 1);
-by (REPEAT (etac bexE 1
-     ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
qed "bex_cong";

+
section "Subsets";

val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
@@ -496,12 +494,10 @@

-val prems = Goal
+val prems = Goalw [UNION_def]
"[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
\    (UN x:A. C(x)) = (UN x:B. D(x))";
-by (REPEAT (etac UN_E 1
-     ORELSE ares_tac ([UN_I,equalityI,subsetI] @
-                      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
+by (asm_simp_tac (simpset() addsimps prems) 1);
qed "UN_cong";

@@ -532,12 +528,10 @@

-val prems = Goal
+val prems = Goalw [INTER_def]
"[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
\    (INT x:A. C(x)) = (INT x:B. D(x))";
-by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
-by (REPEAT (dtac INT_D 1
-     ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
+by (asm_simp_tac (simpset() addsimps prems) 1);
qed "INT_cong";

@@ -676,8 +670,7 @@

val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;