--- a/src/HOL/FixedPoint.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/FixedPoint.thy Sun Nov 12 19:22:10 2006 +0100
@@ -12,42 +12,107 @@
begin
subsection {* Complete lattices *}
-
+(*FIXME Meet \<rightarrow> Inf *)
consts
Meet :: "'a::order set \<Rightarrow> 'a"
- Join :: "'a::order set \<Rightarrow> 'a"
+ Sup :: "'a::order set \<Rightarrow> 'a"
+
+defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
-defs Join_def: "Join A == Meet {b. \<forall>a \<in> A. a <= b}"
-
+definition
+ SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10)
+"SUP x. f x == Sup (f ` UNIV)"
+(*
+abbreviation
+ bot :: "'a::order"
+"bot == Sup {}"
+*)
axclass comp_lat < order
Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"
Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A"
-theorem Join_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Join A"
- by (auto simp: Join_def intro: Meet_greatest)
+theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
+ by (auto simp: Sup_def intro: Meet_greatest)
-theorem Join_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Join A <= z"
- by (auto simp: Join_def intro: Meet_lower)
+theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+ by (auto simp: Sup_def intro: Meet_lower)
text {* A complete lattice is a lattice *}
lemma is_meet_Meet: "is_meet (\<lambda>(x::'a::comp_lat) y. Meet {x, y})"
by (auto simp: is_meet_def intro: Meet_lower Meet_greatest)
-lemma is_join_Join: "is_join (\<lambda>(x::'a::comp_lat) y. Join {x, y})"
- by (auto simp: is_join_def intro: Join_upper Join_least)
+lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
+ by (auto simp: is_join_def intro: Sup_upper Sup_least)
instance comp_lat < lorder
proof
from is_meet_Meet show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
- from is_join_Join show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
+ from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
qed
+subsubsection {* Properties *}
+
lemma mono_join: "mono f \<Longrightarrow> join (f A) (f B) <= f (join A B)"
- by (auto simp add: mono_def intro: join_imp_le join_left_le join_right_le)
+ by (auto simp add: mono_def)
lemma mono_meet: "mono f \<Longrightarrow> f (meet A B) <= meet (f A) (f B)"
- by (auto simp add: mono_def intro: meet_imp_le meet_left_le meet_right_le)
+ by (auto simp add: mono_def)
+
+lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = join a (Sup A)"
+apply(simp add:Sup_def)
+apply(rule order_antisym)
+ apply(rule Meet_lower)
+ apply(clarsimp)
+ apply(rule le_joinI2)
+ apply(rule Meet_greatest)
+ apply blast
+apply simp
+apply rule
+ apply(rule Meet_greatest)apply blast
+apply(rule Meet_greatest)
+apply(rule Meet_lower)
+apply blast
+done
+
+lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
+apply(simp add: Sup_def)
+apply(rule Meet_lower)
+apply blast
+done
+(*
+lemma Meet_singleton[simp]: "Meet{a} = (a::'a::comp_lat)"
+apply(rule order_antisym)
+ apply(simp add: Meet_lower)
+apply(rule Meet_greatest)
+apply(simp)
+done
+*)
+lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
+apply(simp add:Sup_def)
+apply(rule Meet_greatest)
+apply(simp)
+done
+
+lemma le_SUPI: "(l::'a::comp_lat) = M i \<Longrightarrow> l \<le> (SUP i. M i)"
+apply(simp add:SUP_def)
+apply(blast intro:le_SupI)
+done
+
+lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
+apply(simp add:Sup_def)
+apply(rule Meet_lower)
+apply(blast)
+done
+
+
+lemma SUP_leI: "(!!i. M i \<le> u) \<Longrightarrow> (SUP i. M i) \<le> (u::'a::comp_lat)"
+apply(simp add:SUP_def)
+apply(blast intro!:Sup_leI)
+done
+
+lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
+by(simp add:SUP_def join_absorp1)
subsection {* Some instances of the type class of complete lattices *}
@@ -97,7 +162,7 @@
apply (rule le_boolE)
apply (rule meet_right_le)
apply assumption+
- apply (rule meet_imp_le)
+ apply (rule le_meetI)
apply (rule le_boolI)
apply (erule conjunct1)
apply (rule le_boolI)
@@ -106,7 +171,7 @@
theorem join_bool_eq: "join P Q = (P \<or> Q)"
apply (rule order_antisym)
- apply (rule join_imp_le)
+ apply (rule join_leI)
apply (rule le_boolI)
apply (erule disjI1)
apply (rule le_boolI)
@@ -121,15 +186,15 @@
apply assumption+
done
-theorem Join_bool_eq: "Join A = (EX x:A. x)"
+theorem Sup_bool_eq: "Sup A = (EX x:A. x)"
apply (rule order_antisym)
- apply (rule Join_least)
+ 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 Join_upper)
+ apply (rule Sup_upper)
apply assumption+
done
@@ -221,10 +286,10 @@
theorem meet_fun_eq: "meet f g = (\<lambda>x. meet (f x) (g x))"
apply (rule order_antisym)
apply (rule le_funI)
- apply (rule meet_imp_le)
+ apply (rule le_meetI)
apply (rule le_funD [OF meet_left_le])
apply (rule le_funD [OF meet_right_le])
- apply (rule meet_imp_le)
+ apply (rule le_meetI)
apply (rule le_funI)
apply (rule meet_left_le)
apply (rule le_funI)
@@ -233,28 +298,28 @@
theorem join_fun_eq: "join f g = (\<lambda>x. join (f x) (g x))"
apply (rule order_antisym)
- apply (rule join_imp_le)
+ apply (rule join_leI)
apply (rule le_funI)
apply (rule join_left_le)
apply (rule le_funI)
apply (rule join_right_le)
apply (rule le_funI)
- apply (rule join_imp_le)
+ apply (rule join_leI)
apply (rule le_funD [OF join_left_le])
apply (rule le_funD [OF join_right_le])
done
-theorem Join_fun_eq: "Join A = (\<lambda>x. Join {y::'a::comp_lat. EX f:A. y = f x})"
+theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
apply (rule order_antisym)
- apply (rule Join_least)
+ apply (rule Sup_least)
apply (rule le_funI)
- apply (rule Join_upper)
+ apply (rule Sup_upper)
apply fast
apply (rule le_funI)
- apply (rule Join_least)
+ apply (rule Sup_least)
apply (erule CollectE)
apply (erule bexE)
- apply (drule le_funD [OF Join_upper])
+ apply (drule le_funD [OF Sup_upper])
apply simp
done
@@ -270,14 +335,14 @@
apply (rule Int_greatest)
apply (rule meet_left_le)
apply (rule meet_right_le)
- apply (rule meet_imp_le)
+ apply (rule le_meetI)
apply (rule Int_lower1)
apply (rule Int_lower2)
done
theorem join_set_eq: "join A B = A \<union> B"
apply (rule subset_antisym)
- apply (rule join_imp_le)
+ apply (rule join_leI)
apply (rule Un_upper1)
apply (rule Un_upper2)
apply (rule Un_least)
@@ -285,12 +350,12 @@
apply (rule join_right_le)
done
-theorem Join_set_eq: "Join S = \<Union>S"
+theorem Sup_set_eq: "Sup S = \<Union>S"
apply (rule subset_antisym)
- apply (rule Join_least)
+ apply (rule Sup_least)
apply (erule Union_upper)
apply (rule Union_least)
- apply (erule Join_upper)
+ apply (erule Sup_upper)
done
@@ -301,7 +366,7 @@
"lfp f == Meet {u. f u <= u}" --{*least fixed point*}
gfp :: "(('a::comp_lat) => 'a) => 'a"
- "gfp f == Join {u. u <= f u}" --{*greatest fixed point*}
+ "gfp f == Sup {u. u <= f u}" --{*greatest fixed point*}
subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
@@ -335,7 +400,7 @@
with mono have "f (meet (lfp f) P) <= f (lfp f)" ..
also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
finally have "f (meet (lfp f) P) <= lfp f" .
- from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule meet_imp_le)
+ from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule le_meetI)
hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound)
also have "meet (lfp f) P <= P" by (rule meet_right_le)
finally show ?thesis .
@@ -400,10 +465,10 @@
the set @{term "{u. u \<le> f(u)}"} *}
lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
- by (auto simp add: gfp_def intro: Join_upper)
+ by (auto simp add: gfp_def intro: Sup_upper)
lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
- by (auto simp add: gfp_def intro: Join_least)
+ by (auto simp add: gfp_def intro: Sup_least)
lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
@@ -429,7 +494,7 @@
"[| X \<le> f (join X (gfp f)); mono f |] ==> join X (gfp f) \<le> f (join X (gfp f))"
apply (frule gfp_lemma2)
apply (drule mono_join)
- apply (rule join_imp_le)
+ apply (rule join_leI)
apply assumption
apply (rule order_trans)
apply (rule order_trans)
@@ -510,6 +575,7 @@
by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
+
ML
{*
val lfp_def = thm "lfp_def";
--- a/src/HOL/FunDef.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/FunDef.thy Sun Nov 12 19:22:10 2006 +0100
@@ -19,7 +19,7 @@
("Tools/function_package/mutual.ML")
("Tools/function_package/pattern_split.ML")
("Tools/function_package/fundef_package.ML")
-("Tools/function_package/fundef_datatype.ML")
+(*("Tools/function_package/fundef_datatype.ML")*)
("Tools/function_package/auto_term.ML")
begin
--- a/src/HOL/LOrder.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/LOrder.thy Sun Nov 12 19:22:10 2006 +0100
@@ -3,18 +3,14 @@
Author: Steven Obua, TU Muenchen
*)
-header {* Lattice Orders *}
+header "Lattice Orders"
theory LOrder
imports Lattices
begin
-text {*
- The theory of lattices developed here is taken from the book:
- \begin{itemize}
- \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.
- \end{itemize}
-*}
+text {* The theory of lattices developed here is taken from
+\cite{Birkhoff79}. *}
constdefs
is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
@@ -100,7 +96,9 @@
lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
by (insert is_meet_meet, auto simp add: is_meet_def)
-lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
+(* 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)"
@@ -109,10 +107,30 @@
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_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
+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)
-lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
+lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
+
+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
+
+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
+
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
by (auto simp add: is_meet_def min_def)
@@ -139,42 +157,52 @@
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: meet_left_le meet_imp_le)
+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_left_le join_imp_le)
+by (rule order_antisym, simp_all add: join_leI)
lemma meet_comm: "meet x y = meet y x"
-by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
+by (rule order_antisym, (simp add: le_meetI)+)
lemma join_comm: "join x y = join y x"
-by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
+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 meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
-proof -
- have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
- hence "?l <= x & ?l <= y & ?l <= z" by auto
- hence "?l <= ?r" by (simp add: meet_imp_le)
- hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
- have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)
- hence "?r <= x & ?r <= y & ?r <= z" by (auto)
- hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
- hence b:"?r <= ?l" by (simp add: meet_imp_le)
- from a b show "?l = ?r" by auto
-qed
+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 join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
-proof -
- have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
- hence "x <= ?l & y <= ?l & z <= ?l" by auto
- hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
- hence a:"?r <= ?l" by (simp add: join_imp_le)
- have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
- hence "y <= ?r & z <= ?r & x <= ?r" by auto
- hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
- hence b:"?l <= ?r" by (simp add: join_imp_le)
- from a b show "?l = ?r" by auto
-qed
+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)
@@ -192,97 +220,69 @@
lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
-lemma le_def_meet: "(x <= y) = (meet x y = x)"
-proof -
- have u: "x <= y \<longrightarrow> meet x y = x"
- proof
- assume "x <= y"
- hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
- thus "meet x y = x" by auto
- qed
- have v:"meet x y = x \<longrightarrow> x <= y"
- proof
- have a:"meet x y <= y" by (simp add: meet_right_le)
- assume "meet x y = x"
- hence "x = meet x y" by auto
- with a show "x <= y" by (auto)
- qed
- from u v show ?thesis by blast
-qed
+lemma le_def_meet: "(x <= y) = (meet x y = x)"
+apply rule
+apply(simp add: order_antisym)
+apply(subgoal_tac "meet x y <= y")
+apply(simp)
+apply(simp (no_asm))
+done
-lemma le_def_join: "(x <= y) = (join x y = y)"
-proof -
- have u: "x <= y \<longrightarrow> join x y = y"
- proof
- assume "x <= y"
- hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
- thus "join x y = y" by auto
- qed
- have v:"join x y = y \<longrightarrow> x <= y"
- proof
- have a:"x <= join x y" by (simp add: join_left_le)
- assume "join x y = y"
- hence "y = join x y" by auto
- with a show "x <= y" by (auto)
- qed
- from u v show ?thesis by blast
-qed
+lemma le_def_join: "(x <= y) = (join x y = y)"
+apply rule
+apply(simp add: order_antisym)
+apply(subgoal_tac "x <= join x y")
+apply(simp)
+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)
+
+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)
lemma meet_join_absorp: "meet x (join x y) = x"
-proof -
- have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
- have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
- from a b show ?thesis by auto
-qed
+by(simp add:meet_absorp1)
lemma join_meet_absorp: "join x (meet x y) = x"
-proof -
- have a:"x <= join x (meet x y)" by (simp add: join_left_le)
- have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
- from a b show ?thesis by auto
-qed
+by(simp add:join_absorp1)
lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
-proof -
- assume a: "y <= z"
- have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
- with a have "meet x y <= x & meet x y <= z" by auto
- thus "meet x y <= meet x z" by (simp add: meet_imp_le)
-qed
+by(simp add:meet_leI2)
lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
-proof -
- assume a: "y \<le> z"
- have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
- with a have "x <= join x z & y <= join x z" by auto
- thus "join x y <= join x z" by (simp add: join_imp_le)
-qed
+by(simp add:le_joinI2)
lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
proof -
- have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
- from meet_join_le have b: "meet y z <= ?r"
- by (rule_tac meet_imp_le, (blast intro: order_trans)+)
- from a b show ?thesis by (simp add: join_imp_le)
+ have a: "x <= ?r" by (simp_all add:le_meetI)
+ have b: "meet y z <= ?r" by (simp add:le_joinI2)
+ from a b show ?thesis by (simp add: join_leI)
qed
-lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
+lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
proof -
- have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
- from meet_join_le have b: "?l <= join y z"
- by (rule_tac join_imp_le, (blast intro: order_trans)+)
- from a b show ?thesis by (simp add: meet_imp_le)
+ have a: "?l <= x" by (simp_all add: join_leI)
+ have b: "?l <= join y z" by (simp add:meet_leI2)
+ from a b show ?thesis by (simp add: le_meetI)
qed
lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
-by (insert meet_join_le, blast intro: order_trans)
+by (auto simp:meet_leI2 meet_leI1)
lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
proof -
assume a: "x <= z"
- have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
- have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
- from b c show ?thesis by (simp add: meet_imp_le)
+ have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
+ have c: "?t <= z" by (simp_all add: a join_leI)
+ from b c show ?thesis by (simp add: le_meetI)
qed
end
--- a/src/HOL/Lattices.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Lattices.thy Sun Nov 12 19:22:10 2006 +0100
@@ -18,12 +18,12 @@
locale lower_semilattice = partial_order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
- assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
+ 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"
locale upper_semilattice = partial_order +
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
- assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
+ 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"
locale lattice = lower_semilattice + upper_semilattice
--- a/src/HOL/Library/Continuity.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Library/Continuity.thy Sun Nov 12 19:22:10 2006 +0100
@@ -9,6 +9,85 @@
imports Main
begin
+subsection{*Continuity for complete lattices*}
+
+constdefs
+ chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
+"chain M == !i. M i \<le> M(Suc i)"
+ continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
+"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
+
+abbreviation
+ bot :: "'a::order"
+"bot == Sup {}"
+
+lemma SUP_nat_conv:
+ "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
+apply(rule order_antisym)
+ apply(rule SUP_leI)
+ apply(case_tac n)
+ apply simp
+ apply (blast intro:le_SUPI le_joinI2)
+apply(simp)
+apply (blast intro:SUP_leI le_SUPI)
+done
+
+lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
+ assumes "continuous F" shows "mono F"
+proof
+ fix A B :: "'a" assume "A <= B"
+ let ?C = "%i::nat. if i=0 then A else B"
+ have "chain ?C" using `A <= B` by(simp add:chain_def)
+ have "F B = join (F A) (F B)"
+ proof -
+ have "join A B = B" using `A <= B` by (simp add:join_absorp2)
+ hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
+ also have "\<dots> = (SUP i. F(?C i))"
+ using `chain ?C` `continuous F` by(simp add:continuous_def)
+ also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
+ finally show ?thesis .
+ qed
+ thus "F A \<le> F B" by(subst le_def_join, simp)
+qed
+
+lemma continuous_lfp:
+ assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
+proof -
+ note mono = continuous_mono[OF `continuous F`]
+ { fix i have "(F^i) bot \<le> lfp F"
+ proof (induct i)
+ show "(F^0) bot \<le> lfp F" by simp
+ next
+ case (Suc i)
+ have "(F^(Suc i)) bot = F((F^i) bot)" by simp
+ also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
+ also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
+ finally show ?case .
+ qed }
+ hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+ moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
+ proof (rule lfp_lowerbound)
+ have "chain(%i. (F^i) bot)"
+ proof -
+ { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
+ proof (induct i)
+ case 0 show ?case by simp
+ next
+ case Suc thus ?case using monoD[OF mono Suc] by auto
+ qed }
+ thus ?thesis by(auto simp add:chain_def)
+ qed
+ hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
+ also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
+ finally show "F ?U \<le> ?U" .
+ qed
+ ultimately show ?thesis by (blast intro:order_antisym)
+qed
+
+text{* The following development is just for sets but presents an up
+and a down version of chains and continuity and covers @{const gfp}. *}
+
+
subsection "Chains"
definition
--- a/src/HOL/Matrix/Matrix.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Matrix/Matrix.thy Sun Nov 12 19:22:10 2006 +0100
@@ -20,10 +20,10 @@
times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
- by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
+ by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
- by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
+ by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
instance matrix :: (lordered_ab_group) lordered_ab_group_meet
proof
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Nov 12 19:22:10 2006 +0100
@@ -965,7 +965,6 @@
apply (simp only:)
apply (rule check_type_mono) apply assumption
apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append max_ac)
-apply arith
apply (simp add: nth_append)
apply (erule conjE)+
--- a/src/HOL/OrderedGroup.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/OrderedGroup.thy Sun Nov 12 19:22:10 2006 +0100
@@ -573,37 +573,37 @@
lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
apply (rule order_antisym)
-apply (rule meet_imp_le, simp_all add: meet_join_le)
+apply (simp_all add: le_meetI)
apply (rule add_le_imp_le_left [of "-a"])
apply (simp only: add_assoc[symmetric], simp)
-apply (rule meet_imp_le)
-apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
+apply rule
+apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
done
lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
apply (rule order_antisym)
apply (rule add_le_imp_le_left [of "-a"])
apply (simp only: add_assoc[symmetric], simp)
-apply (rule join_imp_le)
-apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
-apply (rule join_imp_le)
-apply (simp_all add: meet_join_le)
+apply rule
+apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
+apply (rule join_leI)
+apply (simp_all)
done
lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
apply (auto simp add: is_join_def)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
+apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
+apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
apply (subst neg_le_iff_le[symmetric])
-apply (simp add: meet_imp_le)
+apply (simp add: le_meetI)
done
lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
apply (auto simp add: is_meet_def)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
+apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
+apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
apply (subst neg_le_iff_le[symmetric])
-apply (simp add: join_imp_le)
+apply (simp add: join_leI)
done
axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
@@ -664,10 +664,10 @@
by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
lemma zero_le_pprt[simp]: "0 \<le> pprt a"
-by (simp add: pprt_def meet_join_le)
+by (simp add: pprt_def)
lemma nprt_le_zero[simp]: "nprt a \<le> 0"
-by (simp add: nprt_def meet_join_le)
+by (simp add: nprt_def)
lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")
proof -
@@ -794,7 +794,7 @@
lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
proof -
- have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
+ have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice)
show ?thesis by (rule add_mono[OF a b, simplified])
qed
@@ -818,27 +818,15 @@
qed
lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice meet_join_le)
+by (simp add: abs_lattice)
lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice meet_join_le)
-
-lemma le_imp_join_eq: "a \<le> b \<Longrightarrow> join a b = b"
-by (simp add: le_def_join)
-
-lemma ge_imp_join_eq: "b \<le> a \<Longrightarrow> join a b = a"
-by (simp add: le_def_join join_aci)
-
-lemma le_imp_meet_eq: "a \<le> b \<Longrightarrow> meet a b = a"
-by (simp add: le_def_meet)
-
-lemma ge_imp_meet_eq: "b \<le> a \<Longrightarrow> meet a b = b"
-by (simp add: le_def_meet meet_aci)
+by (simp add: abs_lattice)
lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
apply (simp add: pprt_def nprt_def diff_minus)
apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
-apply (subst le_imp_join_eq, auto)
+apply (subst join_absorp2, auto)
done
lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
@@ -846,7 +834,7 @@
lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
apply (simp add: abs_lattice[of "abs a"])
-apply (subst ge_imp_join_eq)
+apply (subst join_absorp1)
apply (rule order_trans[of _ 0])
by auto
@@ -900,7 +888,7 @@
by (rule abs_of_nonpos, rule order_less_imp_le)
lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice join_imp_le)
+by (simp add: abs_lattice join_leI)
lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
proof -
@@ -929,10 +917,10 @@
proof -
have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
- have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
- have b:"-a-b <= ?n" by (simp add: meet_join_le)
- have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
- from b c have d: "-a-b <= join ?m ?n" by simp
+ have a:"a+b <= join ?m ?n" by (simp)
+ have b:"-a-b <= ?n" by (simp)
+ have c:"?n <= join ?m ?n" by (simp)
+ from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
have e:"-a-b = -(a+b)" by (simp add: diff_minus)
from a d e have "abs(a+b) <= join ?m ?n"
by (drule_tac abs_leI, auto)
@@ -1174,10 +1162,10 @@
val abs_not_less_zero = thm "abs_not_less_zero";
val abs_ge_self = thm "abs_ge_self";
val abs_ge_minus_self = thm "abs_ge_minus_self";
-val le_imp_join_eq = thm "le_imp_join_eq";
-val ge_imp_join_eq = thm "ge_imp_join_eq";
-val le_imp_meet_eq = thm "le_imp_meet_eq";
-val ge_imp_meet_eq = thm "ge_imp_meet_eq";
+val le_imp_join_eq = thm "join_absorp2";
+val ge_imp_join_eq = thm "join_absorp1";
+val le_imp_meet_eq = thm "meet_absorp1";
+val ge_imp_meet_eq = thm "meet_absorp2";
val abs_prts = thm "abs_prts";
val abs_minus_cancel = thm "abs_minus_cancel";
val abs_idempotent = thm "abs_idempotent";
--- a/src/HOL/Set.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Set.thy Sun Nov 12 19:22:10 2006 +0100
@@ -1231,6 +1231,9 @@
lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
by auto
+lemma image_constant_conv[simp]: "(%x. c) ` A = (if A = {} then {} else {c})"
+by auto
+
lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
by blast
--- a/src/HOL/UNITY/Transformers.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/UNITY/Transformers.thy Sun Nov 12 19:22:10 2006 +0100
@@ -88,7 +88,7 @@
done
lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
text{*These two theorems justify the claim that @{term wens} returns the
weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Join_set_eq, blast)
+ ensures_def transient_def Sup_set_eq, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def Sup_set_eq, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -119,8 +119,8 @@
done
text{*Assertion 4.17 in the thesis*}
-lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
+lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
--{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via @{text meson} after expanding all definitions, but it's
@@ -332,7 +332,7 @@
lemma wens_single_eq:
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOL/document/root.bib Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/document/root.bib Sun Nov 12 19:22:10 2006 +0100
@@ -4,3 +4,6 @@
publisher = {Cambridge University Press},
year = 1992
}
+
+@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
+publisher={American Mathematical Society},year=1979}
\ No newline at end of file
--- a/src/HOL/ex/CTL.thy Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/ex/CTL.thy Sun Nov 12 19:22:10 2006 +0100
@@ -91,7 +91,7 @@
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
- by (auto simp add: gfp_def Join_set_eq)
+ by (auto simp add: gfp_def Sup_set_eq)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto