src/HOL/Orderings.thy

   "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
   by (auto simp add: less_le_not_le intro!: antisym)
 
 end
 
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>")
-
 
 subsection {* Dense orders *}
 
 class dense_linorder = linorder + 
   assumes gt_ex: "\<exists>y. x < y" 

 
 definition
   [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
 
 end

   by simp
 
 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]:
   "False \<le> b \<longleftrightarrow> True"
   "True \<le> b \<longleftrightarrow> b"

 
 instantiation "fun" :: (type, bot) bot
 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
 qed (simp add: le_fun_def bot_apply)
 

 
 instantiation "fun" :: (type, top) top
 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
 qed (simp add: le_fun_def top_apply)
 

 lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding le_fun_def by simp
 
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   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

 lemmas linorder_neqE = linorder_class.neqE
 lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
-end
+no_notation
+  top ("\<top>") and
+  bot ("\<bottom>")
+
+end