src/HOL/Algebra/Group.thy
changeset 13817 7e031a968443
parent 13813 722593f2f068
child 13835 12b2ffbe543a
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 12 17:55:05 2003 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Fri Feb 14 17:35:56 2003 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  header {* Algebraic Structures up to Abelian Groups *}
     1.6  
     1.7 -theory Group = FuncSet:
     1.8 +theory Group = FuncSet + FoldSet:
     1.9  
    1.10  text {*
    1.11    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    1.12 @@ -20,12 +20,14 @@
    1.13  
    1.14  subsection {* Definitions *}
    1.15  
    1.16 -record 'a magma =
    1.17 +record 'a semigroup =
    1.18    carrier :: "'a set"
    1.19    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    1.20  
    1.21 -record 'a group = "'a magma" +
    1.22 +record 'a monoid = "'a semigroup" +
    1.23    one :: 'a ("\<one>\<index>")
    1.24 +
    1.25 +record 'a group = "'a monoid" +
    1.26    m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
    1.27  
    1.28  locale magma = struct G +
    1.29 @@ -37,10 +39,12 @@
    1.30      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.31       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.32  
    1.33 -locale group = semigroup +
    1.34 +locale l_one = struct G +
    1.35    assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    1.36 -    and inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    1.37      and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    1.38 +
    1.39 +locale group = semigroup + l_one +
    1.40 +  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    1.41      and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    1.42  
    1.43  subsection {* Cancellation Laws and Basic Properties *}
    1.44 @@ -156,6 +160,11 @@
    1.45  
    1.46  declare (in subgroup) group.intro [intro]
    1.47  
    1.48 +lemma (in subgroup) l_oneI [intro]:
    1.49 +  includes l_one G
    1.50 +  shows "l_one (G(| carrier := H |))"
    1.51 +  by rule simp_all
    1.52 +
    1.53  lemma (in subgroup) group_axiomsI [intro]:
    1.54    includes group G
    1.55    shows "group_axioms (G(| carrier := H |))"
    1.56 @@ -206,8 +215,8 @@
    1.57  
    1.58  declare magma.m_closed [simp]
    1.59  
    1.60 -declare group.one_closed [iff] group.inv_closed [simp]
    1.61 -  group.l_one [simp] group.r_one [simp] group.inv_inv [simp]
    1.62 +declare l_one.one_closed [iff] group.inv_closed [simp]
    1.63 +  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
    1.64  
    1.65  lemma subgroup_nonempty:
    1.66    "~ subgroup {} G"
    1.67 @@ -227,47 +236,57 @@
    1.68  subsection {* Direct Products *}
    1.69  
    1.70  constdefs
    1.71 -  DirProdMagma ::
    1.72 -    "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a \<times> 'b) magma"
    1.73 +  DirProdSemigroup ::
    1.74 +    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
    1.75 +    => ('a \<times> 'b) semigroup"
    1.76 +    (infixr "\<times>\<^sub>s" 80)
    1.77 +  "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    1.78 +    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    1.79 +
    1.80 +  DirProdMonoid ::
    1.81 +    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
    1.82      (infixr "\<times>\<^sub>m" 80)
    1.83 -  "G \<times>\<^sub>m H == (| carrier = carrier G \<times> carrier H,
    1.84 -    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    1.85 +  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
    1.86 +    mult = mult (G \<times>\<^sub>s H),
    1.87 +    one = (one G, one H) |)"
    1.88  
    1.89    DirProdGroup ::
    1.90      "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
    1.91      (infixr "\<times>\<^sub>g" 80)
    1.92    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    1.93      mult = mult (G \<times>\<^sub>m H),
    1.94 -    one = (one G, one H),
    1.95 +    one = one (G \<times>\<^sub>m H),
    1.96      m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
    1.97  
    1.98 -lemma DirProdMagma_magma:
    1.99 +lemma DirProdSemigroup_magma:
   1.100    includes magma G + magma H
   1.101 -  shows "magma (G \<times>\<^sub>m H)"
   1.102 -  by rule (auto simp add: DirProdMagma_def)
   1.103 +  shows "magma (G \<times>\<^sub>s H)"
   1.104 +  by rule (auto simp add: DirProdSemigroup_def)
   1.105  
   1.106 -lemma DirProdMagma_semigroup_axioms:
   1.107 +lemma DirProdSemigroup_semigroup_axioms:
   1.108    includes semigroup G + semigroup H
   1.109 -  shows "semigroup_axioms (G \<times>\<^sub>m H)"
   1.110 -  by rule (auto simp add: DirProdMagma_def G.m_assoc H.m_assoc)
   1.111 +  shows "semigroup_axioms (G \<times>\<^sub>s H)"
   1.112 +  by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
   1.113  
   1.114 -lemma DirProdMagma_semigroup:
   1.115 +lemma DirProdSemigroup_semigroup:
   1.116    includes semigroup G + semigroup H
   1.117 -  shows "semigroup (G \<times>\<^sub>m H)"
   1.118 +  shows "semigroup (G \<times>\<^sub>s H)"
   1.119    using prems
   1.120    by (fast intro: semigroup.intro
   1.121 -    DirProdMagma_magma DirProdMagma_semigroup_axioms)
   1.122 +    DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
   1.123  
   1.124  lemma DirProdGroup_magma:
   1.125    includes magma G + magma H
   1.126    shows "magma (G \<times>\<^sub>g H)"
   1.127 -  by rule (auto simp add: DirProdGroup_def DirProdMagma_def)
   1.128 +  by rule
   1.129 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
   1.130  
   1.131  lemma DirProdGroup_semigroup_axioms:
   1.132    includes semigroup G + semigroup H
   1.133    shows "semigroup_axioms (G \<times>\<^sub>g H)"
   1.134    by rule
   1.135 -    (auto simp add: DirProdGroup_def DirProdMagma_def G.m_assoc H.m_assoc)
   1.136 +    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   1.137 +      G.m_assoc H.m_assoc)
   1.138  
   1.139  lemma DirProdGroup_semigroup:
   1.140    includes semigroup G + semigroup H
   1.141 @@ -278,18 +297,20 @@
   1.142  
   1.143  (* ... and further lemmas for group ... *)
   1.144  
   1.145 -lemma
   1.146 +lemma DirProdGroup_group:
   1.147    includes group G + group H
   1.148    shows "group (G \<times>\<^sub>g H)"
   1.149  by rule
   1.150 -  (auto intro: magma.intro semigroup_axioms.intro group_axioms.intro
   1.151 -    simp add: DirProdGroup_def DirProdMagma_def
   1.152 +  (auto intro: magma.intro l_one.intro
   1.153 +      semigroup_axioms.intro group_axioms.intro
   1.154 +    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   1.155        G.m_assoc H.m_assoc G.l_inv H.l_inv)
   1.156  
   1.157  subsection {* Homomorphisms *}
   1.158  
   1.159  constdefs
   1.160 -  hom :: "[('a, 'c) magma_scheme, ('b, 'd) magma_scheme] => ('a => 'b)set"
   1.161 +  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
   1.162 +    => ('a => 'b)set"
   1.163    "hom G H ==
   1.164      {h. h \<in> carrier G -> carrier H &
   1.165        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
   1.166 @@ -367,6 +388,291 @@
   1.167  
   1.168  lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
   1.169  
   1.170 -locale abelian_group = abelian_semigroup + group
   1.171 +locale abelian_monoid = abelian_semigroup + l_one
   1.172 +
   1.173 +lemma (in abelian_monoid) l_one [simp]:
   1.174 +  "x \<in> carrier G ==> x \<otimes> \<one> = x"
   1.175 +proof -
   1.176 +  assume G: "x \<in> carrier G"
   1.177 +  then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
   1.178 +  also from G have "... = x" by simp
   1.179 +  finally show ?thesis .
   1.180 +qed
   1.181 +
   1.182 +locale abelian_group = abelian_monoid + group
   1.183 +
   1.184 +subsection {* Products over Finite Sets *}
   1.185 +
   1.186 +locale finite_prod = abelian_monoid + var prod +
   1.187 +  defines "prod == (%f A. if finite A
   1.188 +      then foldD (carrier G) (op \<otimes> o f) \<one> A
   1.189 +      else arbitrary)"
   1.190 +
   1.191 +(* TODO: nice syntax for the summation operator inside the locale
   1.192 +   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
   1.193 +
   1.194 +ML_setup {* 
   1.195 +
   1.196 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.197 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.198 +
   1.199 +lemma (in finite_prod) prod_empty [simp]: 
   1.200 +  "prod f {} = \<one>"
   1.201 +  by (simp add: prod_def)
   1.202 +
   1.203 +ML_setup {* 
   1.204 +
   1.205 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.206 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   1.207 +
   1.208 +declare funcsetI [intro]
   1.209 +  funcset_mem [dest]
   1.210 +
   1.211 +lemma (in finite_prod) prod_insert [simp]:
   1.212 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
   1.213 +   prod f (insert a F) = f a \<otimes> prod f F"
   1.214 +  apply (rule trans)
   1.215 +  apply (simp add: prod_def)
   1.216 +  apply (rule trans)
   1.217 +  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   1.218 +    apply simp
   1.219 +    apply (rule m_lcomm)
   1.220 +      apply fast apply fast apply assumption
   1.221 +    apply (fastsimp intro: m_closed)
   1.222 +    apply simp+ apply fast
   1.223 +  apply (auto simp add: prod_def)
   1.224 +  done
   1.225 +
   1.226 +lemma (in finite_prod) prod_one:
   1.227 +  "finite A ==> prod (%i. \<one>) A = \<one>"
   1.228 +proof (induct set: Finites)
   1.229 +  case empty show ?case by simp
   1.230 +next
   1.231 +  case (insert A a)
   1.232 +  have "(%i. \<one>) \<in> A -> carrier G" by auto
   1.233 +  with insert show ?case by simp
   1.234 +qed
   1.235 +
   1.236 +(*
   1.237 +lemma prod_eq_0_iff [simp]:
   1.238 +    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
   1.239 +  by (induct set: Finites) auto
   1.240 +
   1.241 +lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
   1.242 +  apply (case_tac "finite A")
   1.243 +   prefer 2 apply (simp add: prod_def)
   1.244 +  apply (erule rev_mp)
   1.245 +  apply (erule finite_induct)
   1.246 +   apply auto
   1.247 +  done
   1.248 +
   1.249 +lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
   1.250 +*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
   1.251 +(*
   1.252 +  by (induct set: Finites) auto
   1.253 +*)
   1.254 +
   1.255 +lemma (in finite_prod) prod_closed:
   1.256 +  fixes A
   1.257 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   1.258 +  shows "prod f A \<in> carrier G"
   1.259 +using fin f
   1.260 +proof induct
   1.261 +  case empty show ?case by simp
   1.262 +next
   1.263 +  case (insert A a)
   1.264 +  then have a: "f a \<in> carrier G" by fast
   1.265 +  from insert have A: "f \<in> A -> carrier G" by fast
   1.266 +  from insert A a show ?case by simp
   1.267 +qed
   1.268 +
   1.269 +lemma funcset_Int_left [simp, intro]:
   1.270 +  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   1.271 +  by fast
   1.272 +
   1.273 +lemma funcset_Un_left [iff]:
   1.274 +  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   1.275 +  by fast
   1.276 +
   1.277 +lemma (in finite_prod) prod_Un_Int:
   1.278 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   1.279 +   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
   1.280 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   1.281 +proof (induct set: Finites)
   1.282 +  case empty then show ?case by (simp add: prod_closed)
   1.283 +next
   1.284 +  case (insert A a)
   1.285 +  then have a: "g a \<in> carrier G" by fast
   1.286 +  from insert have A: "g \<in> A -> carrier G" by fast
   1.287 +  from insert A a show ?case
   1.288 +    by (simp add: ac Int_insert_left insert_absorb prod_closed
   1.289 +          Int_mono2 Un_subset_iff) 
   1.290 +qed
   1.291 +
   1.292 +lemma (in finite_prod) prod_Un_disjoint:
   1.293 +  "[| finite A; finite B; A Int B = {};
   1.294 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   1.295 +   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
   1.296 +  apply (subst prod_Un_Int [symmetric])
   1.297 +    apply (auto simp add: prod_closed)
   1.298 +  done
   1.299 +
   1.300 +(*
   1.301 +lemma prod_UN_disjoint:
   1.302 +  fixes f :: "'a => 'b::plus_ac0"
   1.303 +  shows
   1.304 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   1.305 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   1.306 +      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
   1.307 +  apply (induct set: Finites)
   1.308 +   apply simp
   1.309 +  apply atomize
   1.310 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   1.311 +   prefer 2 apply blast
   1.312 +  apply (subgoal_tac "A x Int UNION F A = {}")
   1.313 +   prefer 2 apply blast
   1.314 +  apply (simp add: prod_Un_disjoint)
   1.315 +  done
   1.316 +*)
   1.317 +
   1.318 +lemma (in finite_prod) prod_addf:
   1.319 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   1.320 +   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
   1.321 +proof (induct set: Finites)
   1.322 +  case empty show ?case by simp
   1.323 +next
   1.324 +  case (insert A a) then
   1.325 +  have fA: "f : A -> carrier G" by fast
   1.326 +  from insert have fa: "f a : carrier G" by fast
   1.327 +  from insert have gA: "g : A -> carrier G" by fast
   1.328 +  from insert have ga: "g a : carrier G" by fast
   1.329 +  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   1.330 +  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   1.331 +    by (simp add: Pi_def)
   1.332 +  show ?case  (* check if all simps are really necessary *)
   1.333 +    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   1.334 +qed
   1.335 +
   1.336 +(*
   1.337 +lemma prod_Un: "finite A ==> finite B ==>
   1.338 +    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
   1.339 +  -- {* For the natural numbers, we have subtraction. *}
   1.340 +  apply (subst prod_Un_Int [symmetric])
   1.341 +    apply auto
   1.342 +  done
   1.343 +
   1.344 +lemma prod_diff1: "(prod f (A - {a}) :: nat) =
   1.345 +    (if a:A then prod f A - f a else prod f A)"
   1.346 +  apply (case_tac "finite A")
   1.347 +   prefer 2 apply (simp add: prod_def)
   1.348 +  apply (erule finite_induct)
   1.349 +   apply (auto simp add: insert_Diff_if)
   1.350 +  apply (drule_tac a = a in mk_disjoint_insert)
   1.351 +  apply auto
   1.352 +  done
   1.353 +*)
   1.354 +
   1.355 +lemma (in finite_prod) prod_cong:
   1.356 +  "[| A = B; g : B -> carrier G;
   1.357 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   1.358 +proof -
   1.359 +  assume prems: "A = B" "g : B -> carrier G"
   1.360 +    "!!i. i : B ==> f i = g i"
   1.361 +  show ?thesis
   1.362 +  proof (cases "finite B")
   1.363 +    case True
   1.364 +    then have "!!A. [| A = B; g : B -> carrier G;
   1.365 +      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   1.366 +    proof induct
   1.367 +      case empty thus ?case by simp
   1.368 +    next
   1.369 +      case (insert B x)
   1.370 +      then have "prod f A = prod f (insert x B)" by simp
   1.371 +      also from insert have "... = f x \<otimes> prod f B"
   1.372 +      proof (intro prod_insert)
   1.373 +	show "finite B" .
   1.374 +      next
   1.375 +	show "x ~: B" .
   1.376 +      next
   1.377 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.378 +	  "g \<in> insert x B \<rightarrow> carrier G"
   1.379 +	thus "f : B -> carrier G" by fastsimp
   1.380 +      next
   1.381 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.382 +	  "g \<in> insert x B \<rightarrow> carrier G"
   1.383 +	thus "f x \<in> carrier G" by fastsimp
   1.384 +      qed
   1.385 +      also from insert have "... = g x \<otimes> prod g B" by fastsimp
   1.386 +      also from insert have "... = prod g (insert x B)"
   1.387 +      by (intro prod_insert [THEN sym]) auto
   1.388 +      finally show ?case .
   1.389 +    qed
   1.390 +    with prems show ?thesis by simp
   1.391 +  next
   1.392 +    case False with prems show ?thesis by (simp add: prod_def)
   1.393 +  qed
   1.394 +qed
   1.395 +
   1.396 +lemma (in finite_prod) prod_cong1 [cong]:
   1.397 +  "[| A = B; !!i. i : B ==> f i = g i;
   1.398 +      g : B -> carrier G = True |] ==> prod f A = prod g B"
   1.399 +  by (rule prod_cong) fast+
   1.400 +
   1.401 +text {*Usually, if this rule causes a failed congruence proof error,
   1.402 +   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   1.403 +   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   1.404 +
   1.405 +declare funcsetI [rule del]
   1.406 +  funcset_mem [rule del]
   1.407 +
   1.408 +subsection {* Summation over the integer interval @{term "{..n}"} *}
   1.409 +
   1.410 +text {*
   1.411 +  For technical reasons (locales) a new locale where the index set is
   1.412 +  restricted to @{term "nat"} is necessary.
   1.413 +*}
   1.414 +
   1.415 +locale finite_prod_nat = finite_prod +
   1.416 +  assumes "False ==> prod f (A::nat set) = prod f A"
   1.417 +
   1.418 +lemma (in finite_prod_nat) natSum_0 [simp]:
   1.419 +  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
   1.420 +by (simp add: Pi_def)
   1.421 +
   1.422 +lemma (in finite_prod_nat) natsum_Suc [simp]:
   1.423 +  "f : {..Suc n} -> carrier G ==>
   1.424 +   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
   1.425 +by (simp add: Pi_def atMost_Suc)
   1.426 +
   1.427 +lemma (in finite_prod_nat) natsum_Suc2:
   1.428 +  "f : {..Suc n} -> carrier G ==>
   1.429 +   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
   1.430 +proof (induct n)
   1.431 +  case 0 thus ?case by (simp add: Pi_def)
   1.432 +next
   1.433 +  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
   1.434 +qed
   1.435 +
   1.436 +lemma (in finite_prod_nat) natsum_zero [simp]:
   1.437 +  "prod (%i. \<one>) {..n::nat} = \<one>"
   1.438 +by (induct n) (simp_all add: Pi_def)
   1.439 +
   1.440 +lemma (in finite_prod_nat) natsum_add [simp]:
   1.441 +  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   1.442 +   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
   1.443 +by (induct n) (simp_all add: ac Pi_def prod_closed)
   1.444 +
   1.445 +thm setsum_cong
   1.446 +
   1.447 +ML_setup {* 
   1.448 +
   1.449 +Context.>> (fn thy => (simpset_ref_of thy :=
   1.450 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.451 +
   1.452 +lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
   1.453 +apply simp done
   1.454 +
   1.455 +lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"
   1.456 +apply (simp add: Pi_def)
   1.457  
   1.458  end