moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
authorhaftmann
Fri Feb 24 22:46:44 2012 +0100 (2012-02-24)
changeset 466641f6c140f9c72
parent 46663 7fe029e818c2
child 46665 919dfcdf6d8a
child 46669 c1d2ab32174a
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
src/HOL/Code_Evaluation.thy
src/HOL/Code_Numeral.thy
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile.thy
src/HOL/Quickcheck.thy
src/HOL/Relation.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 24 22:46:16 2012 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 24 22:46:44 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	Fri Feb 24 22:46:16 2012 +0100
     2.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 24 22:46:44 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	Fri Feb 24 22:46:16 2012 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Fri Feb 24 22:46:44 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	Fri Feb 24 22:46:16 2012 +0100
     4.2 +++ b/src/HOL/List.thy	Fri Feb 24 22:46:44 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.thy	Fri Feb 24 22:46:16 2012 +0100
     5.2 +++ b/src/HOL/Predicate.thy	Fri Feb 24 22:46:44 2012 +0100
     5.3 @@ -1,11 +1,11 @@
     5.4  (*  Title:      HOL/Predicate.thy
     5.5 -    Author:     Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
     5.6 +    Author:     Lukas Bulwahn and Florian Haftmann, TU Muenchen
     5.7  *)
     5.8  
     5.9 -header {* Predicates as relations and enumerations *}
    5.10 +header {* Predicates as enumerations *}
    5.11  
    5.12  theory Predicate
    5.13 -imports Inductive Relation
    5.14 +imports List
    5.15  begin
    5.16  
    5.17  notation
    5.18 @@ -22,261 +22,7 @@
    5.19    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    5.20    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    5.21  
    5.22 -
    5.23 -subsection {* Classical rules for reasoning on predicates *}
    5.24 -
    5.25 -declare predicate1D [Pure.dest?, dest?]
    5.26 -declare predicate2I [Pure.intro!, intro!]
    5.27 -declare predicate2D [Pure.dest, dest]
    5.28 -declare bot1E [elim!]
    5.29 -declare bot2E [elim!]
    5.30 -declare top1I [intro!]
    5.31 -declare top2I [intro!]
    5.32 -declare inf1I [intro!]
    5.33 -declare inf2I [intro!]
    5.34 -declare inf1E [elim!]
    5.35 -declare inf2E [elim!]
    5.36 -declare sup1I1 [intro?]
    5.37 -declare sup2I1 [intro?]
    5.38 -declare sup1I2 [intro?]
    5.39 -declare sup2I2 [intro?]
    5.40 -declare sup1E [elim!]
    5.41 -declare sup2E [elim!]
    5.42 -declare sup1CI [intro!]
    5.43 -declare sup2CI [intro!]
    5.44 -declare INF1_I [intro!]
    5.45 -declare INF2_I [intro!]
    5.46 -declare INF1_D [elim]
    5.47 -declare INF2_D [elim]
    5.48 -declare INF1_E [elim]
    5.49 -declare INF2_E [elim]
    5.50 -declare SUP1_I [intro]
    5.51 -declare SUP2_I [intro]
    5.52 -declare SUP1_E [elim!]
    5.53 -declare SUP2_E [elim!]
    5.54 -
    5.55 -
    5.56 -subsection {* Conversion between set and predicate relations *}
    5.57 -
    5.58 -subsubsection {* Equality *}
    5.59 -
    5.60 -lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    5.61 -  by (simp add: set_eq_iff fun_eq_iff)
    5.62 -
    5.63 -lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
    5.64 -  by (simp add: set_eq_iff fun_eq_iff)
    5.65 -
    5.66 -
    5.67 -subsubsection {* Order relation *}
    5.68 -
    5.69 -lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    5.70 -  by (simp add: subset_iff le_fun_def)
    5.71 -
    5.72 -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)"
    5.73 -  by (simp add: subset_iff le_fun_def)
    5.74 -
    5.75 -
    5.76 -subsubsection {* Top and bottom elements *}
    5.77 -
    5.78 -lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    5.79 -  by (auto simp add: fun_eq_iff)
    5.80 -
    5.81 -lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    5.82 -  by (auto simp add: fun_eq_iff)
    5.83 -
    5.84 -
    5.85 -subsubsection {* Binary intersection *}
    5.86 -
    5.87 -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)"
    5.88 -  by (simp add: inf_fun_def)
    5.89 -
    5.90 -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)"
    5.91 -  by (simp add: inf_fun_def)
    5.92 -
    5.93 -
    5.94 -subsubsection {* Binary union *}
    5.95 -
    5.96 -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)"
    5.97 -  by (simp add: sup_fun_def)
    5.98 -
    5.99 -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)"
   5.100 -  by (simp add: sup_fun_def)
   5.101 -
   5.102 -
   5.103 -subsubsection {* Intersections of families *}
   5.104 -
   5.105 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   5.106 -  by (simp add: INF_apply fun_eq_iff)
   5.107 -
   5.108 -lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   5.109 -  by (simp add: INF_apply fun_eq_iff)
   5.110 -
   5.111 -
   5.112 -subsubsection {* Unions of families *}
   5.113 -
   5.114 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   5.115 -  by (simp add: SUP_apply fun_eq_iff)
   5.116 -
   5.117 -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))"
   5.118 -  by (simp add: SUP_apply fun_eq_iff)
   5.119 -
   5.120 -
   5.121 -subsection {* Predicates as relations *}
   5.122 -
   5.123 -subsubsection {* Composition  *}
   5.124 -
   5.125 -inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   5.126 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
   5.127 -  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   5.128 -
   5.129 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
   5.130 -
   5.131 -lemma pred_comp_rel_comp_eq [pred_set_conv]:
   5.132 -  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   5.133 -  by (auto simp add: fun_eq_iff)
   5.134 -
   5.135 -
   5.136 -subsubsection {* Converse *}
   5.137 -
   5.138 -inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   5.139 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   5.140 -  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   5.141 -
   5.142 -notation (xsymbols)
   5.143 -  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   5.144 -
   5.145 -lemma conversepD:
   5.146 -  assumes ab: "r^--1 a b"
   5.147 -  shows "r b a" using ab
   5.148 -  by cases simp
   5.149 -
   5.150 -lemma conversep_iff [iff]: "r^--1 a b = r b a"
   5.151 -  by (iprover intro: conversepI dest: conversepD)
   5.152 -
   5.153 -lemma conversep_converse_eq [pred_set_conv]:
   5.154 -  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   5.155 -  by (auto simp add: fun_eq_iff)
   5.156 -
   5.157 -lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   5.158 -  by (iprover intro: order_antisym conversepI dest: conversepD)
   5.159 -
   5.160 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   5.161 -  by (iprover intro: order_antisym conversepI pred_compI
   5.162 -    elim: pred_compE dest: conversepD)
   5.163 -
   5.164 -lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   5.165 -  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   5.166 -
   5.167 -lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   5.168 -  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   5.169 -
   5.170 -lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   5.171 -  by (auto simp add: fun_eq_iff)
   5.172 -
   5.173 -lemma conversep_eq [simp]: "(op =)^--1 = op ="
   5.174 -  by (auto simp add: fun_eq_iff)
   5.175 -
   5.176 -
   5.177 -subsubsection {* Domain *}
   5.178 -
   5.179 -inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   5.180 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   5.181 -  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   5.182 -
   5.183 -inductive_cases DomainPE [elim!]: "DomainP r a"
   5.184 -
   5.185 -lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   5.186 -  by (blast intro!: Orderings.order_antisym predicate1I)
   5.187 -
   5.188 -
   5.189 -subsubsection {* Range *}
   5.190 -
   5.191 -inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   5.192 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   5.193 -  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   5.194 -
   5.195 -inductive_cases RangePE [elim!]: "RangeP r b"
   5.196 -
   5.197 -lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   5.198 -  by (blast intro!: Orderings.order_antisym predicate1I)
   5.199 -
   5.200 -
   5.201 -subsubsection {* Inverse image *}
   5.202 -
   5.203 -definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   5.204 -  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
   5.205 -
   5.206 -lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
   5.207 -  by (simp add: inv_image_def inv_imagep_def)
   5.208 -
   5.209 -lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   5.210 -  by (simp add: inv_imagep_def)
   5.211 -
   5.212 -
   5.213 -subsubsection {* Powerset *}
   5.214 -
   5.215 -definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   5.216 -  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
   5.217 -
   5.218 -lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   5.219 -  by (auto simp add: Powp_def fun_eq_iff)
   5.220 -
   5.221 -lemmas Powp_mono [mono] = Pow_mono [to_pred]
   5.222 -
   5.223 -
   5.224 -subsubsection {* Properties of relations *}
   5.225 -
   5.226 -abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   5.227 -  "antisymP r \<equiv> antisym {(x, y). r x y}"
   5.228 -
   5.229 -abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   5.230 -  "transP r \<equiv> trans {(x, y). r x y}"
   5.231 -
   5.232 -abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   5.233 -  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   5.234 -
   5.235 -(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   5.236 -
   5.237 -definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   5.238 -  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
   5.239 -
   5.240 -definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   5.241 -  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   5.242 -
   5.243 -definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   5.244 -  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   5.245 -
   5.246 -lemma reflpI:
   5.247 -  "(\<And>x. r x x) \<Longrightarrow> reflp r"
   5.248 -  by (auto intro: refl_onI simp add: reflp_def)
   5.249 -
   5.250 -lemma reflpE:
   5.251 -  assumes "reflp r"
   5.252 -  obtains "r x x"
   5.253 -  using assms by (auto dest: refl_onD simp add: reflp_def)
   5.254 -
   5.255 -lemma sympI:
   5.256 -  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   5.257 -  by (auto intro: symI simp add: symp_def)
   5.258 -
   5.259 -lemma sympE:
   5.260 -  assumes "symp r" and "r x y"
   5.261 -  obtains "r y x"
   5.262 -  using assms by (auto dest: symD simp add: symp_def)
   5.263 -
   5.264 -lemma transpI:
   5.265 -  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   5.266 -  by (auto intro: transI simp add: transp_def)
   5.267 -  
   5.268 -lemma transpE:
   5.269 -  assumes "transp r" and "r x y" and "r y z"
   5.270 -  obtains "r x z"
   5.271 -  using assms by (auto dest: transD simp add: transp_def)
   5.272 -
   5.273 -
   5.274 -subsection {* Predicates as enumerations *}
   5.275 -
   5.276 -subsubsection {* The type of predicate enumerations (a monad) *}
   5.277 +subsection {* The type of predicate enumerations (a monad) *}
   5.278  
   5.279  datatype 'a pred = Pred "'a \<Rightarrow> bool"
   5.280  
   5.281 @@ -465,7 +211,7 @@
   5.282    using assms by (cases A) (auto simp add: bot_pred_def)
   5.283  
   5.284  
   5.285 -subsubsection {* Emptiness check and definite choice *}
   5.286 +subsection {* Emptiness check and definite choice *}
   5.287  
   5.288  definition is_empty :: "'a pred \<Rightarrow> bool" where
   5.289    "is_empty A \<longleftrightarrow> A = \<bottom>"
   5.290 @@ -578,7 +324,7 @@
   5.291  using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
   5.292  
   5.293  
   5.294 -subsubsection {* Derived operations *}
   5.295 +subsection {* Derived operations *}
   5.296  
   5.297  definition if_pred :: "bool \<Rightarrow> unit pred" where
   5.298    if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
   5.299 @@ -668,7 +414,7 @@
   5.300    by (rule ext, rule pred_eqI, auto)+
   5.301  
   5.302  
   5.303 -subsubsection {* Implementation *}
   5.304 +subsection {* Implementation *}
   5.305  
   5.306  datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
   5.307  
   5.308 @@ -762,6 +508,12 @@
   5.309      by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
   5.310  qed
   5.311  
   5.312 +lemma [code]:
   5.313 +  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
   5.314 +
   5.315 +lemma [code]:
   5.316 +  "pred_size f P = 0" by (cases P) simp
   5.317 +
   5.318  primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   5.319    "contained Empty Q \<longleftrightarrow> True"
   5.320  | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
   5.321 @@ -937,6 +689,44 @@
   5.322    "set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq"
   5.323    by auto
   5.324  
   5.325 +text {* Lazy Evaluation of an indexed function *}
   5.326 +
   5.327 +function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
   5.328 +where
   5.329 +  "iterate_upto f n m =
   5.330 +    Predicate.Seq (%u. if n > m then Predicate.Empty
   5.331 +     else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
   5.332 +by pat_completeness auto
   5.333 +
   5.334 +termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
   5.335 +
   5.336 +text {* Misc *}
   5.337 +
   5.338 +declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
   5.339 +
   5.340 +(* FIXME: better implement conversion by bisection *)
   5.341 +
   5.342 +lemma pred_of_set_fold_sup:
   5.343 +  assumes "finite A"
   5.344 +  shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
   5.345 +proof (rule sym)
   5.346 +  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
   5.347 +    by (fact comp_fun_idem_sup)
   5.348 +  from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
   5.349 +qed
   5.350 +
   5.351 +lemma pred_of_set_set_fold_sup:
   5.352 +  "pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot"
   5.353 +proof -
   5.354 +  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
   5.355 +    by (fact comp_fun_idem_sup)
   5.356 +  show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
   5.357 +qed
   5.358 +
   5.359 +lemma pred_of_set_set_foldr_sup [code]:
   5.360 +  "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot"
   5.361 +  by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
   5.362 +
   5.363  no_notation
   5.364    bot ("\<bottom>") and
   5.365    top ("\<top>") and
   5.366 @@ -955,5 +745,8 @@
   5.367  hide_type (open) pred seq
   5.368  hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   5.369    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
   5.370 +  iterate_upto
   5.371 +hide_fact (open) null_def member_def
   5.372  
   5.373  end
   5.374 +
     6.1 --- a/src/HOL/Predicate_Compile.thy	Fri Feb 24 22:46:16 2012 +0100
     6.2 +++ b/src/HOL/Predicate_Compile.thy	Fri Feb 24 22:46:44 2012 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* A compiler for predicates defined by introduction rules *}
     6.5  
     6.6  theory Predicate_Compile
     6.7 -imports New_Random_Sequence Quickcheck_Exhaustive
     6.8 +imports Predicate New_Random_Sequence Quickcheck_Exhaustive
     6.9  uses
    6.10    "Tools/Predicate_Compile/predicate_compile_aux.ML"
    6.11    "Tools/Predicate_Compile/predicate_compile_compilations.ML"
     7.1 --- a/src/HOL/Quickcheck.thy	Fri Feb 24 22:46:16 2012 +0100
     7.2 +++ b/src/HOL/Quickcheck.thy	Fri Feb 24 22:46:44 2012 +0100
     7.3 @@ -233,7 +233,7 @@
     7.4  
     7.5  definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
     7.6  where
     7.7 -  "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
     7.8 +  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
     7.9  
    7.10  definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
    7.11  where
     8.1 --- a/src/HOL/Relation.thy	Fri Feb 24 22:46:16 2012 +0100
     8.2 +++ b/src/HOL/Relation.thy	Fri Feb 24 22:46:44 2012 +0100
     8.3 @@ -1,15 +1,107 @@
     8.4  (*  Title:      HOL/Relation.thy
     8.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.6 -    Copyright   1996  University of Cambridge
     8.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
     8.8  *)
     8.9  
    8.10 -header {* Relations *}
    8.11 +header {* Relations – as sets of pairs, and binary predicates *}
    8.12  
    8.13  theory Relation
    8.14  imports Datatype Finite_Set
    8.15  begin
    8.16  
    8.17 -subsection {* Definitions *}
    8.18 +notation
    8.19 +  bot ("\<bottom>") and
    8.20 +  top ("\<top>") and
    8.21 +  inf (infixl "\<sqinter>" 70) and
    8.22 +  sup (infixl "\<squnion>" 65) and
    8.23 +  Inf ("\<Sqinter>_" [900] 900) and
    8.24 +  Sup ("\<Squnion>_" [900] 900)
    8.25 +
    8.26 +syntax (xsymbols)
    8.27 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    8.28 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    8.29 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    8.30 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    8.31 +
    8.32 +
    8.33 +subsection {* Classical rules for reasoning on predicates *}
    8.34 +
    8.35 +declare predicate1D [Pure.dest?, dest?]
    8.36 +declare predicate2I [Pure.intro!, intro!]
    8.37 +declare predicate2D [Pure.dest, dest]
    8.38 +declare bot1E [elim!]
    8.39 +declare bot2E [elim!]
    8.40 +declare top1I [intro!]
    8.41 +declare top2I [intro!]
    8.42 +declare inf1I [intro!]
    8.43 +declare inf2I [intro!]
    8.44 +declare inf1E [elim!]
    8.45 +declare inf2E [elim!]
    8.46 +declare sup1I1 [intro?]
    8.47 +declare sup2I1 [intro?]
    8.48 +declare sup1I2 [intro?]
    8.49 +declare sup2I2 [intro?]
    8.50 +declare sup1E [elim!]
    8.51 +declare sup2E [elim!]
    8.52 +declare sup1CI [intro!]
    8.53 +declare sup2CI [intro!]
    8.54 +declare INF1_I [intro!]
    8.55 +declare INF2_I [intro!]
    8.56 +declare INF1_D [elim]
    8.57 +declare INF2_D [elim]
    8.58 +declare INF1_E [elim]
    8.59 +declare INF2_E [elim]
    8.60 +declare SUP1_I [intro]
    8.61 +declare SUP2_I [intro]
    8.62 +declare SUP1_E [elim!]
    8.63 +declare SUP2_E [elim!]
    8.64 +
    8.65 +
    8.66 +subsection {* Conversions between set and predicate relations *}
    8.67 +
    8.68 +lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    8.69 +  by (simp add: set_eq_iff fun_eq_iff)
    8.70 +
    8.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)"
    8.72 +  by (simp add: set_eq_iff fun_eq_iff)
    8.73 +
    8.74 +lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    8.75 +  by (simp add: subset_iff le_fun_def)
    8.76 +
    8.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)"
    8.78 +  by (simp add: subset_iff le_fun_def)
    8.79 +
    8.80 +lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    8.81 +  by (auto simp add: fun_eq_iff)
    8.82 +
    8.83 +lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    8.84 +  by (auto simp add: fun_eq_iff)
    8.85 +
    8.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)"
    8.87 +  by (simp add: inf_fun_def)
    8.88 +
    8.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)"
    8.90 +  by (simp add: inf_fun_def)
    8.91 +
    8.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)"
    8.93 +  by (simp add: sup_fun_def)
    8.94 +
    8.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)"
    8.96 +  by (simp add: sup_fun_def)
    8.97 +
    8.98 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    8.99 +  by (simp add: INF_apply fun_eq_iff)
   8.100 +
   8.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))"
   8.102 +  by (simp add: INF_apply fun_eq_iff)
   8.103 +
   8.104 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   8.105 +  by (simp add: SUP_apply fun_eq_iff)
   8.106 +
   8.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))"
   8.108 +  by (simp add: SUP_apply fun_eq_iff)
   8.109 +
   8.110 +
   8.111 +subsection {* Relations as sets of pairs *}
   8.112  
   8.113  type_synonym 'a rel = "('a * 'a) set"
   8.114  
   8.115 @@ -90,7 +182,7 @@
   8.116    "inv_image r f = {(x, y). (f x, f y) : r}"
   8.117  
   8.118  
   8.119 -subsection {* The identity relation *}
   8.120 +subsubsection {* The identity relation *}
   8.121  
   8.122  lemma IdI [intro]: "(a, a) : Id"
   8.123  by (simp add: Id_def)
   8.124 @@ -115,7 +207,7 @@
   8.125  by (simp add: trans_def)
   8.126  
   8.127  
   8.128 -subsection {* Diagonal: identity over a set *}
   8.129 +subsubsection {* Diagonal: identity over a set *}
   8.130  
   8.131  lemma Id_on_empty [simp]: "Id_on {} = {}"
   8.132  by (simp add: Id_on_def) 
   8.133 @@ -142,7 +234,7 @@
   8.134  by blast
   8.135  
   8.136  
   8.137 -subsection {* Composition of two relations *}
   8.138 +subsubsection {* Composition of two relations *}
   8.139  
   8.140  lemma rel_compI [intro]:
   8.141    "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
   8.142 @@ -194,7 +286,7 @@
   8.143  by auto
   8.144  
   8.145  
   8.146 -subsection {* Reflexivity *}
   8.147 +subsubsection {* Reflexivity *}
   8.148  
   8.149  lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
   8.150  by (unfold refl_on_def) (iprover intro!: ballI)
   8.151 @@ -232,7 +324,8 @@
   8.152    "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
   8.153  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
   8.154  
   8.155 -subsection {* Antisymmetry *}
   8.156 +
   8.157 +subsubsection {* Antisymmetry *}
   8.158  
   8.159  lemma antisymI:
   8.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   8.161 @@ -251,7 +344,7 @@
   8.162  by (unfold antisym_def) blast
   8.163  
   8.164  
   8.165 -subsection {* Symmetry *}
   8.166 +subsubsection {* Symmetry *}
   8.167  
   8.168  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   8.169  by (unfold sym_def) iprover
   8.170 @@ -275,7 +368,7 @@
   8.171  by (rule symI) clarify
   8.172  
   8.173  
   8.174 -subsection {* Transitivity *}
   8.175 +subsubsection {* Transitivity *}
   8.176  
   8.177  lemma trans_join [code]:
   8.178    "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
   8.179 @@ -300,7 +393,8 @@
   8.180  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
   8.181  unfolding antisym_def trans_def by blast
   8.182  
   8.183 -subsection {* Irreflexivity *}
   8.184 +
   8.185 +subsubsection {* Irreflexivity *}
   8.186  
   8.187  lemma irrefl_distinct [code]:
   8.188    "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
   8.189 @@ -310,7 +404,7 @@
   8.190  by(simp add:irrefl_def)
   8.191  
   8.192  
   8.193 -subsection {* Totality *}
   8.194 +subsubsection {* Totality *}
   8.195  
   8.196  lemma total_on_empty[simp]: "total_on {} r"
   8.197  by(simp add:total_on_def)
   8.198 @@ -318,7 +412,8 @@
   8.199  lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
   8.200  by(simp add: total_on_def)
   8.201  
   8.202 -subsection {* Converse *}
   8.203 +
   8.204 +subsubsection {* Converse *}
   8.205  
   8.206  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   8.207  by (simp add: converse_def)
   8.208 @@ -383,7 +478,7 @@
   8.209  by (auto simp: total_on_def)
   8.210  
   8.211  
   8.212 -subsection {* Domain *}
   8.213 +subsubsection {* Domain *}
   8.214  
   8.215  declare Domain_def [no_atp]
   8.216  
   8.217 @@ -444,7 +539,7 @@
   8.218  by auto
   8.219  
   8.220  
   8.221 -subsection {* Range *}
   8.222 +subsubsection {* Range *}
   8.223  
   8.224  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   8.225  by (simp add: Domain_def Range_def)
   8.226 @@ -493,7 +588,7 @@
   8.227    by force
   8.228  
   8.229  
   8.230 -subsection {* Field *}
   8.231 +subsubsection {* Field *}
   8.232  
   8.233  lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   8.234  by(auto simp:Field_def Domain_def Range_def)
   8.235 @@ -514,7 +609,7 @@
   8.236  by(auto simp:Field_def)
   8.237  
   8.238  
   8.239 -subsection {* Image of a set under a relation *}
   8.240 +subsubsection {* Image of a set under a relation *}
   8.241  
   8.242  declare Image_def [no_atp]
   8.243  
   8.244 @@ -588,7 +683,7 @@
   8.245  by blast
   8.246  
   8.247  
   8.248 -subsection {* Single valued relations *}
   8.249 +subsubsection {* Single valued relations *}
   8.250  
   8.251  lemma single_valuedI:
   8.252    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   8.253 @@ -613,7 +708,7 @@
   8.254  by (unfold single_valued_def) blast
   8.255  
   8.256  
   8.257 -subsection {* Graphs given by @{text Collect} *}
   8.258 +subsubsection {* Graphs given by @{text Collect} *}
   8.259  
   8.260  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
   8.261  by auto
   8.262 @@ -625,7 +720,7 @@
   8.263  by auto
   8.264  
   8.265  
   8.266 -subsection {* Inverse image *}
   8.267 +subsubsection {* Inverse image *}
   8.268  
   8.269  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   8.270  by (unfold sym_def inv_image_def) blast
   8.271 @@ -643,7 +738,7 @@
   8.272  unfolding inv_image_def converse_def by auto
   8.273  
   8.274  
   8.275 -subsection {* Finiteness *}
   8.276 +subsubsection {* Finiteness *}
   8.277  
   8.278  lemma finite_converse [iff]: "finite (r^-1) = finite r"
   8.279    apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   8.280 @@ -671,7 +766,7 @@
   8.281    done
   8.282  
   8.283  
   8.284 -subsection {* Miscellaneous *}
   8.285 +subsubsection {* Miscellaneous *}
   8.286  
   8.287  text {* Version of @{thm[source] lfp_induct} for binary relations *}
   8.288  
   8.289 @@ -683,4 +778,171 @@
   8.290  lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
   8.291  by auto
   8.292  
   8.293 +
   8.294 +subsection {* Relations as binary predicates *}
   8.295 +
   8.296 +subsubsection {* Composition *}
   8.297 +
   8.298 +inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   8.299 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
   8.300 +  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   8.301 +
   8.302 +inductive_cases pred_compE [elim!]: "(r OO s) a c"
   8.303 +
   8.304 +lemma pred_comp_rel_comp_eq [pred_set_conv]:
   8.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)"
   8.306 +  by (auto simp add: fun_eq_iff)
   8.307 +
   8.308 +
   8.309 +subsubsection {* Converse *}
   8.310 +
   8.311 +inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   8.312 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   8.313 +  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   8.314 +
   8.315 +notation (xsymbols)
   8.316 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   8.317 +
   8.318 +lemma conversepD:
   8.319 +  assumes ab: "r^--1 a b"
   8.320 +  shows "r b a" using ab
   8.321 +  by cases simp
   8.322 +
   8.323 +lemma conversep_iff [iff]: "r^--1 a b = r b a"
   8.324 +  by (iprover intro: conversepI dest: conversepD)
   8.325 +
   8.326 +lemma conversep_converse_eq [pred_set_conv]:
   8.327 +  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   8.328 +  by (auto simp add: fun_eq_iff)
   8.329 +
   8.330 +lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   8.331 +  by (iprover intro: order_antisym conversepI dest: conversepD)
   8.332 +
   8.333 +lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   8.334 +  by (iprover intro: order_antisym conversepI pred_compI
   8.335 +    elim: pred_compE dest: conversepD)
   8.336 +
   8.337 +lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   8.338 +  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   8.339 +
   8.340 +lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   8.341 +  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   8.342 +
   8.343 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   8.344 +  by (auto simp add: fun_eq_iff)
   8.345 +
   8.346 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
   8.347 +  by (auto simp add: fun_eq_iff)
   8.348 +
   8.349 +
   8.350 +subsubsection {* Domain *}
   8.351 +
   8.352 +inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   8.353 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   8.354 +  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   8.355 +
   8.356 +inductive_cases DomainPE [elim!]: "DomainP r a"
   8.357 +
   8.358 +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   8.359 +  by (blast intro!: Orderings.order_antisym predicate1I)
   8.360 +
   8.361 +
   8.362 +subsubsection {* Range *}
   8.363 +
   8.364 +inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   8.365 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   8.366 +  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   8.367 +
   8.368 +inductive_cases RangePE [elim!]: "RangeP r b"
   8.369 +
   8.370 +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   8.371 +  by (blast intro!: Orderings.order_antisym predicate1I)
   8.372 +
   8.373 +
   8.374 +subsubsection {* Inverse image *}
   8.375 +
   8.376 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   8.377 +  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
   8.378 +
   8.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)"
   8.380 +  by (simp add: inv_image_def inv_imagep_def)
   8.381 +
   8.382 +lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   8.383 +  by (simp add: inv_imagep_def)
   8.384 +
   8.385 +
   8.386 +subsubsection {* Powerset *}
   8.387 +
   8.388 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   8.389 +  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
   8.390 +
   8.391 +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   8.392 +  by (auto simp add: Powp_def fun_eq_iff)
   8.393 +
   8.394 +lemmas Powp_mono [mono] = Pow_mono [to_pred]
   8.395 +
   8.396 +
   8.397 +subsubsection {* Properties of predicate relations *}
   8.398 +
   8.399 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.400 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
   8.401 +
   8.402 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.403 +  "transP r \<equiv> trans {(x, y). r x y}"
   8.404 +
   8.405 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   8.406 +  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   8.407 +
   8.408 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   8.409 +
   8.410 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.411 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
   8.412 +
   8.413 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.414 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
   8.415 +
   8.416 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   8.417 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   8.418 +
   8.419 +lemma reflpI:
   8.420 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
   8.421 +  by (auto intro: refl_onI simp add: reflp_def)
   8.422 +
   8.423 +lemma reflpE:
   8.424 +  assumes "reflp r"
   8.425 +  obtains "r x x"
   8.426 +  using assms by (auto dest: refl_onD simp add: reflp_def)
   8.427 +
   8.428 +lemma sympI:
   8.429 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
   8.430 +  by (auto intro: symI simp add: symp_def)
   8.431 +
   8.432 +lemma sympE:
   8.433 +  assumes "symp r" and "r x y"
   8.434 +  obtains "r y x"
   8.435 +  using assms by (auto dest: symD simp add: symp_def)
   8.436 +
   8.437 +lemma transpI:
   8.438 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
   8.439 +  by (auto intro: transI simp add: transp_def)
   8.440 +  
   8.441 +lemma transpE:
   8.442 +  assumes "transp r" and "r x y" and "r y z"
   8.443 +  obtains "r x z"
   8.444 +  using assms by (auto dest: transD simp add: transp_def)
   8.445 +
   8.446 +no_notation
   8.447 +  bot ("\<bottom>") and
   8.448 +  top ("\<top>") and
   8.449 +  inf (infixl "\<sqinter>" 70) and
   8.450 +  sup (infixl "\<squnion>" 65) and
   8.451 +  Inf ("\<Sqinter>_" [900] 900) and
   8.452 +  Sup ("\<Squnion>_" [900] 900)
   8.453 +
   8.454 +no_syntax (xsymbols)
   8.455 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   8.456 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   8.457 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   8.458 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   8.459 +
   8.460  end
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Feb 24 22:46:16 2012 +0100
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Feb 24 22:46:44 2012 +0100
     9.3 @@ -30,7 +30,7 @@
     9.4    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
     9.5  
     9.6  fun mk_iterate_upto T (f, from, to) =
     9.7 -  list_comb (Const (@{const_name Code_Numeral.iterate_upto},
     9.8 +  list_comb (Const (@{const_name Predicate.iterate_upto},
     9.9        [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
    9.10      [f, from, to])
    9.11  
    10.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 24 22:46:16 2012 +0100
    10.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Feb 24 22:46:44 2012 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Reflexive and Transitive closure of a relation *}
    10.5  
    10.6  theory Transitive_Closure
    10.7 -imports Predicate
    10.8 +imports Relation
    10.9  uses "~~/src/Provers/trancl.ML"
   10.10  begin
   10.11  
    11.1 --- a/src/HOL/Wellfounded.thy	Fri Feb 24 22:46:16 2012 +0100
    11.2 +++ b/src/HOL/Wellfounded.thy	Fri Feb 24 22:46:44 2012 +0100
    11.3 @@ -858,10 +858,4 @@
    11.4  
    11.5  declare "prod.size" [no_atp]
    11.6  
    11.7 -lemma [code]:
    11.8 -  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
    11.9 -
   11.10 -lemma [code]:
   11.11 -  "pred_size f P = 0" by (cases P) simp
   11.12 -
   11.13  end