src/HOL/Set.thy
changeset 17589 58eeffd73be1
parent 17508 c84af7f39a6b
child 17702 ea88ddeafabe
     1.1 --- a/src/HOL/Set.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -542,7 +542,7 @@
     1.4  
     1.5  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
     1.6    -- {* Anti-symmetry of the subset relation. *}
     1.7 -  by (rules intro: set_ext subsetD)
     1.8 +  by (iprover intro: set_ext subsetD)
     1.9  
    1.10  lemmas equalityI [intro!] = subset_antisym
    1.11  
    1.12 @@ -1046,10 +1046,10 @@
    1.13  text {* \medskip Big Union -- least upper bound of a set. *}
    1.14  
    1.15  lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
    1.16 -  by (rules intro: subsetI UnionI)
    1.17 +  by (iprover intro: subsetI UnionI)
    1.18  
    1.19  lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
    1.20 -  by (rules intro: subsetI elim: UnionE dest: subsetD)
    1.21 +  by (iprover intro: subsetI elim: UnionE dest: subsetD)
    1.22  
    1.23  
    1.24  text {* \medskip General union. *}
    1.25 @@ -1058,7 +1058,7 @@
    1.26    by blast
    1.27  
    1.28  lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
    1.29 -  by (rules intro: subsetI elim: UN_E dest: subsetD)
    1.30 +  by (iprover intro: subsetI elim: UN_E dest: subsetD)
    1.31  
    1.32  
    1.33  text {* \medskip Big Intersection -- greatest lower bound of a set. *}
    1.34 @@ -1071,13 +1071,13 @@
    1.35    by blast
    1.36  
    1.37  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
    1.38 -  by (rules intro: InterI subsetI dest: subsetD)
    1.39 +  by (iprover intro: InterI subsetI dest: subsetD)
    1.40  
    1.41  lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
    1.42    by blast
    1.43  
    1.44  lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
    1.45 -  by (rules intro: INT_I subsetI dest: subsetD)
    1.46 +  by (iprover intro: INT_I subsetI dest: subsetD)
    1.47  
    1.48  
    1.49  text {* \medskip Finite Union -- the least upper bound of two sets. *}
    1.50 @@ -1809,7 +1809,7 @@
    1.51    by blast
    1.52  
    1.53  lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
    1.54 -  by rules
    1.55 +  by iprover
    1.56  
    1.57  
    1.58  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
    1.59 @@ -1955,21 +1955,21 @@
    1.60    done
    1.61  
    1.62  lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
    1.63 -  by rules
    1.64 +  by iprover
    1.65  
    1.66  lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
    1.67 -  by rules
    1.68 +  by iprover
    1.69  
    1.70  lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
    1.71 -  by rules
    1.72 +  by iprover
    1.73  
    1.74  lemma imp_refl: "P --> P" ..
    1.75  
    1.76  lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
    1.77 -  by rules
    1.78 +  by iprover
    1.79  
    1.80  lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
    1.81 -  by rules
    1.82 +  by iprover
    1.83  
    1.84  lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
    1.85    by blast
    1.86 @@ -1983,10 +1983,10 @@
    1.87    ex_mono Collect_mono in_mono
    1.88  
    1.89  lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
    1.90 -  by rules
    1.91 +  by iprover
    1.92  
    1.93  lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
    1.94 -  by rules
    1.95 +  by iprover
    1.96  
    1.97  lemma Least_mono:
    1.98    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y