src/HOL/Set.ML
changeset 5069 3ea049f7979d
parent 4830 bd73675adbed
child 5143 b94cd208f073
     1.1 --- a/src/HOL/Set.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  Addsimps [Collect_mem_eq];
     1.5  AddIffs  [mem_Collect_eq];
     1.6  
     1.7 -goal Set.thy "!!a. P(a) ==> a : {x. P(x)}";
     1.8 +Goal "!!a. P(a) ==> a : {x. P(x)}";
     1.9  by (Asm_simp_tac 1);
    1.10  qed "CollectI";
    1.11  
    1.12 @@ -82,12 +82,12 @@
    1.13  AddSEs [bexE];
    1.14  
    1.15  (*Trival rewrite rule*)
    1.16 -goal Set.thy "(! x:A. P) = ((? x. x:A) --> P)";
    1.17 +Goal "(! x:A. P) = ((? x. x:A) --> P)";
    1.18  by (simp_tac (simpset() addsimps [Ball_def]) 1);
    1.19  qed "ball_triv";
    1.20  
    1.21  (*Dual form for existentials*)
    1.22 -goal Set.thy "(? x:A. P) = ((? x. x:A) & P)";
    1.23 +Goal "(? x:A. P) = ((? x. x:A) & P)";
    1.24  by (simp_tac (simpset() addsimps [Bex_def]) 1);
    1.25  qed "bex_triv";
    1.26  
    1.27 @@ -227,11 +227,11 @@
    1.28  (** Eta-contracting these two rules (to remove P) causes them to be ignored
    1.29      because of their interaction with congruence rules. **)
    1.30  
    1.31 -goalw Set.thy [Ball_def] "Ball UNIV P = All P";
    1.32 +Goalw [Ball_def] "Ball UNIV P = All P";
    1.33  by (Simp_tac 1);
    1.34  qed "ball_UNIV";
    1.35  
    1.36 -goalw Set.thy [Bex_def] "Bex UNIV P = Ex P";
    1.37 +Goalw [Bex_def] "Bex UNIV P = Ex P";
    1.38  by (Simp_tac 1);
    1.39  qed "bex_UNIV";
    1.40  Addsimps [ball_UNIV, bex_UNIV];
    1.41 @@ -259,16 +259,16 @@
    1.42  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.43   (fn _ => [ (Blast_tac 1) ]);
    1.44  
    1.45 -goalw Set.thy [Ball_def] "Ball {} P = True";
    1.46 +Goalw [Ball_def] "Ball {} P = True";
    1.47  by (Simp_tac 1);
    1.48  qed "ball_empty";
    1.49  
    1.50 -goalw Set.thy [Bex_def] "Bex {} P = False";
    1.51 +Goalw [Bex_def] "Bex {} P = False";
    1.52  by (Simp_tac 1);
    1.53  qed "bex_empty";
    1.54  Addsimps [ball_empty, bex_empty];
    1.55  
    1.56 -goal thy "UNIV ~= {}";
    1.57 +Goal "UNIV ~= {}";
    1.58  by (blast_tac (claset() addEs [equalityE]) 1);
    1.59  qed "UNIV_not_empty";
    1.60  AddIffs [UNIV_not_empty];
    1.61 @@ -325,11 +325,11 @@
    1.62  
    1.63  Addsimps [Un_iff];
    1.64  
    1.65 -goal Set.thy "!!c. c:A ==> c : A Un B";
    1.66 +Goal "!!c. c:A ==> c : A Un B";
    1.67  by (Asm_simp_tac 1);
    1.68  qed "UnI1";
    1.69  
    1.70 -goal Set.thy "!!c. c:B ==> c : A Un B";
    1.71 +Goal "!!c. c:B ==> c : A Un B";
    1.72  by (Asm_simp_tac 1);
    1.73  qed "UnI2";
    1.74  
    1.75 @@ -356,15 +356,15 @@
    1.76  
    1.77  Addsimps [Int_iff];
    1.78  
    1.79 -goal Set.thy "!!c. [| c:A;  c:B |] ==> c : A Int B";
    1.80 +Goal "!!c. [| c:A;  c:B |] ==> c : A Int B";
    1.81  by (Asm_simp_tac 1);
    1.82  qed "IntI";
    1.83  
    1.84 -goal Set.thy "!!c. c : A Int B ==> c:A";
    1.85 +Goal "!!c. c : A Int B ==> c:A";
    1.86  by (Asm_full_simp_tac 1);
    1.87  qed "IntD1";
    1.88  
    1.89 -goal Set.thy "!!c. c : A Int B ==> c:B";
    1.90 +Goal "!!c. c : A Int B ==> c:B";
    1.91  by (Asm_full_simp_tac 1);
    1.92  qed "IntD2";
    1.93  
    1.94 @@ -436,7 +436,7 @@
    1.95  qed_goal "singletonI" Set.thy "a : {a}"
    1.96   (fn _=> [ (rtac insertI1 1) ]);
    1.97  
    1.98 -goal Set.thy "!!a. b : {a} ==> b=a";
    1.99 +Goal "!!a. b : {a} ==> b=a";
   1.100  by (Blast_tac 1);
   1.101  qed "singletonD";
   1.102  
   1.103 @@ -445,7 +445,7 @@
   1.104  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
   1.105  (fn _ => [Blast_tac 1]);
   1.106  
   1.107 -goal Set.thy "!!a b. {a}={b} ==> a=b";
   1.108 +Goal "!!a b. {a}={b} ==> a=b";
   1.109  by (blast_tac (claset() addEs [equalityE]) 1);
   1.110  qed "singleton_inject";
   1.111  
   1.112 @@ -454,7 +454,7 @@
   1.113  AddSDs [singleton_inject];
   1.114  AddSEs [singletonE];
   1.115  
   1.116 -goal Set.thy "{x. x=a} = {a}";
   1.117 +Goal "{x. x=a} = {a}";
   1.118  by (Blast_tac 1);
   1.119  qed "singleton_conv";
   1.120  Addsimps [singleton_conv];
   1.121 @@ -462,14 +462,14 @@
   1.122  
   1.123  section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
   1.124  
   1.125 -goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
   1.126 +Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
   1.127  by (Blast_tac 1);
   1.128  qed "UN_iff";
   1.129  
   1.130  Addsimps [UN_iff];
   1.131  
   1.132  (*The order of the premises presupposes that A is rigid; b may be flexible*)
   1.133 -goal Set.thy "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   1.134 +Goal "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   1.135  by Auto_tac;
   1.136  qed "UN_I";
   1.137  
   1.138 @@ -493,7 +493,7 @@
   1.139  
   1.140  section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
   1.141  
   1.142 -goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
   1.143 +Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
   1.144  by Auto_tac;
   1.145  qed "INT_iff";
   1.146  
   1.147 @@ -504,7 +504,7 @@
   1.148  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
   1.149  qed "INT_I";
   1.150  
   1.151 -goal Set.thy "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   1.152 +Goal "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   1.153  by Auto_tac;
   1.154  qed "INT_D";
   1.155  
   1.156 @@ -529,14 +529,14 @@
   1.157  
   1.158  section "Union";
   1.159  
   1.160 -goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
   1.161 +Goalw [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
   1.162  by (Blast_tac 1);
   1.163  qed "Union_iff";
   1.164  
   1.165  Addsimps [Union_iff];
   1.166  
   1.167  (*The order of the premises presupposes that C is rigid; A may be flexible*)
   1.168 -goal Set.thy "!!X. [| X:C;  A:X |] ==> A : Union(C)";
   1.169 +Goal "!!X. [| X:C;  A:X |] ==> A : Union(C)";
   1.170  by Auto_tac;
   1.171  qed "UnionI";
   1.172  
   1.173 @@ -552,7 +552,7 @@
   1.174  
   1.175  section "Inter";
   1.176  
   1.177 -goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
   1.178 +Goalw [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
   1.179  by (Blast_tac 1);
   1.180  qed "Inter_iff";
   1.181  
   1.182 @@ -565,7 +565,7 @@
   1.183  
   1.184  (*A "destruct" rule -- every X in C contains A as an element, but
   1.185    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   1.186 -goal Set.thy "!!X. [| A : Inter(C);  X:C |] ==> A:X";
   1.187 +Goal "!!X. [| A : Inter(C);  X:C |] ==> A:X";
   1.188  by Auto_tac;
   1.189  qed "InterD";
   1.190  
   1.191 @@ -600,20 +600,20 @@
   1.192  AddIs  [image_eqI];
   1.193  AddSEs [imageE]; 
   1.194  
   1.195 -goalw thy [o_def] "(f o g)``r = f``(g``r)";
   1.196 +Goalw [o_def] "(f o g)``r = f``(g``r)";
   1.197  by (Blast_tac 1);
   1.198  qed "image_compose";
   1.199  
   1.200 -goal thy "f``(A Un B) = f``A Un f``B";
   1.201 +Goal "f``(A Un B) = f``A Un f``B";
   1.202  by (Blast_tac 1);
   1.203  qed "image_Un";
   1.204  
   1.205 -goal thy "(z : f``A) = (EX x:A. z = f x)";
   1.206 +Goal "(z : f``A) = (EX x:A. z = f x)";
   1.207  by (Blast_tac 1);
   1.208  qed "image_iff";
   1.209  
   1.210  (*This rewrite rule would confuse users if made default.*)
   1.211 -goal thy "(f``A <= B) = (ALL x:A. f(x): B)";
   1.212 +Goal "(f``A <= B) = (ALL x:A. f(x): B)";
   1.213  by (Blast_tac 1);
   1.214  qed "image_subset_iff";
   1.215  
   1.216 @@ -626,7 +626,7 @@
   1.217  
   1.218  (*** Range of a function -- just a translation for image! ***)
   1.219  
   1.220 -goal thy "!!b. b=f(x) ==> b : range(f)";
   1.221 +Goal "!!b. b=f(x) ==> b : range(f)";
   1.222  by (EVERY1 [etac image_eqI, rtac UNIV_I]);
   1.223  bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
   1.224  
   1.225 @@ -663,7 +663,7 @@
   1.226                   mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
   1.227  
   1.228  (*Not for Addsimps -- it can cause goals to blow up!*)
   1.229 -goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
   1.230 +Goal "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
   1.231  by (Simp_tac 1);
   1.232  qed "mem_if";
   1.233  
   1.234 @@ -677,11 +677,11 @@
   1.235  
   1.236  (*** < ***)
   1.237  
   1.238 -goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
   1.239 +Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
   1.240  by (Blast_tac 1);
   1.241  qed "psubsetI";
   1.242  
   1.243 -goalw Set.thy [psubset_def]
   1.244 +Goalw [psubset_def]
   1.245      "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
   1.246  by Auto_tac;
   1.247  qed "psubset_insertD";