more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
authorhaftmann
Thu Mar 01 19:34:52 2012 +0100 (2012-03-01)
changeset 46752e9e7209eb375
parent 46751 6b94c39b7366
child 46753 40e2ada74ce8
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
NEWS
src/HOL/Equiv_Relations.thy
src/HOL/Library/Zorn.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Client.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/ZF/Games.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ex/Set_Theory.thy
src/HOL/ex/Tarski.thy
     1.1 --- a/NEWS	Thu Mar 01 17:13:54 2012 +0000
     1.2 +++ b/NEWS	Thu Mar 01 19:34:52 2012 +0100
     1.3 @@ -90,6 +90,18 @@
     1.4  
     1.5  * New type synonym 'a rel = ('a * 'a) set
     1.6  
     1.7 +* More default pred/set conversions on a couple of relation operations
     1.8 +and predicates.  Consolidation of some relation theorems:
     1.9 +
    1.10 +  converse_def ~> converse_unfold
    1.11 +  rel_comp_def ~> rel_comp_unfold
    1.12 +  symp_def ~> (dropped, use symp_def and sym_def instead)
    1.13 +  transp_def ~> transp_trans
    1.14 +  Domain_def ~> Domain_unfold
    1.15 +  Range_def ~> Domain_converse [symmetric]
    1.16 +
    1.17 +INCOMPATIBILITY.
    1.18 +
    1.19  * Consolidated various theorem names relating to Finite_Set.fold
    1.20  combinator:
    1.21  
    1.22 @@ -99,7 +111,7 @@
    1.23    SUPR_fold_sup ~> SUP_fold_sup
    1.24    union_set ~> union_set_fold
    1.25    minus_set ~> minus_set_fold
    1.26 -  
    1.27 +
    1.28  INCOMPATIBILITY.
    1.29  
    1.30  * Consolidated theorem names concerning fold combinators:
     2.1 --- a/src/HOL/Equiv_Relations.thy	Thu Mar 01 17:13:54 2012 +0000
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Mar 01 19:34:52 2012 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4  
     2.5  lemma sym_trans_comp_subset:
     2.6      "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
     2.7 -  by (unfold trans_def sym_def converse_def) blast
     2.8 +  by (unfold trans_def sym_def converse_unfold) blast
     2.9  
    2.10  lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
    2.11    by (unfold refl_on_def) blast
    2.12 @@ -426,7 +426,7 @@
    2.13  
    2.14  lemma equivp_equiv:
    2.15    "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
    2.16 -  by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def)
    2.17 +  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])
    2.18  
    2.19  lemma equivp_reflp_symp_transp:
    2.20    shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
    2.21 @@ -449,3 +449,4 @@
    2.22    by (erule equivpE, erule transpE)
    2.23  
    2.24  end
    2.25 +
     3.1 --- a/src/HOL/Library/Zorn.thy	Thu Mar 01 17:13:54 2012 +0000
     3.2 +++ b/src/HOL/Library/Zorn.thy	Thu Mar 01 19:34:52 2012 +0100
     3.3 @@ -453,7 +453,7 @@
     3.4      proof
     3.5        assume "m={}"
     3.6        moreover have "Well_order {(x,x)}"
     3.7 -        by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
     3.8 +        by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_unfold Domain_converse [symmetric])
     3.9        ultimately show False using max
    3.10          by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    3.11      qed
    3.12 @@ -470,14 +470,14 @@
    3.13  --{*We show that the extension is a well-order*}
    3.14      have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
    3.15      moreover have "trans ?m" using `trans m` `x \<notin> Field m`
    3.16 -      unfolding trans_def Field_def Domain_def Range_def by blast
    3.17 +      unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
    3.18      moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
    3.19 -      unfolding antisym_def Field_def Domain_def Range_def by blast
    3.20 +      unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast
    3.21      moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def)
    3.22      moreover have "wf(?m-Id)"
    3.23      proof-
    3.24        have "wf ?s" using `x \<notin> Field m`
    3.25 -        by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
    3.26 +        by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
    3.27        thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
    3.28          wf_subset[OF `wf ?s` Diff_subset]
    3.29          by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
    3.30 @@ -485,7 +485,7 @@
    3.31      ultimately have "Well_order ?m" by(simp add:order_on_defs)
    3.32  --{*We show that the extension is above m*}
    3.33      moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
    3.34 -      by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def)
    3.35 +      by(fastforce simp:I_def init_seg_of_def Field_def Domain_unfold Domain_converse [symmetric])
    3.36      ultimately
    3.37  --{*This contradicts maximality of m:*}
    3.38      have False using max `x \<notin> Field m` unfolding Field_def by blast
    3.39 @@ -501,7 +501,7 @@
    3.40      using well_ordering[where 'a = "'a"] by blast
    3.41    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
    3.42    have 1: "Field ?r = A" using wo univ
    3.43 -    by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    3.44 +    by(fastforce simp: Field_def Domain_unfold Domain_converse [symmetric] order_on_defs refl_on_def)
    3.45    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
    3.46      using `Well_order r` by(simp_all add:order_on_defs)
    3.47    have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
     4.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Thu Mar 01 17:13:54 2012 +0000
     4.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Thu Mar 01 19:34:52 2012 +0100
     4.3 @@ -189,10 +189,10 @@
     4.4  by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
     4.5  
     4.6  lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
     4.7 -by (simp add: isLub_def isGlb_def dual_def converse_def)
     4.8 +by (simp add: isLub_def isGlb_def dual_def converse_unfold)
     4.9  
    4.10  lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
    4.11 -by (simp add: isLub_def isGlb_def dual_def converse_def)
    4.12 +by (simp add: isLub_def isGlb_def dual_def converse_unfold)
    4.13  
    4.14  lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
    4.15  apply (insert cl_po)
    4.16 @@ -212,10 +212,10 @@
    4.17  done
    4.18  
    4.19  lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
    4.20 -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
    4.21 +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
    4.22  
    4.23  lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
    4.24 -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
    4.25 +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
    4.26  
    4.27  lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder"
    4.28  by (simp add: PartialOrder_def CompleteLattice_def, fast)
     5.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 01 17:13:54 2012 +0000
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 01 19:34:52 2012 +0100
     5.3 @@ -1043,14 +1043,14 @@
     5.4    (i => bool) => o * i => bool,
     5.5    (i => bool) => i => bool) [inductify] Id_on .
     5.6  thm Id_on.equation
     5.7 -thm Domain_def
     5.8 +thm Domain_unfold
     5.9  code_pred (modes:
    5.10    (o * o => bool) => o => bool,
    5.11    (o * o => bool) => i => bool,
    5.12    (i * o => bool) => i => bool) [inductify] Domain .
    5.13  thm Domain.equation
    5.14  
    5.15 -thm Range_def
    5.16 +thm Domain_converse [symmetric]
    5.17  code_pred (modes:
    5.18    (o * o => bool) => o => bool,
    5.19    (o * o => bool) => i => bool,
     6.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 01 17:13:54 2012 +0000
     6.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 01 19:34:52 2012 +0100
     6.3 @@ -534,7 +534,7 @@
     6.4    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
     6.5    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
     6.6    by (auto intro!: fun_relI)
     6.7 -     (metis (full_types) assms fun_relE pred_comp.intros)
     6.8 +     (metis (full_types) assms fun_relE pred_compI)
     6.9  
    6.10  lemma append_rsp2 [quot_respect]:
    6.11    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
    6.12 @@ -560,7 +560,7 @@
    6.13      by (induct y ya rule: list_induct2')
    6.14         (simp_all, metis apply_rsp' list_eq_def)
    6.15    show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
    6.16 -    by (metis a b c list_eq_def pred_comp.intros)
    6.17 +    by (metis a b c list_eq_def pred_compI)
    6.18  qed
    6.19  
    6.20  lemma map_prs2 [quot_preserve]:
     7.1 --- a/src/HOL/Relation.thy	Thu Mar 01 17:13:54 2012 +0000
     7.2 +++ b/src/HOL/Relation.thy	Thu Mar 01 19:34:52 2012 +0100
     7.3 @@ -113,28 +113,33 @@
     7.4  
     7.5  subsubsection {* Reflexivity *}
     7.6  
     7.7 -definition
     7.8 -  refl_on :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
     7.9 -  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
    7.10 +definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
    7.11 +where
    7.12 +  "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
    7.13  
    7.14 -abbreviation
    7.15 -  refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
    7.16 +abbreviation refl :: "'a rel \<Rightarrow> bool"
    7.17 +where -- {* reflexivity over a type *}
    7.18    "refl \<equiv> refl_on UNIV"
    7.19  
    7.20 -definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
    7.21 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    7.22 +where
    7.23    "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
    7.24  
    7.25 +lemma reflp_refl_eq [pred_set_conv]:
    7.26 +  "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r" 
    7.27 +  by (simp add: refl_on_def reflp_def)
    7.28 +
    7.29  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
    7.30 -by (unfold refl_on_def) (iprover intro!: ballI)
    7.31 +  by (unfold refl_on_def) (iprover intro!: ballI)
    7.32  
    7.33  lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
    7.34 -by (unfold refl_on_def) blast
    7.35 +  by (unfold refl_on_def) blast
    7.36  
    7.37  lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
    7.38 -by (unfold refl_on_def) blast
    7.39 +  by (unfold refl_on_def) blast
    7.40  
    7.41  lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
    7.42 -by (unfold refl_on_def) blast
    7.43 +  by (unfold refl_on_def) blast
    7.44  
    7.45  lemma reflpI:
    7.46    "(\<And>x. r x x) \<Longrightarrow> reflp r"
    7.47 @@ -146,32 +151,40 @@
    7.48    using assms by (auto dest: refl_onD simp add: reflp_def)
    7.49  
    7.50  lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
    7.51 -by (unfold refl_on_def) blast
    7.52 +  by (unfold refl_on_def) blast
    7.53 +
    7.54 +lemma reflp_inf:
    7.55 +  "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)"
    7.56 +  by (auto intro: reflpI elim: reflpE)
    7.57  
    7.58  lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
    7.59 -by (unfold refl_on_def) blast
    7.60 +  by (unfold refl_on_def) blast
    7.61 +
    7.62 +lemma reflp_sup:
    7.63 +  "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)"
    7.64 +  by (auto intro: reflpI elim: reflpE)
    7.65  
    7.66  lemma refl_on_INTER:
    7.67    "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
    7.68 -by (unfold refl_on_def) fast
    7.69 +  by (unfold refl_on_def) fast
    7.70  
    7.71  lemma refl_on_UNION:
    7.72    "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
    7.73 -by (unfold refl_on_def) blast
    7.74 +  by (unfold refl_on_def) blast
    7.75  
    7.76 -lemma refl_on_empty[simp]: "refl_on {} {}"
    7.77 -by(simp add:refl_on_def)
    7.78 +lemma refl_on_empty [simp]: "refl_on {} {}"
    7.79 +  by (simp add:refl_on_def)
    7.80  
    7.81  lemma refl_on_def' [nitpick_unfold, code]:
    7.82 -  "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
    7.83 -by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
    7.84 +  "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
    7.85 +  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
    7.86  
    7.87  
    7.88  subsubsection {* Irreflexivity *}
    7.89  
    7.90 -definition
    7.91 -  irrefl :: "('a * 'a) set => bool" where
    7.92 -  "irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)"
    7.93 +definition irrefl :: "'a rel \<Rightarrow> bool"
    7.94 +where
    7.95 +  "irrefl r \<longleftrightarrow> (\<forall>x. (x, x) \<notin> r)"
    7.96  
    7.97  lemma irrefl_distinct [code]:
    7.98    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
    7.99 @@ -180,166 +193,231 @@
   7.100  
   7.101  subsubsection {* Symmetry *}
   7.102  
   7.103 -definition
   7.104 -  sym :: "('a * 'a) set => bool" where
   7.105 -  "sym r \<longleftrightarrow> (ALL x y. (x,y): r --> (y,x): r)"
   7.106 +definition sym :: "'a rel \<Rightarrow> bool"
   7.107 +where
   7.108 +  "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)"
   7.109 +
   7.110 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   7.111 +where
   7.112 +  "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)"
   7.113  
   7.114 -lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   7.115 -by (unfold sym_def) iprover
   7.116 +lemma symp_sym_eq [pred_set_conv]:
   7.117 +  "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" 
   7.118 +  by (simp add: sym_def symp_def)
   7.119  
   7.120 -lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
   7.121 -by (unfold sym_def, blast)
   7.122 -
   7.123 -definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.124 -  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   7.125 +lemma symI:
   7.126 +  "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
   7.127 +  by (unfold sym_def) iprover
   7.128  
   7.129  lemma sympI:
   7.130 -  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   7.131 -  by (auto intro: symI simp add: symp_def)
   7.132 +  "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r"
   7.133 +  by (fact symI [to_pred])
   7.134 +
   7.135 +lemma symE:
   7.136 +  assumes "sym r" and "(b, a) \<in> r"
   7.137 +  obtains "(a, b) \<in> r"
   7.138 +  using assms by (simp add: sym_def)
   7.139  
   7.140  lemma sympE:
   7.141 -  assumes "symp r" and "r x y"
   7.142 -  obtains "r y x"
   7.143 -  using assms by (auto dest: symD simp add: symp_def)
   7.144 +  assumes "symp r" and "r b a"
   7.145 +  obtains "r a b"
   7.146 +  using assms by (rule symE [to_pred])
   7.147 +
   7.148 +lemma symD:
   7.149 +  assumes "sym r" and "(b, a) \<in> r"
   7.150 +  shows "(a, b) \<in> r"
   7.151 +  using assms by (rule symE)
   7.152  
   7.153 -lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
   7.154 -by (fast intro: symI dest: symD)
   7.155 +lemma sympD:
   7.156 +  assumes "symp r" and "r b a"
   7.157 +  shows "r a b"
   7.158 +  using assms by (rule symD [to_pred])
   7.159 +
   7.160 +lemma sym_Int:
   7.161 +  "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
   7.162 +  by (fast intro: symI elim: symE)
   7.163  
   7.164 -lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
   7.165 -by (fast intro: symI dest: symD)
   7.166 +lemma symp_inf:
   7.167 +  "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)"
   7.168 +  by (fact sym_Int [to_pred])
   7.169 +
   7.170 +lemma sym_Un:
   7.171 +  "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)"
   7.172 +  by (fast intro: symI elim: symE)
   7.173 +
   7.174 +lemma symp_sup:
   7.175 +  "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)"
   7.176 +  by (fact sym_Un [to_pred])
   7.177  
   7.178 -lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
   7.179 -by (fast intro: symI dest: symD)
   7.180 +lemma sym_INTER:
   7.181 +  "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
   7.182 +  by (fast intro: symI elim: symE)
   7.183 +
   7.184 +(* FIXME thm sym_INTER [to_pred] *)
   7.185  
   7.186 -lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
   7.187 -by (fast intro: symI dest: symD)
   7.188 +lemma sym_UNION:
   7.189 +  "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
   7.190 +  by (fast intro: symI elim: symE)
   7.191 +
   7.192 +(* FIXME thm sym_UNION [to_pred] *)
   7.193  
   7.194  
   7.195  subsubsection {* Antisymmetry *}
   7.196  
   7.197 -definition
   7.198 -  antisym :: "('a * 'a) set => bool" where
   7.199 -  "antisym r \<longleftrightarrow> (ALL x y. (x,y):r --> (y,x):r --> x=y)"
   7.200 +definition antisym :: "'a rel \<Rightarrow> bool"
   7.201 +where
   7.202 +  "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
   7.203 +
   7.204 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   7.205 +where
   7.206 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
   7.207  
   7.208  lemma antisymI:
   7.209    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   7.210 -by (unfold antisym_def) iprover
   7.211 +  by (unfold antisym_def) iprover
   7.212  
   7.213  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   7.214 -by (unfold antisym_def) iprover
   7.215 -
   7.216 -abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.217 -  "antisymP r \<equiv> antisym {(x, y). r x y}"
   7.218 +  by (unfold antisym_def) iprover
   7.219  
   7.220  lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
   7.221 -by (unfold antisym_def) blast
   7.222 +  by (unfold antisym_def) blast
   7.223  
   7.224  lemma antisym_empty [simp]: "antisym {}"
   7.225 -by (unfold antisym_def) blast
   7.226 +  by (unfold antisym_def) blast
   7.227  
   7.228  
   7.229  subsubsection {* Transitivity *}
   7.230  
   7.231 -definition
   7.232 -  trans :: "('a * 'a) set => bool" where
   7.233 -  "trans r \<longleftrightarrow> (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
   7.234 +definition trans :: "'a rel \<Rightarrow> bool"
   7.235 +where
   7.236 +  "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
   7.237 +
   7.238 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   7.239 +where
   7.240 +  "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)"
   7.241 +
   7.242 +lemma transp_trans_eq [pred_set_conv]:
   7.243 +  "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" 
   7.244 +  by (simp add: trans_def transp_def)
   7.245 +
   7.246 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   7.247 +where -- {* FIXME drop *}
   7.248 +  "transP r \<equiv> trans {(x, y). r x y}"
   7.249  
   7.250  lemma transI:
   7.251 -  "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   7.252 -by (unfold trans_def) iprover
   7.253 -
   7.254 -lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   7.255 -by (unfold trans_def) iprover
   7.256 -
   7.257 -abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.258 -  "transP r \<equiv> trans {(x, y). r x y}"
   7.259 -
   7.260 -definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.261 -  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   7.262 +  "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
   7.263 +  by (unfold trans_def) iprover
   7.264  
   7.265  lemma transpI:
   7.266    "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   7.267 -  by (auto intro: transI simp add: transp_def)
   7.268 -  
   7.269 +  by (fact transI [to_pred])
   7.270 +
   7.271 +lemma transE:
   7.272 +  assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
   7.273 +  obtains "(x, z) \<in> r"
   7.274 +  using assms by (unfold trans_def) iprover
   7.275 +
   7.276  lemma transpE:
   7.277    assumes "transp r" and "r x y" and "r y z"
   7.278    obtains "r x z"
   7.279 -  using assms by (auto dest: transD simp add: transp_def)
   7.280 +  using assms by (rule transE [to_pred])
   7.281 +
   7.282 +lemma transD:
   7.283 +  assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
   7.284 +  shows "(x, z) \<in> r"
   7.285 +  using assms by (rule transE)
   7.286 +
   7.287 +lemma transpD:
   7.288 +  assumes "transp r" and "r x y" and "r y z"
   7.289 +  shows "r x z"
   7.290 +  using assms by (rule transD [to_pred])
   7.291  
   7.292 -lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
   7.293 -by (fast intro: transI elim: transD)
   7.294 +lemma trans_Int:
   7.295 +  "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
   7.296 +  by (fast intro: transI elim: transE)
   7.297  
   7.298 -lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
   7.299 -by (fast intro: transI elim: transD)
   7.300 +lemma transp_inf:
   7.301 +  "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)"
   7.302 +  by (fact trans_Int [to_pred])
   7.303 +
   7.304 +lemma trans_INTER:
   7.305 +  "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)"
   7.306 +  by (fast intro: transI elim: transD)
   7.307 +
   7.308 +(* FIXME thm trans_INTER [to_pred] *)
   7.309  
   7.310  lemma trans_join [code]:
   7.311    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
   7.312    by (auto simp add: trans_def)
   7.313  
   7.314 +lemma transp_trans:
   7.315 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   7.316 +  by (simp add: trans_def transp_def)
   7.317 +
   7.318  
   7.319  subsubsection {* Totality *}
   7.320  
   7.321 -definition
   7.322 -  total_on :: "'a set => ('a * 'a) set => bool" where
   7.323 -  "total_on A r \<longleftrightarrow> (\<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r)"
   7.324 +definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   7.325 +where
   7.326 +  "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)"
   7.327  
   7.328  abbreviation "total \<equiv> total_on UNIV"
   7.329  
   7.330 -lemma total_on_empty[simp]: "total_on {} r"
   7.331 -by(simp add:total_on_def)
   7.332 +lemma total_on_empty [simp]: "total_on {} r"
   7.333 +  by (simp add: total_on_def)
   7.334  
   7.335  
   7.336  subsubsection {* Single valued relations *}
   7.337  
   7.338 -definition
   7.339 -  single_valued :: "('a * 'b) set => bool" where
   7.340 -  "single_valued r \<longleftrightarrow> (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))"
   7.341 -
   7.342 -lemma single_valuedI:
   7.343 -  "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   7.344 -by (unfold single_valued_def)
   7.345 -
   7.346 -lemma single_valuedD:
   7.347 -  "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   7.348 -by (simp add: single_valued_def)
   7.349 +definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
   7.350 +where
   7.351 +  "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
   7.352  
   7.353  abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   7.354    "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   7.355  
   7.356 +lemma single_valuedI:
   7.357 +  "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   7.358 +  by (unfold single_valued_def)
   7.359 +
   7.360 +lemma single_valuedD:
   7.361 +  "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   7.362 +  by (simp add: single_valued_def)
   7.363 +
   7.364  lemma single_valued_subset:
   7.365    "r \<subseteq> s ==> single_valued s ==> single_valued r"
   7.366 -by (unfold single_valued_def) blast
   7.367 +  by (unfold single_valued_def) blast
   7.368  
   7.369  
   7.370  subsection {* Relation operations *}
   7.371  
   7.372  subsubsection {* The identity relation *}
   7.373  
   7.374 -definition
   7.375 -  Id :: "('a * 'a) set" where
   7.376 -  "Id = {p. EX x. p = (x,x)}"
   7.377 +definition Id :: "'a rel"
   7.378 +where
   7.379 +  "Id = {p. \<exists>x. p = (x, x)}"
   7.380  
   7.381  lemma IdI [intro]: "(a, a) : Id"
   7.382 -by (simp add: Id_def)
   7.383 +  by (simp add: Id_def)
   7.384  
   7.385  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
   7.386 -by (unfold Id_def) (iprover elim: CollectE)
   7.387 +  by (unfold Id_def) (iprover elim: CollectE)
   7.388  
   7.389  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
   7.390 -by (unfold Id_def) blast
   7.391 +  by (unfold Id_def) blast
   7.392  
   7.393  lemma refl_Id: "refl Id"
   7.394 -by (simp add: refl_on_def)
   7.395 +  by (simp add: refl_on_def)
   7.396  
   7.397  lemma antisym_Id: "antisym Id"
   7.398    -- {* A strange result, since @{text Id} is also symmetric. *}
   7.399 -by (simp add: antisym_def)
   7.400 +  by (simp add: antisym_def)
   7.401  
   7.402  lemma sym_Id: "sym Id"
   7.403 -by (simp add: sym_def)
   7.404 +  by (simp add: sym_def)
   7.405  
   7.406  lemma trans_Id: "trans Id"
   7.407 -by (simp add: trans_def)
   7.408 +  by (simp add: trans_def)
   7.409  
   7.410  lemma single_valued_Id [simp]: "single_valued Id"
   7.411    by (unfold single_valued_def) blast
   7.412 @@ -356,45 +434,45 @@
   7.413  
   7.414  subsubsection {* Diagonal: identity over a set *}
   7.415  
   7.416 -definition
   7.417 -  Id_on  :: "'a set => ('a * 'a) set" where
   7.418 -  "Id_on A = (\<Union>x\<in>A. {(x,x)})"
   7.419 +definition Id_on  :: "'a set \<Rightarrow> 'a rel"
   7.420 +where
   7.421 +  "Id_on A = (\<Union>x\<in>A. {(x, x)})"
   7.422  
   7.423  lemma Id_on_empty [simp]: "Id_on {} = {}"
   7.424 -by (simp add: Id_on_def) 
   7.425 +  by (simp add: Id_on_def) 
   7.426  
   7.427  lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
   7.428 -by (simp add: Id_on_def)
   7.429 +  by (simp add: Id_on_def)
   7.430  
   7.431  lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
   7.432 -by (rule Id_on_eqI) (rule refl)
   7.433 +  by (rule Id_on_eqI) (rule refl)
   7.434  
   7.435  lemma Id_onE [elim!]:
   7.436    "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   7.437    -- {* The general elimination rule. *}
   7.438 -by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
   7.439 +  by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
   7.440  
   7.441  lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
   7.442 -by blast
   7.443 +  by blast
   7.444  
   7.445  lemma Id_on_def' [nitpick_unfold]:
   7.446    "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)"
   7.447 -by auto
   7.448 +  by auto
   7.449  
   7.450  lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
   7.451 -by blast
   7.452 +  by blast
   7.453  
   7.454  lemma refl_on_Id_on: "refl_on A (Id_on A)"
   7.455 -by (rule refl_onI [OF Id_on_subset_Times Id_onI])
   7.456 +  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
   7.457  
   7.458  lemma antisym_Id_on [simp]: "antisym (Id_on A)"
   7.459 -by (unfold antisym_def) blast
   7.460 +  by (unfold antisym_def) blast
   7.461  
   7.462  lemma sym_Id_on [simp]: "sym (Id_on A)"
   7.463 -by (rule symI) clarify
   7.464 +  by (rule symI) clarify
   7.465  
   7.466  lemma trans_Id_on [simp]: "trans (Id_on A)"
   7.467 -by (fast intro: transI elim: transD)
   7.468 +  by (fast intro: transI elim: transD)
   7.469  
   7.470  lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
   7.471    by (unfold single_valued_def) blast
   7.472 @@ -402,184 +480,228 @@
   7.473  
   7.474  subsubsection {* Composition *}
   7.475  
   7.476 -definition rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a * 'c) set" (infixr "O" 75)
   7.477 +inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
   7.478 +  for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
   7.479  where
   7.480 -  "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   7.481 +  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
   7.482  
   7.483 -lemma rel_compI [intro]:
   7.484 -  "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
   7.485 -by (unfold rel_comp_def) blast
   7.486 +abbreviation pred_comp (infixr "OO" 75) where
   7.487 +  "pred_comp \<equiv> rel_compp"
   7.488  
   7.489 -lemma rel_compE [elim!]: "xz : r O s ==>
   7.490 -  (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s  ==> P) ==> P"
   7.491 -by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
   7.492 +lemmas pred_compI = rel_compp.intros
   7.493  
   7.494 -inductive pred_comp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   7.495 -for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
   7.496 -where
   7.497 -  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   7.498 +text {*
   7.499 +  For historic reasons, the elimination rules are not wholly corresponding.
   7.500 +  Feel free to consolidate this.
   7.501 +*}
   7.502  
   7.503 +inductive_cases rel_compEpair: "(a, c) \<in> r O s"
   7.504  inductive_cases pred_compE [elim!]: "(r OO s) a c"
   7.505  
   7.506 -lemma pred_comp_rel_comp_eq [pred_set_conv]:
   7.507 -  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   7.508 -  by (auto simp add: fun_eq_iff)
   7.509 +lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
   7.510 +  (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
   7.511 +  by (cases xz) (simp, erule rel_compEpair, iprover)
   7.512 +
   7.513 +lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
   7.514 +
   7.515 +lemma R_O_Id [simp]:
   7.516 +  "R O Id = R"
   7.517 +  by fast
   7.518  
   7.519 -lemma rel_compEpair:
   7.520 -  "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
   7.521 -by (iprover elim: rel_compE Pair_inject ssubst)
   7.522 +lemma Id_O_R [simp]:
   7.523 +  "Id O R = R"
   7.524 +  by fast
   7.525 +
   7.526 +lemma rel_comp_empty1 [simp]:
   7.527 +  "{} O R = {}"
   7.528 +  by blast
   7.529  
   7.530 -lemma R_O_Id [simp]: "R O Id = R"
   7.531 -by fast
   7.532 +(* CANDIDATE lemma pred_comp_bot1 [simp]:
   7.533 +  ""
   7.534 +  by (fact rel_comp_empty1 [to_pred]) *)
   7.535  
   7.536 -lemma Id_O_R [simp]: "Id O R = R"
   7.537 -by fast
   7.538 +lemma rel_comp_empty2 [simp]:
   7.539 +  "R O {} = {}"
   7.540 +  by blast
   7.541  
   7.542 -lemma rel_comp_empty1[simp]: "{} O R = {}"
   7.543 -by blast
   7.544 +(* CANDIDATE lemma pred_comp_bot2 [simp]:
   7.545 +  ""
   7.546 +  by (fact rel_comp_empty2 [to_pred]) *)
   7.547  
   7.548 -lemma rel_comp_empty2[simp]: "R O {} = {}"
   7.549 -by blast
   7.550 +lemma O_assoc:
   7.551 +  "(R O S) O T = R O (S O T)"
   7.552 +  by blast
   7.553 +
   7.554 +lemma pred_comp_assoc:
   7.555 +  "(r OO s) OO t = r OO (s OO t)"
   7.556 +  by (fact O_assoc [to_pred])
   7.557  
   7.558 -lemma O_assoc: "(R O S) O T = R O (S O T)"
   7.559 -by blast
   7.560 +lemma trans_O_subset:
   7.561 +  "trans r \<Longrightarrow> r O r \<subseteq> r"
   7.562 +  by (unfold trans_def) blast
   7.563 +
   7.564 +lemma transp_pred_comp_less_eq:
   7.565 +  "transp r \<Longrightarrow> r OO r \<le> r "
   7.566 +  by (fact trans_O_subset [to_pred])
   7.567  
   7.568 -lemma trans_O_subset: "trans r ==> r O r \<subseteq> r"
   7.569 -by (unfold trans_def) blast
   7.570 +lemma rel_comp_mono:
   7.571 +  "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
   7.572 +  by blast
   7.573  
   7.574 -lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)"
   7.575 -by blast
   7.576 +lemma pred_comp_mono:
   7.577 +  "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
   7.578 +  by (fact rel_comp_mono [to_pred])
   7.579  
   7.580  lemma rel_comp_subset_Sigma:
   7.581 -    "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
   7.582 -by blast
   7.583 +  "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
   7.584 +  by blast
   7.585 +
   7.586 +lemma rel_comp_distrib [simp]:
   7.587 +  "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   7.588 +  by auto
   7.589  
   7.590 -lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   7.591 -by auto
   7.592 +lemma pred_comp_distrib (* CANDIDATE [simp] *):
   7.593 +  "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   7.594 +  by (fact rel_comp_distrib [to_pred])
   7.595 +
   7.596 +lemma rel_comp_distrib2 [simp]:
   7.597 +  "(S \<union> T) O R = (S O R) \<union> (T O R)"
   7.598 +  by auto
   7.599  
   7.600 -lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
   7.601 -by auto
   7.602 +lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
   7.603 +  "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   7.604 +  by (fact rel_comp_distrib2 [to_pred])
   7.605 +
   7.606 +lemma rel_comp_UNION_distrib:
   7.607 +  "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   7.608 +  by auto
   7.609  
   7.610 -lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
   7.611 -by auto
   7.612 +(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   7.613  
   7.614 -lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
   7.615 -by auto
   7.616 +lemma rel_comp_UNION_distrib2:
   7.617 +  "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   7.618 +  by auto
   7.619 +
   7.620 +(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   7.621  
   7.622  lemma single_valued_rel_comp:
   7.623 -  "single_valued r ==> single_valued s ==> single_valued (r O s)"
   7.624 -by (unfold single_valued_def) blast
   7.625 +  "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   7.626 +  by (unfold single_valued_def) blast
   7.627 +
   7.628 +lemma rel_comp_unfold:
   7.629 +  "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   7.630 +  by (auto simp add: set_eq_iff)
   7.631  
   7.632  
   7.633  subsubsection {* Converse *}
   7.634  
   7.635 -definition
   7.636 -  converse :: "('a * 'b) set => ('b * 'a) set"
   7.637 -    ("(_^-1)" [1000] 999) where
   7.638 -  "r^-1 = {(y, x). (x, y) : r}"
   7.639 +inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^-1)" [1000] 999)
   7.640 +  for r :: "('a \<times> 'b) set"
   7.641 +where
   7.642 +  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r^-1"
   7.643  
   7.644  notation (xsymbols)
   7.645    converse  ("(_\<inverse>)" [1000] 999)
   7.646  
   7.647 -lemma converseI [sym]: "(a, b) : r ==> (b, a) : r^-1"
   7.648 -  by (simp add: converse_def)
   7.649 -
   7.650 -lemma converseD [sym]: "(a,b) : r^-1 ==> (b, a) : r"
   7.651 -  by (simp add: converse_def)
   7.652 -
   7.653 -lemma converseE [elim!]:
   7.654 -  "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
   7.655 -    -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   7.656 -  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   7.657 -
   7.658 -lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   7.659 -  by (simp add: converse_def)
   7.660 -
   7.661 -inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   7.662 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.663 -  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   7.664 +notation
   7.665 +  conversep ("(_^--1)" [1000] 1000)
   7.666  
   7.667  notation (xsymbols)
   7.668    conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   7.669  
   7.670 -lemma conversepD:
   7.671 -  assumes ab: "r^--1 a b"
   7.672 -  shows "r b a" using ab
   7.673 -  by cases simp
   7.674 +lemma converseI [sym]:
   7.675 +  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
   7.676 +  by (fact converse.intros)
   7.677 +
   7.678 +lemma conversepI (* CANDIDATE [sym] *):
   7.679 +  "r a b \<Longrightarrow> r\<inverse>\<inverse> b a"
   7.680 +  by (fact conversep.intros)
   7.681 +
   7.682 +lemma converseD [sym]:
   7.683 +  "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r"
   7.684 +  by (erule converse.cases) iprover
   7.685 +
   7.686 +lemma conversepD (* CANDIDATE [sym] *):
   7.687 +  "r\<inverse>\<inverse> b a \<Longrightarrow> r a b"
   7.688 +  by (fact converseD [to_pred])
   7.689 +
   7.690 +lemma converseE [elim!]:
   7.691 +  -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   7.692 +  "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
   7.693 +  by (cases yx) (simp, erule converse.cases, iprover)
   7.694  
   7.695 -lemma conversep_iff [iff]: "r^--1 a b = r b a"
   7.696 -  by (iprover intro: conversepI dest: conversepD)
   7.697 +lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
   7.698 +
   7.699 +lemma converse_iff [iff]:
   7.700 +  "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
   7.701 +  by (auto intro: converseI)
   7.702 +
   7.703 +lemma conversep_iff [iff]:
   7.704 +  "r\<inverse>\<inverse> a b = r b a"
   7.705 +  by (fact converse_iff [to_pred])
   7.706  
   7.707 -lemma conversep_converse_eq [pred_set_conv]:
   7.708 -  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   7.709 -  by (auto simp add: fun_eq_iff)
   7.710 +lemma converse_converse [simp]:
   7.711 +  "(r\<inverse>)\<inverse> = r"
   7.712 +  by (simp add: set_eq_iff)
   7.713  
   7.714 -lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   7.715 -  by (iprover intro: order_antisym conversepI dest: conversepD)
   7.716 +lemma conversep_conversep [simp]:
   7.717 +  "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   7.718 +  by (fact converse_converse [to_pred])
   7.719 +
   7.720 +lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   7.721 +  by blast
   7.722  
   7.723  lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   7.724    by (iprover intro: order_antisym conversepI pred_compI
   7.725      elim: pred_compE dest: conversepD)
   7.726  
   7.727 +lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   7.728 +  by blast
   7.729 +
   7.730  lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   7.731    by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   7.732  
   7.733 +lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
   7.734 +  by blast
   7.735 +
   7.736  lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   7.737    by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   7.738  
   7.739 -lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   7.740 -  by (auto simp add: fun_eq_iff)
   7.741 -
   7.742 -lemma conversep_eq [simp]: "(op =)^--1 = op ="
   7.743 -  by (auto simp add: fun_eq_iff)
   7.744 -
   7.745 -lemma converse_converse [simp]: "(r^-1)^-1 = r"
   7.746 -by (unfold converse_def) blast
   7.747 -
   7.748 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   7.749 -by blast
   7.750 -
   7.751 -lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   7.752 -by blast
   7.753 -
   7.754 -lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
   7.755 -by blast
   7.756 -
   7.757  lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
   7.758 -by fast
   7.759 +  by fast
   7.760  
   7.761  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
   7.762 -by blast
   7.763 +  by blast
   7.764  
   7.765  lemma converse_Id [simp]: "Id^-1 = Id"
   7.766 -by blast
   7.767 +  by blast
   7.768  
   7.769  lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A"
   7.770 -by blast
   7.771 +  by blast
   7.772  
   7.773  lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
   7.774 -by (unfold refl_on_def) auto
   7.775 +  by (unfold refl_on_def) auto
   7.776  
   7.777  lemma sym_converse [simp]: "sym (converse r) = sym r"
   7.778 -by (unfold sym_def) blast
   7.779 +  by (unfold sym_def) blast
   7.780  
   7.781  lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   7.782 -by (unfold antisym_def) blast
   7.783 +  by (unfold antisym_def) blast
   7.784  
   7.785  lemma trans_converse [simp]: "trans (converse r) = trans r"
   7.786 -by (unfold trans_def) blast
   7.787 +  by (unfold trans_def) blast
   7.788  
   7.789  lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
   7.790 -by (unfold sym_def) fast
   7.791 +  by (unfold sym_def) fast
   7.792  
   7.793  lemma sym_Un_converse: "sym (r \<union> r^-1)"
   7.794 -by (unfold sym_def) blast
   7.795 +  by (unfold sym_def) blast
   7.796  
   7.797  lemma sym_Int_converse: "sym (r \<inter> r^-1)"
   7.798 -by (unfold sym_def) blast
   7.799 +  by (unfold sym_def) blast
   7.800  
   7.801 -lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
   7.802 -by (auto simp: total_on_def)
   7.803 +lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r"
   7.804 +  by (auto simp: total_on_def)
   7.805  
   7.806  lemma finite_converse [iff]: "finite (r^-1) = finite r"
   7.807    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   7.808 @@ -588,50 +710,61 @@
   7.809      apply (erule finite_imageD [unfolded inj_on_def])
   7.810      apply (simp split add: split_split)
   7.811     apply (erule finite_imageI)
   7.812 -  apply (simp add: converse_def image_def, auto)
   7.813 +  apply (simp add: set_eq_iff image_def, auto)
   7.814    apply (rule bexI)
   7.815     prefer 2 apply assumption
   7.816    apply simp
   7.817    done
   7.818  
   7.819 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   7.820 +  by (auto simp add: fun_eq_iff)
   7.821 +
   7.822 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
   7.823 +  by (auto simp add: fun_eq_iff)
   7.824 +
   7.825 +lemma converse_unfold:
   7.826 +  "r\<inverse> = {(y, x). (x, y) \<in> r}"
   7.827 +  by (simp add: set_eq_iff)
   7.828 +
   7.829  
   7.830  subsubsection {* Domain, range and field *}
   7.831  
   7.832 -definition
   7.833 -  Domain :: "('a * 'b) set => 'a set" where
   7.834 -  "Domain r = {x. EX y. (x,y):r}"
   7.835 +definition Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set"
   7.836 +where
   7.837 +  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
   7.838  
   7.839 -definition
   7.840 -  Range  :: "('a * 'b) set => 'b set" where
   7.841 -  "Range r = Domain(r^-1)"
   7.842 +definition Range  :: "('a \<times> 'b) set \<Rightarrow> 'b set"
   7.843 +where
   7.844 +  "Range r = Domain (r\<inverse>)"
   7.845  
   7.846 -definition
   7.847 -  Field :: "('a * 'a) set => 'a set" where
   7.848 +definition Field :: "'a rel \<Rightarrow> 'a set"
   7.849 +where
   7.850    "Field r = Domain r \<union> Range r"
   7.851  
   7.852  declare Domain_def [no_atp]
   7.853  
   7.854  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   7.855 -by (unfold Domain_def) blast
   7.856 +  by (unfold Domain_def) blast
   7.857  
   7.858  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
   7.859 -by (iprover intro!: iffD2 [OF Domain_iff])
   7.860 +  by (iprover intro!: iffD2 [OF Domain_iff])
   7.861  
   7.862  lemma DomainE [elim!]:
   7.863    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
   7.864 -by (iprover dest!: iffD1 [OF Domain_iff])
   7.865 +  by (iprover dest!: iffD1 [OF Domain_iff])
   7.866  
   7.867  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   7.868 -by (simp add: Domain_def Range_def)
   7.869 +  by (simp add: Domain_def Range_def)
   7.870  
   7.871  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
   7.872 -by (unfold Range_def) (iprover intro!: converseI DomainI)
   7.873 +  by (unfold Range_def) (iprover intro!: converseI DomainI)
   7.874  
   7.875  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
   7.876 -by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   7.877 +  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   7.878  
   7.879  inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   7.880 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.881 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   7.882 +where
   7.883    DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   7.884  
   7.885  inductive_cases DomainPE [elim!]: "DomainP r a"
   7.886 @@ -640,7 +773,8 @@
   7.887    by (blast intro!: Orderings.order_antisym predicate1I)
   7.888  
   7.889  inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   7.890 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.891 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   7.892 +where
   7.893    RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   7.894  
   7.895  inductive_cases RangePE [elim!]: "RangeP r b"
   7.896 @@ -679,8 +813,8 @@
   7.897  lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
   7.898    by blast
   7.899  
   7.900 -lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   7.901 -  by(auto simp: Range_def)
   7.902 +lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r"
   7.903 +  by auto
   7.904  
   7.905  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
   7.906    by blast
   7.907 @@ -731,7 +865,7 @@
   7.908  lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
   7.909    by blast
   7.910  
   7.911 -lemma Range_converse [simp]: "Range(r^-1) = Domain r"
   7.912 +lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r"
   7.913    by blast
   7.914  
   7.915  lemma snd_eq_Range: "snd ` R = Range R"
   7.916 @@ -767,73 +901,76 @@
   7.917     apply (auto simp add: Field_def Domain_insert Range_insert)
   7.918    done
   7.919  
   7.920 +lemma Domain_unfold:
   7.921 +  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
   7.922 +  by (fact Domain_def)
   7.923 +
   7.924  
   7.925  subsubsection {* Image of a set under a relation *}
   7.926  
   7.927 -definition
   7.928 -  Image :: "[('a * 'b) set, 'a set] => 'b set"
   7.929 -    (infixl "``" 90) where
   7.930 -  "r `` s = {y. EX x:s. (x,y):r}"
   7.931 +definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixl "``" 90)
   7.932 +where
   7.933 +  "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
   7.934  
   7.935  declare Image_def [no_atp]
   7.936  
   7.937  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   7.938 -by (simp add: Image_def)
   7.939 +  by (simp add: Image_def)
   7.940  
   7.941  lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   7.942 -by (simp add: Image_def)
   7.943 +  by (simp add: Image_def)
   7.944  
   7.945  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   7.946 -by (rule Image_iff [THEN trans]) simp
   7.947 +  by (rule Image_iff [THEN trans]) simp
   7.948  
   7.949  lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
   7.950 -by (unfold Image_def) blast
   7.951 +  by (unfold Image_def) blast
   7.952  
   7.953  lemma ImageE [elim!]:
   7.954 -    "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   7.955 -by (unfold Image_def) (iprover elim!: CollectE bexE)
   7.956 +  "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   7.957 +  by (unfold Image_def) (iprover elim!: CollectE bexE)
   7.958  
   7.959  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   7.960    -- {* This version's more effective when we already have the required @{text a} *}
   7.961 -by blast
   7.962 +  by blast
   7.963  
   7.964  lemma Image_empty [simp]: "R``{} = {}"
   7.965 -by blast
   7.966 +  by blast
   7.967  
   7.968  lemma Image_Id [simp]: "Id `` A = A"
   7.969 -by blast
   7.970 +  by blast
   7.971  
   7.972  lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B"
   7.973 -by blast
   7.974 +  by blast
   7.975  
   7.976  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
   7.977 -by blast
   7.978 +  by blast
   7.979  
   7.980  lemma Image_Int_eq:
   7.981       "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
   7.982 -by (simp add: single_valued_def, blast) 
   7.983 +     by (simp add: single_valued_def, blast) 
   7.984  
   7.985  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
   7.986 -by blast
   7.987 +  by blast
   7.988  
   7.989  lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
   7.990 -by blast
   7.991 +  by blast
   7.992  
   7.993  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
   7.994 -by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   7.995 +  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   7.996  
   7.997  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   7.998    -- {* NOT suitable for rewriting *}
   7.999 -by blast
  7.1000 +  by blast
  7.1001  
  7.1002  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
  7.1003 -by blast
  7.1004 +  by blast
  7.1005  
  7.1006  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
  7.1007 -by blast
  7.1008 +  by blast
  7.1009  
  7.1010  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
  7.1011 -by blast
  7.1012 +  by blast
  7.1013  
  7.1014  text{*Converse inclusion requires some assumptions*}
  7.1015  lemma Image_INT_eq:
  7.1016 @@ -844,26 +981,27 @@
  7.1017  done
  7.1018  
  7.1019  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
  7.1020 -by blast
  7.1021 +  by blast
  7.1022  
  7.1023  lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
  7.1024 -by auto
  7.1025 +  by auto
  7.1026  
  7.1027  
  7.1028  subsubsection {* Inverse image *}
  7.1029  
  7.1030 -definition
  7.1031 -  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
  7.1032 -  "inv_image r f = {(x, y). (f x, f y) : r}"
  7.1033 +definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel"
  7.1034 +where
  7.1035 +  "inv_image r f = {(x, y). (f x, f y) \<in> r}"
  7.1036  
  7.1037 -definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
  7.1038 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
  7.1039 +where
  7.1040    "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
  7.1041  
  7.1042  lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
  7.1043    by (simp add: inv_image_def inv_imagep_def)
  7.1044  
  7.1045  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
  7.1046 -by (unfold sym_def inv_image_def) blast
  7.1047 +  by (unfold sym_def inv_image_def) blast
  7.1048  
  7.1049  lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
  7.1050    apply (unfold trans_def inv_image_def)
  7.1051 @@ -875,7 +1013,7 @@
  7.1052    by (auto simp:inv_image_def)
  7.1053  
  7.1054  lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
  7.1055 -unfolding inv_image_def converse_def by auto
  7.1056 +  unfolding inv_image_def converse_unfold by auto
  7.1057  
  7.1058  lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
  7.1059    by (simp add: inv_imagep_def)
  7.1060 @@ -883,7 +1021,8 @@
  7.1061  
  7.1062  subsubsection {* Powerset *}
  7.1063  
  7.1064 -definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
  7.1065 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
  7.1066 +where
  7.1067    "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
  7.1068  
  7.1069  lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
     8.1 --- a/src/HOL/Transitive_Closure.thy	Thu Mar 01 17:13:54 2012 +0000
     8.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Mar 01 19:34:52 2012 +0100
     8.3 @@ -628,10 +628,10 @@
     8.4    by (blast intro: subsetD [OF rtrancl_Un_subset])
     8.5  
     8.6  lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
     8.7 -  by (unfold Domain_def) (blast dest: tranclD)
     8.8 +  by (unfold Domain_unfold) (blast dest: tranclD)
     8.9  
    8.10  lemma trancl_range [simp]: "Range (r^+) = Range r"
    8.11 -unfolding Range_def by(simp add: trancl_converse [symmetric])
    8.12 +  unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])
    8.13  
    8.14  lemma Not_Domain_rtrancl:
    8.15      "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
    8.16 @@ -839,7 +839,7 @@
    8.17     apply (drule tranclD2)
    8.18     apply (clarsimp simp: rtrancl_is_UN_relpow)
    8.19     apply (rule_tac x="Suc n" in exI)
    8.20 -   apply (clarsimp simp: rel_comp_def)
    8.21 +   apply (clarsimp simp: rel_comp_unfold)
    8.22     apply fastforce
    8.23    apply clarsimp
    8.24    apply (case_tac n, simp)
    8.25 @@ -860,7 +860,7 @@
    8.26  next
    8.27    case (Suc n)
    8.28    show ?case
    8.29 -  proof (simp add: rel_comp_def Suc)
    8.30 +  proof (simp add: rel_comp_unfold Suc)
    8.31      show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R)
    8.32       = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
    8.33      (is "?l = ?r")
    8.34 @@ -1175,3 +1175,4 @@
    8.35    {* simple transitivity reasoner (predicate version) *}
    8.36  
    8.37  end
    8.38 +
     9.1 --- a/src/HOL/UNITY/Comp/Client.thy	Thu Mar 01 17:13:54 2012 +0000
     9.2 +++ b/src/HOL/UNITY/Comp/Client.thy	Thu Mar 01 19:34:52 2012 +0100
     9.3 @@ -138,7 +138,7 @@
     9.4       "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
     9.5  apply (simp add: Client_def mk_total_program_def)
     9.6  apply (rule_tac act = rel_act in totalize_transientI)
     9.7 -  apply (auto simp add: Domain_def Client_def)
     9.8 +  apply (auto simp add: Domain_unfold Client_def)
     9.9   apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
    9.10  apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
    9.11  apply (blast intro: strict_prefix_length_less)
    10.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Mar 01 17:13:54 2012 +0000
    10.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Mar 01 19:34:52 2012 +0100
    10.3 @@ -46,7 +46,7 @@
    10.4        ORELSE res_inst_tac ctxt
    10.5          [(("act", 0), sact)] @{thm transientI} 2,
    10.6           (*simplify the command's domain*)
    10.7 -      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
    10.8 +      simp_tac (simpset_of ctxt addsimps @{thms Domain_unfold}) 3,
    10.9        constrains_tac ctxt 1,
   10.10        ALLGOALS (clarify_tac ctxt),
   10.11        ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
    11.1 --- a/src/HOL/ZF/Games.thy	Thu Mar 01 17:13:54 2012 +0000
    11.2 +++ b/src/HOL/ZF/Games.thy	Thu Mar 01 19:34:52 2012 +0100
    11.3 @@ -330,7 +330,7 @@
    11.4      by (simp add: option_to_is_option_of) 
    11.5    show ?thesis
    11.6      apply (simp add: option_of)
    11.7 -    apply (auto intro: wf_inv_image wf_is_option_of)
    11.8 +    apply (auto intro: wf_is_option_of)
    11.9      done
   11.10  qed
   11.11    
   11.12 @@ -359,7 +359,7 @@
   11.13  lemma "neg_game (neg_game g) = g"
   11.14    apply (induct g rule: neg_game.induct)
   11.15    apply (subst neg_game.simps)+
   11.16 -  apply (simp add: right_options left_options comp_zimage_eq)
   11.17 +  apply (simp add: comp_zimage_eq)
   11.18    apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g")
   11.19    apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g")
   11.20    apply (auto simp add: game_split[symmetric])
   11.21 @@ -552,7 +552,7 @@
   11.22          apply (simp only: plus_game.simps[where G=G and H=H])
   11.23          apply (simp add: game_ext_eq goal1)
   11.24          apply (auto simp add: 
   11.25 -          zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
   11.26 +          zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
   11.27            induct_hyp)
   11.28          done
   11.29      qed
   11.30 @@ -974,3 +974,4 @@
   11.31  qed
   11.32  
   11.33  end
   11.34 +
    12.1 --- a/src/HOL/ZF/HOLZF.thy	Thu Mar 01 17:13:54 2012 +0000
    12.2 +++ b/src/HOL/ZF/HOLZF.thy	Thu Mar 01 19:34:52 2012 +0100
    12.3 @@ -660,7 +660,7 @@
    12.4    "Ext R y \<equiv> { x . (x, y) \<in> R }" 
    12.5  
    12.6  lemma Ext_Elem: "Ext is_Elem_of = explode"
    12.7 -  by (auto intro: ext simp add: Ext_def is_Elem_of_def explode_def)
    12.8 +  by (auto simp add: Ext_def is_Elem_of_def explode_def)
    12.9  
   12.10  lemma "Ext SpecialR Empty \<noteq> explode z"
   12.11  proof 
   12.12 @@ -892,3 +892,4 @@
   12.13    by (auto intro: set_like_subset wf_subset simp add: wf_eq_wfzf[symmetric])  
   12.14  
   12.15  end
   12.16 +
    13.1 --- a/src/HOL/ex/Set_Theory.thy	Thu Mar 01 17:13:54 2012 +0000
    13.2 +++ b/src/HOL/ex/Set_Theory.thy	Thu Mar 01 19:34:52 2012 +0100
    13.3 @@ -128,7 +128,7 @@
    13.4    let ?n = "card A"
    13.5    have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
    13.6    have 0: "R `` A <= A" using `sym R` `Domain R <= A`
    13.7 -    unfolding Domain_def sym_def by blast
    13.8 +    unfolding Domain_unfold sym_def by blast
    13.9    have h: "ALL a:A. R `` {a} <= A" using 0 by blast
   13.10    hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
   13.11      by(blast intro: finite_subset)
    14.1 --- a/src/HOL/ex/Tarski.thy	Thu Mar 01 17:13:54 2012 +0000
    14.2 +++ b/src/HOL/ex/Tarski.thy	Thu Mar 01 19:34:52 2012 +0100
    14.3 @@ -227,10 +227,10 @@
    14.4  by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
    14.5  
    14.6  lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
    14.7 -by (simp add: isLub_def isGlb_def dual_def converse_def)
    14.8 +by (simp add: isLub_def isGlb_def dual_def converse_unfold)
    14.9  
   14.10  lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
   14.11 -by (simp add: isLub_def isGlb_def dual_def converse_def)
   14.12 +by (simp add: isLub_def isGlb_def dual_def converse_unfold)
   14.13  
   14.14  lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
   14.15  apply (insert cl_po)
   14.16 @@ -251,10 +251,10 @@
   14.17  done
   14.18  
   14.19  lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
   14.20 -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
   14.21 +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
   14.22  
   14.23  lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
   14.24 -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
   14.25 +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
   14.26  
   14.27  lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder"
   14.28  by (simp add: PartialOrder_def CompleteLattice_def, fast)