1.1 --- a/doc-src/TutorialI/Sets/Examples.thy	Wed Jan 10 20:41:14 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Jan 11 11:35:39 2001 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4  text{*complement, union and universal set*}
     1.5  
     1.6  lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
     1.7 -  apply (blast)
     1.8 -  done
     1.9 +by blast
    1.10  
    1.11  text{*
    1.12  @{thm[display] IntI[no_vars]}
    1.13 @@ -24,8 +23,7 @@
    1.14  *}
    1.15  
    1.16  lemma "(x \<in> -A) = (x \<notin> A)"
    1.17 -  apply (blast)
    1.18 -  done
    1.19 +by blast
    1.20  
    1.21  text{*
    1.22  @{thm[display] Compl_iff[no_vars]}
    1.23 @@ -33,8 +31,7 @@
    1.24  *}
    1.25  
    1.26  lemma "- (A \<union> B) = -A \<inter> -B"
    1.27 -  apply (blast)
    1.28 -  done
    1.29 +by blast
    1.30  
    1.31  text{*
    1.32  @{thm[display] Compl_Un[no_vars]}
    1.33 @@ -42,8 +39,7 @@
    1.34  *}
    1.35  
    1.36  lemma "A-A = {}"
    1.37 -  apply (blast)
    1.38 -  done
    1.39 +by blast
    1.40  
    1.41  text{*
    1.42  @{thm[display] Diff_disjoint[no_vars]}
    1.43 @@ -53,8 +49,7 @@
    1.44    
    1.45  
    1.46  lemma "A \<union> -A = UNIV"
    1.47 -  apply (blast)
    1.48 -  done
    1.49 +by blast
    1.50  
    1.51  text{*
    1.52  @{thm[display] Compl_partition[no_vars]}
    1.53 @@ -73,8 +68,7 @@
    1.54  *}
    1.55  
    1.56  lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
    1.57 -  apply (blast)
    1.58 -  done
    1.59 +by blast
    1.60  
    1.61  text{*
    1.62  @{thm[display] Un_subset_iff[no_vars]}
    1.63 @@ -82,8 +76,7 @@
    1.64  *}
    1.65  
    1.66  lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
    1.67 -  apply (blast)
    1.68 -  done
    1.69 +by blast
    1.70  
    1.71  lemma "(A <= -B) = (B <= -A)"
    1.72    oops
    1.73 @@ -92,8 +85,7 @@
    1.74   it doesn't have to be sets*}
    1.75  
    1.76  lemma "((A:: 'a set) <= -B) = (B <= -A)"
    1.77 -  apply (blast)
    1.78 -  done
    1.79 +by blast
    1.80  
    1.81  text{*A type constraint lets it work*}
    1.82  
    1.83 @@ -119,8 +111,7 @@
    1.84  text{*finite set notation*}
    1.85  
    1.86  lemma "insert x A = {x} \<union> A"
    1.87 -  apply (blast)
    1.88 -  done
    1.89 +by blast
    1.90  
    1.91  text{*
    1.92  @{thm[display] insert_is_Un[no_vars]}
    1.93 @@ -128,26 +119,23 @@
    1.94  *}
    1.95  
    1.96  lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
    1.97 -  apply (blast)
    1.98 -  done
    1.99 +by blast
   1.100  
   1.101  lemma "{a,b} \<inter> {b,c} = {b}"
   1.102 -  apply (auto)
   1.103 -  oops
   1.104 +apply auto
   1.105 +oops
   1.106  text{*fails because it isn't valid*}
   1.107  
   1.108  lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
   1.109 -  apply (simp)
   1.110 -  apply (blast)
   1.111 -  done
   1.112 +apply simp
   1.113 +by blast
   1.114  
   1.115  text{*or just force or auto.  blast alone can't handle the if-then-else*}
   1.116  
   1.117  text{*next: some comprehension examples*}
   1.118  
   1.119  lemma "(a \<in> {z. P z}) = P a"
   1.120 -  apply (blast)
   1.121 -  done
   1.122 +by blast
   1.123  
   1.124  text{*
   1.125  @{thm[display] mem_Collect_eq[no_vars]}
   1.126 @@ -155,8 +143,7 @@
   1.127  *}
   1.128  
   1.129  lemma "{x. x \<in> A} = A"
   1.130 -  apply (blast)
   1.131 -  done
   1.132 +by blast
   1.133    
   1.134  text{*
   1.135  @{thm[display] Collect_mem_eq[no_vars]}
   1.136 @@ -164,12 +151,10 @@
   1.137  *}
   1.138  
   1.139  lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
   1.140 -  apply (blast)
   1.141 -  done
   1.142 +by blast
   1.143  
   1.144  lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
   1.145 -  apply (blast)
   1.146 -  done
   1.147 +by blast
   1.148  
   1.149  constdefs
   1.150    prime   :: "nat set"
   1.151 @@ -177,16 +162,14 @@
   1.152  
   1.153  lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = 
   1.154         {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
   1.155 -  apply (blast)
   1.156 -  done
   1.157 +by (rule refl)
   1.158  
   1.159  text{*binders*}
   1.160  
   1.161  text{*bounded quantifiers*}
   1.162  
   1.163  lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
   1.164 -  apply (blast)
   1.165 -  done
   1.166 +by blast
   1.167  
   1.168  text{*
   1.169  @{thm[display] bexI[no_vars]}
   1.170 @@ -199,8 +182,7 @@
   1.171  *}
   1.172  
   1.173  lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
   1.174 -  apply (blast)
   1.175 -  done
   1.176 +by blast
   1.177  
   1.178  text{*
   1.179  @{thm[display] ballI[no_vars]}
   1.180 @@ -215,8 +197,7 @@
   1.181  text{*indexed unions and variations*}
   1.182  
   1.183  lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
   1.184 -  apply (blast)
   1.185 -  done
   1.186 +by blast
   1.187  
   1.188  text{*
   1.189  @{thm[display] UN_iff[no_vars]}
   1.190 @@ -229,12 +210,10 @@
   1.191  *}
   1.192  
   1.193  lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   1.194 -  apply (blast)
   1.195 -  done
   1.196 +by blast
   1.197  
   1.198  lemma "\<Union>S = (\<Union>x\<in>S. x)"
   1.199 -  apply (blast)
   1.200 -  done
   1.201 +by blast
   1.202  
   1.203  text{*
   1.204  @{thm[display] UN_I[no_vars]}
   1.205 @@ -249,8 +228,7 @@
   1.206  text{*indexed intersections*}
   1.207  
   1.208  lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
   1.209 -  apply (blast)
   1.210 -  done
   1.211 +by blast
   1.212  
   1.213  text{*
   1.214  @{thm[display] INT_iff[no_vars]}