simpler proofs of congruence rules
authorpaulson
Mon Mar 01 15:57:29 1999 +0100 (1999-03-01)
changeset 62912c3f72d9f5d1
parent 6290 31483ca40e91
child 6292 e50e1142dd06
simpler proofs of congruence rules
src/HOL/Set.ML
     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.24 +by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps prems) 1);
    1.25  qed "bex_cong";
    1.26  
    1.27 +Addcongs [ball_cong,bex_cong];
    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.33  AddIs  [UN_I];
    1.34  AddSEs [UN_E];
    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.48  AddSIs [INT_I];
    1.49  AddEs  [INT_D, INT_E];
    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  
    1.70  Addsimps[subset_UNIV, subset_refl];
    1.71