diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Mon Aug 20 18:07:28 2007 +0200 +++ b/src/HOL/Lattices.thy Mon Aug 20 18:07:29 2007 +0200 @@ -327,26 +327,21 @@ class complete_lattice = lattice + fixes Inf :: "'a set \ 'a" ("\_" [900] 900) + and Sup :: "'a set \ 'a" ("\_" [900] 900) assumes Inf_lower: "x \ A \ \A \ x" - assumes Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A" + and Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A" + assumes Sup_upper: "x \ A \ x \ \A" + and Sup_least: "(\x. x \ A \ x \ z) \ \A \ z" begin -definition - Sup :: "'a set \ 'a" ("\_" [900] 900) -where - "\A = \{b. \a \ A. a \<^loc>\ b}" - lemma Inf_Sup: "\A = \{b. \a \ A. b \<^loc>\ a}" - unfolding Sup_def by (auto intro: Inf_greatest Inf_lower) + by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least) -lemma Sup_upper: "x \ A \ x \<^loc>\ \A" - by (auto simp: Sup_def intro: Inf_greatest) - -lemma Sup_least: "(\x. x \ A \ x \<^loc>\ z) \ \A \<^loc>\ z" - by (auto simp: Sup_def intro: Inf_lower) +lemma Sup_Inf: "\A = \{b. \a \ A. a \<^loc>\ b}" + by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least) lemma Inf_Univ: "\UNIV = \{}" - unfolding Sup_def by auto + unfolding Sup_Inf by auto lemma Sup_Univ: "\UNIV = \{}" unfolding Inf_Sup by auto @@ -367,7 +362,7 @@ apply (erule Inf_lower) done -lemma Sup_insert [code func]: "\insert a A = a \ \A" +lemma Sup_insert: "\insert a A = a \ \A" apply (rule antisym) apply (rule Sup_least) apply (erule insertE) @@ -387,7 +382,7 @@ "\{a} = a" by (auto intro: antisym Inf_lower Inf_greatest) -lemma Sup_singleton [simp, code func]: +lemma Sup_singleton [simp]: "\{a} = a" by (auto intro: antisym Sup_upper Sup_least) @@ -491,23 +486,8 @@ instance bool :: complete_lattice Inf_bool_def: "Inf A \ \x\A. x" - apply intro_classes - apply (unfold Inf_bool_def) - apply (iprover intro!: le_boolI elim: ballE) - apply (iprover intro!: ballI le_boolI elim: ballE le_boolE) - done - -theorem Sup_bool_eq: "Sup A \ (\x\A. x)" - apply (rule order_antisym) - apply (rule Sup_least) - apply (rule le_boolI) - apply (erule bexI, assumption) - apply (rule le_boolI) - apply (erule bexE) - apply (rule le_boolE) - apply (rule Sup_upper) - apply assumption+ - done + Sup_bool_def: "Sup A \ \x\A. x" + by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) lemma Inf_empty_bool [simp]: "Inf {}" @@ -515,7 +495,7 @@ lemma not_Sup_empty_bool [simp]: "\ Sup {}" - unfolding Sup_def Inf_bool_def by auto + unfolding Sup_bool_def by auto lemma top_bool_eq: "top = True" by (iprover intro!: order_antisym le_boolI top_greatest) @@ -541,17 +521,10 @@ instance set :: (type) complete_lattice Inf_set_def: "Inf S \ \S" - by intro_classes (auto simp add: Inf_set_def) - -lemmas [code func del] = Inf_set_def + Sup_set_def: "Sup S \ \S" + by intro_classes (auto simp add: Inf_set_def Sup_set_def) -theorem Sup_set_eq: "Sup S = \S" - apply (rule subset_antisym) - apply (rule Sup_least) - apply (erule Union_upper) - apply (rule Union_least) - apply (erule Sup_upper) - done +lemmas [code func del] = Inf_set_def Sup_set_def lemma top_set_eq: "top = UNIV" by (iprover intro!: subset_antisym subset_UNIV top_greatest) @@ -581,36 +554,12 @@ instance "fun" :: (type, complete_lattice) complete_lattice Inf_fun_def: "Inf A \ (\x. Inf {y. \f\A. y = f x})" - apply intro_classes - apply (unfold Inf_fun_def) - apply (rule le_funI) - apply (rule Inf_lower) - apply (rule CollectI) - apply (rule bexI) - apply (rule refl) - apply assumption - apply (rule le_funI) - apply (rule Inf_greatest) - apply (erule CollectE) - apply (erule bexE) - apply (iprover elim: le_funE) - done + Sup_fun_def: "Sup A \ (\x. Sup {y. \f\A. y = f x})" + by intro_classes + (auto simp add: Inf_fun_def Sup_fun_def le_fun_def + intro: Inf_lower Sup_upper Inf_greatest Sup_least) -lemmas [code func del] = Inf_fun_def - -theorem Sup_fun_eq: "Sup A = (\x. Sup {y. \f\A. y = f x})" - apply (rule order_antisym) - apply (rule Sup_least) - apply (rule le_funI) - apply (rule Sup_upper) - apply fast - apply (rule le_funI) - apply (rule Sup_least) - apply (erule CollectE) - apply (erule bexE) - apply (drule le_funD [OF Sup_upper]) - apply simp - done +lemmas [code func del] = Inf_fun_def Sup_fun_def lemma Inf_empty_fun: "Inf {} = (\_. Inf {})" @@ -618,11 +567,7 @@ lemma Sup_empty_fun: "Sup {} = (\_. Sup {})" -proof - - have aux: "\x. {y. \f. y = f x} = UNIV" by auto - show ?thesis - by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux) -qed + by rule (auto simp add: Sup_fun_def) lemma top_fun_eq: "top = (\x. top)" by (iprover intro!: order_antisym le_funI top_greatest)