# HG changeset patch # User nipkow # Date 1165731146 -3600 # Node ID 131dd2a271370ffc34dc7d0ee6c0c2ac5dfcc953 # Parent 4d4cde71450089864613f937a718e2dabc016c83 Modified lattice locale diff -r 4d4cde714500 -r 131dd2a27137 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Dec 09 18:06:17 2006 +0100 +++ b/src/HOL/Finite_Set.thy Sun Dec 10 07:12:26 2006 +0100 @@ -428,7 +428,7 @@ *} consts - foldSet :: "('a => 'b => 'b) => ('c => 'a) => 'b => ('c set \ 'b) set" + foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \ 'a) set" inductive "foldSet f g z" intros @@ -440,7 +440,7 @@ inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z" constdefs - fold :: "('a => 'b => 'b) => ('c => 'a) => 'b => 'c set => 'b" + fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" "fold f g z A == THE x. (A, x) : foldSet f g z" text{*A tempting alternative for the definiens is @@ -1211,7 +1211,7 @@ proof induct case empty thus ?case by simp next - case (insert x A) thus ?case by (auto intro: order_trans) + case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) qed next case False thus ?thesis by (simp add: setsum_def) @@ -2213,7 +2213,7 @@ apply(rule ACIf.axioms[OF ACIf_inf]) apply(rule ACIfSL_axioms.intro) apply(rule iffI) - apply(blast intro: antisym inf_le1 inf_le2 inf_least refl) + apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl) apply(erule subst) apply(rule inf_le2) done @@ -2226,7 +2226,7 @@ apply(rule ACIf.axioms[OF ACIf_sup]) apply(rule ACIfSL_axioms.intro) apply(rule iffI) - apply(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl) + apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl) apply(erule subst) apply(rule sup_ge2) done @@ -2247,12 +2247,12 @@ lemma (in Lattice) sup_Inf_absorb[simp]: "\ finite A; A \ {}; a \ A \ \ (a \ \A) = a" apply(subst sup_commute) -apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf]) +apply(simp add:Inf_def sup_absorb2 ACIfSL.fold1_belowI[OF ACIfSL_inf]) done lemma (in Lattice) inf_Sup_absorb[simp]: "\ finite A; A \ {}; a \ A \ \ (a \ \A) = a" -by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup]) +by(simp add:Sup_def inf_absorb1 ACIfSL.fold1_belowI[OF ACIfSL_sup]) lemma (in ACIf) hom_fold1_commute: @@ -2289,7 +2289,7 @@ next case (insert x A) have finB: "finite {x \ b |b. b \ B}" - by(fast intro: finite_surj[where f = "%b. x \ b", OF B(1)]) + by(rule finite_surj[where f = "%b. x \ b", OF B(1)], auto) have finAB: "finite {a \ b |a b. a \ A \ b \ B}" proof - have "{a \ b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {a \ b})" @@ -2330,7 +2330,7 @@ next case (insert x A) have finB: "finite {x \ b |b. b \ B}" - by(fast intro: finite_surj[where f = "%b. x \ b", OF B(1)]) + by(rule finite_surj[where f = "%b. x \ b", OF B(1)], auto) have finAB: "finite {a \ b |a b. a \ A \ b \ B}" proof - have "{a \ b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {a \ b})" diff -r 4d4cde714500 -r 131dd2a27137 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat Dec 09 18:06:17 2006 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Sun Dec 10 07:12:26 2006 +0100 @@ -966,7 +966,7 @@ and aux: "\x. \x \ a; norm (x - a) < s\ \ norm (X x - L) < r" by fast from LIMSEQ_D [OF S sgz] - obtain no where "\n\no. norm (S n - a) < s" by fast + obtain no where "\n\no. norm (S n - a) < s" by blast hence "\n\no. norm (X (S n) - L) < r" by (simp add: aux as) thus "\no. \n\no. norm (X (S n) - L) < r" .. qed diff -r 4d4cde714500 -r 131dd2a27137 src/HOL/LOrder.thy --- a/src/HOL/LOrder.thy Sat Dec 09 18:06:17 2006 +0100 +++ b/src/HOL/LOrder.thy Sun Dec 10 07:12:26 2006 +0100 @@ -90,63 +90,49 @@ lemma join_unique: "(is_join j) = (j = join)" by (insert is_join_join, auto simp add: is_join_unique) -interpretation lattice: - lattice ["op \ \ 'a\lorder \ 'a \ bool" "op <" meet join] +interpretation meet_semilat: + lower_semilattice ["op \ \ 'a\meet_semilorder \ 'a \ bool" "op <" meet] proof unfold_locales - fix x y z :: "'a\lorder" + fix x y z :: "'a\meet_semilorder" from is_meet_meet have "is_meet meet" by blast note meet = this is_meet_def from meet show "meet x y \ x" by blast from meet show "meet x y \ y" by blast from meet show "x \ y \ x \ z \ x \ meet y z" by blast +qed + +interpretation join_semilat: + upper_semilattice ["op \ \ 'a\join_semilorder \ 'a \ bool" "op <" join] +proof unfold_locales + fix x y z :: "'a\join_semilorder" from is_join_join have "is_join join" by blast note join = this is_join_def from join show "x \ join x y" by blast from join show "y \ join x y" by blast - from join show "y \ x \ z \ x \ join y z \ x" by blast + from join show "x \ z \ y \ z \ join x y \ z" by blast qed -lemma meet_left_le: "meet a b \ (a::'a::meet_semilorder)" -by (insert is_meet_meet, auto simp add: is_meet_def) - -lemma meet_right_le: "meet a b \ (b::'a::meet_semilorder)" -by (insert is_meet_meet, auto simp add: is_meet_def) +declare + join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del] + join_semilat.less_eq_supE[rule del] meet_semilat.less_eq_infE[rule del] -(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *) -lemma le_meetI: - "x \ a \ x \ b \ x \ meet a (b::'a::meet_semilorder)" -by (insert is_meet_meet, auto simp add: is_meet_def) - -lemma join_left_le: "a \ join a (b::'a::join_semilorder)" -by (insert is_join_join, auto simp add: is_join_def) - -lemma join_right_le: "b \ join a (b::'a::join_semilorder)" -by (insert is_join_join, auto simp add: is_join_def) - -lemma join_leI: - "a \ x \ b \ x \ join a b \ (x::'a::join_semilorder)" -by (insert is_join_join, auto simp add: is_join_def) +interpretation meet_join_lat: + lattice ["op \ \ 'a\lorder \ 'a \ bool" "op <" meet join] +by unfold_locales -lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le +lemmas meet_left_le = meet_semilat.inf_le1 +lemmas meet_right_le = meet_semilat.inf_le2 +lemmas le_meetI[rule del] = meet_semilat.less_eq_infI +(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *) +lemmas join_left_le = join_semilat.sup_ge1 +lemmas join_right_le = join_semilat.sup_ge2 +lemmas join_leI[rule del] = join_semilat.less_eq_supI -lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R") -proof - assume ?L - moreover have "meet y z \ y" "meet y z <= z" by(simp_all) - ultimately show ?R by(blast intro:order_trans) -next - assume ?R thus ?L by (blast intro!:le_meetI) -qed +lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le -lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R") -proof - assume ?L - moreover have "x \ join x y" "y \ join x y" by(simp_all) - ultimately show ?R by(blast intro:order_trans) -next - assume ?R thus ?L by (blast intro:join_leI) -qed +lemmas le_meet = meet_semilat.less_eq_inf_conv +lemmas le_join = join_semilat.above_sup_conv lemma is_meet_min: "is_meet (min::'a \ 'a \ ('a::linorder))" by (auto simp add: is_meet_def min_def) @@ -172,68 +158,22 @@ lemma join_max: "join = (max :: 'a\'a\('a::linorder))" by (simp add: is_join_join is_join_max is_join_unique) -lemma meet_idempotent[simp]: "meet x x = x" -by (rule order_antisym, simp_all add: le_meetI) - -lemma join_idempotent[simp]: "join x x = x" -by (rule order_antisym, simp_all add: join_leI) - -lemma meet_comm: "meet x y = meet y x" -by (rule order_antisym, (simp add: le_meetI)+) - -lemma join_comm: "join x y = join y x" -by (rule order_antisym, (simp add: join_leI)+) - -lemma meet_leI1: "x \ z \ meet x y \ z" -apply(subgoal_tac "meet x y <= x") - apply(blast intro:order_trans) -apply simp -done - -lemma meet_leI2: "y \ z \ meet x y \ z" -apply(subgoal_tac "meet x y <= y") - apply(blast intro:order_trans) -apply simp -done - -lemma le_joinI1: "x \ y \ x \ join y z" -apply(subgoal_tac "y <= join y z") - apply(blast intro:order_trans) -apply simp -done - -lemma le_joinI2: "x \ z \ x \ join y z" -apply(subgoal_tac "z <= join y z") - apply(blast intro:order_trans) -apply simp -done - -lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" -apply(rule order_antisym) -apply (simp add:meet_leI1 meet_leI2) -apply (simp add:meet_leI1 meet_leI2) -done - -lemma join_assoc: "join (join x y) z = join x (join y z)" -apply(rule order_antisym) -apply (simp add:le_joinI1 le_joinI2) -apply (simp add:le_joinI1 le_joinI2) -done - -lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)" -by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc) - -lemma meet_left_idempotent: "meet y (meet y x) = meet y x" -by (simp add: meet_assoc meet_comm meet_left_comm) - -lemma join_left_comm: "join a (join b c) = join b (join a c)" -by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc) - -lemma join_left_idempotent: "join y (join y x) = join y x" -by (simp add: join_assoc join_comm join_left_comm) +lemmas meet_idempotent = meet_semilat.inf_idem +lemmas join_idempotent = join_semilat.sup_idem +lemmas meet_comm = meet_semilat.inf_commute +lemmas join_comm = join_semilat.sup_commute +lemmas meet_leI1[rule del] = meet_semilat.less_eq_infI1 +lemmas meet_leI2[rule del] = meet_semilat.less_eq_infI2 +lemmas le_joinI1[rule del] = join_semilat.less_eq_supI1 +lemmas le_joinI2[rule del] = join_semilat.less_eq_supI2 +lemmas meet_assoc = meet_semilat.inf_assoc +lemmas join_assoc = join_semilat.sup_assoc +lemmas meet_left_comm = meet_semilat.inf_left_commute +lemmas meet_left_idempotent = meet_semilat.inf_left_idem +lemmas join_left_comm = join_semilat.sup_left_commute +lemmas join_left_idempotent= join_semilat.sup_left_idem lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent - lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent lemma le_def_meet: "(x <= y) = (meet x y = x)" @@ -252,17 +192,11 @@ apply(simp (no_asm)) done -lemma join_absorp2: "a \ b \ join a b = b" -by (simp add: le_def_join) - -lemma join_absorp1: "b \ a \ join a b = a" -by (simp add: le_def_join join_aci) +lemmas join_absorp2 = join_semilat.sup_absorb2 +lemmas join_absorp1 = join_semilat.sup_absorb1 -lemma meet_absorp1: "a \ b \ meet a b = a" -by (simp add: le_def_meet) - -lemma meet_absorp2: "b \ a \ meet a b = b" -by (simp add: le_def_meet meet_aci) +lemmas meet_absorp1 = meet_semilat.inf_absorb1 +lemmas meet_absorp2 = meet_semilat.inf_absorb2 lemma meet_join_absorp: "meet x (join x y) = x" by(simp add:meet_absorp1) diff -r 4d4cde714500 -r 131dd2a27137 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sat Dec 09 18:06:17 2006 +0100 +++ b/src/HOL/Lattices.thy Sun Dec 10 07:12:26 2006 +0100 @@ -3,7 +3,7 @@ Author: Tobias Nipkow *) -header {* Abstract lattices *} +header {* Lattices via Locales *} theory Lattices imports Orderings @@ -19,67 +19,154 @@ locale lower_semilattice = partial_order + fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) assumes inf_le1[simp]: "x \ y \ x" and inf_le2[simp]: "x \ y \ y" - and inf_least: "x \ y \ x \ z \ x \ y \ z" + and inf_greatest: "x \ y \ x \ z \ x \ y \ z" locale upper_semilattice = partial_order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) assumes sup_ge1[simp]: "x \ x \ y" and sup_ge2[simp]: "y \ x \ y" - and sup_greatest: "y \ x \ z \ x \ y \ z \ x" + and sup_least: "y \ x \ z \ x \ y \ z \ x" locale lattice = lower_semilattice + upper_semilattice -lemma (in lower_semilattice) inf_commute: "(x \ y) = (y \ x)" -by(blast intro: antisym inf_le1 inf_le2 inf_least) +subsubsection{* Intro and elim rules*} + +context lower_semilattice +begin -lemma (in upper_semilattice) sup_commute: "(x \ y) = (y \ x)" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest) +lemmas antisym_intro[intro!] = antisym -lemma (in lower_semilattice) inf_assoc: "(x \ y) \ z = x \ (y \ z)" -by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl) +lemma less_eq_infI1[intro]: "a \ x \ a \ b \ x" +apply(subgoal_tac "a \ b \ a") + apply(blast intro:trans) +apply simp +done -lemma (in upper_semilattice) sup_assoc: "(x \ y) \ z = x \ (y \ z)" -by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl) +lemma less_eq_infI2[intro]: "b \ x \ a \ b \ x" +apply(subgoal_tac "a \ b \ b") + apply(blast intro:trans) +apply simp +done + +lemma less_eq_infI[intro!]: "x \ a \ x \ b \ x \ a \ b" +by(blast intro: inf_greatest) -lemma (in lower_semilattice) inf_idem[simp]: "x \ x = x" -by(blast intro: antisym inf_le1 inf_le2 inf_least refl) +lemma less_eq_infE[elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" +by(blast intro: trans) -lemma (in upper_semilattice) sup_idem[simp]: "x \ x = x" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl) +lemma less_eq_inf_conv [simp]: + "x \ y \ z = (x \ y \ x \ z)" +by blast + +lemmas below_inf_conv = less_eq_inf_conv + -- {* a duplicate for backward compatibility *} -lemma (in lower_semilattice) inf_left_idem[simp]: "x \ (x \ y) = x \ y" -by (simp add: inf_assoc[symmetric]) +end + + +context upper_semilattice +begin -lemma (in upper_semilattice) sup_left_idem[simp]: "x \ (x \ y) = x \ y" -by (simp add: sup_assoc[symmetric]) +lemmas antisym_intro[intro!] = antisym -lemma (in lattice) inf_sup_absorb: "x \ (x \ y) = x" -by(blast intro: antisym inf_le1 inf_least sup_ge1) +lemma less_eq_supI1[intro]: "x \ a \ x \ a \ b" +apply(subgoal_tac "a \ a \ b") + apply(blast intro:trans) +apply simp +done -lemma (in lattice) sup_inf_absorb: "x \ (x \ y) = x" -by(blast intro: antisym sup_ge1 sup_greatest inf_le1) +lemma less_eq_supI2[intro]: "x \ b \ x \ a \ b" +apply(subgoal_tac "b \ a \ b") + apply(blast intro:trans) +apply simp +done + +lemma less_eq_supI[intro!]: "a \ x \ b \ x \ a \ b \ x" +by(blast intro: sup_least) -lemma (in lower_semilattice) inf_absorb: "x \ y \ x \ y = x" -by(blast intro: antisym inf_le1 inf_least refl) +lemma less_eq_supE[elim!]: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" +by(blast intro: trans) -lemma (in upper_semilattice) sup_absorb: "x \ y \ x \ y = y" -by(blast intro: antisym sup_ge2 sup_greatest refl) +lemma above_sup_conv[simp]: + "x \ y \ z = (x \ z \ y \ z)" +by blast + +end + + +subsubsection{* Equational laws *} -lemma (in lower_semilattice) less_eq_inf_conv [simp]: - "x \ y \ z = (x \ y \ x \ z)" -by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans) +context lower_semilattice +begin + +lemma inf_commute: "(x \ y) = (y \ x)" +by blast + +lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" +by blast + +lemma inf_idem[simp]: "x \ x = x" +by blast + +lemma inf_left_idem[simp]: "x \ (x \ y) = x \ y" +by blast + +lemma inf_absorb1: "x \ y \ x \ y = x" +by blast + +lemma inf_absorb2: "y \ x \ x \ y = y" +by blast + +lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)" +by blast + +lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem + +end + + +context upper_semilattice +begin -lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv - -- {* a duplicate for backward compatibility *} +lemma sup_commute: "(x \ y) = (y \ x)" +by blast + +lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" +by blast + +lemma sup_idem[simp]: "x \ x = x" +by blast + +lemma sup_left_idem[simp]: "x \ (x \ y) = x \ y" +by blast + +lemma sup_absorb1: "y \ x \ x \ y = x" +by blast + +lemma sup_absorb2: "x \ y \ x \ y = y" +by blast -lemma (in upper_semilattice) above_sup_conv[simp]: - "x \ y \ z = (x \ z \ y \ z)" -by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans) +lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)" +by blast + +lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem + +end +context lattice +begin + +lemma inf_sup_absorb: "x \ (x \ y) = x" +by(blast intro: antisym inf_le1 inf_greatest sup_ge1) + +lemma sup_inf_absorb: "x \ (x \ y) = x" +by(blast intro: antisym sup_ge1 sup_least inf_le1) + +lemmas (in lattice) ACI = inf_ACI sup_ACI text{* Towards distributivity: if you have one of them, you have them all. *} -lemma (in lattice) distrib_imp1: +lemma distrib_imp1: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- @@ -91,7 +178,7 @@ finally show ?thesis . qed -lemma (in lattice) distrib_imp2: +lemma distrib_imp2: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- @@ -103,46 +190,7 @@ finally show ?thesis . qed -text{* A package of rewrite rules for deciding equivalence wrt ACI: *} - -lemma (in lower_semilattice) inf_left_commute: "x \ (y \ z) = y \ (x \ z)" -proof - - have "x \ (y \ z) = (y \ z) \ x" by (simp only: inf_commute) - also have "... = y \ (z \ x)" by (simp only: inf_assoc) - also have "z \ x = x \ z" by (simp only: inf_commute) - finally(back_subst) show ?thesis . -qed - -lemma (in upper_semilattice) sup_left_commute: "x \ (y \ z) = y \ (x \ z)" -proof - - have "x \ (y \ z) = (y \ z) \ x" by (simp only: sup_commute) - also have "... = y \ (z \ x)" by (simp only: sup_assoc) - also have "z \ x = x \ z" by (simp only: sup_commute) - finally(back_subst) show ?thesis . -qed - -lemma (in lower_semilattice) inf_left_idem: "x \ (x \ y) = x \ y" -proof - - have "x \ (x \ y) = (x \ x) \ y" by(simp only:inf_assoc) - also have "\ = x \ y" by(simp) - finally show ?thesis . -qed - -lemma (in upper_semilattice) sup_left_idem: "x \ (x \ y) = x \ y" -proof - - have "x \ (x \ y) = (x \ x) \ y" by(simp only:sup_assoc) - also have "\ = x \ y" by(simp) - finally show ?thesis . -qed - - -lemmas (in lower_semilattice) inf_ACI = - inf_commute inf_assoc inf_left_commute inf_left_idem - -lemmas (in upper_semilattice) sup_ACI = - sup_commute sup_assoc sup_left_commute sup_left_idem - -lemmas (in lattice) ACI = inf_ACI sup_ACI +end subsection{* Distributive lattices *} @@ -150,21 +198,26 @@ locale distrib_lattice = lattice + assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" -lemma (in distrib_lattice) sup_inf_distrib2: +context distrib_lattice +begin + +lemma sup_inf_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by(simp add:ACI sup_inf_distrib1) -lemma (in distrib_lattice) inf_sup_distrib1: +lemma inf_sup_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" by(rule distrib_imp2[OF sup_inf_distrib1]) -lemma (in distrib_lattice) inf_sup_distrib2: +lemma inf_sup_distrib2: "(y \