src/HOL/Groups_Big.thy
 changeset 60758 d8d85a8172b5 parent 60494 e726f88232d3 child 60974 6a6f15d8fbc4
```     1.1 --- a/src/HOL/Groups_Big.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Groups_Big.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -3,13 +3,13 @@
1.4                  with contributions by Jeremy Avigad
1.5  *)
1.6
1.7 -section {* Big sum and product over finite (non-empty) sets *}
1.8 +section \<open>Big sum and product over finite (non-empty) sets\<close>
1.9
1.10  theory Groups_Big
1.11  imports Finite_Set
1.12  begin
1.13
1.14 -subsection {* Generic monoid operation over a set *}
1.15 +subsection \<open>Generic monoid operation over a set\<close>
1.16
1.17  no_notation times (infixl "*" 70)
1.18  no_notation Groups.one ("1")
1.19 @@ -44,9 +44,9 @@
1.20    assumes "finite A" and "x \<in> A"
1.21    shows "F g A = g x * F g (A - {x})"
1.22  proof -
1.23 -  from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
1.24 +  from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
1.25      by (auto dest: mk_disjoint_insert)
1.26 -  moreover from `finite A` A have "finite B" by simp
1.27 +  moreover from \<open>finite A\<close> A have "finite B" by simp
1.28    ultimately show ?thesis by simp
1.29  qed
1.30
1.31 @@ -67,7 +67,7 @@
1.32  lemma union_inter:
1.33    assumes "finite A" and "finite B"
1.34    shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
1.35 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.36 +  -- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
1.37  using assms proof (induct A)
1.38    case empty then show ?case by simp
1.39  next
1.40 @@ -140,7 +140,7 @@
1.41    assumes "A = B"
1.42    assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
1.43    shows "F g A = F h B"
1.44 -  using g_h unfolding `A = B`
1.45 +  using g_h unfolding \<open>A = B\<close>
1.46    by (induct B rule: infinite_finite_induct) auto
1.47
1.48  lemma strong_cong [cong]:
1.49 @@ -207,9 +207,9 @@
1.50    assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
1.51    and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
1.52  proof-
1.53 -  have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
1.54 -  have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
1.55 -  from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
1.56 +  have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast
1.57 +  have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast
1.58 +  from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)"
1.59      by (auto intro: finite_subset)
1.60    show ?thesis using assms(4)
1.61      by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
1.62 @@ -268,7 +268,7 @@
1.63      also have "\<dots> = F g (T - T')"
1.64        using bij by (rule reindex_bij_betw)
1.65      also have "\<dots> = F g T"
1.66 -      using nn `finite S` by (intro mono_neutral_cong_left) auto
1.67 +      using nn \<open>finite S\<close> by (intro mono_neutral_cong_left) auto
1.68      finally show ?thesis .
1.69    qed simp
1.70  qed
1.71 @@ -280,7 +280,7 @@
1.72  proof (subst reindex_bij_betw_not_neutral [symmetric])
1.73    show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
1.74      using nz by (auto intro!: inj_onI simp: bij_betw_def)
1.75 -qed (insert `finite A`, auto)
1.76 +qed (insert \<open>finite A\<close>, auto)
1.77
1.78  lemma reindex_bij_witness_not_neutral:
1.79    assumes fin: "finite S'" "finite T'"
1.80 @@ -369,7 +369,7 @@
1.81    have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
1.82     by simp
1.83    moreover have "A \<inter> B \<subseteq> A" by blast
1.84 -  ultimately have "F ?g (A \<inter> B) = F ?g A" using `finite A`
1.85 +  ultimately have "F ?g (A \<inter> B) = F ?g A" using \<open>finite A\<close>
1.86      by (intro mono_neutral_left) auto
1.87    then show ?thesis by simp
1.88  qed
1.89 @@ -395,7 +395,7 @@
1.90      and H: "F g (\<Union>B) = (F o F) g B" by auto
1.91    then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
1.93 -  with `finite B` `A \<notin> B` show ?case
1.94 +  with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
1.96  qed
1.97
1.98 @@ -430,7 +430,7 @@
1.99    assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
1.100    shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
1.101  proof -
1.102 -  from `finite C` subset have
1.103 +  from \<open>finite C\<close> subset have
1.104      "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
1.105      by (auto elim: finite_subset)
1.106    from subset have [simp]: "A - (C - A) = A" by auto
1.107 @@ -438,12 +438,12 @@
1.108    from subset have "C = A \<union> (C - A)" by auto
1.109    then have "F g C = F g (A \<union> (C - A))" by simp
1.110    also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
1.111 -    using `finite A` `finite (C - A)` by (simp only: union_diff2)
1.112 +    using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
1.113    finally have P: "F g C = F g A" using trivial by simp
1.114    from subset have "C = B \<union> (C - B)" by auto
1.115    then have "F h C = F h (B \<union> (C - B))" by simp
1.116    also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
1.117 -    using `finite B` `finite (C - B)` by (simp only: union_diff2)
1.118 +    using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
1.119    finally have Q: "F h C = F h B" using trivial by simp
1.120    from P Q show ?thesis by simp
1.121  qed
1.122 @@ -462,7 +462,7 @@
1.123  notation Groups.one ("1")
1.124
1.125
1.126 -subsection {* Generalized summation over a set *}
1.127 +subsection \<open>Generalized summation over a set\<close>
1.128
1.130  begin
1.131 @@ -486,8 +486,8 @@
1.132
1.133  end
1.134
1.135 -text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
1.136 -written @{text"\<Sum>x\<in>A. e"}. *}
1.137 +text\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
1.138 +written @{text"\<Sum>x\<in>A. e"}.\<close>
1.139
1.140  syntax
1.141    "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
1.142 @@ -496,12 +496,12 @@
1.143  syntax (HTML output)
1.144    "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
1.145
1.146 -translations -- {* Beware of argument permutation! *}
1.147 +translations -- \<open>Beware of argument permutation!\<close>
1.148    "SUM i:A. b" == "CONST setsum (%i. b) A"
1.149    "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
1.150
1.151 -text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
1.152 - @{text"\<Sum>x|P. e"}. *}
1.153 +text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
1.154 + @{text"\<Sum>x|P. e"}.\<close>
1.155
1.156  syntax
1.157    "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
1.158 @@ -514,7 +514,7 @@
1.159    "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
1.160    "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
1.161
1.162 -print_translation {*
1.163 +print_translation \<open>
1.164  let
1.165    fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) \$ Abs (y, Ty, P)] =
1.166          if x <> y then raise Match
1.167 @@ -528,9 +528,9 @@
1.168            end
1.169      | setsum_tr' _ = raise Match;
1.170  in [(@{const_syntax setsum}, K setsum_tr')] end
1.171 -*}
1.172 +\<close>
1.173
1.174 -text {* TODO generalization candidates *}
1.175 +text \<open>TODO generalization candidates\<close>
1.176
1.177  lemma setsum_image_gen:
1.178    assumes fS: "finite S"
1.179 @@ -545,7 +545,7 @@
1.180  qed
1.181
1.182
1.183 -subsubsection {* Properties in more restricted classes of structures *}
1.184 +subsubsection \<open>Properties in more restricted classes of structures\<close>
1.185
1.186  lemma setsum_Un: "finite A ==> finite B ==>
1.187    (setsum f (A Un B) :: 'a :: ab_group_add) =
1.188 @@ -618,15 +618,15 @@
1.189  proof-
1.190    from assms(3) obtain a where a: "a:A" "f a < g a" by blast
1.191    have "setsum f A = setsum f ((A-{a}) \<union> {a})"
1.194    also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
1.195 -    using `finite A` by(subst setsum.union_disjoint) auto
1.196 +    using \<open>finite A\<close> by(subst setsum.union_disjoint) auto
1.197    also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
1.199    also have "setsum f {a} < setsum g {a}" using a by simp
1.200    also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
1.201 -    using `finite A` by(subst setsum.union_disjoint[symmetric]) auto
1.202 -  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
1.203 +    using \<open>finite A\<close> by(subst setsum.union_disjoint[symmetric]) auto
1.204 +  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF \<open>a:A\<close>])
1.206  qed
1.207
1.208 @@ -880,7 +880,7 @@
1.209
1.210  lemma setsum_Un_nat: "finite A ==> finite B ==>
1.211    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1.212 -  -- {* For the natural numbers, we have subtraction. *}
1.213 +  -- \<open>For the natural numbers, we have subtraction.\<close>
1.214  by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
1.215
1.216  lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
1.217 @@ -932,7 +932,7 @@
1.218    by (induct A rule: infinite_finite_induct) simp_all
1.219
1.220
1.221 -subsubsection {* Cardinality as special case of @{const setsum} *}
1.222 +subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
1.223
1.224  lemma card_eq_setsum:
1.225    "card A = setsum (\<lambda>x. 1) A"
1.226 @@ -1008,7 +1008,7 @@
1.227    by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
1.228
1.229
1.230 -subsubsection {* Cardinality of products *}
1.231 +subsubsection \<open>Cardinality of products\<close>
1.232
1.233  lemma card_SigmaI [simp]:
1.234    "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
1.235 @@ -1029,7 +1029,7 @@
1.237
1.238
1.239 -subsection {* Generalized product over a set *}
1.240 +subsection \<open>Generalized product over a set\<close>
1.241
1.242  context comm_monoid_mult
1.243  begin
1.244 @@ -1060,12 +1060,12 @@
1.245  syntax (HTML output)
1.246    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
1.247
1.248 -translations -- {* Beware of argument permutation! *}
1.249 +translations -- \<open>Beware of argument permutation!\<close>
1.250    "PROD i:A. b" == "CONST setprod (%i. b) A"
1.251    "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
1.252
1.253 -text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
1.254 - @{text"\<Prod>x|P. e"}. *}
1.255 +text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
1.256 + @{text"\<Prod>x|P. e"}.\<close>
1.257
1.258  syntax
1.259    "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
1.260 @@ -1102,7 +1102,7 @@
1.261  end
1.262
1.263
1.264 -subsubsection {* Properties in more restricted classes of structures *}
1.265 +subsubsection \<open>Properties in more restricted classes of structures\<close>
1.266
1.267  context comm_semiring_1
1.268  begin
1.269 @@ -1111,11 +1111,11 @@
1.270    assumes "finite A" and "a \<in> A" and "b = f a"
1.271    shows "b dvd setprod f A"
1.272  proof -
1.273 -  from `finite A` have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
1.274 +  from \<open>finite A\<close> have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
1.275      by (intro setprod.insert) auto
1.276 -  also from `a \<in> A` have "insert a (A - {a}) = A" by blast
1.277 +  also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A" by blast
1.278    finally have "setprod f A = f a * setprod f (A - {a})" .
1.279 -  with `b = f a` show ?thesis by simp
1.280 +  with \<open>b = f a\<close> show ?thesis by simp
1.281  qed
1.282
1.283  lemma dvd_setprodI [intro]:
1.284 @@ -1170,7 +1170,7 @@
1.285      next
1.286        case False with insert have "a \<in> B" by simp
1.287        def C \<equiv> "B - {a}"
1.288 -      with `finite B` `a \<in> B`
1.289 +      with \<open>finite B\<close> \<open>a \<in> B\<close>
1.290          have *: "B = insert a C" "finite C" "a \<notin> C" by auto
1.291        with insert show ?thesis by (auto simp add: insert_commute ac_simps)
1.292      qed
```