--- a/src/HOL/List.thy Fri Dec 11 14:32:37 2009 +0100
+++ b/src/HOL/List.thy Fri Dec 11 14:44:08 2009 +0100
@@ -3463,7 +3463,7 @@
inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
-by (rule predicate1I, erule listsp.induct, blast+)
+by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 11 14:32:37 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 11 14:44:08 2009 +0100
@@ -790,8 +790,11 @@
unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
unfolding mem_def by auto
-lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])
- using convex_Inter[unfolded Ball_def mem_def] by auto
+lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
+ apply (rule hull_eq [unfolded mem_def])
+ apply (rule convex_Inter [unfolded Ball_def mem_def])
+ apply (simp add: le_fun_def le_bool_def)
+ done
lemma bounded_convex_hull:
fixes s :: "'a::real_normed_vector set"
--- a/src/HOL/Orderings.thy Fri Dec 11 14:32:37 2009 +0100
+++ b/src/HOL/Orderings.thy Fri Dec 11 14:44:08 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
--- a/src/HOL/Predicate.thy Fri Dec 11 14:32:37 2009 +0100
+++ b/src/HOL/Predicate.thy Fri Dec 11 14:44:08 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)"
--- a/src/HOL/Tools/Function/function_core.ML Fri Dec 11 14:32:37 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Dec 11 14:44:08 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 =