1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Feb 23 21:16:54 2012 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Feb 23 21:25:59 2012 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Term evaluation using the generic code generator *}
     1.5  
     1.6  theory Code_Evaluation
     1.7 -imports Plain Typerep Code_Numeral
     1.8 +imports Plain Typerep Code_Numeral Predicate
     1.9  uses ("Tools/code_evaluation.ML")
    1.10  begin
    1.11  

     2.1 --- a/src/HOL/Code_Numeral.thy	Thu Feb 23 21:16:54 2012 +0100
     2.2 +++ b/src/HOL/Code_Numeral.thy	Thu Feb 23 21:25:59 2012 +0100
     2.3 @@ -281,18 +281,7 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -text {* Lazy Evaluation of an indexed function *}
     2.8 -
     2.9 -function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
    2.10 -where
    2.11 -  "iterate_upto f n m =
    2.12 -    Predicate.Seq (%u. if n > m then Predicate.Empty
    2.13 -     else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
    2.14 -by pat_completeness auto
    2.15 -
    2.16 -termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    2.17 -
    2.18 -hide_const (open) of_nat nat_of Suc  subtract int_of iterate_upto
    2.19 +hide_const (open) of_nat nat_of Suc subtract int_of
    2.20  
    2.21  
    2.22  subsection {* Code generator setup *}
    2.23 @@ -377,3 +366,4 @@
    2.24    Code_Numeral Arith
    2.25  
    2.26  end
    2.27 +

     3.1 --- a/src/HOL/IsaMakefile	Thu Feb 23 21:16:54 2012 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Thu Feb 23 21:25:59 2012 +0100
     3.3 @@ -197,7 +197,6 @@
     3.4    Partial_Function.thy \
     3.5    Plain.thy \
     3.6    Power.thy \
     3.7 -  Predicate.thy \
     3.8    Product_Type.thy \
     3.9    Relation.thy \
    3.10    Rings.thy \
    3.11 @@ -294,6 +293,7 @@
    3.12    Nitpick.thy \
    3.13    Numeral_Simprocs.thy \
    3.14    Presburger.thy \
    3.15 +  Predicate.thy \
    3.16    Predicate_Compile.thy \
    3.17    Quickcheck.thy \
    3.18    Quickcheck_Exhaustive.thy \

     4.1 --- a/src/HOL/List.thy	Thu Feb 23 21:16:54 2012 +0100
     4.2 +++ b/src/HOL/List.thy	Thu Feb 23 21:25:59 2012 +0100
     4.3 @@ -2662,7 +2662,6 @@
     4.4    by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
     4.5  
     4.6  declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
     4.7 -declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
     4.8  
     4.9  lemma (in complete_lattice) INF_set_foldr [code]:
    4.10    "INFI (set xs) f = foldr (inf \<circ> f) xs top"
    4.11 @@ -2672,29 +2671,6 @@
    4.12    "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
    4.13    by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
    4.14  
    4.15 -(* FIXME: better implement conversion by bisection *)
    4.16 -
    4.17 -lemma pred_of_set_fold_sup:
    4.18 -  assumes "finite A"
    4.19 -  shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
    4.20 -proof (rule sym)
    4.21 -  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    4.22 -    by (fact comp_fun_idem_sup)
    4.23 -  from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
    4.24 -qed
    4.25 -
    4.26 -lemma pred_of_set_set_fold_sup:
    4.27 -  "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
    4.28 -proof -
    4.29 -  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
    4.30 -    by (fact comp_fun_idem_sup)
    4.31 -  show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
    4.32 -qed
    4.33 -
    4.34 -lemma pred_of_set_set_foldr_sup [code]:
    4.35 -  "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
    4.36 -  by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
    4.37 -
    4.38  
    4.39  subsubsection {* @{text upt} *}
    4.40  

     5.1 --- a/src/HOL/Predicate_Compile.thy	Thu Feb 23 21:16:54 2012 +0100
     5.2 +++ b/src/HOL/Predicate_Compile.thy	Thu Feb 23 21:25:59 2012 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* A compiler for predicates defined by introduction rules *}
     5.5  
     5.6  theory Predicate_Compile
     5.7 -imports New_Random_Sequence Quickcheck_Exhaustive
     5.8 +imports Predicate New_Random_Sequence Quickcheck_Exhaustive
     5.9  uses
    5.10    "Tools/Predicate_Compile/predicate_compile_aux.ML"
    5.11    "Tools/Predicate_Compile/predicate_compile_compilations.ML"

     6.1 --- a/src/HOL/Quickcheck.thy	Thu Feb 23 21:16:54 2012 +0100
     6.2 +++ b/src/HOL/Quickcheck.thy	Thu Feb 23 21:25:59 2012 +0100
     6.3 @@ -233,7 +233,7 @@
     6.4  
     6.5  definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
     6.6  where
     6.7 -  "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
     6.8 +  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
     6.9  
    6.10  definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    6.11  where

     7.1 --- a/src/HOL/Relation.thy	Thu Feb 23 21:16:54 2012 +0100
     7.2 +++ b/src/HOL/Relation.thy	Thu Feb 23 21:25:59 2012 +0100
     7.3 @@ -1,15 +1,107 @@
     7.4  (*  Title:      HOL/Relation.thy
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 -    Copyright   1996  University of Cambridge
     7.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     7.8  *)
     7.9  
    7.10 -header {* Relations *}
    7.11 +header {* Relations – as sets of pairs, and binary predicates *}
    7.12  
    7.13  theory Relation
    7.14  imports Datatype Finite_Set
    7.15  begin
    7.16  
    7.17 -subsection {* Definitions *}
    7.18 +notation
    7.19 +  bot ("\<bottom>") and
    7.20 +  top ("\<top>") and
    7.21 +  inf (infixl "\<sqinter>" 70) and
    7.22 +  sup (infixl "\<squnion>" 65) and
    7.23 +  Inf ("\<Sqinter>_" [900] 900) and
    7.24 +  Sup ("\<Squnion>_" [900] 900)
    7.25 +
    7.26 +syntax (xsymbols)
    7.27 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    7.28 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    7.29 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    7.30 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    7.31 +
    7.32 +
    7.33 +subsection {* Classical rules for reasoning on predicates *}
    7.34 +
    7.35 +declare predicate1D [Pure.dest?, dest?]
    7.36 +declare predicate2I [Pure.intro!, intro!]
    7.37 +declare predicate2D [Pure.dest, dest]
    7.38 +declare bot1E [elim!]
    7.39 +declare bot2E [elim!]
    7.40 +declare top1I [intro!]
    7.41 +declare top2I [intro!]
    7.42 +declare inf1I [intro!]
    7.43 +declare inf2I [intro!]
    7.44 +declare inf1E [elim!]
    7.45 +declare inf2E [elim!]
    7.46 +declare sup1I1 [intro?]
    7.47 +declare sup2I1 [intro?]
    7.48 +declare sup1I2 [intro?]
    7.49 +declare sup2I2 [intro?]
    7.50 +declare sup1E [elim!]
    7.51 +declare sup2E [elim!]
    7.52 +declare sup1CI [intro!]
    7.53 +declare sup2CI [intro!]
    7.54 +declare INF1_I [intro!]
    7.55 +declare INF2_I [intro!]
    7.56 +declare INF1_D [elim]
    7.57 +declare INF2_D [elim]
    7.58 +declare INF1_E [elim]
    7.59 +declare INF2_E [elim]
    7.60 +declare SUP1_I [intro]
    7.61 +declare SUP2_I [intro]
    7.62 +declare SUP1_E [elim!]
    7.63 +declare SUP2_E [elim!]
    7.64 +
    7.65 +
    7.66 +subsection {* Conversions between set and predicate relations *}
    7.67 +
    7.68 +lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    7.69 +  by (simp add: set_eq_iff fun_eq_iff)
    7.70 +
    7.71 +lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
    7.72 +  by (simp add: set_eq_iff fun_eq_iff)
    7.73 +
    7.74 +lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    7.75 +  by (simp add: subset_iff le_fun_def)
    7.76 +
    7.77 +lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    7.78 +  by (simp add: subset_iff le_fun_def)
    7.79 +
    7.80 +lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    7.81 +  by (auto simp add: fun_eq_iff)
    7.82 +
    7.83 +lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    7.84 +  by (auto simp add: fun_eq_iff)
    7.85 +
    7.86 +lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    7.87 +  by (simp add: inf_fun_def)
    7.88 +
    7.89 +lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
    7.90 +  by (simp add: inf_fun_def)
    7.91 +
    7.92 +lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    7.93 +  by (simp add: sup_fun_def)
    7.94 +
    7.95 +lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
    7.96 +  by (simp add: sup_fun_def)
    7.97 +
    7.98 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    7.99 +  by (simp add: INF_apply fun_eq_iff)
   7.100 +
   7.101 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   7.102 +  by (simp add: INF_apply fun_eq_iff)
   7.103 +
   7.104 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   7.105 +  by (simp add: SUP_apply fun_eq_iff)
   7.106 +
   7.107 +lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
   7.108 +  by (simp add: SUP_apply fun_eq_iff)
   7.109 +
   7.110 +
   7.111 +subsection {* Relations as sets of pairs *}
   7.112  
   7.113  type_synonym 'a rel = "('a * 'a) set"
   7.114  
   7.115 @@ -90,7 +182,7 @@
   7.116    "inv_image r f = {(x, y). (f x, f y) : r}"
   7.117  
   7.118  
   7.119 -subsection {* The identity relation *}
   7.120 +subsubsection {* The identity relation *}
   7.121  
   7.122  lemma IdI [intro]: "(a, a) : Id"
   7.123  by (simp add: Id_def)
   7.124 @@ -115,7 +207,7 @@
   7.125  by (simp add: trans_def)
   7.126  
   7.127  
   7.128 -subsection {* Diagonal: identity over a set *}
   7.129 +subsubsection {* Diagonal: identity over a set *}
   7.130  
   7.131  lemma Id_on_empty [simp]: "Id_on {} = {}"
   7.132  by (simp add: Id_on_def) 
   7.133 @@ -142,7 +234,7 @@
   7.134  by blast
   7.135  
   7.136  
   7.137 -subsection {* Composition of two relations *}
   7.138 +subsubsection {* Composition of two relations *}
   7.139  
   7.140  lemma rel_compI [intro]:
   7.141    "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
   7.142 @@ -194,7 +286,7 @@
   7.143  by auto
   7.144  
   7.145  
   7.146 -subsection {* Reflexivity *}
   7.147 +subsubsection {* Reflexivity *}
   7.148  
   7.149  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
   7.150  by (unfold refl_on_def) (iprover intro!: ballI)
   7.151 @@ -232,7 +324,8 @@
   7.152    "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
   7.153  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
   7.154  
   7.155 -subsection {* Antisymmetry *}
   7.156 +
   7.157 +subsubsection {* Antisymmetry *}
   7.158  
   7.159  lemma antisymI:
   7.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   7.161 @@ -251,7 +344,7 @@
   7.162  by (unfold antisym_def) blast
   7.163  
   7.164  
   7.165 -subsection {* Symmetry *}
   7.166 +subsubsection {* Symmetry *}
   7.167  
   7.168  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   7.169  by (unfold sym_def) iprover
   7.170 @@ -275,7 +368,7 @@
   7.171  by (rule symI) clarify
   7.172  
   7.173  
   7.174 -subsection {* Transitivity *}
   7.175 +subsubsection {* Transitivity *}
   7.176  
   7.177  lemma trans_join [code]:
   7.178    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
   7.179 @@ -300,7 +393,8 @@
   7.180  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
   7.181  unfolding antisym_def trans_def by blast
   7.182  
   7.183 -subsection {* Irreflexivity *}
   7.184 +
   7.185 +subsubsection {* Irreflexivity *}
   7.186  
   7.187  lemma irrefl_distinct [code]:
   7.188    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
   7.189 @@ -310,7 +404,7 @@
   7.190  by(simp add:irrefl_def)
   7.191  
   7.192  
   7.193 -subsection {* Totality *}
   7.194 +subsubsection {* Totality *}
   7.195  
   7.196  lemma total_on_empty[simp]: "total_on {} r"
   7.197  by(simp add:total_on_def)
   7.198 @@ -318,7 +412,8 @@
   7.199  lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
   7.200  by(simp add: total_on_def)
   7.201  
   7.202 -subsection {* Converse *}
   7.203 +
   7.204 +subsubsection {* Converse *}
   7.205  
   7.206  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   7.207  by (simp add: converse_def)
   7.208 @@ -383,7 +478,7 @@
   7.209  by (auto simp: total_on_def)
   7.210  
   7.211  
   7.212 -subsection {* Domain *}
   7.213 +subsubsection {* Domain *}
   7.214  
   7.215  declare Domain_def [no_atp]
   7.216  
   7.217 @@ -444,7 +539,7 @@
   7.218  by auto
   7.219  
   7.220  
   7.221 -subsection {* Range *}
   7.222 +subsubsection {* Range *}
   7.223  
   7.224  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   7.225  by (simp add: Domain_def Range_def)
   7.226 @@ -493,7 +588,7 @@
   7.227    by force
   7.228  
   7.229  
   7.230 -subsection {* Field *}
   7.231 +subsubsection {* Field *}
   7.232  
   7.233  lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   7.234  by(auto simp:Field_def Domain_def Range_def)
   7.235 @@ -514,7 +609,7 @@
   7.236  by(auto simp:Field_def)
   7.237  
   7.238  
   7.239 -subsection {* Image of a set under a relation *}
   7.240 +subsubsection {* Image of a set under a relation *}
   7.241  
   7.242  declare Image_def [no_atp]
   7.243  
   7.244 @@ -588,7 +683,7 @@
   7.245  by blast
   7.246  
   7.247  
   7.248 -subsection {* Single valued relations *}
   7.249 +subsubsection {* Single valued relations *}
   7.250  
   7.251  lemma single_valuedI:
   7.252    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   7.253 @@ -613,7 +708,7 @@
   7.254  by (unfold single_valued_def) blast
   7.255  
   7.256  
   7.257 -subsection {* Graphs given by @{text Collect} *}
   7.258 +subsubsection {* Graphs given by @{text Collect} *}
   7.259  
   7.260  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
   7.261  by auto
   7.262 @@ -625,7 +720,7 @@
   7.263  by auto
   7.264  
   7.265  
   7.266 -subsection {* Inverse image *}
   7.267 +subsubsection {* Inverse image *}
   7.268  
   7.269  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   7.270  by (unfold sym_def inv_image_def) blast
   7.271 @@ -643,7 +738,7 @@
   7.272  unfolding inv_image_def converse_def by auto
   7.273  
   7.274  
   7.275 -subsection {* Finiteness *}
   7.276 +subsubsection {* Finiteness *}
   7.277  
   7.278  lemma finite_converse [iff]: "finite (r^-1) = finite r"
   7.279    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   7.280 @@ -671,7 +766,7 @@
   7.281    done
   7.282  
   7.283  
   7.284 -subsection {* Miscellaneous *}
   7.285 +subsubsection {* Miscellaneous *}
   7.286  
   7.287  text {* Version of @{thm[source] lfp_induct} for binary relations *}
   7.288  
   7.289 @@ -683,4 +778,157 @@
   7.290  lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
   7.291  by auto
   7.292  
   7.293 +
   7.294 +subsection {* Relations as binary predicates *}
   7.295 +
   7.296 +subsubsection {* Composition *}
   7.297 +
   7.298 +inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   7.299 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
   7.300 +  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   7.301 +
   7.302 +inductive_cases pred_compE [elim!]: "(r OO s) a c"
   7.303 +
   7.304 +lemma pred_comp_rel_comp_eq [pred_set_conv]:
   7.305 +  "((\<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.306 +  by (auto simp add: fun_eq_iff)
   7.307 +
   7.308 +
   7.309 +subsubsection {* Converse *}
   7.310 +
   7.311 +inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   7.312 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.313 +  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   7.314 +
   7.315 +notation (xsymbols)
   7.316 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   7.317 +
   7.318 +lemma conversepD:
   7.319 +  assumes ab: "r^--1 a b"
   7.320 +  shows "r b a" using ab
   7.321 +  by cases simp
   7.322 +
   7.323 +lemma conversep_iff [iff]: "r^--1 a b = r b a"
   7.324 +  by (iprover intro: conversepI dest: conversepD)
   7.325 +
   7.326 +lemma conversep_converse_eq [pred_set_conv]:
   7.327 +  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   7.328 +  by (auto simp add: fun_eq_iff)
   7.329 +
   7.330 +lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   7.331 +  by (iprover intro: order_antisym conversepI dest: conversepD)
   7.332 +
   7.333 +lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   7.334 +  by (iprover intro: order_antisym conversepI pred_compI
   7.335 +    elim: pred_compE dest: conversepD)
   7.336 +
   7.337 +lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   7.338 +  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   7.339 +
   7.340 +lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   7.341 +  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   7.342 +
   7.343 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   7.344 +  by (auto simp add: fun_eq_iff)
   7.345 +
   7.346 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
   7.347 +  by (auto simp add: fun_eq_iff)
   7.348 +
   7.349 +
   7.350 +subsubsection {* Domain *}
   7.351 +
   7.352 +inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   7.353 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.354 +  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   7.355 +
   7.356 +inductive_cases DomainPE [elim!]: "DomainP r a"
   7.357 +
   7.358 +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   7.359 +  by (blast intro!: Orderings.order_antisym predicate1I)
   7.360 +
   7.361 +
   7.362 +subsubsection {* Range *}
   7.363 +
   7.364 +inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   7.365 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   7.366 +  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   7.367 +
   7.368 +inductive_cases RangePE [elim!]: "RangeP r b"
   7.369 +
   7.370 +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   7.371 +  by (blast intro!: Orderings.order_antisym predicate1I)
   7.372 +
   7.373 +
   7.374 +subsubsection {* Inverse image *}
   7.375 +
   7.376 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   7.377 +  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
   7.378 +
   7.379 +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.380 +  by (simp add: inv_image_def inv_imagep_def)
   7.381 +
   7.382 +lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   7.383 +  by (simp add: inv_imagep_def)
   7.384 +
   7.385 +
   7.386 +subsubsection {* Powerset *}
   7.387 +
   7.388 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   7.389 +  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
   7.390 +
   7.391 +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   7.392 +  by (auto simp add: Powp_def fun_eq_iff)
   7.393 +
   7.394 +lemmas Powp_mono [mono] = Pow_mono [to_pred]
   7.395 +
   7.396 +
   7.397 +subsubsection {* Properties of predicate relations *}
   7.398 +
   7.399 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.400 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
   7.401 +
   7.402 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.403 +  "transP r \<equiv> trans {(x, y). r x y}"
   7.404 +
   7.405 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   7.406 +  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   7.407 +
   7.408 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   7.409 +
   7.410 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.411 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
   7.412 +
   7.413 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.414 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   7.415 +
   7.416 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   7.417 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   7.418 +
   7.419 +lemma reflpI:
   7.420 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
   7.421 +  by (auto intro: refl_onI simp add: reflp_def)
   7.422 +
   7.423 +lemma reflpE:
   7.424 +  assumes "reflp r"
   7.425 +  obtains "r x x"
   7.426 +  using assms by (auto dest: refl_onD simp add: reflp_def)
   7.427 +
   7.428 +lemma sympI:
   7.429 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   7.430 +  by (auto intro: symI simp add: symp_def)
   7.431 +
   7.432 +lemma sympE:
   7.433 +  assumes "symp r" and "r x y"
   7.434 +  obtains "r y x"
   7.435 +  using assms by (auto dest: symD simp add: symp_def)
   7.436 +
   7.437 +lemma transpI:
   7.438 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   7.439 +  by (auto intro: transI simp add: transp_def)
   7.440 +  
   7.441 +lemma transpE:
   7.442 +  assumes "transp r" and "r x y" and "r y z"
   7.443 +  obtains "r x z"
   7.444 +  using assms by (auto dest: transD simp add: transp_def)
   7.445 +
   7.446  end

     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 23 21:16:54 2012 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 23 21:25:59 2012 +0100
     8.3 @@ -30,7 +30,7 @@
     8.4    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
     8.5  
     8.6  fun mk_iterate_upto T (f, from, to) =
     8.7 -  list_comb (Const (@{const_name Code_Numeral.iterate_upto},
     8.8 +  list_comb (Const (@{const_name Predicate.iterate_upto},
     8.9        [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
    8.10      [f, from, to])
    8.11  

     9.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 23 21:16:54 2012 +0100
     9.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 23 21:25:59 2012 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Reflexive and Transitive closure of a relation *}
     9.5  
     9.6  theory Transitive_Closure
     9.7 -imports Predicate
     9.8 +imports Relation
     9.9  uses "~~/src/Provers/trancl.ML"
    9.10  begin
    9.11  

    10.1 --- a/src/HOL/Wellfounded.thy	Thu Feb 23 21:16:54 2012 +0100
    10.2 +++ b/src/HOL/Wellfounded.thy	Thu Feb 23 21:25:59 2012 +0100
    10.3 @@ -858,10 +858,4 @@
    10.4  
    10.5  declare "prod.size" [no_atp]
    10.6  
    10.7 -lemma [code]:
    10.8 -  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
    10.9 -
   10.10 -lemma [code]:
   10.11 -  "pred_size f P = 0" by (cases P) simp
   10.12 -
   10.13  end