src/HOL/Lattices.thy
changeset 41080 294956ff285b
parent 41075 4bed56dc95fb
child 41082 9ff94e7cc3b3
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
     1.3 @@ -587,34 +587,33 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  bool_Compl_def: "uminus = Not"
     1.8 +  bool_Compl_def [simp]: "uminus = Not"
     1.9  
    1.10  definition
    1.11 -  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
    1.12 +  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
    1.13  
    1.14  definition
    1.15 -  inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    1.16 +  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    1.17  
    1.18  definition
    1.19 -  sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    1.20 +  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    1.21  
    1.22  instance proof
    1.23 -qed (simp_all add: inf_bool_def sup_bool_def le_bool_def
    1.24 -  bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto)
    1.25 +qed auto
    1.26  
    1.27  end
    1.28  
    1.29  lemma sup_boolI1:
    1.30    "P \<Longrightarrow> P \<squnion> Q"
    1.31 -  by (simp add: sup_bool_def)
    1.32 +  by simp
    1.33  
    1.34  lemma sup_boolI2:
    1.35    "Q \<Longrightarrow> P \<squnion> Q"
    1.36 -  by (simp add: sup_bool_def)
    1.37 +  by simp
    1.38  
    1.39  lemma sup_boolE:
    1.40    "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.41 -  by (auto simp add: sup_bool_def)
    1.42 +  by auto
    1.43  
    1.44  
    1.45  subsection {* Fun as lattice *}
    1.46 @@ -623,19 +622,26 @@
    1.47  begin
    1.48  
    1.49  definition
    1.50 -  inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.51 +  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.52 +
    1.53 +lemma inf_apply:
    1.54 +  "(f \<sqinter> g) x = f x \<sqinter> g x"
    1.55 +  by (simp add: inf_fun_def)
    1.56  
    1.57  definition
    1.58 -  sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.59 +  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.60 +
    1.61 +lemma sup_apply:
    1.62 +  "(f \<squnion> g) x = f x \<squnion> g x"
    1.63 +  by (simp add: sup_fun_def)
    1.64  
    1.65  instance proof
    1.66 -qed (simp_all add: le_fun_def inf_fun_def sup_fun_def)
    1.67 +qed (simp_all add: le_fun_def inf_apply sup_apply)
    1.68  
    1.69  end
    1.70  
    1.71 -instance "fun" :: (type, distrib_lattice) distrib_lattice
    1.72 -proof
    1.73 -qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1)
    1.74 +instance "fun" :: (type, distrib_lattice) distrib_lattice proof
    1.75 +qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
    1.76  
    1.77  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
    1.78  
    1.79 @@ -645,6 +651,10 @@
    1.80  definition
    1.81    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    1.82  
    1.83 +lemma uminus_apply:
    1.84 +  "(- A) x = - (A x)"
    1.85 +  by (simp add: fun_Compl_def)
    1.86 +
    1.87  instance ..
    1.88  
    1.89  end
    1.90 @@ -655,15 +665,16 @@
    1.91  definition
    1.92    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    1.93  
    1.94 +lemma minus_apply:
    1.95 +  "(A - B) x = A x - B x"
    1.96 +  by (simp add: fun_diff_def)
    1.97 +
    1.98  instance ..
    1.99  
   1.100  end
   1.101  
   1.102 -instance "fun" :: (type, boolean_algebra) boolean_algebra
   1.103 -proof
   1.104 -qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def
   1.105 -  inf_compl_bot sup_compl_top diff_eq)
   1.106 -
   1.107 +instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   1.108 +qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
   1.109  
   1.110  no_notation
   1.111    less_eq  (infix "\<sqsubseteq>" 50) and