src/HOL/Orderings.thy
changeset 46557 ae926869a311
parent 46553 50a7e97fe653
child 46631 2c5c003cee35
     1.1 --- a/src/HOL/Orderings.thy	Mon Feb 20 21:04:00 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Feb 21 08:15:42 2012 +0100
     1.3 @@ -1111,6 +1111,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +no_notation
     1.8 +  bot ("\<bottom>") and
     1.9 +  top ("\<top>")
    1.10 +
    1.11  
    1.12  subsection {* Dense orders *}
    1.13  
    1.14 @@ -1235,10 +1239,10 @@
    1.15    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.16  
    1.17  definition
    1.18 -  [simp]: "\<bottom> \<longleftrightarrow> False"
    1.19 +  [simp]: "bot \<longleftrightarrow> False"
    1.20  
    1.21  definition
    1.22 -  [simp]: "\<top> \<longleftrightarrow> True"
    1.23 +  [simp]: "top \<longleftrightarrow> True"
    1.24  
    1.25  instance proof
    1.26  qed auto
    1.27 @@ -1257,10 +1261,10 @@
    1.28  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.29    by simp
    1.30  
    1.31 -lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
    1.32 +lemma bot_boolE: "bot \<Longrightarrow> P"
    1.33    by simp
    1.34  
    1.35 -lemma top_boolI: \<top>
    1.36 +lemma top_boolI: top
    1.37    by simp
    1.38  
    1.39  lemma [code]:
    1.40 @@ -1297,10 +1301,10 @@
    1.41  begin
    1.42  
    1.43  definition
    1.44 -  "\<bottom> = (\<lambda>x. \<bottom>)"
    1.45 +  "bot = (\<lambda>x. bot)"
    1.46  
    1.47  lemma bot_apply:
    1.48 -  "\<bottom> x = \<bottom>"
    1.49 +  "bot x = bot"
    1.50    by (simp add: bot_fun_def)
    1.51  
    1.52  instance proof
    1.53 @@ -1312,11 +1316,11 @@
    1.54  begin
    1.55  
    1.56  definition
    1.57 -  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    1.58 +  [no_atp]: "top = (\<lambda>x. top)"
    1.59  declare top_fun_def_raw [no_atp]
    1.60  
    1.61  lemma top_apply:
    1.62 -  "\<top> x = \<top>"
    1.63 +  "top x = top"
    1.64    by (simp add: top_fun_def)
    1.65  
    1.66  instance proof
    1.67 @@ -1334,61 +1338,6 @@
    1.68    unfolding le_fun_def by simp
    1.69  
    1.70  
    1.71 -subsection {* Order on unary and binary predicates *}
    1.72 -
    1.73 -lemma predicate1I:
    1.74 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.75 -  shows "P \<le> Q"
    1.76 -  apply (rule le_funI)
    1.77 -  apply (rule le_boolI)
    1.78 -  apply (rule PQ)
    1.79 -  apply assumption
    1.80 -  done
    1.81 -
    1.82 -lemma predicate1D [Pure.dest?, dest?]:
    1.83 -  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    1.84 -  apply (erule le_funE)
    1.85 -  apply (erule le_boolE)
    1.86 -  apply assumption+
    1.87 -  done
    1.88 -
    1.89 -lemma rev_predicate1D:
    1.90 -  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    1.91 -  by (rule predicate1D)
    1.92 -
    1.93 -lemma predicate2I [Pure.intro!, intro!]:
    1.94 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    1.95 -  shows "P \<le> Q"
    1.96 -  apply (rule le_funI)+
    1.97 -  apply (rule le_boolI)
    1.98 -  apply (rule PQ)
    1.99 -  apply assumption
   1.100 -  done
   1.101 -
   1.102 -lemma predicate2D [Pure.dest, dest]:
   1.103 -  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.104 -  apply (erule le_funE)+
   1.105 -  apply (erule le_boolE)
   1.106 -  apply assumption+
   1.107 -  done
   1.108 -
   1.109 -lemma rev_predicate2D:
   1.110 -  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   1.111 -  by (rule predicate2D)
   1.112 -
   1.113 -lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
   1.114 -  by (simp add: bot_fun_def)
   1.115 -
   1.116 -lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
   1.117 -  by (simp add: bot_fun_def)
   1.118 -
   1.119 -lemma top1I [intro!]: "\<top> x"
   1.120 -  by (simp add: top_fun_def)
   1.121 -
   1.122 -lemma top2I [intro!]: "\<top> x y"
   1.123 -  by (simp add: top_fun_def)
   1.124 -
   1.125 -
   1.126  subsection {* Name duplicates *}
   1.127  
   1.128  lemmas order_eq_refl = preorder_class.eq_refl
   1.129 @@ -1426,8 +1375,4 @@
   1.130  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   1.131  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.132  
   1.133 -no_notation
   1.134 -  top ("\<top>") and
   1.135 -  bot ("\<bottom>")
   1.136 -
   1.137  end