--- a/NEWS Tue May 04 14:11:28 2010 +0200
+++ b/NEWS Tue May 04 14:10:42 2010 +0200
@@ -89,6 +89,9 @@
*** Pure ***
+* Predicates of locales introduces by classes carry a mandatory "class"
+prefix. INCOMPATIBILITY.
+
* 'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
@@ -137,6 +140,9 @@
*** HOL ***
+* Theory 'Finite_Set': various folding_* locales facilitate the application
+of the various fold combinators on finite sets.
+
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
provides abstract red-black tree type which is backed by RBT_Impl
as implementation. INCOMPATIBILTY.
--- a/src/HOL/Bali/TypeSafe.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Tue May 04 14:10:42 2010 +0200
@@ -9,8 +9,6 @@
section "error free"
-hide_const field
-
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
error_free_s0: "error_free s0"
--- a/src/HOL/Big_Operators.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Big_Operators.thy Tue May 04 14:10:42 2010 +0200
@@ -33,7 +33,7 @@
text {* for ad-hoc proofs for @{const fold_image} *}
lemma (in comm_monoid_add) comm_monoid_mult:
- "comm_monoid_mult (op +) 0"
+ "class.comm_monoid_mult (op +) 0"
proof qed (auto intro: add_assoc add_commute)
notation times (infixl "*" 70)
@@ -1200,7 +1200,8 @@
context semilattice_inf
begin
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+ "class.ab_semigroup_idem_mult inf"
proof qed (rule inf_assoc inf_commute inf_idem)+
lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1270,7 +1271,7 @@
context semilattice_sup
begin
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1490,15 +1491,15 @@
using assms by (rule Max.hom_commute)
lemma ab_semigroup_idem_mult_min:
- "ab_semigroup_idem_mult min"
+ "class.ab_semigroup_idem_mult min"
proof qed (auto simp add: min_def)
lemma ab_semigroup_idem_mult_max:
- "ab_semigroup_idem_mult max"
+ "class.ab_semigroup_idem_mult max"
proof qed (auto simp add: max_def)
lemma max_lattice:
- "semilattice_inf (op \<ge>) (op >) max"
+ "class.semilattice_inf (op \<ge>) (op >) max"
by (fact min_max.dual_semilattice)
lemma dual_max:
--- a/src/HOL/Complete_Lattice.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Tue May 04 14:10:42 2010 +0200
@@ -33,8 +33,8 @@
begin
lemma dual_complete_lattice:
- "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+ "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
(unfold_locales, (fact bot_least top_greatest
Sup_upper Sup_least Inf_lower Inf_greatest)+)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue May 04 14:10:42 2010 +0200
@@ -265,7 +265,7 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
--- a/src/HOL/Divides.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Divides.thy Tue May 04 14:10:42 2010 +0200
@@ -379,6 +379,8 @@
class ring_div = semiring_div + comm_ring_1
begin
+subclass ring_1_no_zero_divisors ..
+
text {* Negation respects modular equivalence. *}
lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
--- a/src/HOL/Finite_Set.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 04 14:10:42 2010 +0200
@@ -509,13 +509,8 @@
subsection {* Class @{text finite} *}
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
class finite =
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
begin
lemma finite [simp]: "finite (A \<Colon> 'a set)"
@@ -1734,12 +1729,10 @@
qed
lemma insert [simp]:
- assumes "finite A" and "x \<notin> A"
- shows "F (insert x A) = (if A = {} then x else x * F A)"
-proof (cases "A = {}")
- case True then show ?thesis by simp
-next
- case False then obtain b where "b \<in> A" by blast
+ assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
+ shows "F (insert x A) = x * F A"
+proof -
+ from `A \<noteq> {}` obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` have "finite B" by simp
interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
@@ -1833,8 +1826,6 @@
(simp_all add: assoc in_idem `finite A`)
qed
-declare insert [simp del]
-
lemma eq_fold_idem':
assumes "finite A"
shows "F (insert a A) = fold (op *) a A"
@@ -1844,13 +1835,13 @@
qed
lemma insert_idem [simp]:
- assumes "finite A"
- shows "F (insert x A) = (if A = {} then x else x * F A)"
+ assumes "finite A" and "A \<noteq> {}"
+ shows "F (insert x A) = x * F A"
proof (cases "x \<in> A")
- case False with `finite A` show ?thesis by (rule insert)
+ case False from `finite A` `x \<notin> A` `A \<noteq> {}` show ?thesis by (rule insert)
next
- case True then have "A \<noteq> {}" by auto
- with `finite A` show ?thesis by (simp add: in_idem insert_absorb True)
+ case True
+ from `finite A` `A \<noteq> {}` show ?thesis by (simp add: in_idem insert_absorb True)
qed
lemma union_idem:
--- a/src/HOL/HOL.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/HOL.thy Tue May 04 14:10:42 2010 +0200
@@ -1886,7 +1886,6 @@
*}
hide_const (open) eq
-hide_const eq
text {* Cases *}
--- a/src/HOL/Imperative_HOL/Heap.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue May 04 14:10:42 2010 +0200
@@ -216,6 +216,9 @@
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
unfolding noteq_refs_def noteq_arrs_def by auto
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+ unfolding noteq_refs_def by auto
+
lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
--- a/src/HOL/Lattices.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Lattices.thy Tue May 04 14:10:42 2010 +0200
@@ -67,8 +67,8 @@
text {* Dual lattice *}
lemma dual_semilattice:
- "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+ "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
(unfold_locales, simp_all add: sup_least)
end
@@ -235,8 +235,8 @@
begin
lemma dual_lattice:
- "lattice (op \<ge>) (op >) sup inf"
- by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+ "class.lattice (op \<ge>) (op >) sup inf"
+ by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
(unfold_locales, auto)
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -347,8 +347,8 @@
by(simp add: inf_sup_aci inf_sup_distrib1)
lemma dual_distrib_lattice:
- "distrib_lattice (op \<ge>) (op >) sup inf"
- by (rule distrib_lattice.intro, rule dual_lattice)
+ "class.distrib_lattice (op \<ge>) (op >) sup inf"
+ by (rule class.distrib_lattice.intro, rule dual_lattice)
(unfold_locales, fact inf_sup_distrib1)
lemmas sup_inf_distrib =
@@ -419,7 +419,7 @@
begin
lemma dual_bounded_lattice:
- "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
by unfold_locales (auto simp add: less_le_not_le)
end
@@ -431,8 +431,8 @@
begin
lemma dual_boolean_algebra:
- "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+ "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+ by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
lemma compl_inf_bot:
--- a/src/HOL/Library/FrechetDeriv.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Tue May 04 14:10:42 2010 +0200
@@ -54,11 +54,6 @@
subsection {* Addition *}
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
lemma bounded_linear_add:
assumes "bounded_linear f"
assumes "bounded_linear g"
@@ -402,11 +397,6 @@
subsection {* Inverse *}
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
-
lemmas bounded_linear_mult_const =
mult.bounded_linear_left [THEN bounded_linear_compose]
--- a/src/HOL/Library/Multiset.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Tue May 04 14:10:42 2010 +0200
@@ -1239,7 +1239,7 @@
qed
have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+ show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
qed (auto simp add: le_multiset_def irrefl dest: trans)
qed
--- a/src/HOL/Library/Product_plus.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Library/Product_plus.thy Tue May 04 14:10:42 2010 +0200
@@ -112,4 +112,10 @@
instance "*" :: (ab_group_add, ab_group_add) ab_group_add
by default (simp_all add: expand_prod_eq)
+lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
+lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
+by (cases "finite A", induct set: finite, simp_all)
+
end
--- a/src/HOL/Limits.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Limits.thy Tue May 04 14:10:42 2010 +0200
@@ -11,7 +11,7 @@
subsection {* Nets *}
text {*
- A net is now defined simply as a filter.
+ A net is now defined simply as a filter on a set.
The definition also allows non-proper filters.
*}
@@ -53,6 +53,12 @@
unfolding eventually_def
by (rule is_filter.True [OF is_filter_Rep_net])
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
+proof -
+ assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+ thus "eventually P net" by simp
+qed
+
lemma eventually_mono:
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
unfolding eventually_def
@@ -101,15 +107,15 @@
subsection {* Finer-than relation *}
-text {* @{term "net \<le> net'"} means that @{term net'} is finer than
-@{term net}. *}
+text {* @{term "net \<le> net'"} means that @{term net} is finer than
+@{term net'}. *}
-instantiation net :: (type) "{order,top}"
+instantiation net :: (type) complete_lattice
begin
definition
le_net_def [code del]:
- "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
+ "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
definition
less_net_def [code del]:
@@ -117,12 +123,64 @@
definition
top_net_def [code del]:
- "top = Abs_net (\<lambda>P. True)"
+ "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+
+definition
+ bot_net_def [code del]:
+ "bot = Abs_net (\<lambda>P. True)"
+
+definition
+ sup_net_def [code del]:
+ "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+
+definition
+ inf_net_def [code del]:
+ "inf a b = Abs_net
+ (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+
+definition
+ Sup_net_def [code del]:
+ "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+
+definition
+ Inf_net_def [code del]:
+ "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+
+lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
+unfolding top_net_def
+by (rule eventually_Abs_net, rule is_filter.intro, auto)
-lemma eventually_top [simp]: "eventually P top"
-unfolding top_net_def
+lemma eventually_bot [simp]: "eventually P bot"
+unfolding bot_net_def
by (subst eventually_Abs_net, rule is_filter.intro, auto)
+lemma eventually_sup:
+ "eventually P (sup net net') \<longleftrightarrow> eventually P net \<and> eventually P net'"
+unfolding sup_net_def
+by (rule eventually_Abs_net, rule is_filter.intro)
+ (auto elim!: eventually_rev_mp)
+
+lemma eventually_inf:
+ "eventually P (inf a b) \<longleftrightarrow>
+ (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+unfolding inf_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (fast intro: eventually_True)
+apply clarify
+apply (intro exI conjI)
+apply (erule (1) eventually_conj)
+apply (erule (1) eventually_conj)
+apply simp
+apply auto
+done
+
+lemma eventually_Sup:
+ "eventually P (Sup A) \<longleftrightarrow> (\<forall>net\<in>A. eventually P net)"
+unfolding Sup_net_def
+apply (rule eventually_Abs_net, rule is_filter.intro)
+apply (auto intro: eventually_conj elim!: eventually_rev_mp)
+done
+
instance proof
fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
by (rule less_net_def)
@@ -137,21 +195,49 @@
unfolding le_net_def expand_net_eq by fast
next
fix x :: "'a net" show "x \<le> top"
+ unfolding le_net_def eventually_top by (simp add: always_eventually)
+next
+ fix x :: "'a net" show "bot \<le> x"
unfolding le_net_def by simp
+next
+ fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
+ unfolding le_net_def eventually_sup by simp_all
+next
+ fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
+ unfolding le_net_def eventually_sup by simp
+next
+ fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
+ unfolding le_net_def eventually_inf by (auto intro: eventually_True)
+next
+ fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
+ unfolding le_net_def eventually_inf
+ by (auto elim!: eventually_mono intro: eventually_conj)
+next
+ fix x :: "'a net" and A assume "x \<in> A" thus "x \<le> Sup A"
+ unfolding le_net_def eventually_Sup by simp
+next
+ fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
+ unfolding le_net_def eventually_Sup by simp
+next
+ fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
+ unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
+next
+ fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
+ unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
qed
end
lemma net_leD:
- "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
+ "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
unfolding le_net_def by simp
lemma net_leI:
- "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
+ "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
unfolding le_net_def by simp
lemma eventually_False:
- "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
+ "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
unfolding expand_net_eq by (auto elim: eventually_rev_mp)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 04 14:10:42 2010 +0200
@@ -1931,14 +1931,6 @@
subsection {* Use this to derive general bound property of convex function. *}
-(* TODO: move *)
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
-(* TODO: move *)
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
lemma convex_on:
assumes "convex s"
shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>
--- a/src/HOL/Orderings.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Orderings.thy Tue May 04 14:10:42 2010 +0200
@@ -106,7 +106,7 @@
text {* Dual order *}
lemma dual_preorder:
- "preorder (op \<ge>) (op >)"
+ "class.preorder (op \<ge>) (op >)"
proof qed (auto simp add: less_le_not_le intro: order_trans)
end
@@ -186,7 +186,7 @@
text {* Dual order *}
lemma dual_order:
- "order (op \<ge>) (op >)"
+ "class.order (op \<ge>) (op >)"
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
end
@@ -257,8 +257,8 @@
text {* Dual order *}
lemma dual_linorder:
- "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+ "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
text {* min/max *}
--- a/src/HOL/Quotient_Examples/FSet.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue May 04 14:10:42 2010 +0200
@@ -359,6 +359,10 @@
then show "concat a \<approx> concat b" by simp
qed
+lemma [quot_respect]:
+ "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+ by auto
+
text {* Distributive lattice with bot *}
lemma sub_list_not_eq:
@@ -551,6 +555,11 @@
is
"concat"
+quotient_definition
+ "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+ "filter"
+
text {* Compositional Respectfullness and Preservation *}
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
@@ -868,6 +877,14 @@
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
+text {* Raw theorems of ffilter *}
+
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
+
text {* Lifted theorems *}
lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -1142,6 +1159,76 @@
lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
by (lifting concat_append)
+text {* ffilter *}
+
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+
+lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+
+
+section {* lemmas transferred from Finite_Set theory *}
+
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+by (induct S) auto
+
+text {* @{thm subset_empty} transferred is: *}
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+by (cases xs) (auto simp add: fsubset_finsert not_fin_fnil)
+
+text {* @{thm not_psubset_empty} transferred is: *}
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+unfolding less_fset by (auto simp add: fsubseteq_fnil)
+
+text {* @{thm card_mono} transferred is: *}
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+proof (induct xs arbitrary: ys)
+ case fempty
+ thus ?case by simp
+next
+ case (finsert x xs ys)
+ from finsert(1,3) have "xs |\<subseteq>| fdelete ys x"
+ by (auto simp add: fsubset_fin fin_fdelete)
+ from finsert(2) this have hyp: "fcard xs \<le> fcard (fdelete ys x)" by simp
+ from finsert(3) have "x |\<in>| ys" by (auto simp add: fsubset_fin)
+ from this have ys_is: "ys = finsert x (fdelete ys x)"
+ unfolding expand_fset_eq by (auto simp add: fin_fdelete)
+ from finsert(1) hyp have "fcard (finsert x xs) \<le> fcard (finsert x (fdelete ys x))"
+ by (auto simp add: fin_fdelete_ident)
+ from ys_is this show ?case by auto
+qed
+
+text {* @{thm card_seteq} transferred is: *}
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+proof (induct xs arbitrary: ys)
+ case fempty
+ thus ?case by (simp add: fcard_0)
+next
+ case (finsert x xs ys)
+ from finsert have subset: "xs |\<subseteq>| fdelete ys x"
+ by (auto simp add: fsubset_fin fin_fdelete)
+ from finsert have x: "x |\<in>| ys"
+ by (auto simp add: fsubset_fin fin_fdelete)
+ from finsert(1,4) this have "fcard (fdelete ys x) \<le> fcard xs"
+ by (auto simp add: fcard_delete)
+ from finsert(2) this subset have hyp: "xs = fdelete ys x" by auto
+ from finsert have "x |\<in>| ys"
+ by (auto simp add: fsubset_fin fin_fdelete)
+ from this hyp show ?case
+ unfolding expand_fset_eq by (auto simp add: fin_fdelete)
+qed
+
+text {* @{thm psubset_card_mono} transferred is: *}
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+unfolding less_fset linorder_not_le[symmetric]
+by (auto simp add: fcard_fseteq)
+
+
ML {*
fun dest_fsetT (Type (@{type_name fset}, [T])) = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
--- a/src/HOL/SEQ.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/SEQ.thy Tue May 04 14:10:42 2010 +0200
@@ -532,6 +532,33 @@
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
+lemma convergent_const: "convergent (\<lambda>n. c)"
+by (rule convergentI, rule LIMSEQ_const)
+
+lemma convergent_add:
+ fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+ assumes "convergent (\<lambda>n. X n)"
+ assumes "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n + Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ_add)
+
+lemma convergent_setsum:
+ fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
+ assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+ shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+using assms
+by (induct A set: finite, simp_all add: convergent_const convergent_add)
+
+lemma (in bounded_linear) convergent:
+ assumes "convergent (\<lambda>n. X n)"
+ shows "convergent (\<lambda>n. f (X n))"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
+lemma (in bounded_bilinear) convergent:
+ assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
+ shows "convergent (\<lambda>n. X n ** Y n)"
+using assms unfolding convergent_def by (fast intro: LIMSEQ)
+
lemma convergent_minus_iff:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
--- a/src/HOL/Tools/Function/relation.ML Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Tools/Function/relation.ML Tue May 04 14:10:42 2010 +0200
@@ -14,19 +14,20 @@
structure Function_Relation : FUNCTION_RELATION =
struct
-fun inst_thm ctxt rel st =
+fun inst_state_tac ctxt rel st =
let
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
- val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
- in
- Drule.cterm_instantiate [(Rvar, rel')] st'
+ in case Term.add_vars (prop_of st') [] of
+ [v] =>
+ PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
+ | _ => Seq.empty
end
fun relation_tac ctxt rel i =
TRY (Function_Common.apply_termination_rule ctxt i)
- THEN PRIMITIVE (inst_thm ctxt rel)
+ THEN inst_state_tac ctxt rel
val setup =
Method.setup @{binding relation}
--- a/src/HOL/Wellfounded.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Wellfounded.thy Tue May 04 14:10:42 2010 +0200
@@ -68,7 +68,7 @@
assumes lin: "OFCLASS('a::ord, linorder_class)"
shows "OFCLASS('a::ord, wellorder_class)"
using lin by (rule wellorder_class.intro)
- (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+ (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
lemma (in wellorder) wf:
"wf {(x, y). x < y}"
--- a/src/HOL/Word/WordArith.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/Word/WordArith.thy Tue May 04 14:10:42 2010 +0200
@@ -17,7 +17,7 @@
by (auto simp del: word_uint.Rep_inject
simp: word_uint.Rep_inject [symmetric])
-lemma signed_linorder: "linorder word_sle word_sless"
+lemma signed_linorder: "class.linorder word_sle word_sless"
proof
qed (unfold word_sle_def word_sless_def, auto)
--- a/src/HOL/ex/Landau.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOL/ex/Landau.thy Tue May 04 14:10:42 2010 +0200
@@ -187,7 +187,7 @@
proof -
interpret preorder_equiv less_eq_fun less_fun proof
qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
- show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+ show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
show "preorder_equiv.equiv less_eq_fun = equiv_fun"
by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
qed
--- a/src/HOLCF/CompactBasis.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOLCF/CompactBasis.thy Tue May 04 14:10:42 2010 +0200
@@ -237,12 +237,12 @@
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
lemma fold_pd_PDUnit:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDUnit x) = g x"
unfolding fold_pd_def Rep_PDUnit by simp
lemma fold_pd_PDPlus:
- assumes "ab_semigroup_idem_mult f"
+ assumes "class.ab_semigroup_idem_mult f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
interpret ab_semigroup_idem_mult f by fact
--- a/src/HOLCF/ConvexPD.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy Tue May 04 14:10:42 2010 +0200
@@ -412,7 +412,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
lemma ACI_convex_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
apply unfold_locales
apply (simp add: convex_plus_assoc)
apply (simp add: convex_plus_commute)
--- a/src/HOLCF/LowerPD.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOLCF/LowerPD.thy Tue May 04 14:10:42 2010 +0200
@@ -393,7 +393,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
lemma ACI_lower_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
apply unfold_locales
apply (simp add: lower_plus_assoc)
apply (simp add: lower_plus_commute)
--- a/src/HOLCF/Tools/fixrec.ML Tue May 04 14:11:28 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Tue May 04 14:10:42 2010 +0200
@@ -337,10 +337,10 @@
(* proves a block of pattern matching equations as theorems, using unfold *)
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
let
- val tacs =
- [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
- asm_simp_tac (simpset_of ctxt) 1];
- fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs));
+ val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
+ val rule = unfold_thm RS @{thm ssubst_lhs};
+ val tac = rtac rule 1 THEN asm_simp_tac ss 1;
+ fun prove_term t = Goal.prove ctxt [] [] t (K tac);
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
in
map prove_eqn eqns
--- a/src/HOLCF/UpperPD.thy Tue May 04 14:11:28 2010 +0200
+++ b/src/HOLCF/UpperPD.thy Tue May 04 14:10:42 2010 +0200
@@ -388,7 +388,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
lemma ACI_upper_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)
--- a/src/Pure/Isar/class.ML Tue May 04 14:11:28 2010 +0200
+++ b/src/Pure/Isar/class.ML Tue May 04 14:10:42 2010 +0200
@@ -276,16 +276,16 @@
#> pair (param_map, params, assm_axiom)))
end;
-fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
let
- val class = Sign.full_name thy bname;
+ val class = Sign.full_name thy b;
val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_class_spec thy raw_supclasses raw_elems;
in
thy
- |> Expression.add_locale bname Binding.empty supexpr elems
+ |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
|> snd |> Local_Theory.exit_global
- |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
+ |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)