--- a/src/HOL/Big_Operators.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Big_Operators.thy Thu Mar 18 13:57:00 2010 +0100
@@ -9,13 +9,44 @@
imports Plain
begin
+subsection {* Generic monoid operation over a set *}
+
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
+locale comm_monoid_big = comm_monoid +
+ fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
+ assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
+
+sublocale comm_monoid_big < folding_image proof
+qed (simp add: F_eq)
+
+context comm_monoid_big
+begin
+
+lemma infinite [simp]:
+ "\<not> finite A \<Longrightarrow> F g A = 1"
+ by (simp add: F_eq)
+
+end
+
+text {* for ad-hoc proofs for @{const fold_image} *}
+
+lemma (in comm_monoid_add) comm_monoid_mult:
+ "comm_monoid_mult (op +) 0"
+proof qed (auto intro: add_assoc add_commute)
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
+
+
subsection {* Generalized summation over a set *}
-interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
- proof qed (auto intro: add_assoc add_commute)
+definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
+ "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
-definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
-where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
+sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
+qed (fact setsum_def)
abbreviation
Setsum ("\<Sum>_" [1000] 999) where
@@ -63,26 +94,30 @@
in [(@{const_syntax setsum}, setsum_tr')] end
*}
-
-lemma setsum_empty [simp]: "setsum f {} = 0"
-by (simp add: setsum_def)
+lemma setsum_empty:
+ "setsum f {} = 0"
+ by (fact setsum.empty)
-lemma setsum_insert [simp]:
+lemma setsum_insert:
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-by (simp add: setsum_def)
+ by (fact setsum.insert)
+
+lemma setsum_infinite:
+ "~ finite A ==> setsum f A = 0"
+ by (fact setsum.infinite)
-lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
-by (simp add: setsum_def)
+lemma (in comm_monoid_add) setsum_reindex:
+ assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
+proof -
+ interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+ from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
+qed
-lemma setsum_reindex:
- "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
-by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
+lemma (in comm_monoid_add) setsum_reindex_id:
+ "inj_on f B ==> setsum f B = setsum id (f ` B)"
+ by (simp add: setsum_reindex)
-lemma setsum_reindex_id:
- "inj_on f B ==> setsum f B = setsum id (f ` B)"
-by (auto simp add: setsum_reindex)
-
-lemma setsum_reindex_nonzero:
+lemma (in comm_monoid_add) setsum_reindex_nonzero:
assumes fS: "finite S"
and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
shows "setsum h (f ` S) = setsum (h o f) S"
@@ -98,8 +133,8 @@
from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
also have "\<dots> = setsum (h o f) (insert x F)"
- unfolding setsum_insert[OF `finite F` `x\<notin>F`]
- using h0
+ unfolding setsum.insert[OF `finite F` `x\<notin>F`]
+ using h0
apply simp
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in "2.prems")
@@ -111,9 +146,9 @@
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
using fxF "2.hyps" by simp
also have "\<dots> = setsum (h o f) (insert x F)"
- unfolding setsum_insert[OF `finite F` `x\<notin>F`]
+ unfolding setsum.insert[OF `finite F` `x\<notin>F`]
apply simp
- apply (rule cong[OF refl[of "op + (h (f x))"]])
+ apply (rule cong [OF refl [of "op + (h (f x))"]])
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in "2.prems")
apply simp_all
@@ -122,40 +157,37 @@
ultimately show ?case by blast
qed
-lemma setsum_cong:
+lemma (in comm_monoid_add) setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
-by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
+ by (cases "finite A") (auto intro: setsum.cong)
-lemma strong_setsum_cong[cong]:
+lemma (in comm_monoid_add) strong_setsum_cong [cong]:
"A = B ==> (!!x. x:B =simp=> f x = g x)
==> setsum (%x. f x) A = setsum (%x. g x) B"
-by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
+ by (rule setsum_cong) (simp_all add: simp_implies_def)
-lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
-by (rule setsum_cong[OF refl], auto)
+lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
+ by (auto intro: setsum_cong)
-lemma setsum_reindex_cong:
+lemma (in comm_monoid_add) setsum_reindex_cong:
"[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
==> setsum h B = setsum g A"
-by (simp add: setsum_reindex cong: setsum_cong)
+ by (simp add: setsum_reindex cong: setsum_cong)
+lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
+ by (cases "finite A") (erule finite_induct, auto)
-lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
-apply (clarsimp simp: setsum_def)
-apply (erule finite_induct, auto)
-done
+lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
+ by (simp add:setsum_cong)
-lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
-by(simp add:setsum_cong)
-
-lemma setsum_Un_Int: "finite A ==> finite B ==>
+lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
+ by (fact setsum.union_inter)
-lemma setsum_Un_disjoint: "finite A ==> finite B
+lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
-by (subst setsum_Un_Int [symmetric], auto)
+ by (fact setsum.union_disjoint)
lemma setsum_mono_zero_left:
assumes fT: "finite T" and ST: "S \<subseteq> T"
@@ -250,11 +282,14 @@
(*But we can't get rid of finite I. If infinite, although the rhs is 0,
the lhs need not be, since UNION I A could still be finite.*)
-lemma setsum_UN_disjoint:
- "finite I ==> (ALL i:I. finite (A i)) ==>
- (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
- setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
-by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
+lemma (in comm_monoid_add) setsum_UN_disjoint:
+ assumes "finite I" and "ALL i:I. finite (A i)"
+ and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
+ shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
+proof -
+ interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+ from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
+qed
text{*No need to assume that @{term C} is finite. If infinite, the rhs is
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
@@ -270,9 +305,13 @@
(*But we can't get rid of finite A. If infinite, although the lhs is 0,
the rhs need not be, since SIGMA A B could still be finite.*)
-lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
- (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
+lemma (in comm_monoid_add) setsum_Sigma:
+ assumes "finite A" and "ALL x:A. finite (B x)"
+ shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
+proof -
+ interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+ from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
+qed
text{*Here we can eliminate the finiteness assumptions, by cases.*}
lemma setsum_cartesian_product:
@@ -286,8 +325,8 @@
dest: finite_cartesian_productD1 finite_cartesian_productD2)
done
-lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
+lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
+ by (cases "finite A") (simp_all add: setsum.distrib)
subsubsection {* Properties in more restricted classes of structures *}
@@ -321,43 +360,34 @@
setsum f A + setsum f B - setsum f (A Int B)"
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
-lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
- apply (induct set: finite)
- apply simp by auto
-
-lemma (in comm_monoid_mult) fold_image_Un_one:
- assumes fS: "finite S" and fT: "finite T"
- and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
- shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
-proof-
- have "fold_image op * f 1 (S \<inter> T) = 1"
- apply (rule fold_image_1)
- using fS fT I0 by auto
- with fold_image_Un_Int[OF fS fT] show ?thesis by simp
-qed
-
-lemma setsum_eq_general_reverses:
+lemma (in comm_monoid_add) setsum_eq_general_reverses:
assumes fS: "finite S" and fT: "finite T"
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
shows "setsum f S = setsum g T"
+proof -
+ interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+ show ?thesis
apply (simp add: setsum_def fS fT)
- apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
+ apply (rule fold_image_eq_general_inverses)
+ apply (rule fS)
apply (erule kh)
apply (erule hk)
done
-
+qed
-
-lemma setsum_Un_zero:
+lemma (in comm_monoid_add) setsum_Un_zero:
assumes fS: "finite S" and fT: "finite T"
and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
shows "setsum f (S \<union> T) = setsum f S + setsum f T"
+proof -
+ interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
+ show ?thesis
using fS fT
apply (simp add: setsum_def)
- apply (rule comm_monoid_add.fold_image_Un_one)
+ apply (rule fold_image_Un_one)
using I0 by auto
-
+qed
lemma setsum_UNION_zero:
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
@@ -376,7 +406,6 @@
by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
qed
-
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
(if a:A then setsum f A - f a else setsum f A)"
apply (case_tac "finite A")
@@ -651,7 +680,6 @@
case False thus ?thesis by (simp add: setsum_def)
qed
-
lemma setsum_Plus:
fixes A :: "'a set" and B :: "'b set"
assumes fin: "finite A" "finite B"
@@ -668,14 +696,6 @@
text {* Commuting outer and inner summation *}
-lemma swap_inj_on:
- "inj_on (%(i, j). (j, i)) (A \<times> B)"
- by (unfold inj_on_def) fast
-
-lemma swap_product:
- "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
- by (simp add: split_def image_def) blast
-
lemma setsum_commute:
"(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
proof (simp add: setsum_cartesian_product)
@@ -781,8 +801,11 @@
subsection {* Generalized product over a set *}
-definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
-where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
+definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
+ "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
+
+sublocale comm_monoid_add < setprod!: comm_monoid_big "op *" 1 setprod proof
+qed (fact setprod_def)
abbreviation
Setprod ("\<Prod>_" [1000] 999) where
@@ -813,16 +836,15 @@
"PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
"\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
-
-lemma setprod_empty [simp]: "setprod f {} = 1"
-by (auto simp add: setprod_def)
+lemma setprod_empty: "setprod f {} = 1"
+ by (fact setprod.empty)
-lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
+lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
setprod f (insert a A) = f a * setprod f A"
-by (simp add: setprod_def)
+ by (fact setprod.insert)
-lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
-by (simp add: setprod_def)
+lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
+ by (fact setprod.infinite)
lemma setprod_reindex:
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
@@ -1123,17 +1145,63 @@
qed
-subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
+subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
+
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
+locale semilattice_big = semilattice +
+ fixes F :: "'a set \<Rightarrow> 'a"
+ assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
+
+sublocale semilattice_big < folding_one_idem proof
+qed (simp_all add: F_eq)
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
-text{*
- As an application of @{text fold1} we define infimum
- and supremum in (not necessarily complete!) lattices
- over (non-empty) sets by means of @{text fold1}.
-*}
+context lattice
+begin
+
+definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where
+ "Inf_fin = fold1 inf"
+
+definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where
+ "Sup_fin = fold1 sup"
+
+end
+
+sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
+qed (simp add: Inf_fin_def)
+
+sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
+qed (simp add: Sup_fin_def)
context semilattice_inf
begin
+lemma ab_semigroup_idem_mult_inf: "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)"
+by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
+
+lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
+by (induct pred: finite) (auto intro: le_infI1)
+
+lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
+proof(induct arbitrary: a pred:finite)
+ case empty thus ?case by simp
+next
+ case (insert x A)
+ show ?case
+ proof cases
+ assume "A = {}" thus ?thesis using insert by simp
+ next
+ assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
+ qed
+qed
+
lemma below_fold1_iff:
assumes "finite A" "A \<noteq> {}"
shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
@@ -1179,18 +1247,25 @@
end
-context lattice
+context semilattice_sup
begin
-definition
- Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
-where
- "Inf_fin = fold1 inf"
+lemma ab_semigroup_idem_mult_sup: "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)"
+by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
-definition
- Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
-where
- "Sup_fin = fold1 sup"
+lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
+by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
+
+lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
+by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
+
+end
+
+context lattice
+begin
lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
apply(unfold Sup_fin_def Inf_fin_def)
@@ -1342,17 +1417,58 @@
end
-subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
+subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
+
+definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
+ "Min = fold1 min"
-text{*
- As an application of @{text fold1} we define minimum
- and maximum in (not necessarily complete!) linear orders
- over (non-empty) sets by means of @{text fold1}.
-*}
+definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
+ "Max = fold1 max"
+
+sublocale linorder < Min!: semilattice_big min Min proof
+qed (simp add: Min_def)
+
+sublocale linorder < Max!: semilattice_big max Max proof
+qed (simp add: Max_def)
context linorder
begin
+lemmas Min_singleton = Min.singleton
+lemmas Max_singleton = Max.singleton
+
+lemma Min_insert:
+ assumes "finite A" and "A \<noteq> {}"
+ shows "Min (insert x A) = min x (Min A)"
+ using assms by simp
+
+lemma Max_insert:
+ assumes "finite A" and "A \<noteq> {}"
+ shows "Max (insert x A) = max x (Max A)"
+ using assms by simp
+
+lemma Min_Un:
+ assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+ shows "Min (A \<union> B) = min (Min A) (Min B)"
+ using assms by (rule Min.union_idem)
+
+lemma Max_Un:
+ assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
+ shows "Max (A \<union> B) = max (Max A) (Max B)"
+ using assms by (rule Max.union_idem)
+
+lemma hom_Min_commute:
+ assumes "\<And>x y. h (min x y) = min (h x) (h y)"
+ and "finite N" and "N \<noteq> {}"
+ shows "h (Min N) = Min (h ` N)"
+ using assms by (rule Min.hom_commute)
+
+lemma hom_Max_commute:
+ assumes "\<And>x y. h (max x y) = max (h x) (h y)"
+ and "finite N" and "N \<noteq> {}"
+ shows "h (Max N) = Max (h ` N)"
+ using assms by (rule Max.hom_commute)
+
lemma ab_semigroup_idem_mult_min:
"ab_semigroup_idem_mult min"
proof qed (auto simp add: min_def)
@@ -1429,37 +1545,6 @@
finally show ?thesis .
qed
-definition
- Min :: "'a set \<Rightarrow> 'a"
-where
- "Min = fold1 min"
-
-definition
- Max :: "'a set \<Rightarrow> 'a"
-where
- "Max = fold1 max"
-
-lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
-lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
-
-lemma Min_insert [simp]:
- assumes "finite A" and "A \<noteq> {}"
- shows "Min (insert x A) = min x (Min A)"
-proof -
- interpret ab_semigroup_idem_mult min
- by (rule ab_semigroup_idem_mult_min)
- from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
-qed
-
-lemma Max_insert [simp]:
- assumes "finite A" and "A \<noteq> {}"
- shows "Max (insert x A) = max x (Max A)"
-proof -
- interpret ab_semigroup_idem_mult max
- by (rule ab_semigroup_idem_mult_max)
- from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
-qed
-
lemma Min_in [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A \<in> A"
@@ -1478,48 +1563,6 @@
from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
qed
-lemma Min_Un:
- assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
- shows "Min (A \<union> B) = min (Min A) (Min B)"
-proof -
- interpret ab_semigroup_idem_mult min
- by (rule ab_semigroup_idem_mult_min)
- from assms show ?thesis
- by (simp add: Min_def fold1_Un2)
-qed
-
-lemma Max_Un:
- assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
- shows "Max (A \<union> B) = max (Max A) (Max B)"
-proof -
- interpret ab_semigroup_idem_mult max
- by (rule ab_semigroup_idem_mult_max)
- from assms show ?thesis
- by (simp add: Max_def fold1_Un2)
-qed
-
-lemma hom_Min_commute:
- assumes "\<And>x y. h (min x y) = min (h x) (h y)"
- and "finite N" and "N \<noteq> {}"
- shows "h (Min N) = Min (h ` N)"
-proof -
- interpret ab_semigroup_idem_mult min
- by (rule ab_semigroup_idem_mult_min)
- from assms show ?thesis
- by (simp add: Min_def hom_fold1_commute)
-qed
-
-lemma hom_Max_commute:
- assumes "\<And>x y. h (max x y) = max (h x) (h y)"
- and "finite N" and "N \<noteq> {}"
- shows "h (Max N) = Max (h ` N)"
-proof -
- interpret ab_semigroup_idem_mult max
- by (rule ab_semigroup_idem_mult_max)
- from assms show ?thesis
- by (simp add: Max_def hom_fold1_commute [of h])
-qed
-
lemma Min_le [simp]:
assumes "finite A" and "x \<in> A"
shows "Min A \<le> x"
--- a/src/HOL/Finite_Set.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Finite_Set.thy Thu Mar 18 13:57:00 2010 +0100
@@ -9,7 +9,7 @@
imports Power Option
begin
-subsection {* Definition and basic properties *}
+subsection {* Predicate for finite sets *}
inductive finite :: "'a set => bool"
where
@@ -171,8 +171,7 @@
lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
by(fastsimp simp: finite_conv_nat_seg_image)
-
-subsubsection{* Finiteness and set theoretic constructions *}
+text {* Finiteness and set theoretic constructions *}
lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
by (induct set: finite) simp_all
@@ -567,7 +566,7 @@
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-subsection {* A fold functional for finite sets *}
+subsection {* A basic fold functional for finite sets *}
text {* The intended behaviour is
@{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
@@ -826,63 +825,122 @@
end
-context ab_semigroup_idem_mult
-begin
+
+subsubsection {* Expressing set operations via @{const fold} *}
+
+lemma (in fun_left_comm) fun_left_comm_apply:
+ "fun_left_comm (\<lambda>x. f (g x))"
+proof
+qed (simp_all add: fun_left_comm)
+
+lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
+ "fun_left_comm_idem (\<lambda>x. f (g x))"
+ by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
+ (simp_all add: fun_left_idem)
+
+lemma fun_left_comm_idem_insert:
+ "fun_left_comm_idem insert"
+proof
+qed auto
+
+lemma fun_left_comm_idem_remove:
+ "fun_left_comm_idem (\<lambda>x A. A - {x})"
+proof
+qed auto
-lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
-apply unfold_locales
- apply (rule mult_left_commute)
-apply (rule mult_left_idem)
-done
+lemma (in semilattice_inf) fun_left_comm_idem_inf:
+ "fun_left_comm_idem inf"
+proof
+qed (auto simp add: inf_left_commute)
+
+lemma (in semilattice_sup) fun_left_comm_idem_sup:
+ "fun_left_comm_idem sup"
+proof
+qed (auto simp add: sup_left_commute)
-end
+lemma union_fold_insert:
+ assumes "finite A"
+ shows "A \<union> B = fold insert B A"
+proof -
+ interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
+ from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
+qed
-context semilattice_inf
+lemma minus_fold_remove:
+ assumes "finite A"
+ shows "B - A = fold (\<lambda>x A. A - {x}) B A"
+proof -
+ interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+ from `finite A` show ?thesis by (induct A arbitrary: B) auto
+qed
+
+context complete_lattice
begin
-lemma ab_semigroup_idem_mult_inf: "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)"
-by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
-
-lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred: finite) (auto intro: le_infI1)
+lemma inf_Inf_fold_inf:
+ assumes "finite A"
+ shows "inf B (Inf A) = fold inf B A"
+proof -
+ interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
+qed
-lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
-proof(induct arbitrary: a pred:finite)
- case empty thus ?case by simp
-next
- case (insert x A)
- show ?case
- proof cases
- assume "A = {}" thus ?thesis using insert by simp
- next
- assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
- qed
+lemma sup_Sup_fold_sup:
+ assumes "finite A"
+ shows "sup B (Sup A) = fold sup B A"
+proof -
+ interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
qed
-end
+lemma Inf_fold_inf:
+ assumes "finite A"
+ shows "Inf A = fold inf top A"
+ using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
+ assumes "finite A"
+ shows "Sup A = fold sup bot A"
+ using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-context semilattice_sup
-begin
-
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
-by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
+lemma inf_INFI_fold_inf:
+ assumes "finite A"
+ shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold")
+proof (rule sym)
+ interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+ interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?inf"
+ by (induct A arbitrary: B)
+ (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
+qed
-lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
-by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
+lemma sup_SUPR_fold_sup:
+ assumes "finite A"
+ shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold")
+proof (rule sym)
+ interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+ interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?sup"
+ by (induct A arbitrary: B)
+ (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
+qed
-lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
-by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
+lemma INFI_fold_inf:
+ assumes "finite A"
+ shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
+ using assms inf_INFI_fold_inf [of A top] by simp
-lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
-by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
+lemma SUPR_fold_sup:
+ assumes "finite A"
+ shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
+ using assms sup_SUPR_fold_sup [of A bot] by simp
end
-subsubsection{* The derived combinator @{text fold_image} *}
+subsection {* The derived combinator @{text fold_image} *}
definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
where "fold_image f g = fold (%x y. f (g x) y)"
@@ -969,6 +1027,11 @@
context comm_monoid_mult
begin
+lemma fold_image_1:
+ "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
+ apply (induct set: finite)
+ apply simp by auto
+
lemma fold_image_Un_Int:
"finite A ==> finite B ==>
fold_image times g 1 A * fold_image times g 1 B =
@@ -976,6 +1039,17 @@
by (induct set: finite)
(auto simp add: mult_ac insert_absorb Int_insert_left)
+lemma fold_image_Un_one:
+ assumes fS: "finite S" and fT: "finite T"
+ and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
+ shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
+proof-
+ have "fold_image op * f 1 (S \<inter> T) = 1"
+ apply (rule fold_image_1)
+ using fS fT I0 by auto
+ with fold_image_Un_Int[OF fS fT] show ?thesis by simp
+qed
+
corollary fold_Un_disjoint:
"finite A ==> finite B ==> A Int B = {} ==>
fold_image times g 1 (A Un B) =
@@ -1061,7 +1135,7 @@
end
-subsection{* A fold functional for non-empty sets *}
+subsection {* A fold functional for non-empty sets *}
text{* Does not require start value. *}
@@ -1187,6 +1261,12 @@
context ab_semigroup_idem_mult
begin
+lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
+apply unfold_locales
+ apply (rule mult_left_commute)
+apply (rule mult_left_idem)
+done
+
lemma fold1_insert_idem [simp]:
assumes nonempty: "A \<noteq> {}" and A: "finite A"
shows "fold1 times (insert x A) = x * fold1 times A"
@@ -1354,138 +1434,17 @@
qed
-subsection {* Expressing set operations via @{const fold} *}
-
-lemma (in fun_left_comm) fun_left_comm_apply:
- "fun_left_comm (\<lambda>x. f (g x))"
-proof
-qed (simp_all add: fun_left_comm)
-
-lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
- "fun_left_comm_idem (\<lambda>x. f (g x))"
- by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
- (simp_all add: fun_left_idem)
-
-lemma fun_left_comm_idem_insert:
- "fun_left_comm_idem insert"
-proof
-qed auto
-
-lemma fun_left_comm_idem_remove:
- "fun_left_comm_idem (\<lambda>x A. A - {x})"
-proof
-qed auto
-
-lemma (in semilattice_inf) fun_left_comm_idem_inf:
- "fun_left_comm_idem inf"
-proof
-qed (auto simp add: inf_left_commute)
-
-lemma (in semilattice_sup) fun_left_comm_idem_sup:
- "fun_left_comm_idem sup"
-proof
-qed (auto simp add: sup_left_commute)
-
-lemma union_fold_insert:
- assumes "finite A"
- shows "A \<union> B = fold insert B A"
-proof -
- interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
- from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
-qed
-
-lemma minus_fold_remove:
- assumes "finite A"
- shows "B - A = fold (\<lambda>x A. A - {x}) B A"
-proof -
- interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
- from `finite A` show ?thesis by (induct A arbitrary: B) auto
-qed
-
-context complete_lattice
-begin
+subsection {* Locales as mini-packages for fold operations *}
-lemma inf_Inf_fold_inf:
- assumes "finite A"
- shows "inf B (Inf A) = fold inf B A"
-proof -
- interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
- from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
-qed
-
-lemma sup_Sup_fold_sup:
- assumes "finite A"
- shows "sup B (Sup A) = fold sup B A"
-proof -
- interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
- from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
-qed
-
-lemma Inf_fold_inf:
- assumes "finite A"
- shows "Inf A = fold inf top A"
- using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
-
-lemma Sup_fold_sup:
- assumes "finite A"
- shows "Sup A = fold sup bot A"
- using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-
-lemma inf_INFI_fold_inf:
- assumes "finite A"
- shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold")
-proof (rule sym)
- interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
- interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
- from `finite A` show "?fold = ?inf"
- by (induct A arbitrary: B)
- (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
-qed
-
-lemma sup_SUPR_fold_sup:
- assumes "finite A"
- shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold")
-proof (rule sym)
- interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
- interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
- from `finite A` show "?fold = ?sup"
- by (induct A arbitrary: B)
- (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
-qed
-
-lemma INFI_fold_inf:
- assumes "finite A"
- shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
- using assms inf_INFI_fold_inf [of A top] by simp
-
-lemma SUPR_fold_sup:
- assumes "finite A"
- shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
- using assms sup_SUPR_fold_sup [of A bot] by simp
-
-end
-
-
-subsection {* Locales as mini-packages *}
+subsubsection {* The natural case *}
locale folding =
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes commute_comp: "f x \<circ> f y = f y \<circ> f x"
+ assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A"
begin
-lemma fun_left_commute:
- "f x (f y s) = f y (f x s)"
- using commute_comp [of x y] by (simp add: expand_fun_eq)
-
-lemma fun_left_comm:
- "fun_left_comm f"
-proof
-qed (fact fun_left_commute)
-
lemma empty [simp]:
"F {} = id"
by (simp add: eq_fold expand_fun_eq)
@@ -1494,7 +1453,8 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = F A \<circ> f x"
proof -
- interpret fun_left_comm f by (fact fun_left_comm)
+ interpret fun_left_comm f proof
+ qed (insert commute_comp, simp add: expand_fun_eq)
from fold_insert2 assms
have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
with `finite A` show ?thesis by (simp add: eq_fold expand_fun_eq)
@@ -1515,89 +1475,112 @@
shows "F (insert x A) = F (A - {x}) \<circ> f x"
using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
+lemma commute_left_comp:
+ "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
+ by (simp add: o_assoc commute_comp)
+
lemma commute_comp':
assumes "finite A"
shows "f x \<circ> F A = F A \<circ> f x"
-proof (rule ext)
- fix s
- from assms show "(f x \<circ> F A) s = (F A \<circ> f x) s"
- by (induct A arbitrary: s) (simp_all add: fun_left_commute)
-qed
+ using assms by (induct A)
+ (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] commute_comp)
+
+lemma commute_left_comp':
+ assumes "finite A"
+ shows "f x \<circ> (F A \<circ> g) = F A \<circ> (f x \<circ> g)"
+ using assms by (simp add: o_assoc commute_comp')
+
+lemma commute_comp'':
+ assumes "finite A" and "finite B"
+ shows "F B \<circ> F A = F A \<circ> F B"
+ using assms by (induct A)
+ (simp_all add: o_assoc, simp add: o_assoc [symmetric] commute_comp')
-lemma fun_left_commute':
- assumes "finite A"
- shows "f x (F A s) = F A (f x s)"
- using commute_comp' assms by (simp add: expand_fun_eq)
+lemma commute_left_comp'':
+ assumes "finite A" and "finite B"
+ shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
+ using assms by (simp add: o_assoc commute_comp'')
+
+lemmas commute_comps = o_assoc [symmetric] commute_comp commute_left_comp
+ commute_comp' commute_left_comp' commute_comp'' commute_left_comp''
+
+lemma union_inter:
+ assumes "finite A" and "finite B"
+ shows "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B"
+ using assms by (induct A)
+ (simp_all del: o_apply add: insert_absorb Int_insert_left commute_comps,
+ simp add: o_assoc)
lemma union:
assumes "finite A" and "finite B"
and "A \<inter> B = {}"
shows "F (A \<union> B) = F A \<circ> F B"
-using `finite A` `A \<inter> B = {}` proof (induct A)
- case empty show ?case by simp
-next
- case (insert x A)
- then have "A \<inter> B = {}" by auto
- with insert(3) have "F (A \<union> B) = F A \<circ> F B" .
- moreover from insert have "x \<notin> B" by simp
- moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
- moreover from `x \<notin> A` `x \<notin> B` have "x \<notin> A \<union> B" by simp
- ultimately show ?case by (simp add: fun_left_commute')
+proof -
+ from union_inter `finite A` `finite B` have "F (A \<union> B) \<circ> F (A \<inter> B) = F A \<circ> F B" .
+ with `A \<inter> B = {}` show ?thesis by simp
qed
end
+
+subsubsection {* The natural case with idempotency *}
+
locale folding_idem = folding +
assumes idem_comp: "f x \<circ> f x = f x"
begin
-declare insert [simp del]
+lemma idem_left_comp:
+ "f x \<circ> (f x \<circ> g) = f x \<circ> g"
+ by (simp add: o_assoc idem_comp)
+
+lemma in_comp_idem:
+ assumes "finite A" and "x \<in> A"
+ shows "F A \<circ> f x = F A"
+using assms by (induct A)
+ (auto simp add: commute_comps idem_comp, simp add: commute_left_comp' [symmetric] commute_comp')
-lemma fun_idem:
- "f x (f x s) = f x s"
- using idem_comp [of x] by (simp add: expand_fun_eq)
+lemma subset_comp_idem:
+ assumes "finite A" and "B \<subseteq> A"
+ shows "F A \<circ> F B = F A"
+proof -
+ from assms have "finite B" by (blast dest: finite_subset)
+ then show ?thesis using `B \<subseteq> A` by (induct B)
+ (simp_all add: o_assoc in_comp_idem `finite A`)
+qed
-lemma fun_left_comm_idem:
- "fun_left_comm_idem f"
-proof
-qed (fact fun_left_commute fun_idem)+
+declare insert [simp del]
lemma insert_idem [simp]:
assumes "finite A"
shows "F (insert x A) = F A \<circ> f x"
-proof -
- interpret fun_left_comm_idem f by (fact fun_left_comm_idem)
- from fold_insert_idem2 assms
- have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
- with assms show ?thesis by (simp add: eq_fold expand_fun_eq)
-qed
+ using assms by (cases "x \<in> A") (simp_all add: insert in_comp_idem insert_absorb)
lemma union_idem:
assumes "finite A" and "finite B"
shows "F (A \<union> B) = F A \<circ> F B"
-using `finite A` proof (induct A)
- case empty show ?case by simp
-next
- case (insert x A)
- from insert(3) have "F (A \<union> B) = F A \<circ> F B" .
- moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
- ultimately show ?case by (simp add: fun_left_commute')
+proof -
+ from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+ then have "F (A \<union> B) \<circ> F (A \<inter> B) = F (A \<union> B)" by (rule subset_comp_idem)
+ with assms show ?thesis by (simp add: union_inter)
qed
end
+
+subsubsection {* The image case with fixed function *}
+
no_notation times (infixl "*" 70)
no_notation Groups.one ("1")
locale folding_image_simple = comm_monoid +
fixes g :: "('b \<Rightarrow> 'a)"
fixes F :: "'b set \<Rightarrow> 'a"
- assumes eq_fold: "finite A \<Longrightarrow> F A = fold_image f g 1 A"
+ assumes eq_fold_g: "finite A \<Longrightarrow> F A = fold_image f g 1 A"
begin
lemma empty [simp]:
"F {} = 1"
- by (simp add: eq_fold)
+ by (simp add: eq_fold_g)
lemma insert [simp]:
assumes "finite A" and "x \<notin> A"
@@ -1607,7 +1590,7 @@
qed (simp add: ac_simps)
with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
by (simp add: fold_image_def)
- with `finite A` show ?thesis by (simp add: eq_fold)
+ with `finite A` show ?thesis by (simp add: eq_fold_g)
qed
lemma remove:
@@ -1625,9 +1608,14 @@
shows "F (insert x A) = g x * F (A - {x})"
using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
+lemma neutral:
+ assumes "finite A" and "\<forall>x\<in>A. g x = 1"
+ shows "F A = 1"
+ using assms by (induct A) simp_all
+
lemma union_inter:
assumes "finite A" and "finite B"
- shows "F A * F B = F (A \<union> B) * F (A \<inter> B)"
+ shows "F (A \<union> B) * F (A \<inter> B) = F A * F B"
using assms proof (induct A)
case empty then show ?case by simp
next
@@ -1635,14 +1623,23 @@
by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
qed
+corollary union_inter_neutral:
+ assumes "finite A" and "finite B"
+ and I0: "\<forall>x \<in> A\<inter>B. g x = 1"
+ shows "F (A \<union> B) = F A * F B"
+ using assms by (simp add: union_inter [symmetric] neutral)
+
corollary union_disjoint:
assumes "finite A" and "finite B"
assumes "A \<inter> B = {}"
shows "F (A \<union> B) = F A * F B"
- using assms by (simp add: union_inter)
+ using assms by (simp add: union_inter_neutral)
end
+
+subsubsection {* The image case with flexible function *}
+
locale folding_image = comm_monoid +
fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
assumes eq_fold: "\<And>g. finite A \<Longrightarrow> F g A = fold_image f g 1 A"
@@ -1653,7 +1650,7 @@
context folding_image
begin
-lemma reindex:
+lemma reindex: (* FIXME polymorhism *)
assumes "finite A" and "inj_on h A"
shows "F g (h ` A) = F (g \<circ> h) A"
using assms by (induct A) auto
@@ -1742,6 +1739,229 @@
end
+
+subsubsection {* The image case with fixed function and idempotency *}
+
+locale folding_image_simple_idem = folding_image_simple +
+ assumes idem: "x * x = x"
+
+sublocale folding_image_simple_idem < semilattice proof
+qed (fact idem)
+
+context folding_image_simple_idem
+begin
+
+lemma in_idem:
+ assumes "finite A" and "x \<in> A"
+ shows "g x * F A = F A"
+ using assms by (induct A) (auto simp add: left_commute)
+
+lemma subset_idem:
+ assumes "finite A" and "B \<subseteq> A"
+ shows "F B * F A = F A"
+proof -
+ from assms have "finite B" by (blast dest: finite_subset)
+ then show ?thesis using `B \<subseteq> A` by (induct B)
+ (auto simp add: assoc in_idem `finite A`)
+qed
+
+declare insert [simp del]
+
+lemma insert_idem [simp]:
+ assumes "finite A"
+ shows "F (insert x A) = g x * F A"
+ using assms by (cases "x \<in> A") (simp_all add: insert in_idem insert_absorb)
+
+lemma union_idem:
+ assumes "finite A" and "finite B"
+ shows "F (A \<union> B) = F A * F B"
+proof -
+ from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+ then have "F (A \<inter> B) * F (A \<union> B) = F (A \<union> B)" by (rule subset_idem)
+ with assms show ?thesis by (simp add: union_inter [of A B, symmetric] commute)
+qed
+
+end
+
+
+subsubsection {* The image case with flexible function and idempotency *}
+
+locale folding_image_idem = folding_image +
+ assumes idem: "x * x = x"
+
+sublocale folding_image_idem < folding_image_simple_idem "op *" 1 g "F g" proof
+qed (fact idem)
+
+
+subsubsection {* The neutral-less case *}
+
+locale folding_one = abel_semigroup +
+ fixes F :: "'a set \<Rightarrow> 'a"
+ assumes eq_fold: "finite A \<Longrightarrow> F A = fold1 f A"
+begin
+
+lemma singleton [simp]:
+ "F {x} = x"
+ by (simp add: eq_fold)
+
+lemma eq_fold':
+ assumes "finite A" and "x \<notin> A"
+ shows "F (insert x A) = fold (op *) x A"
+proof -
+ interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps)
+ with assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
+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
+ 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
+ qed (simp_all add: expand_fun_eq ac_simps)
+ thm fold.commute_comp' [of B b, simplified expand_fun_eq, simplified]
+ from `finite B` fold.commute_comp' [of B x]
+ have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
+ then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: expand_fun_eq commute)
+ from `finite B` * fold.insert [of B b]
+ have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp
+ then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: expand_fun_eq)
+ from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert)
+qed
+
+lemma remove:
+ assumes "finite A" and "x \<in> A"
+ shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
+proof -
+ from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
+ with assms show ?thesis by simp
+qed
+
+lemma insert_remove:
+ assumes "finite A"
+ shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
+ using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
+
+lemma union_disjoint:
+ assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}" and "A \<inter> B = {}"
+ shows "F (A \<union> B) = F A * F B"
+ using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
+
+lemma union_inter:
+ assumes "finite A" and "finite B" and "A \<inter> B \<noteq> {}"
+ shows "F (A \<union> B) * F (A \<inter> B) = F A * F B"
+proof -
+ from assms have "A \<noteq> {}" and "B \<noteq> {}" by auto
+ from `finite A` `A \<noteq> {}` `A \<inter> B \<noteq> {}` show ?thesis proof (induct A rule: finite_ne_induct)
+ case (singleton x) then show ?case by (simp add: insert_absorb ac_simps)
+ next
+ case (insert x A) show ?case proof (cases "x \<in> B")
+ case True then have "B \<noteq> {}" by auto
+ with insert True `finite B` show ?thesis by (cases "A \<inter> B = {}")
+ (simp_all add: insert_absorb ac_simps union_disjoint)
+ next
+ case False with insert have "F (A \<union> B) * F (A \<inter> B) = F A * F B" by simp
+ moreover from False `finite B` insert have "finite (A \<union> B)" "x \<notin> A \<union> B" "A \<union> B \<noteq> {}"
+ by auto
+ ultimately show ?thesis using False `finite A` `x \<notin> A` `A \<noteq> {}` by (simp add: assoc)
+ qed
+ qed
+qed
+
+lemma closed:
+ assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+ shows "F A \<in> A"
+using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
+ case singleton then show ?case by simp
+next
+ case insert with elem show ?case by force
+qed
+
+end
+
+
+subsubsection {* The neutral-less case with idempotency *}
+
+locale folding_one_idem = folding_one +
+ assumes idem: "x * x = x"
+
+sublocale folding_one_idem < semilattice proof
+qed (fact idem)
+
+context folding_one_idem
+begin
+
+lemma in_idem:
+ assumes "finite A" and "x \<in> A"
+ shows "x * F A = F A"
+proof -
+ from assms have "A \<noteq> {}" by auto
+ with `finite A` show ?thesis using `x \<in> A` by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
+qed
+
+lemma subset_idem:
+ assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
+ shows "F B * F A = F A"
+proof -
+ from assms have "finite B" by (blast dest: finite_subset)
+ then show ?thesis using `B \<noteq> {}` `B \<subseteq> A` by (induct B rule: finite_ne_induct)
+ (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"
+proof -
+ interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps)
+ with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
+qed
+
+lemma insert_idem [simp]:
+ assumes "finite A"
+ shows "F (insert x A) = (if A = {} then x else x * F A)"
+proof (cases "x \<in> A")
+ case False with `finite A` 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)
+qed
+
+lemma union_idem:
+ assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
+ shows "F (A \<union> B) = F A * F B"
+proof (cases "A \<inter> B = {}")
+ case True with assms show ?thesis by (simp add: union_disjoint)
+next
+ case False
+ from assms have "finite (A \<union> B)" and "A \<inter> B \<subseteq> A \<union> B" by auto
+ with False have "F (A \<inter> B) * F (A \<union> B) = F (A \<union> B)" by (auto intro: subset_idem)
+ with assms False show ?thesis by (simp add: union_inter [of A B, symmetric] commute)
+qed
+
+lemma hom_commute:
+ assumes hom: "\<And>x y. h (x * y) = h x * h y"
+ and N: "finite N" "N \<noteq> {}" shows "h (F N) = F (h ` N)"
+using N proof (induct rule: finite_ne_induct)
+ case singleton thus ?case by simp
+next
+ case (insert n N)
+ then have "h (F (insert n N)) = h (n * F N)" by simp
+ also have "\<dots> = h n * h (F N)" by (rule hom)
+ also have "h (F N) = F (h ` N)" by(rule insert)
+ also have "h n * \<dots> = F (insert (h n) (h ` N))"
+ using insert by(simp)
+ also have "insert (h n) (h ` N) = h ` insert n N" by simp
+ finally show ?case .
+qed
+
+end
+
notation times (infixl "*" 70)
notation Groups.one ("1")
@@ -1854,7 +2074,7 @@
lemma card_Un_Int: "finite A ==> finite B
==> card A + card B = card (A Un B) + card (A Int B)"
- by (fact card.union_inter)
+ by (fact card.union_inter [symmetric])
lemma card_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> card (A Un B) = card A + card B"
--- a/src/HOL/Matrix/Matrix.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy Thu Mar 18 13:57:00 2010 +0100
@@ -1015,7 +1015,7 @@
apply (subst foldseq_almostzero[of _ j])
apply (simp add: assms)+
apply (auto)
- apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+ apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
done
lemma mult_matrix_ext:
--- a/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.cert Thu Mar 18 13:57:00 2010 +0100
@@ -3506,3 +3506,215 @@
#328 := [unit-resolution #319 #327]: #300
[th-lemma #326 #334 #195 #328 #187 #138]: false
unsat
+WrIjxhfF5EcRCmS6xKG3XQ 211 0
+#2 := false
+#33 := 0::real
+decl uf_11 :: (-> T5 T6 real)
+decl uf_15 :: T6
+#28 := uf_15
+decl uf_16 :: T5
+#30 := uf_16
+#31 := (uf_11 uf_16 uf_15)
+decl uf_12 :: (-> T7 T8 T5)
+decl uf_14 :: T8
+#26 := uf_14
+decl uf_13 :: (-> T1 T7)
+decl uf_8 :: T1
+#16 := uf_8
+#25 := (uf_13 uf_8)
+#27 := (uf_12 #25 uf_14)
+#29 := (uf_11 #27 uf_15)
+#73 := -1::real
+#84 := (* -1::real #29)
+#85 := (+ #84 #31)
+#74 := (* -1::real #31)
+#75 := (+ #29 #74)
+#112 := (>= #75 0::real)
+#119 := (ite #112 #75 #85)
+#127 := (* -1::real #119)
+decl uf_17 :: T5
+#37 := uf_17
+#38 := (uf_11 uf_17 uf_15)
+#102 := -1/3::real
+#103 := (* -1/3::real #38)
+#128 := (+ #103 #127)
+#100 := 1/3::real
+#101 := (* 1/3::real #31)
+#129 := (+ #101 #128)
+#130 := (<= #129 0::real)
+#131 := (not #130)
+#40 := 3::real
+#39 := (- #31 #38)
+#41 := (/ #39 3::real)
+#32 := (- #29 #31)
+#35 := (- #32)
+#34 := (< #32 0::real)
+#36 := (ite #34 #35 #32)
+#42 := (< #36 #41)
+#136 := (iff #42 #131)
+#104 := (+ #101 #103)
+#78 := (< #75 0::real)
+#90 := (ite #78 #85 #75)
+#109 := (< #90 #104)
+#134 := (iff #109 #131)
+#124 := (< #119 #104)
+#132 := (iff #124 #131)
+#133 := [rewrite]: #132
+#125 := (iff #109 #124)
+#122 := (= #90 #119)
+#113 := (not #112)
+#116 := (ite #113 #85 #75)
+#120 := (= #116 #119)
+#121 := [rewrite]: #120
+#117 := (= #90 #116)
+#114 := (iff #78 #113)
+#115 := [rewrite]: #114
+#118 := [monotonicity #115]: #117
+#123 := [trans #118 #121]: #122
+#126 := [monotonicity #123]: #125
+#135 := [trans #126 #133]: #134
+#110 := (iff #42 #109)
+#107 := (= #41 #104)
+#93 := (* -1::real #38)
+#94 := (+ #31 #93)
+#97 := (/ #94 3::real)
+#105 := (= #97 #104)
+#106 := [rewrite]: #105
+#98 := (= #41 #97)
+#95 := (= #39 #94)
+#96 := [rewrite]: #95
+#99 := [monotonicity #96]: #98
+#108 := [trans #99 #106]: #107
+#91 := (= #36 #90)
+#76 := (= #32 #75)
+#77 := [rewrite]: #76
+#88 := (= #35 #85)
+#81 := (- #75)
+#86 := (= #81 #85)
+#87 := [rewrite]: #86
+#82 := (= #35 #81)
+#83 := [monotonicity #77]: #82
+#89 := [trans #83 #87]: #88
+#79 := (iff #34 #78)
+#80 := [monotonicity #77]: #79
+#92 := [monotonicity #80 #89 #77]: #91
+#111 := [monotonicity #92 #108]: #110
+#137 := [trans #111 #135]: #136
+#72 := [asserted]: #42
+#138 := [mp #72 #137]: #131
+decl uf_1 :: T1
+#4 := uf_1
+#43 := (uf_13 uf_1)
+#44 := (uf_12 #43 uf_14)
+#45 := (uf_11 #44 uf_15)
+#149 := (* -1::real #45)
+#150 := (+ #38 #149)
+#140 := (+ #93 #45)
+#161 := (<= #150 0::real)
+#168 := (ite #161 #140 #150)
+#176 := (* -1::real #168)
+#177 := (+ #103 #176)
+#178 := (+ #101 #177)
+#179 := (<= #178 0::real)
+#180 := (not #179)
+#46 := (- #45 #38)
+#48 := (- #46)
+#47 := (< #46 0::real)
+#49 := (ite #47 #48 #46)
+#50 := (< #49 #41)
+#185 := (iff #50 #180)
+#143 := (< #140 0::real)
+#155 := (ite #143 #150 #140)
+#158 := (< #155 #104)
+#183 := (iff #158 #180)
+#173 := (< #168 #104)
+#181 := (iff #173 #180)
+#182 := [rewrite]: #181
+#174 := (iff #158 #173)
+#171 := (= #155 #168)
+#162 := (not #161)
+#165 := (ite #162 #150 #140)
+#169 := (= #165 #168)
+#170 := [rewrite]: #169
+#166 := (= #155 #165)
+#163 := (iff #143 #162)
+#164 := [rewrite]: #163
+#167 := [monotonicity #164]: #166
+#172 := [trans #167 #170]: #171
+#175 := [monotonicity #172]: #174
+#184 := [trans #175 #182]: #183
+#159 := (iff #50 #158)
+#156 := (= #49 #155)
+#141 := (= #46 #140)
+#142 := [rewrite]: #141
+#153 := (= #48 #150)
+#146 := (- #140)
+#151 := (= #146 #150)
+#152 := [rewrite]: #151
+#147 := (= #48 #146)
+#148 := [monotonicity #142]: #147
+#154 := [trans #148 #152]: #153
+#144 := (iff #47 #143)
+#145 := [monotonicity #142]: #144
+#157 := [monotonicity #145 #154 #142]: #156
+#160 := [monotonicity #157 #108]: #159
+#186 := [trans #160 #184]: #185
+#139 := [asserted]: #50
+#187 := [mp #139 #186]: #180
+#299 := (+ #140 #176)
+#300 := (<= #299 0::real)
+#290 := (= #140 #168)
+#329 := [hypothesis]: #162
+#191 := (+ #29 #149)
+#192 := (<= #191 0::real)
+#51 := (<= #29 #45)
+#193 := (iff #51 #192)
+#194 := [rewrite]: #193
+#188 := [asserted]: #51
+#195 := [mp #188 #194]: #192
+#298 := (+ #75 #127)
+#301 := (<= #298 0::real)
+#284 := (= #75 #119)
+#302 := [hypothesis]: #113
+#296 := (+ #85 #127)
+#297 := (<= #296 0::real)
+#285 := (= #85 #119)
+#288 := (or #112 #285)
+#289 := [def-axiom]: #288
+#303 := [unit-resolution #289 #302]: #285
+#304 := (not #285)
+#305 := (or #304 #297)
+#306 := [th-lemma]: #305
+#307 := [unit-resolution #306 #303]: #297
+#315 := (not #290)
+#310 := (not #300)
+#311 := (or #310 #112)
+#308 := [hypothesis]: #300
+#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
+#312 := [lemma #309]: #311
+#322 := [unit-resolution #312 #302]: #310
+#316 := (or #315 #300)
+#313 := [hypothesis]: #310
+#314 := [hypothesis]: #290
+#317 := [th-lemma]: #316
+#318 := [unit-resolution #317 #314 #313]: false
+#319 := [lemma #318]: #316
+#323 := [unit-resolution #319 #322]: #315
+#292 := (or #162 #290)
+#293 := [def-axiom]: #292
+#324 := [unit-resolution #293 #323]: #162
+#325 := [th-lemma #324 #307 #138 #302 #195]: false
+#326 := [lemma #325]: #112
+#286 := (or #113 #284)
+#287 := [def-axiom]: #286
+#330 := [unit-resolution #287 #326]: #284
+#331 := (not #284)
+#332 := (or #331 #301)
+#333 := [th-lemma]: #332
+#334 := [unit-resolution #333 #330]: #301
+#335 := [th-lemma #326 #334 #195 #329 #138]: false
+#336 := [lemma #335]: #161
+#327 := [unit-resolution #293 #336]: #290
+#328 := [unit-resolution #319 #327]: #300
+[th-lemma #326 #334 #195 #328 #187 #138]: false
+unsat
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Mar 18 13:57:00 2010 +0100
@@ -1459,7 +1459,7 @@
{ fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
hence "f (a + x) \<in> S" using d
apply(erule_tac x="x+a" in allE)
- by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+ by (auto simp add: add_commute dist_norm dist_commute)
}
hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
using d(1) by auto
@@ -1476,7 +1476,7 @@
unfolding Limits.eventually_at by fast
{ fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
- by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+ by(auto simp add: add_commute dist_norm dist_commute)
}
hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
@@ -2755,8 +2755,8 @@
have "d>0" using `e>0` unfolding d_def e_def using zero_le_dist[of _ l', unfolded order_le_less] by auto
obtain k where k:"f k \<noteq> l'" "dist (f k) l' < d" using `d>0` and assms(3)[unfolded islimpt_approachable, THEN spec[where x="d"]] by auto
have "k\<ge>N" using k(1)[unfolded dist_nz] using k(2)[unfolded d_def]
- by force
- hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by auto
+ by (force simp del: Min.insert_idem)
+ hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by (auto simp del: Min.insert_idem)
thus False unfolding e_def by auto
qed
--- a/src/HOL/Nat_Transfer.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Nat_Transfer.thy Thu Mar 18 13:57:00 2010 +0100
@@ -10,12 +10,13 @@
subsection {* Generic transfer machinery *}
-definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "transfer_morphism f A \<longleftrightarrow> True"
+definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "transfer_morphism f A \<longleftrightarrow> (\<forall>P. (\<forall>x. P x) \<longrightarrow> (\<forall>y. A y \<longrightarrow> P (f y)))"
lemma transfer_morphismI:
- "transfer_morphism f A"
- by (simp add: transfer_morphism_def)
+ assumes "\<And>P y. (\<And>x. P x) \<Longrightarrow> A y \<Longrightarrow> P (f y)"
+ shows "transfer_morphism f A"
+ using assms by (auto simp add: transfer_morphism_def)
use "Tools/transfer.ML"
@@ -27,7 +28,7 @@
text {* set up transfer direction *}
lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
- by (fact transfer_morphismI)
+ by (rule transfer_morphismI) simp
declare transfer_morphism_nat_int [transfer add
mode: manual
@@ -266,7 +267,7 @@
text {* set up transfer direction *}
lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
- by (fact transfer_morphismI)
+by (rule transfer_morphismI) simp
declare transfer_morphism_int_nat [transfer add
mode: manual
--- a/src/HOL/Product_Type.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 18 13:57:00 2010 +0100
@@ -998,6 +998,15 @@
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
by (auto, rule_tac p = "f x" in PairE, auto)
+lemma swap_inj_on:
+ "inj_on (%(i, j). (j, i)) (A \<times> B)"
+ by (unfold inj_on_def) fast
+
+lemma swap_product:
+ "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
+ by (simp add: split_def image_def) blast
+
+
subsubsection {* Code generator setup *}
lemma [code]:
--- a/src/HOL/SupInf.thy Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/SupInf.thy Thu Mar 18 13:57:00 2010 +0100
@@ -355,13 +355,13 @@
lemma Inf_greater:
fixes z :: real
- shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+ shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
by (metis Inf_real_iff mem_def not_leE)
lemma Inf_close:
fixes e :: real
shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
- by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
+ by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
lemma Inf_finite_Min:
fixes S :: "real set"
@@ -417,7 +417,7 @@
also have "... \<le> e"
apply (rule Sup_asclose)
apply (auto simp add: S)
- apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def)
+ apply (metis abs_minus_add_cancel b add_commute real_diff_def)
done
finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
thus ?thesis
--- a/src/HOL/Tools/transfer.ML Wed Mar 17 19:55:07 2010 +0100
+++ b/src/HOL/Tools/transfer.ML Thu Mar 18 13:57:00 2010 +0100
@@ -23,11 +23,13 @@
val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of;
+val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI});
+
fun check_morphism_key ctxt key =
let
- val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key)
- handle Pattern.MATCH => error
- ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
+ val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key)
+ handle Pattern.MATCH => error ("Transfer: expected theorem of the form "
+ ^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key)));
in direction_of key end;
type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,