src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Mon Feb 20 15:17:03 2012 +0100
+++ b/src/HOL/Orderings.thy	Sun Feb 19 15:30:35 2012 +0100
@@ -1111,10 +1111,6 @@
 
 end
 
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>")
-
 
 subsection {* Dense orders *}
 
@@ -1239,10 +1235,10 @@
   [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
 
 definition
-  [simp]: "bot \<longleftrightarrow> False"
+  [simp]: "\<bottom> \<longleftrightarrow> False"
 
 definition
-  [simp]: "top \<longleftrightarrow> True"
+  [simp]: "\<top> \<longleftrightarrow> True"
 
 instance proof
 qed auto
@@ -1261,10 +1257,10 @@
 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   by simp
 
-lemma bot_boolE: "bot \<Longrightarrow> P"
+lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
   by simp
 
-lemma top_boolI: top
+lemma top_boolI: \<top>
   by simp
 
 lemma [code]:
@@ -1301,10 +1297,10 @@
 begin
 
 definition
-  "bot = (\<lambda>x. bot)"
+  "\<bottom> = (\<lambda>x. \<bottom>)"
 
 lemma bot_apply:
-  "bot x = bot"
+  "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
 instance proof
@@ -1316,11 +1312,11 @@
 begin
 
 definition
-  [no_atp]: "top = (\<lambda>x. top)"
+  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 declare top_fun_def_raw [no_atp]
 
 lemma top_apply:
-  "top x = top"
+  "\<top> x = \<top>"
   by (simp add: top_fun_def)
 
 instance proof
@@ -1338,6 +1334,61 @@
   unfolding le_fun_def by simp
 
 
+subsection {* Order 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 \<Longrightarrow> P \<le> Q \<Longrightarrow> 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 \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
+  by (rule predicate2D)
+
+lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
+  by (simp add: bot_fun_def)
+
+lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
+  by (simp add: bot_fun_def)
+
+lemma top1I [intro!]: "\<top> x"
+  by (simp add: top_fun_def)
+
+lemma top2I [intro!]: "\<top> x y"
+  by (simp add: top_fun_def)
+
+
 subsection {* Name duplicates *}
 
 lemmas order_eq_refl = preorder_class.eq_refl
@@ -1375,4 +1426,8 @@
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
+no_notation
+  top ("\<top>") and
+  bot ("\<bottom>")
+
 end