better miniscoping rules: the premise C~={} is not good
authorpaulson
Fri Nov 20 10:37:12 1998 +0100 (1998-11-20)
changeset 59411db9fad40a4f
parent 5940 33bdc03bba7e
child 5942 9a7bf515fde1
better miniscoping rules: the premise C~={} is not good
because Safe_tac eliminates such assumptions.
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Thu Nov 19 11:49:57 1998 +0100
     1.2 +++ b/src/HOL/equalities.ML	Fri Nov 20 10:37:12 1998 +0100
     1.3 @@ -85,7 +85,7 @@
     1.4  bind_thm ("insert_Collect", prove_goal thy 
     1.5  	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
     1.6  
     1.7 -Goal "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
     1.8 +Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
     1.9  by (Blast_tac 1);
    1.10  qed "UN_insert_distrib";
    1.11  
    1.12 @@ -442,7 +442,6 @@
    1.13  (*Basic identities*)
    1.14  
    1.15  val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
    1.16 -(*Addsimps[not_empty];*)
    1.17  
    1.18  Goal "(UN x:{}. B x) = {}";
    1.19  by (Blast_tac 1);
    1.20 @@ -490,7 +489,7 @@
    1.21  qed "INT_insert";
    1.22  Addsimps[INT_insert];
    1.23  
    1.24 -Goal "A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
    1.25 +Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
    1.26  by (Blast_tac 1);
    1.27  qed "INT_insert_distrib";
    1.28  
    1.29 @@ -502,12 +501,12 @@
    1.30  by (Blast_tac 1);
    1.31  qed "Inter_image_eq";
    1.32  
    1.33 -Goal "A~={} ==> (UN y:A. c) = c";
    1.34 +Goal "u: A ==> (UN y:A. c) = c";
    1.35  by (Blast_tac 1);
    1.36  qed "UN_constant";
    1.37  Addsimps[UN_constant];
    1.38  
    1.39 -Goal "A~={} ==> (INT y:A. c) = c";
    1.40 +Goal "u: A ==> (INT y:A. c) = c";
    1.41  by (Blast_tac 1);
    1.42  qed "INT_constant";
    1.43  Addsimps[INT_constant];
    1.44 @@ -783,9 +782,9 @@
    1.45    fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
    1.46  in
    1.47  val UN_simps = map prover 
    1.48 -    ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
    1.49 -     "!!C. C ~= {} ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
    1.50 -     "!!C. C ~= {} ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
    1.51 +    ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
    1.52 +     "!!C. c: C ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
    1.53 +     "!!C. c: C ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
    1.54       "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
    1.55       "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
    1.56       "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
    1.57 @@ -793,10 +792,10 @@
    1.58       "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
    1.59  
    1.60  val INT_simps = map prover
    1.61 -    ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
    1.62 -     "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
    1.63 -     "!!C. C ~= {} ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
    1.64 -     "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
    1.65 +    ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
    1.66 +     "!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
    1.67 +     "!!C. c: C ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
    1.68 +     "!!C. c: C ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
    1.69       "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
    1.70       "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
    1.71       "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",