bind_thms;
authorwenzelm
Wed Sep 29 14:38:03 1999 +0200 (1999-09-29)
changeset 76488258b93cdd32
parent 7647 2ceddd91cd0a
child 7649 ae25e28e5ce9
bind_thms;
src/HOL/equalities.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/equalities.ML	Wed Sep 29 14:36:36 1999 +0200
     1.2 +++ b/src/HOL/equalities.ML	Wed Sep 29 14:38:03 1999 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  qed "Int_assoc";
     1.5  
     1.6  (*Intersection is an AC-operator*)
     1.7 -val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
     1.8 +bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
     1.9  
    1.10  Goal "B<=A ==> A Int B = B";
    1.11  by (Blast_tac 1);
    1.12 @@ -240,7 +240,7 @@
    1.13  qed "Un_assoc";
    1.14  
    1.15  (*Union is an AC-operator*)
    1.16 -val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
    1.17 +bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
    1.18  
    1.19  Goal "A<=B ==> A Un B = B";
    1.20  by (Blast_tac 1);
    1.21 @@ -436,7 +436,7 @@
    1.22  
    1.23  (*Basic identities*)
    1.24  
    1.25 -val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
    1.26 +bind_thm ("not_empty", prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]));
    1.27  
    1.28  Goal "(UN x:{}. B x) = {}";
    1.29  by (Blast_tac 1);
    1.30 @@ -896,4 +896,11 @@
    1.31  
    1.32  end;
    1.33  
    1.34 +bind_thms ("UN_simps", UN_simps);
    1.35 +bind_thms ("INT_simps", INT_simps);
    1.36 +bind_thms ("ball_simps", ball_simps);
    1.37 +bind_thms ("bex_simps", bex_simps);
    1.38 +bind_thm ("ball_conj_distrib", ball_conj_distrib);
    1.39 +bind_thm ("bex_disj_distrib", bex_disj_distrib);
    1.40 +
    1.41  Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
     2.1 --- a/src/HOL/simpdata.ML	Wed Sep 29 14:36:36 1999 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Wed Sep 29 14:38:03 1999 +0200
     2.3 @@ -161,7 +161,7 @@
     2.4          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
     2.5  
     2.6  (*Miniscoping: pushing in existential quantifiers*)
     2.7 -val ex_simps = map prover 
     2.8 +val ex_simps = map prover
     2.9                  ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
    2.10                   "(EX x. P & Q x)   = (P & (EX x. Q x))",
    2.11                   "(EX x. P x | Q)   = ((EX x. P x) | Q)",
    2.12 @@ -192,6 +192,10 @@
    2.13  
    2.14  end;
    2.15  
    2.16 +bind_thms ("ex_simps", ex_simps);
    2.17 +bind_thms ("all_simps", all_simps);
    2.18 +
    2.19 +
    2.20  (* Elimination of True from asumptions: *)
    2.21  
    2.22  val True_implies_equals = prove_goal (the_context ())