--- 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 \<times> 'b) set"
+ foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> '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]:
"\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>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]:
"\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>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 \<squnion> b |b. b \<in> B}"
- by(fast intro: finite_surj[where f = "%b. x \<squnion> b", OF B(1)])
+ by(rule finite_surj[where f = "%b. x \<squnion> b", OF B(1)], auto)
have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
@@ -2330,7 +2330,7 @@
next
case (insert x A)
have finB: "finite {x \<sqinter> b |b. b \<in> B}"
- by(fast intro: finite_surj[where f = "%b. x \<sqinter> b", OF B(1)])
+ by(rule finite_surj[where f = "%b. x \<sqinter> b", OF B(1)], auto)
have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
--- 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: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
by fast
from LIMSEQ_D [OF S sgz]
- obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by fast
+ obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
qed
--- 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 \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
+interpretation meet_semilat:
+ lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet]
proof unfold_locales
- fix x y z :: "'a\<Colon>lorder"
+ fix x y z :: "'a\<Colon>meet_semilorder"
from is_meet_meet have "is_meet meet" by blast
note meet = this is_meet_def
from meet show "meet x y \<le> x" by blast
from meet show "meet x y \<le> y" by blast
from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
+qed
+
+interpretation join_semilat:
+ upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" join]
+proof unfold_locales
+ fix x y z :: "'a\<Colon>join_semilorder"
from is_join_join have "is_join join" by blast
note join = this is_join_def
from join show "x \<le> join x y" by blast
from join show "y \<le> join x y" by blast
- from join show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> join y z \<le> x" by blast
+ from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> join x y \<le> z" by blast
qed
-lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
-by (insert is_meet_meet, auto simp add: is_meet_def)
-
-lemma meet_right_le: "meet a b \<le> (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 \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
-by (insert is_meet_meet, auto simp add: is_meet_def)
-
-lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
-by (insert is_join_join, auto simp add: is_join_def)
-
-lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
-by (insert is_join_join, auto simp add: is_join_def)
-
-lemma join_leI:
- "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
-by (insert is_join_join, auto simp add: is_join_def)
+interpretation meet_join_lat:
+ lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> 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 \<le> 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 \<le> join x y" "y \<le> 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 \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
by (auto simp add: is_meet_def min_def)
@@ -172,68 +158,22 @@
lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('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 \<le> z \<Longrightarrow> meet x y \<le> z"
-apply(subgoal_tac "meet x y <= x")
- apply(blast intro:order_trans)
-apply simp
-done
-
-lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
-apply(subgoal_tac "meet x y <= y")
- apply(blast intro:order_trans)
-apply simp
-done
-
-lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
-apply(subgoal_tac "y <= join y z")
- apply(blast intro:order_trans)
-apply simp
-done
-
-lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> 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 \<le> b \<Longrightarrow> join a b = b"
-by (simp add: le_def_join)
-
-lemma join_absorp1: "b \<le> a \<Longrightarrow> 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 \<le> b \<Longrightarrow> meet a b = a"
-by (simp add: le_def_meet)
-
-lemma meet_absorp2: "b \<le> a \<Longrightarrow> 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)
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
- and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+ and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
locale upper_semilattice = partial_order +
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
- and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
+ and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
locale lattice = lower_semilattice + upper_semilattice
-lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> 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 \<squnion> y) = (y \<squnion> x)"
-by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
+lemmas antisym_intro[intro!] = antisym
-lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl)
+lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
+ apply(blast intro:trans)
+apply simp
+done
-lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl)
+lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
+ apply(blast intro:trans)
+apply simp
+done
+
+lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+by(blast intro: inf_greatest)
-lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x"
-by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
+lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+by(blast intro: trans)
-lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
-by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
+lemma less_eq_inf_conv [simp]:
+ "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> 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 \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-by (simp add: inf_assoc[symmetric])
+end
+
+
+context upper_semilattice
+begin
-lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-by (simp add: sup_assoc[symmetric])
+lemmas antisym_intro[intro!] = antisym
-lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
-by(blast intro: antisym inf_le1 inf_least sup_ge1)
+lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
+ apply(blast intro:trans)
+apply simp
+done
-lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
-by(blast intro: antisym sup_ge1 sup_greatest inf_le1)
+lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
+ apply(blast intro:trans)
+apply simp
+done
+
+lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+by(blast intro: sup_least)
-lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
-by(blast intro: antisym inf_le1 inf_least refl)
+lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+by(blast intro: trans)
-lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
-by(blast intro: antisym sup_ge2 sup_greatest refl)
+lemma above_sup_conv[simp]:
+ "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
+by blast
+
+end
+
+
+subsubsection{* Equational laws *}
-lemma (in lower_semilattice) less_eq_inf_conv [simp]:
- "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
-by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
+context lower_semilattice
+begin
+
+lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
+by blast
+
+lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+by blast
+
+lemma inf_idem[simp]: "x \<sqinter> x = x"
+by blast
+
+lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+by blast
+
+lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+by blast
+
+lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+by blast
+
+lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> 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 \<squnion> y) = (y \<squnion> x)"
+by blast
+
+lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+by blast
+
+lemma sup_idem[simp]: "x \<squnion> x = x"
+by blast
+
+lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+by blast
+
+lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+by blast
+
+lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+by blast
-lemma (in upper_semilattice) above_sup_conv[simp]:
- "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
+lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> 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 \<sqinter> (x \<squnion> y) = x"
+by(blast intro: antisym inf_le1 inf_greatest sup_ge1)
+
+lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> 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 \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
proof-
@@ -91,7 +178,7 @@
finally show ?thesis .
qed
-lemma (in lattice) distrib_imp2:
+lemma distrib_imp2:
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> 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 \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
-proof -
- have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
- also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
- also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
- finally(back_subst) show ?thesis .
-qed
-
-lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
-proof -
- have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
- also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
- also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
- finally(back_subst) show ?thesis .
-qed
-
-lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-proof -
- have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc)
- also have "\<dots> = x \<sqinter> y" by(simp)
- finally show ?thesis .
-qed
-
-lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-proof -
- have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc)
- also have "\<dots> = x \<squnion> 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 \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
-lemma (in distrib_lattice) sup_inf_distrib2:
+context distrib_lattice
+begin
+
+lemma sup_inf_distrib2:
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
by(simp add:ACI sup_inf_distrib1)
-lemma (in distrib_lattice) inf_sup_distrib1:
+lemma inf_sup_distrib1:
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
by(rule distrib_imp2[OF sup_inf_distrib1])
-lemma (in distrib_lattice) inf_sup_distrib2:
+lemma inf_sup_distrib2:
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
by(simp add:ACI inf_sup_distrib1)
-lemmas (in distrib_lattice) distrib =
+lemmas distrib =
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
+end
+
subsection {* min/max on linear orders as special case of inf/sup *}
@@ -178,6 +231,17 @@
apply (simp add: max_def linorder_not_le order_less_imp_le)
unfolding min_def max_def by auto
+text{* Now we have inherited antisymmetry as an intro-rule on all
+linear orders. This is a problem because it applies to bool, which is
+undesirable. *}
+
+declare
+ min_max.antisym_intro[rule del]
+ min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
+ min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
+ min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
+ min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
+
lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
@@ -187,4 +251,29 @@
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
+text {* ML legacy bindings *}
+
+ML {*
+val Least_def = thm "Least_def";
+val Least_equality = thm "Least_equality";
+val min_def = thm "min_def";
+val min_of_mono = thm "min_of_mono";
+val max_def = thm "max_def";
+val max_of_mono = thm "max_of_mono";
+val min_leastL = thm "min_leastL";
+val max_leastL = thm "max_leastL";
+val min_leastR = thm "min_leastR";
+val max_leastR = thm "max_leastR";
+val le_max_iff_disj = thm "le_max_iff_disj";
+val le_maxI1 = thm "le_maxI1";
+val le_maxI2 = thm "le_maxI2";
+val less_max_iff_disj = thm "less_max_iff_disj";
+val max_less_iff_conj = thm "max_less_iff_conj";
+val min_less_iff_conj = thm "min_less_iff_conj";
+val min_le_iff_disj = thm "min_le_iff_disj";
+val min_less_iff_disj = thm "min_less_iff_disj";
+val split_min = thm "split_min";
+val split_max = thm "split_max";
+*}
+
end
--- a/src/HOL/UNITY/Transformers.thy Sat Dec 09 18:06:17 2006 +0100
+++ b/src/HOL/UNITY/Transformers.thy Sun Dec 10 07:12:26 2006 +0100
@@ -444,11 +444,11 @@
apply (rule subsetI)
apply (erule wens_set.induct)
txt{*Basis*}
- apply (force simp add: wens_single_finite_def)
+ apply (fastsimp simp add: wens_single_finite_def)
txt{*Wens inductive step*}
- apply (case_tac "acta = Id", simp)
+ apply (case_tac "acta = Id", simp)
apply (simp add: wens_single_eq)
- apply (elim disjE)
+ apply (elim disjE)
apply (simp add: wens_single_Un_eq)
apply (force simp add: wens_single_finite_Un_eq)
txt{*Union inductive step*}