src/HOL/Set.ML
changeset 7031 972b5f62f476
parent 7007 b46ccfee8e59
child 7441 20b3e2d2fcb6
     1.1 --- a/src/HOL/Set.ML	Mon Jul 19 15:19:11 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Jul 19 15:24:35 1999 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "rev_bexI";
     1.6  
     1.7 -val prems = goal Set.thy 
     1.8 +val prems = Goal 
     1.9     "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)";
    1.10  by (rtac classical 1);
    1.11  by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ;
    1.12 @@ -223,14 +223,18 @@
    1.13  
    1.14  section "The universal set -- UNIV";
    1.15  
    1.16 -qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
    1.17 -  (fn _ => [rtac CollectI 1, rtac TrueI 1]);
    1.18 +Goalw [UNIV_def] "x : UNIV";
    1.19 +by (rtac CollectI 1);
    1.20 +by (rtac TrueI 1);
    1.21 +qed "UNIV_I";
    1.22  
    1.23  Addsimps [UNIV_I];
    1.24  AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
    1.25  
    1.26 -qed_goal "subset_UNIV" Set.thy "A <= UNIV"
    1.27 -  (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
    1.28 +Goal "A <= UNIV";
    1.29 +by (rtac subsetI 1);
    1.30 +by (rtac UNIV_I 1);
    1.31 +qed "subset_UNIV";
    1.32  
    1.33  (** Eta-contracting these two rules (to remove P) causes them to be ignored
    1.34      because of their interaction with congruence rules. **)
    1.35 @@ -266,7 +270,7 @@
    1.36  (*One effect is to delete the ASSUMPTION {} <= A*)
    1.37  AddIffs [empty_subsetI];
    1.38  
    1.39 -val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}";
    1.40 +val [prem]= Goal "[| !!y. y:A ==> False |] ==> A={}";
    1.41  by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
    1.42  qed "equals0I";
    1.43  
    1.44 @@ -301,11 +305,11 @@
    1.45  
    1.46  AddIffs [Pow_iff]; 
    1.47  
    1.48 -Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)";
    1.49 +Goalw [Pow_def] "A <= B ==> A : Pow(B)";
    1.50  by (etac CollectI 1);
    1.51  qed "PowI";
    1.52  
    1.53 -Goalw [Pow_def] "!!A B. A : Pow(B)  ==>  A<=B";
    1.54 +Goalw [Pow_def] "A : Pow(B)  ==>  A<=B";
    1.55  by (etac CollectD 1);
    1.56  qed "PowD";
    1.57  
    1.58 @@ -316,8 +320,9 @@
    1.59  
    1.60  section "Set complement";
    1.61  
    1.62 -qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
    1.63 - (fn _ => [ (Blast_tac 1) ]);
    1.64 +Goalw [Compl_def] "(c : -A) = (c~:A)";
    1.65 +by (Blast_tac 1);
    1.66 +qed "Compl_iff";
    1.67  
    1.68  Addsimps [Compl_iff];
    1.69  
    1.70 @@ -340,9 +345,9 @@
    1.71  
    1.72  section "Binary union -- Un";
    1.73  
    1.74 -qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
    1.75 - (fn _ => [ Blast_tac 1 ]);
    1.76 -
    1.77 +Goalw [Un_def] "(c : A Un B) = (c:A | c:B)";
    1.78 +by (Blast_tac 1);
    1.79 +qed "Un_iff";
    1.80  Addsimps [Un_iff];
    1.81  
    1.82  Goal "c:A ==> c : A Un B";
    1.83 @@ -355,7 +360,7 @@
    1.84  
    1.85  (*Classical introduction rule: no commitment to A vs B*)
    1.86  
    1.87 -val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B";
    1.88 +val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";
    1.89  by (Simp_tac 1);
    1.90  by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
    1.91  qed "UnCI";
    1.92 @@ -372,9 +377,9 @@
    1.93  
    1.94  section "Binary intersection -- Int";
    1.95  
    1.96 -qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
    1.97 - (fn _ => [ (Blast_tac 1) ]);
    1.98 -
    1.99 +Goalw [Int_def] "(c : A Int B) = (c:A & c:B)";
   1.100 +by (Blast_tac 1);
   1.101 +qed "Int_iff";
   1.102  Addsimps [Int_iff];
   1.103  
   1.104  Goal "[| c:A;  c:B |] ==> c : A Int B";
   1.105 @@ -401,9 +406,9 @@
   1.106  
   1.107  section "Set difference";
   1.108  
   1.109 -qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
   1.110 - (fn _ => [ (Blast_tac 1) ]);
   1.111 -
   1.112 +Goalw [set_diff_def] "(c : A-B) = (c:A & c~:B)";
   1.113 +by (Blast_tac 1);
   1.114 +qed "Diff_iff";
   1.115  Addsimps [Diff_iff];
   1.116  
   1.117  Goal "[| c : A;  c ~: B |] ==> c : A - B";
   1.118 @@ -418,7 +423,7 @@
   1.119  by (Asm_full_simp_tac 1) ;
   1.120  qed "DiffD2";
   1.121  
   1.122 -val prems= goal Set.thy "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
   1.123 +val prems = Goal "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
   1.124  by (resolve_tac prems 1);
   1.125  by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
   1.126  qed "DiffE";
   1.127 @@ -429,12 +434,12 @@
   1.128  
   1.129  section "Augmenting a set -- insert";
   1.130  
   1.131 -qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
   1.132 - (fn _ => [Blast_tac 1]);
   1.133 -
   1.134 +Goalw [insert_def] "a : insert b A = (a=b | a:A)";
   1.135 +by (Blast_tac 1);
   1.136 +qed "insert_iff";
   1.137  Addsimps [insert_iff];
   1.138  
   1.139 -val _ = goal Set.thy "a : insert a B";
   1.140 +Goal "a : insert a B";
   1.141  by (Simp_tac 1);
   1.142  qed "insertI1";
   1.143  
   1.144 @@ -449,7 +454,7 @@
   1.145  qed "insertE";
   1.146  
   1.147  (*Classical introduction rule*)
   1.148 -val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B";
   1.149 +val prems = Goal "(a~:B ==> a=b) ==> a: insert b B";
   1.150  by (Simp_tac 1);
   1.151  by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
   1.152  qed "insertCI";