src/HOL/Orderings.thy
changeset 46631 2c5c003cee35
parent 46557 ae926869a311
child 46689 f559866a7aa2
     1.1 --- a/src/HOL/Orderings.thy	Thu Feb 23 20:15:59 2012 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Feb 23 20:33:35 2012 +0100
     1.3 @@ -1111,10 +1111,6 @@
     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 @@ -1227,7 +1223,7 @@
    1.15  end
    1.16  
    1.17  
    1.18 -subsection {* Order on bool *}
    1.19 +subsection {* Order on @{typ bool} *}
    1.20  
    1.21  instantiation bool :: "{bot, top, linorder}"
    1.22  begin
    1.23 @@ -1239,10 +1235,10 @@
    1.24    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.25  
    1.26  definition
    1.27 -  [simp]: "bot \<longleftrightarrow> False"
    1.28 +  [simp]: "\<bottom> \<longleftrightarrow> False"
    1.29  
    1.30  definition
    1.31 -  [simp]: "top \<longleftrightarrow> True"
    1.32 +  [simp]: "\<top> \<longleftrightarrow> True"
    1.33  
    1.34  instance proof
    1.35  qed auto
    1.36 @@ -1261,10 +1257,10 @@
    1.37  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.38    by simp
    1.39  
    1.40 -lemma bot_boolE: "bot \<Longrightarrow> P"
    1.41 +lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
    1.42    by simp
    1.43  
    1.44 -lemma top_boolI: top
    1.45 +lemma top_boolI: \<top>
    1.46    by simp
    1.47  
    1.48  lemma [code]:
    1.49 @@ -1275,7 +1271,7 @@
    1.50    by simp_all
    1.51  
    1.52  
    1.53 -subsection {* Order on functions *}
    1.54 +subsection {* Order on @{typ "_ \<Rightarrow> _"} *}
    1.55  
    1.56  instantiation "fun" :: (type, ord) ord
    1.57  begin
    1.58 @@ -1301,10 +1297,10 @@
    1.59  begin
    1.60  
    1.61  definition
    1.62 -  "bot = (\<lambda>x. bot)"
    1.63 +  "\<bottom> = (\<lambda>x. \<bottom>)"
    1.64  
    1.65  lemma bot_apply:
    1.66 -  "bot x = bot"
    1.67 +  "\<bottom> x = \<bottom>"
    1.68    by (simp add: bot_fun_def)
    1.69  
    1.70  instance proof
    1.71 @@ -1316,11 +1312,11 @@
    1.72  begin
    1.73  
    1.74  definition
    1.75 -  [no_atp]: "top = (\<lambda>x. top)"
    1.76 +  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    1.77  declare top_fun_def_raw [no_atp]
    1.78  
    1.79  lemma top_apply:
    1.80 -  "top x = top"
    1.81 +  "\<top> x = \<top>"
    1.82    by (simp add: top_fun_def)
    1.83  
    1.84  instance proof
    1.85 @@ -1338,6 +1334,61 @@
    1.86    unfolding le_fun_def by simp
    1.87  
    1.88  
    1.89 +subsection {* Order on unary and binary predicates *}
    1.90 +
    1.91 +lemma predicate1I:
    1.92 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.93 +  shows "P \<le> Q"
    1.94 +  apply (rule le_funI)
    1.95 +  apply (rule le_boolI)
    1.96 +  apply (rule PQ)
    1.97 +  apply assumption
    1.98 +  done
    1.99 +
   1.100 +lemma predicate1D:
   1.101 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   1.102 +  apply (erule le_funE)
   1.103 +  apply (erule le_boolE)
   1.104 +  apply assumption+
   1.105 +  done
   1.106 +
   1.107 +lemma rev_predicate1D:
   1.108 +  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
   1.109 +  by (rule predicate1D)
   1.110 +
   1.111 +lemma predicate2I:
   1.112 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   1.113 +  shows "P \<le> Q"
   1.114 +  apply (rule le_funI)+
   1.115 +  apply (rule le_boolI)
   1.116 +  apply (rule PQ)
   1.117 +  apply assumption
   1.118 +  done
   1.119 +
   1.120 +lemma predicate2D:
   1.121 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.122 +  apply (erule le_funE)+
   1.123 +  apply (erule le_boolE)
   1.124 +  apply assumption+
   1.125 +  done
   1.126 +
   1.127 +lemma rev_predicate2D:
   1.128 +  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   1.129 +  by (rule predicate2D)
   1.130 +
   1.131 +lemma bot1E [no_atp]: "\<bottom> x \<Longrightarrow> P"
   1.132 +  by (simp add: bot_fun_def)
   1.133 +
   1.134 +lemma bot2E: "\<bottom> x y \<Longrightarrow> P"
   1.135 +  by (simp add: bot_fun_def)
   1.136 +
   1.137 +lemma top1I: "\<top> x"
   1.138 +  by (simp add: top_fun_def)
   1.139 +
   1.140 +lemma top2I: "\<top> x y"
   1.141 +  by (simp add: top_fun_def)
   1.142 +
   1.143 +
   1.144  subsection {* Name duplicates *}
   1.145  
   1.146  lemmas order_eq_refl = preorder_class.eq_refl
   1.147 @@ -1375,4 +1426,8 @@
   1.148  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   1.149  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.150  
   1.151 +no_notation
   1.152 +  top ("\<top>") and
   1.153 +  bot ("\<bottom>")
   1.154 +
   1.155  end