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.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 *}
```