src/HOL/Set.thy
changeset 14208 144f45277d5a
parent 14098 54f130df1136
child 14302 6c24235e8d5d
     1.1 --- a/src/HOL/Set.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -779,8 +779,7 @@
     1.4  lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
     1.5    apply safe
     1.6     prefer 2 apply fast
     1.7 -  apply (rule_tac x = "{a. a : A & f a : B}" in exI)
     1.8 -  apply fast
     1.9 +  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
    1.10    done
    1.11  
    1.12  lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
    1.13 @@ -1044,8 +1043,7 @@
    1.14  
    1.15  lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
    1.16    -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
    1.17 -  apply (rule_tac x = "A - {a}" in exI)
    1.18 -  apply blast
    1.19 +  apply (rule_tac x = "A - {a}" in exI, blast)
    1.20    done
    1.21  
    1.22  lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
    1.23 @@ -1103,9 +1101,7 @@
    1.24    by auto
    1.25  
    1.26  lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
    1.27 -  apply (subst image_image)
    1.28 -  apply simp
    1.29 -  done
    1.30 +by (subst image_image, simp)
    1.31  
    1.32  
    1.33  text {* \medskip @{text Int} *}
    1.34 @@ -1345,7 +1341,7 @@
    1.35  lemma Inter_UNIV_conv [iff]:
    1.36    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
    1.37    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
    1.38 -  by(blast)+
    1.39 +  by blast+
    1.40  
    1.41  
    1.42  text {*
    1.43 @@ -1578,8 +1574,7 @@
    1.44  
    1.45  lemma all_bool_eq: "(\<forall>b::bool. P b) = (P True & P False)"
    1.46    apply auto
    1.47 -  apply (tactic {* case_tac "b" 1 *})
    1.48 -   apply auto
    1.49 +  apply (tactic {* case_tac "b" 1 *}, auto)
    1.50    done
    1.51  
    1.52  lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
    1.53 @@ -1587,8 +1582,7 @@
    1.54  
    1.55  lemma ex_bool_eq: "(\<exists>b::bool. P b) = (P True | P False)"
    1.56    apply auto
    1.57 -  apply (tactic {* case_tac "b" 1 *})
    1.58 -   apply auto
    1.59 +  apply (tactic {* case_tac "b" 1 *}, auto)
    1.60    done
    1.61  
    1.62  lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
    1.63 @@ -1596,14 +1590,12 @@
    1.64  
    1.65  lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
    1.66    apply auto
    1.67 -  apply (tactic {* case_tac "b" 1 *})
    1.68 -   apply auto
    1.69 +  apply (tactic {* case_tac "b" 1 *}, auto)
    1.70    done
    1.71  
    1.72  lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
    1.73    apply auto
    1.74 -  apply (tactic {* case_tac "b" 1 *})
    1.75 -  apply auto
    1.76 +  apply (tactic {* case_tac "b" 1 *}, auto)
    1.77    done
    1.78  
    1.79  
    1.80 @@ -1800,8 +1792,7 @@
    1.81  
    1.82  lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
    1.83    apply (rule impI)
    1.84 -  apply (erule subsetD)
    1.85 -  apply assumption
    1.86 +  apply (erule subsetD, assumption)
    1.87    done
    1.88  
    1.89  lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
    1.90 @@ -1843,8 +1834,7 @@
    1.91      ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    1.92      -- {* Courtesy of Stephan Merz *}
    1.93    apply clarify
    1.94 -  apply (erule_tac P = "%x. x : S" in LeastI2)
    1.95 -   apply fast
    1.96 +  apply (erule_tac P = "%x. x : S" in LeastI2, fast)
    1.97    apply (rule LeastI2)
    1.98    apply (auto elim: monoD intro!: order_antisym)
    1.99    done