# HG changeset patch
# User haftmann
# Date 1260539036 -3600
# Node ID 6f8f9835e219736d64eda1463a399db5b8af87a3
# Parent  eee04bbbae7e208fdb71c29d609d3d0ea8dff6ae
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

diff -r eee04bbbae7e -r 6f8f9835e219 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Dec 11 14:43:55 2009 +0100
+++ b/src/HOL/Orderings.thy	Fri Dec 11 14:43:56 2009 +0100
@@ -1257,45 +1257,4 @@
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   unfolding le_fun_def by simp
 
-text {*
-  Handy introduction and elimination rules for @{text "\<le>"}
-  on unary and binary predicates
-*}
-
-lemma predicate1I:
-  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "P \<le> Q"
-  apply (rule le_funI)
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
-  apply (erule le_funE)
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma predicate2I [Pure.intro!, intro!]:
-  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
-  shows "P \<le> Q"
-  apply (rule le_funI)+
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
-  apply (erule le_funE)+
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
-  by (rule predicate1D)
-
-lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
-  by (rule predicate2D)
-
 end
diff -r eee04bbbae7e -r 6f8f9835e219 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Dec 11 14:43:55 2009 +0100
+++ b/src/HOL/Predicate.thy	Fri Dec 11 14:43:56 2009 +0100
@@ -19,6 +19,53 @@
 
 subsection {* Predicates as (complete) lattices *}
 
+
+text {*
+  Handy introduction and elimination rules for @{text "\<le>"}
+  on unary and binary predicates
+*}
+
+lemma predicate1I:
+  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+  shows "P \<le> Q"
+  apply (rule le_funI)
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate1D [Pure.dest?, dest?]:
+  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+  apply (erule le_funE)
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate1D:
+  "P x ==> P <= Q ==> Q x"
+  by (rule predicate1D)
+
+lemma predicate2I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+  shows "P \<le> Q"
+  apply (rule le_funI)+
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate2D [Pure.dest, dest]:
+  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  apply (erule le_funE)+
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate2D:
+  "P x y ==> P <= Q ==> Q x y"
+  by (rule predicate2D)
+
+
 subsubsection {* Equality *}
 
 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
diff -r eee04bbbae7e -r 6f8f9835e219 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Dec 11 14:43:55 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Dec 11 14:43:56 2009 +0100
@@ -605,7 +605,7 @@
 (** Induction rule **)
 
 
-val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
+val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
 
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =