src/HOL/Lattices.thy
changeset 23948 261bd4678076
parent 23878 bd651ecd4b8a
child 24164 911b46812018
     1.1 --- a/src/HOL/Lattices.thy	Mon Jul 23 22:18:05 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Jul 24 15:20:45 2007 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  
     1.5  interpretation min_max:
     1.6    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
     1.7 -  by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
     1.8 +  by (rule distrib_lattice_min_max)
     1.9  
    1.10  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.11    by (rule ext)+ auto
    1.12 @@ -367,7 +367,7 @@
    1.13    apply (erule Inf_lower)
    1.14    done
    1.15  
    1.16 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.17 +lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    1.18    apply (rule antisym)
    1.19    apply (rule Sup_least)
    1.20    apply (erule insertE)
    1.21 @@ -387,7 +387,7 @@
    1.22    "\<Sqinter>{a} = a"
    1.23    by (auto intro: antisym Inf_lower Inf_greatest)
    1.24  
    1.25 -lemma Sup_singleton [simp]:
    1.26 +lemma Sup_singleton [simp, code func]:
    1.27    "\<Squnion>{a} = a"
    1.28    by (auto intro: antisym Sup_upper Sup_least)
    1.29  
    1.30 @@ -409,15 +409,6 @@
    1.31  
    1.32  end
    1.33  
    1.34 -lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup]
    1.35 -lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup]
    1.36 -lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup]
    1.37 -
    1.38 -lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup]
    1.39 -lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup]
    1.40 -lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup]
    1.41 -lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup]
    1.42 -
    1.43  definition
    1.44    top :: "'a::complete_lattice"
    1.45  where