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.92      by (simp add: union_inter_neutral)
    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.95      by (simp add: H)
    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.129  context comm_monoid_add
   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.192 -    by(simp add:insert_absorb[OF `a:A`])
   1.193 +    by(simp add:insert_absorb[OF \<open>a:A\<close>])
   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.198      by(rule setsum_mono)(simp add: assms(2))
   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.205    finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   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.236  by (simp add: card_cartesian_product)
   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