--- a/src/HOL/FixedPoint.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/FixedPoint.thy Fri Mar 16 21:32:08 2007 +0100
@@ -5,37 +5,35 @@
Copyright 1992 University of Cambridge
*)
-header{* Fixed Points and the Knaster-Tarski Theorem*}
+header {* Fixed Points and the Knaster-Tarski Theorem*}
theory FixedPoint
-imports Product_Type LOrder
+imports Product_Type
begin
subsection {* Complete lattices *}
-consts
- Inf :: "'a::order set \<Rightarrow> 'a"
-
-definition
- Sup :: "'a::order set \<Rightarrow> 'a" where
- "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
-
-class comp_lat = order +
+class complete_lattice = lattice +
+ fixes Inf :: "'a set \<Rightarrow> 'a"
assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
-theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
+definition
+ Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
+ "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
+
+theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
by (auto simp: Sup_def intro: Inf_greatest)
-theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
by (auto simp: Sup_def intro: Inf_lower)
definition
- SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+ SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
"SUPR A f == Sup (f ` A)"
definition
- INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
+ INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
"INFI A f == Inf (f ` A)"
syntax
@@ -80,17 +78,6 @@
text {* A complete lattice is a lattice *}
-lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
- by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
-
-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_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
- from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
-qed
subsubsection {* Properties *}
@@ -100,7 +87,7 @@
lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
by (auto simp add: mono_def)
-lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
+lemma Sup_insert[simp]: "Sup (insert (a::'a::complete_lattice) A) = sup a (Sup A)"
apply (rule order_antisym)
apply (rule Sup_least)
apply (erule insertE)
@@ -116,7 +103,7 @@
apply simp
done
-lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
+lemma Inf_insert[simp]: "Inf (insert (a::'a::complete_lattice) A) = inf a (Inf A)"
apply (rule order_antisym)
apply (rule le_infI)
apply (rule Inf_lower)
@@ -132,10 +119,10 @@
apply (erule Inf_lower)
done
-lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
+lemma bot_least[simp]: "Sup{} \<le> (x::'a::complete_lattice)"
by (rule Sup_least) simp
-lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
+lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
by (rule Inf_greatest) simp
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
@@ -149,51 +136,15 @@
subsubsection {* Booleans *}
-defs
- Inf_bool_def: "Inf A == ALL x:A. x"
-
-instance bool :: comp_lat
+instance bool :: complete_lattice
+ Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>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 inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
- apply (rule order_antisym)
- apply (rule le_boolI)
- apply (rule conjI)
- apply (rule le_boolE)
- apply (rule inf_le1)
- apply assumption+
- apply (rule le_boolE)
- apply (rule inf_le2)
- apply assumption+
- apply (rule le_infI)
- apply (rule le_boolI)
- apply (erule conjunct1)
- apply (rule le_boolI)
- apply (erule conjunct2)
- done
-
-theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
- apply (rule order_antisym)
- apply (rule le_supI)
- apply (rule le_boolI)
- apply (erule disjI1)
- apply (rule le_boolI)
- apply (erule disjI2)
- apply (rule le_boolI)
- apply (erule disjE)
- apply (rule le_boolE)
- apply (rule sup_ge1)
- apply assumption+
- apply (rule le_boolE)
- apply (rule sup_ge2)
- apply assumption+
- done
-
-theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
+theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
apply (rule order_antisym)
apply (rule Sup_least)
apply (rule le_boolI)
@@ -208,51 +159,8 @@
subsubsection {* Functions *}
-text {*
- Handy introduction and elimination rules for @{text "\<le>"}
- on unary and binary predicates
-*}
-
-lemma predicate1I [Pure.intro!, intro!]:
- assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
- shows "P \<le> Q"
- apply (rule le_funI)
- apply (rule le_boolI)
- apply (rule PQ)
- apply assumption
- done
-
-lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
- apply (erule le_funE)
- apply (erule le_boolE)
- apply assumption+
- done
-
-lemma predicate2I [Pure.intro!, intro!]:
- assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
- shows "P \<le> Q"
- apply (rule le_funI)+
- apply (rule le_boolI)
- apply (rule PQ)
- apply assumption
- done
-
-lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
- apply (erule le_funE)+
- apply (erule le_boolE)
- apply assumption+
- done
-
-lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
- by (rule predicate1D)
-
-lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
- by (rule predicate2D)
-
-defs
- Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
-
-instance "fun" :: (type, comp_lat) comp_lat
+instance "fun" :: (type, complete_lattice) complete_lattice
+ Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
apply intro_classes
apply (unfold Inf_fun_def)
apply (rule le_funI)
@@ -268,33 +176,7 @@
apply (iprover elim: le_funE)
done
-theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
- apply (rule order_antisym)
- apply (rule le_funI)
- apply (rule le_infI)
- apply (rule le_funD [OF inf_le1])
- apply (rule le_funD [OF inf_le2])
- apply (rule le_infI)
- apply (rule le_funI)
- apply (rule inf_le1)
- apply (rule le_funI)
- apply (rule inf_le2)
- done
-
-theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
- apply (rule order_antisym)
- apply (rule le_supI)
- apply (rule le_funI)
- apply (rule sup_ge1)
- apply (rule le_funI)
- apply (rule sup_ge2)
- apply (rule le_funI)
- apply (rule le_supI)
- apply (rule le_funD [OF sup_ge1])
- apply (rule le_funD [OF sup_ge2])
- done
-
-theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
+theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
apply (rule order_antisym)
apply (rule Sup_least)
apply (rule le_funI)
@@ -308,34 +190,13 @@
apply simp
done
+
subsubsection {* Sets *}
-defs
- Inf_set_def: "Inf S == \<Inter>S"
-
-instance set :: (type) comp_lat
+instance set :: (type) complete_lattice
+ Inf_set_def: "Inf S \<equiv> \<Inter>S"
by intro_classes (auto simp add: Inf_set_def)
-theorem inf_set_eq: "inf A B = A \<inter> B"
- apply (rule subset_antisym)
- apply (rule Int_greatest)
- apply (rule inf_le1)
- apply (rule inf_le2)
- apply (rule le_infI)
- apply (rule Int_lower1)
- apply (rule Int_lower2)
- done
-
-theorem sup_set_eq: "sup A B = A \<union> B"
- apply (rule subset_antisym)
- apply (rule le_supI)
- apply (rule Un_upper1)
- apply (rule Un_upper2)
- apply (rule Un_least)
- apply (rule sup_ge1)
- apply (rule sup_ge2)
- done
-
theorem Sup_set_eq: "Sup S = \<Union>S"
apply (rule subset_antisym)
apply (rule Sup_least)
@@ -348,11 +209,11 @@
subsection {* Least and greatest fixed points *}
definition
- lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
"lfp f = Inf {u. f u \<le> u}" --{*least fixed point*}
definition
- gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
"gfp f = Sup {u. u \<le> f u}" --{*greatest fixed point*}
@@ -403,10 +264,8 @@
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
(auto simp: inf_set_eq intro: indhyp)
-
-text{*Version of induction for binary relations*}
-lemmas lfp_induct2 = lfp_induct_set [of "(a,b)", split_format (complete)]
-
+text {* Version of induction for binary relations *}
+lemmas lfp_induct2 = lfp_induct_set [of "(a, b)", split_format (complete)]
lemma lfp_ordinal_induct:
assumes mono: "mono f"
@@ -563,8 +422,6 @@
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
-
-
ML
{*
val lfp_def = thm "lfp_def";
--- a/src/HOL/Hyperreal/StarClasses.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy Fri Mar 16 21:32:08 2007 +0100
@@ -11,10 +11,6 @@
subsection {* Syntactic classes *}
-instance star :: (ord) ord
- star_le_def: "(op \<le>) \<equiv> *p2* (op \<le>)"
- star_less_def: "(op <) \<equiv> *p2* (op <)" ..
-
instance star :: (zero) zero
star_zero_def: "0 \<equiv> star_of 0" ..
@@ -24,7 +20,6 @@
instance star :: (plus) plus
star_add_def: "(op +) \<equiv> *f2* (op +)" ..
-
instance star :: (times) times
star_mult_def: "(op *) \<equiv> *f2* (op *)" ..
@@ -47,6 +42,10 @@
instance star :: (power) power
star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
+instance star :: (ord) ord
+ star_le_def: "(op \<le>) \<equiv> *p2* (op \<le>)"
+ star_less_def: "(op <) \<equiv> *p2* (op <)" ..
+
lemmas star_class_defs [transfer_unfold] =
star_zero_def star_one_def star_number_def
star_add_def star_diff_def star_minus_def
@@ -206,7 +205,7 @@
star_of_number_less star_of_number_le star_of_number_eq
star_of_less_number star_of_le_number star_of_eq_number
-subsection {* Ordering classes *}
+subsection {* Ordering and lattice classes *}
instance star :: (order) order
apply (intro_classes)
@@ -216,6 +215,33 @@
apply (transfer, erule (1) order_antisym)
done
+instance star :: (lower_semilattice) lower_semilattice
+ star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
+ by default (transfer star_inf_def, auto)+
+
+instance star :: (upper_semilattice) upper_semilattice
+ star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
+ by default (transfer star_sup_def, auto)+
+
+instance star :: (lattice) lattice ..
+
+instance star :: (distrib_lattice) distrib_lattice
+ by default (transfer, auto simp add: sup_inf_distrib1)
+
+lemma Standard_inf [simp]:
+ "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
+by (simp add: star_inf_def)
+
+lemma Standard_sup [simp]:
+ "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
+by (simp add: star_sup_def)
+
+lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
+by transfer (rule refl)
+
+lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
+by transfer (rule refl)
+
instance star :: (linorder) linorder
by (intro_classes, transfer, rule linorder_linear)
@@ -245,63 +271,6 @@
lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
by transfer (rule refl)
-subsection {* Lattice ordering classes *}
-
-text {*
- Some extra trouble is necessary because the class axioms
- for @{term inf} and @{term sup} use quantification over
- function spaces.
-*}
-
-lemma ex_star_fun:
- "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
- \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
-by (erule exE, erule exI)
-
-lemma ex_star_fun2:
- "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
- \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
-by (erule exE, erule exI)
-
-instance star :: (join_semilorder) join_semilorder
-apply (intro_classes)
-apply (rule ex_star_fun2)
-apply (transfer is_join_def)
-apply (rule join_exists)
-done
-
-instance star :: (meet_semilorder) meet_semilorder
-apply (intro_classes)
-apply (rule ex_star_fun2)
-apply (transfer is_meet_def)
-apply (rule meet_exists)
-done
-
-instance star :: (lorder) lorder ..
-
-lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
-apply (rule is_meet_unique [OF is_meet_meet])
-apply (transfer is_meet_def, rule is_meet_meet)
-done
-
-lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
-apply (rule is_join_unique [OF is_join_join])
-apply (transfer is_join_def, rule is_join_join)
-done
-
-lemma Standard_inf [simp]:
- "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
-by (simp add: star_inf_def)
-
-lemma Standard_sup [simp]:
- "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
-by (simp add: star_sup_def)
-
-lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
-by transfer (rule refl)
-
-lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
-by transfer (rule refl)
subsection {* Ordered group classes *}
--- a/src/HOL/Library/Continuity.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Library/Continuity.thy Fri Mar 16 21:32:08 2007 +0100
@@ -12,15 +12,15 @@
subsection {* Continuity for complete lattices *}
definition
- chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+ chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
"chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
definition
- continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
+ continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
"continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
abbreviation
- bot :: "'a::order" where
+ bot :: "'a::complete_lattice" where
"bot \<equiv> Sup {}"
lemma SUP_nat_conv:
@@ -34,7 +34,7 @@
apply (blast intro:SUP_leI le_SUPI)
done
-lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
+lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
assumes "continuous F" shows "mono F"
proof
fix A B :: "'a" assume "A <= B"
--- a/src/HOL/Library/Graphs.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Library/Graphs.thy Fri Mar 16 21:32:08 2007 +0100
@@ -20,6 +20,19 @@
"Graph (dest_graph G) = G"
by (cases G) simp
+lemma split_graph_all:
+ "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
+proof
+ fix set
+ assume "\<And>gr. PROP P gr"
+ then show "PROP P (Graph set)" .
+next
+ fix gr
+ assume "\<And>set. PROP P (Graph set)"
+ then have "PROP P (Graph (dest_graph gr))" .
+ then show "PROP P gr" by simp
+qed
+
definition
has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
@@ -132,11 +145,9 @@
subsection {* Order on Graphs *}
-instance graph :: (type, type) ord
- graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
- graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
-
instance graph :: (type, type) order
+ graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
+ graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
proof
fix x y z :: "('a,'b) graph"
@@ -153,27 +164,14 @@
by (cases x, cases y) auto
qed
-
-defs (overloaded)
- Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
-
-instance graph :: (type, type) comp_lat
- by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
+instance graph :: (type, type) distrib_lattice
+ "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
+ "sup G H \<equiv> G + H"
+ by default (auto simp add: split_graph_all graph_plus_def inf_graph_def sup_graph_def graph_leq_def graph_less_def)
-lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
- unfolding is_join_def
-proof (intro allI conjI impI)
- fix a b x :: "('a, 'b) graph"
-
- show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
- unfolding graph_leq_def graph_plus_def
- by (cases a, cases b) auto
-qed
-
-lemma plus_is_join:
- "(op +) =
- (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
- using plus_graph_is_join by (simp add:join_unique)
+instance graph :: (type, type) complete_lattice
+ Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+ by default (auto simp: Inf_graph_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
instance graph :: (type, monoid_mult) semiring_1
proof
@@ -199,11 +197,10 @@
by simp
qed
-
instance graph :: (type, monoid_mult) idem_add
proof
fix a :: "('a, 'b) graph"
- show "a + a = a" unfolding plus_is_join by simp
+ show "a + a = a" unfolding graph_plus_def by simp
qed
@@ -270,7 +267,7 @@
unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
by simp
-instance graph :: (type, monoid_mult) kleene_by_comp_lat
+instance graph :: (type, monoid_mult) kleene_by_complete_lattice
proof
fix a b c :: "('a, 'b) graph"
--- a/src/HOL/Matrix/Matrix.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy Fri Mar 16 21:32:08 2007 +0100
@@ -7,6 +7,11 @@
imports MatrixGeneral
begin
+instance matrix :: ("{zero, lattice}") lattice
+ "inf \<equiv> combine_matrix inf"
+ "sup \<equiv> combine_matrix sup"
+ by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
+
instance matrix :: ("{plus, zero}") plus
plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
@@ -17,13 +22,8 @@
instance matrix :: ("{plus, times, zero}") times
times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
-lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
- by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
-
-lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
- by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
-
instance matrix :: (lordered_ab_group) lordered_ab_group_meet
+ abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
proof
fix A B C :: "('a::lordered_ab_group) matrix"
show "A + B + C = A + (B + C)"
@@ -45,8 +45,6 @@
by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
show "A - B = A + - B"
by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
- show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
- by (auto intro: is_meet_combine_matrix_meet)
assume "A <= B"
then show "C + A <= C + B"
apply (simp add: plus_matrix_def)
@@ -55,9 +53,6 @@
done
qed
-defs (overloaded)
- abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
-
instance matrix :: (lordered_ring) lordered_ring
proof
fix A B C :: "('a :: lordered_ring) matrix"
@@ -90,7 +85,7 @@
apply (rule le_right_mult)
apply (simp_all add: add_mono mult_right_mono)
done
-qed
+qed
lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)"
by (simp add: plus_matrix_def)
@@ -286,17 +281,7 @@
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
by (simp add: minus_matrix_def)
-lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"
- apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
- apply (simp)
- done
-
-lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
- apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
- apply (simp)
- done
-
lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
- by (simp add: abs_lattice join_matrix)
+ by (simp add: abs_lattice sup_matrix_def)
end
--- a/src/HOL/Matrix/SparseMatrix.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy Fri Mar 16 21:32:08 2007 +0100
@@ -922,7 +922,7 @@
lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
- apply (simp add: pprt_def join_matrix)
+ apply (simp add: pprt_def sup_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply simp
@@ -931,7 +931,7 @@
done
lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
- apply (simp add: nprt_def meet_matrix)
+ apply (simp add: nprt_def inf_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply simp
@@ -940,14 +940,14 @@
done
lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
- apply (simp add: pprt_def join_matrix)
+ apply (simp add: pprt_def sup_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply simp
done
lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
- apply (simp add: nprt_def meet_matrix)
+ apply (simp add: nprt_def inf_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply simp
@@ -978,7 +978,7 @@
lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
apply (simp add: pprt_def)
- apply (simp add: join_matrix)
+ apply (simp add: sup_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
@@ -986,7 +986,7 @@
lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
apply (simp add: nprt_def)
- apply (simp add: meet_matrix)
+ apply (simp add: inf_matrix_def)
apply (simp add: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
--- a/src/HOL/OrderedGroup.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/OrderedGroup.thy Fri Mar 16 21:32:08 2007 +0100
@@ -1,4 +1,3 @@
-
(* Title: HOL/OrderedGroup.thy
ID: $Id$
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
@@ -8,7 +7,7 @@
header {* Ordered Groups *}
theory OrderedGroup
-imports LOrder
+imports Lattices
uses "~~/src/Provers/Arith/abel_cancel.ML"
begin
@@ -204,7 +203,7 @@
instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
- assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
+ assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
@@ -565,13 +564,19 @@
lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
by (simp add: compare_rls)
+
subsection {* Lattice Ordered (Abelian) Groups *}
-axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
+class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
+
+class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
-axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
+class lordered_ab_group = pordered_ab_group_add + lattice
-lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
+instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
+instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
+
+lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
apply (rule order_antisym)
apply (simp_all add: le_infI)
apply (rule add_le_imp_le_left [of "-a"])
@@ -580,7 +585,7 @@
apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
done
-lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
+lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))"
apply (rule order_antisym)
apply (rule add_le_imp_le_left [of "-a"])
apply (simp only: add_assoc[symmetric], simp)
@@ -590,55 +595,53 @@
apply (simp_all)
done
-lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
-apply (auto simp add: is_join_def)
-apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
-apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
-apply (subst neg_le_iff_le[symmetric])
-apply (simp add: le_infI)
-done
-
-lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
-apply (auto simp add: is_meet_def)
-apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
-apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
-apply (subst neg_le_iff_le[symmetric])
-apply (simp add: le_supI)
-done
-
-axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
-
-instance lordered_ab_group_join \<subseteq> lordered_ab_group
-proof
- show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
-qed
-
-instance lordered_ab_group_meet \<subseteq> lordered_ab_group
-proof
- show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
-qed
-
-lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
+lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
proof -
- have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
+ have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
thus ?thesis by (simp add: add_commute)
qed
-lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
+lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
proof -
- have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
+ have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
thus ?thesis by (simp add: add_commute)
qed
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
-lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
-by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
+lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
+proof (rule inf_unique)
+ fix a b :: 'a
+ show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
+ (simp, simp add: add_sup_distrib_left)
+next
+ fix a b :: 'a
+ show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
+ (simp, simp add: add_sup_distrib_left)
+next
+ fix a b c :: 'a
+ assume "a \<le> b" "a \<le> c"
+ then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
+ (simp add: le_supI)
+qed
+
+lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
+proof (rule sup_unique)
+ fix a b :: 'a
+ show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
+ (simp, simp add: add_inf_distrib_left)
+next
+ fix a b :: 'a
+ show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
+ (simp, simp add: add_inf_distrib_left)
+next
+ fix a b c :: 'a
+ assume "a \<le> c" "b \<le> c"
+ then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
+ (simp add: le_infI)
+qed
-lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
-by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
-
-lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
+lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
proof -
have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
@@ -761,8 +764,8 @@
with a show ?thesis by simp
qed
-axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
- abs_lattice: "abs x = sup x (-x)"
+class lordered_ab_group_abs = lordered_ab_group +
+ assumes abs_lattice: "abs x = sup x (uminus x)"
lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
by (simp add: abs_lattice)
@@ -786,7 +789,7 @@
proof -
note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
- show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
+ show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
qed
lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
@@ -1131,8 +1134,6 @@
val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
val add_inf_distrib_left = thm "add_inf_distrib_left";
val add_sup_distrib_left = thm "add_sup_distrib_left";
-val is_join_neg_inf = thm "is_join_neg_inf";
-val is_meet_neg_sup = thm "is_meet_neg_sup";
val add_sup_distrib_right = thm "add_sup_distrib_right";
val add_inf_distrib_right = thm "add_inf_distrib_right";
val add_sup_inf_distribs = thms "add_sup_inf_distribs";
--- a/src/HOL/Ring_and_Field.thy Fri Mar 16 21:32:07 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Mar 16 21:32:08 2007 +0100
@@ -265,7 +265,7 @@
instance pordered_ring \<subseteq> pordered_ab_group_add ..
-axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
+class lordered_ring = pordered_ring + lordered_ab_group_abs
instance lordered_ring \<subseteq> lordered_ab_group_meet ..
@@ -274,9 +274,7 @@
class abs_if = minus + ord + zero +
assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
-class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
-
-instance ordered_ring_strict \<subseteq> lordered_ab_group ..
+class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group
instance ordered_ring_strict \<subseteq> lordered_ring
by intro_classes (simp add: abs_if sup_eq_if)
@@ -287,7 +285,7 @@
(*previously ordered_semiring*)
assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
-class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
+class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group
(*previously ordered_ring*)
instance ordered_idom \<subseteq> ordered_ring_strict ..