src/HOL/Relation.thy
changeset 17589 58eeffd73be1
parent 15177 e7616269fdca
child 19228 30fce6da8cbe
     1.1 --- a/src/HOL/Relation.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    by (simp add: Id_def)
     1.5  
     1.6  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
     1.7 -  by (unfold Id_def) (rules elim: CollectE)
     1.8 +  by (unfold Id_def) (iprover elim: CollectE)
     1.9  
    1.10  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
    1.11    by (unfold Id_def) blast
    1.12 @@ -100,7 +100,7 @@
    1.13  lemma diagE [elim!]:
    1.14    "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.15    -- {* The general elimination rule. *}
    1.16 -  by (unfold diag_def) (rules elim!: UN_E singletonE)
    1.17 +  by (unfold diag_def) (iprover elim!: UN_E singletonE)
    1.18  
    1.19  lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
    1.20    by blast
    1.21 @@ -117,11 +117,11 @@
    1.22  
    1.23  lemma rel_compE [elim!]: "xz : r O s ==>
    1.24    (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
    1.25 -  by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE)
    1.26 +  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    1.27  
    1.28  lemma rel_compEpair:
    1.29    "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
    1.30 -  by (rules elim: rel_compE Pair_inject ssubst)
    1.31 +  by (iprover elim: rel_compE Pair_inject ssubst)
    1.32  
    1.33  lemma R_O_Id [simp]: "R O Id = R"
    1.34    by fast
    1.35 @@ -146,7 +146,7 @@
    1.36  subsection {* Reflexivity *}
    1.37  
    1.38  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
    1.39 -  by (unfold refl_def) (rules intro!: ballI)
    1.40 +  by (unfold refl_def) (iprover intro!: ballI)
    1.41  
    1.42  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
    1.43    by (unfold refl_def) blast
    1.44 @@ -156,10 +156,10 @@
    1.45  
    1.46  lemma antisymI:
    1.47    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
    1.48 -  by (unfold antisym_def) rules
    1.49 +  by (unfold antisym_def) iprover
    1.50  
    1.51  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
    1.52 -  by (unfold antisym_def) rules
    1.53 +  by (unfold antisym_def) iprover
    1.54  
    1.55  
    1.56  subsection {* Symmetry and Transitivity *}
    1.57 @@ -169,10 +169,10 @@
    1.58  
    1.59  lemma transI:
    1.60    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
    1.61 -  by (unfold trans_def) rules
    1.62 +  by (unfold trans_def) iprover
    1.63  
    1.64  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
    1.65 -  by (unfold trans_def) rules
    1.66 +  by (unfold trans_def) iprover
    1.67  
    1.68  
    1.69  subsection {* Converse *}
    1.70 @@ -189,7 +189,7 @@
    1.71  lemma converseE [elim!]:
    1.72    "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
    1.73      -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
    1.74 -  by (unfold converse_def) (rules elim!: CollectE splitE bexE)
    1.75 +  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
    1.76  
    1.77  lemma converse_converse [simp]: "(r^-1)^-1 = r"
    1.78    by (unfold converse_def) blast
    1.79 @@ -219,11 +219,11 @@
    1.80    by (unfold Domain_def) blast
    1.81  
    1.82  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
    1.83 -  by (rules intro!: iffD2 [OF Domain_iff])
    1.84 +  by (iprover intro!: iffD2 [OF Domain_iff])
    1.85  
    1.86  lemma DomainE [elim!]:
    1.87    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
    1.88 -  by (rules dest!: iffD1 [OF Domain_iff])
    1.89 +  by (iprover dest!: iffD1 [OF Domain_iff])
    1.90  
    1.91  lemma Domain_empty [simp]: "Domain {} = {}"
    1.92    by blast
    1.93 @@ -259,10 +259,10 @@
    1.94    by (simp add: Domain_def Range_def)
    1.95  
    1.96  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
    1.97 -  by (unfold Range_def) (rules intro!: converseI DomainI)
    1.98 +  by (unfold Range_def) (iprover intro!: converseI DomainI)
    1.99  
   1.100  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
   1.101 -  by (unfold Range_def) (rules elim!: DomainE dest!: converseD)
   1.102 +  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   1.103  
   1.104  lemma Range_empty [simp]: "Range {} = {}"
   1.105    by blast
   1.106 @@ -305,7 +305,7 @@
   1.107  
   1.108  lemma ImageE [elim!]:
   1.109      "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   1.110 -  by (unfold Image_def) (rules elim!: CollectE bexE)
   1.111 +  by (unfold Image_def) (iprover elim!: CollectE bexE)
   1.112  
   1.113  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   1.114    -- {* This version's more effective when we already have the required @{text a} *}
   1.115 @@ -334,7 +334,7 @@
   1.116    by blast
   1.117  
   1.118  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
   1.119 -  by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.120 +  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.121  
   1.122  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   1.123    -- {* NOT suitable for rewriting *}