# HG changeset patch
# User berghofe
# Date 1170867580 -3600
# Node ID 96a4db55a0b3e1e852855bf266bac553891e72dd
# Parent  51411098e49bd98664566665f0254203c04b74d3
Introduction and elimination rules for <= on predicates
are now declared properly.

diff -r 51411098e49b -r 96a4db55a0b3 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Wed Feb 07 17:58:50 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Wed Feb 07 17:59:40 2007 +0100
@@ -182,7 +182,7 @@
 on unary and binary predicates
 *}
 
-lemma predicate1I [intro]:
+lemma predicate1I [Pure.intro!, intro!]:
   assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
   shows "P \<le> Q"
   apply (rule le_funI)
@@ -191,13 +191,13 @@
   apply assumption
   done
 
-lemma predicate1D [elim]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+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 [intro]:
+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)+
@@ -206,12 +206,18 @@
   apply assumption
   done
 
-lemma predicate2D [elim]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+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)
+
 defs Meet_fun_def: "Meet A == (\<lambda>x. Meet {y. EX f:A. y = f x})"
 
 instance "fun" :: (type, comp_lat) comp_lat
@@ -556,6 +562,7 @@
 val meet_fun_eq = thm "meet_fun_eq";
 val meet_bool_eq = thm "meet_bool_eq";
 val le_funE = thm "le_funE";
+val le_funD = thm "le_funD";
 val le_boolE = thm "le_boolE";
 val le_boolD = thm "le_boolD";
 val le_bool_def = thm "le_bool_def";