tuned: unnamed contexts, interpretation and sublocale in locale target;
authorhaftmann
Tue Apr 23 11:14:51 2013 +0200 (2013-04-23)
changeset 517389e4220605179
parent 51737 718866dda2fa
child 51739 3514b90d0a8b
tuned: unnamed contexts, interpretation and sublocale in locale target;
corrected slip in List.thy: setsum requires commmutativity
src/HOL/Big_Operators.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Apr 23 11:14:50 2013 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Apr 23 11:14:51 2013 +0200
     1.3 @@ -17,6 +17,12 @@
     1.4  locale comm_monoid_set = comm_monoid
     1.5  begin
     1.6  
     1.7 +interpretation comp_fun_commute f
     1.8 +  by default (simp add: fun_eq_iff left_commute)
     1.9 +
    1.10 +interpretation comp_fun_commute "f \<circ> g"
    1.11 +  by (rule comp_comp_fun_commute)
    1.12 +
    1.13  definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    1.14  where
    1.15    eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    1.16 @@ -32,13 +38,7 @@
    1.17  lemma insert [simp]:
    1.18    assumes "finite A" and "x \<notin> A"
    1.19    shows "F g (insert x A) = g x * F g A"
    1.20 -proof -
    1.21 -  interpret comp_fun_commute f
    1.22 -    by default (simp add: fun_eq_iff left_commute)
    1.23 -  interpret comp_fun_commute "f \<circ> g"
    1.24 -    by (rule comp_comp_fun_commute)
    1.25 -  from assms show ?thesis by (simp add: eq_fold)
    1.26 -qed
    1.27 +  using assms by (simp add: eq_fold)
    1.28  
    1.29  lemma remove:
    1.30    assumes "finite A" and "x \<in> A"
    1.31 @@ -58,11 +58,7 @@
    1.32  lemma neutral:
    1.33    assumes "\<forall>x\<in>A. g x = 1"
    1.34    shows "F g A = 1"
    1.35 -proof (cases "finite A")
    1.36 -  case True from `finite A` assms show ?thesis by (induct A) simp_all
    1.37 -next
    1.38 -  case False then show ?thesis by simp
    1.39 -qed
    1.40 +  using assms by (induct A rule: infinite_finite_induct) simp_all
    1.41  
    1.42  lemma neutral_const [simp]:
    1.43    "F (\<lambda>_. 1) A = 1"
    1.44 @@ -100,11 +96,7 @@
    1.45    shows "F g (h ` A) = F (g \<circ> h) A"
    1.46  proof (cases "finite A")
    1.47    case True
    1.48 -  interpret comp_fun_commute f
    1.49 -    by default (simp add: fun_eq_iff left_commute)
    1.50 -  interpret comp_fun_commute "f \<circ> g"
    1.51 -    by (rule comp_comp_fun_commute)
    1.52 -  from assms `finite A` show ?thesis by (simp add: eq_fold fold_image comp_assoc)
    1.53 +  with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
    1.54  next
    1.55    case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
    1.56    with False show ?thesis by simp
    1.57 @@ -168,11 +160,7 @@
    1.58  
    1.59  lemma distrib:
    1.60    "F (\<lambda>x. g x * h x) A = F g A * F h A"
    1.61 -proof (cases "finite A")
    1.62 -  case False then show ?thesis by simp
    1.63 -next
    1.64 -  case True then show ?thesis by (rule finite_induct) (simp_all add: assoc commute left_commute)
    1.65 -qed
    1.66 +  using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
    1.67  
    1.68  lemma Sigma:
    1.69    "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
    1.70 @@ -319,11 +307,14 @@
    1.71  
    1.72  subsection {* Generalized summation over a set *}
    1.73  
    1.74 -definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    1.75 +context comm_monoid_add
    1.76 +begin
    1.77 +
    1.78 +definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    1.79  where
    1.80    "setsum = comm_monoid_set.F plus 0"
    1.81  
    1.82 -sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0
    1.83 +sublocale setsum!: comm_monoid_set plus 0
    1.84  where
    1.85    "comm_monoid_set.F plus 0 = setsum"
    1.86  proof -
    1.87 @@ -336,6 +327,8 @@
    1.88    Setsum ("\<Sum>_" [1000] 999) where
    1.89    "\<Sum>A \<equiv> setsum (%x. x) A"
    1.90  
    1.91 +end
    1.92 +
    1.93  text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    1.94  written @{text"\<Sum>x\<in>A. e"}. *}
    1.95  
    1.96 @@ -1050,11 +1043,14 @@
    1.97  
    1.98  subsection {* Generalized product over a set *}
    1.99  
   1.100 -definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   1.101 +context comm_monoid_mult
   1.102 +begin
   1.103 +
   1.104 +definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   1.105  where
   1.106    "setprod = comm_monoid_set.F times 1"
   1.107  
   1.108 -sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1
   1.109 +sublocale setprod!: comm_monoid_set times 1
   1.110  where
   1.111    "comm_monoid_set.F times 1 = setprod"
   1.112  proof -
   1.113 @@ -1067,6 +1063,8 @@
   1.114    Setprod ("\<Prod>_" [1000] 999) where
   1.115    "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
   1.116  
   1.117 +end
   1.118 +
   1.119  syntax
   1.120    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
   1.121  syntax (xsymbols)
   1.122 @@ -1386,6 +1384,9 @@
   1.123  locale semilattice_set = semilattice
   1.124  begin
   1.125  
   1.126 +interpretation comp_fun_idem f
   1.127 +  by default (simp_all add: fun_eq_iff left_commute)
   1.128 +
   1.129  definition F :: "'a set \<Rightarrow> 'a"
   1.130  where
   1.131    eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
   1.132 @@ -1395,8 +1396,6 @@
   1.133    shows "F (insert x A) = Finite_Set.fold f x A"
   1.134  proof (rule sym)
   1.135    let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
   1.136 -  interpret comp_fun_idem f
   1.137 -    by default (simp_all add: fun_eq_iff left_commute)
   1.138    interpret comp_fun_idem "?f"
   1.139      by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
   1.140    from assms show "Finite_Set.fold f x A = F (insert x A)"
   1.141 @@ -1415,8 +1414,6 @@
   1.142    assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
   1.143    shows "F (insert x A) = x * F A"
   1.144  proof -
   1.145 -  interpret comp_fun_idem f
   1.146 -    by default (simp_all add: fun_eq_iff left_commute)
   1.147    from `A \<noteq> {}` obtain b where "b \<in> A" by blast
   1.148    then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
   1.149    with `finite A` and `x \<notin> A`
   1.150 @@ -1552,6 +1549,9 @@
   1.151  locale semilattice_neutr_set = semilattice_neutr
   1.152  begin
   1.153  
   1.154 +interpretation comp_fun_idem f
   1.155 +  by default (simp_all add: fun_eq_iff left_commute)
   1.156 +
   1.157  definition F :: "'a set \<Rightarrow> 'a"
   1.158  where
   1.159    eq_fold: "F A = Finite_Set.fold f 1 A"
   1.160 @@ -1567,11 +1567,7 @@
   1.161  lemma insert [simp]:
   1.162    assumes "finite A"
   1.163    shows "F (insert x A) = x * F A"
   1.164 -proof -
   1.165 -  interpret comp_fun_idem f
   1.166 -    by default (simp_all add: fun_eq_iff left_commute)
   1.167 -  from assms show ?thesis by (simp add: eq_fold)
   1.168 -qed
   1.169 +  using assms by (simp add: eq_fold)
   1.170  
   1.171  lemma in_idem:
   1.172    assumes "finite A" and "x \<in> A"
   1.173 @@ -1693,15 +1689,18 @@
   1.174  where
   1.175    "Sup_fin = semilattice_set.F sup"
   1.176  
   1.177 -definition (in linorder) Min :: "'a set \<Rightarrow> 'a"
   1.178 +context linorder
   1.179 +begin
   1.180 +
   1.181 +definition Min :: "'a set \<Rightarrow> 'a"
   1.182  where
   1.183    "Min = semilattice_set.F min"
   1.184  
   1.185 -definition (in linorder) Max :: "'a set \<Rightarrow> 'a"
   1.186 +definition Max :: "'a set \<Rightarrow> 'a"
   1.187  where
   1.188    "Max = semilattice_set.F max"
   1.189  
   1.190 -sublocale linorder < Min!: semilattice_order_set min less_eq less
   1.191 +sublocale Min!: semilattice_order_set min less_eq less
   1.192    + Max!: semilattice_order_set max greater_eq greater
   1.193  where
   1.194    "semilattice_set.F min = Min"
   1.195 @@ -1718,7 +1717,7 @@
   1.196  
   1.197  text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
   1.198  
   1.199 -sublocale linorder < min_max!: distrib_lattice min less_eq less max
   1.200 +sublocale min_max!: distrib_lattice min less_eq less max
   1.201  where
   1.202    "semilattice_inf.Inf_fin min = Min"
   1.203    and "semilattice_sup.Sup_fin max = Max"
   1.204 @@ -1745,6 +1744,8 @@
   1.205  lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.206    max.left_commute
   1.207  
   1.208 +end
   1.209 +
   1.210  
   1.211  text {* Lattice operations proper *}
   1.212  
   1.213 @@ -1993,45 +1994,44 @@
   1.214    from assms show "x \<le> Max A" by simp
   1.215  qed
   1.216  
   1.217 +context
   1.218 +  fixes A :: "'a set"
   1.219 +  assumes fin_nonempty: "finite A" "A \<noteq> {}"
   1.220 +begin
   1.221 +
   1.222  lemma Min_ge_iff [simp, no_atp]:
   1.223 -  assumes "finite A" and "A \<noteq> {}"
   1.224 -  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.225 -  using assms by (fact Min.bounded_iff)
   1.226 +  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.227 +  using fin_nonempty by (fact Min.bounded_iff)
   1.228  
   1.229  lemma Max_le_iff [simp, no_atp]:
   1.230 -  assumes "finite A" and "A \<noteq> {}"
   1.231 -  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   1.232 -  using assms by (fact Max.bounded_iff)
   1.233 +  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   1.234 +  using fin_nonempty by (fact Max.bounded_iff)
   1.235  
   1.236  lemma Min_gr_iff [simp, no_atp]:
   1.237 -  assumes "finite A" and "A \<noteq> {}"
   1.238 -  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   1.239 -  using assms by (induct rule: finite_ne_induct) simp_all
   1.240 +  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   1.241 +  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   1.242  
   1.243  lemma Max_less_iff [simp, no_atp]:
   1.244 -  assumes "finite A" and "A \<noteq> {}"
   1.245 -  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   1.246 -  using assms by (induct rule: finite_ne_induct) simp_all
   1.247 +  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   1.248 +  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   1.249  
   1.250  lemma Min_le_iff [no_atp]:
   1.251 -  assumes "finite A" and "A \<noteq> {}"
   1.252 -  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   1.253 -  using assms by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   1.254 +  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   1.255 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   1.256  
   1.257  lemma Max_ge_iff [no_atp]:
   1.258 -  assumes "finite A" and "A \<noteq> {}"
   1.259 -  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   1.260 -  using assms by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   1.261 +  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   1.262 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   1.263  
   1.264  lemma Min_less_iff [no_atp]:
   1.265 -  assumes "finite A" and "A \<noteq> {}"
   1.266 -  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   1.267 -  using assms by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   1.268 +  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   1.269 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   1.270  
   1.271  lemma Max_gr_iff [no_atp]:
   1.272 -  assumes "finite A" and "A \<noteq> {}"
   1.273 -  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   1.274 -  using assms by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   1.275 +  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   1.276 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   1.277 +
   1.278 +end
   1.279  
   1.280  lemma Min_antimono:
   1.281    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
     2.1 --- a/src/HOL/List.thy	Tue Apr 23 11:14:50 2013 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Apr 23 11:14:51 2013 +0200
     2.3 @@ -3376,7 +3376,7 @@
     2.4    shows "listsum (map f (filter P xs)) = listsum (map f xs)"
     2.5    using assms by (induct xs) auto
     2.6  
     2.7 -lemma (in monoid_add) distinct_listsum_conv_Setsum:
     2.8 +lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
     2.9    "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
    2.10    by (induct xs) simp_all
    2.11