1.1 --- a/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
     1.3 @@ -1208,46 +1208,46 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     1.8 +  le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     1.9  
    1.10  definition
    1.11 -  less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.12 +  [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.13  
    1.14  definition
    1.15 -  top_bool_def: "top = True"
    1.16 +  [simp]: "top \<longleftrightarrow> True"
    1.17  
    1.18  definition
    1.19 -  bot_bool_def: "bot = False"
    1.20 +  [simp]: "bot \<longleftrightarrow> False"
    1.21  
    1.22  instance proof
    1.23 -qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
    1.24 +qed auto
    1.25  
    1.26  end
    1.27  
    1.28  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    1.29 -  by (simp add: le_bool_def)
    1.30 +  by simp
    1.31  
    1.32  lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    1.33 -  by (simp add: le_bool_def)
    1.34 +  by simp
    1.35  
    1.36  lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.37 -  by (simp add: le_bool_def)
    1.38 +  by simp
    1.39  
    1.40  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.41 -  by (simp add: le_bool_def)
    1.42 +  by simp
    1.43  
    1.44  lemma bot_boolE: "bot \<Longrightarrow> P"
    1.45 -  by (simp add: bot_bool_def)
    1.46 +  by simp
    1.47  
    1.48  lemma top_boolI: top
    1.49 -  by (simp add: top_bool_def)
    1.50 +  by simp
    1.51  
    1.52  lemma [code]:
    1.53    "False \<le> b \<longleftrightarrow> True"
    1.54    "True \<le> b \<longleftrightarrow> b"
    1.55    "False < b \<longleftrightarrow> b"
    1.56    "True < b \<longleftrightarrow> False"
    1.57 -  unfolding le_bool_def less_bool_def by simp_all
    1.58 +  by simp_all
    1.59  
    1.60  
    1.61  subsection {* Order on functions *}
    1.62 @@ -1259,7 +1259,7 @@
    1.63    le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.64  
    1.65  definition
    1.66 -  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    1.67 +  "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    1.68  
    1.69  instance ..
    1.70  
    1.71 @@ -1276,11 +1276,15 @@
    1.72  begin
    1.73  
    1.74  definition
    1.75 -  top_fun_def [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 +  by (simp add: top_fun_def)
    1.82 +
    1.83  instance proof
    1.84 -qed (simp add: top_fun_def le_fun_def)
    1.85 +qed (simp add: le_fun_def top_apply)
    1.86  
    1.87  end
    1.88  
    1.89 @@ -1288,10 +1292,14 @@
    1.90  begin
    1.91  
    1.92  definition
    1.93 -  bot_fun_def: "bot = (\<lambda>x. bot)"
    1.94 +  "bot = (\<lambda>x. bot)"
    1.95 +
    1.96 +lemma bot_apply:
    1.97 +  "bot x = bot"
    1.98 +  by (simp add: bot_fun_def)
    1.99  
   1.100  instance proof
   1.101 -qed (simp add: bot_fun_def le_fun_def)
   1.102 +qed (simp add: le_fun_def bot_apply)
   1.103  
   1.104  end
   1.105