Change to meta simplifier: congruence rules may now have frees as head of term.
authorballarin
Thu Feb 27 15:12:29 2003 +0100 (2003-02-27)
changeset 1383512b2ffbe543a
parent 13834 4d50cf8ea3d7
child 13836 6d0392fc6dc5
Change to meta simplifier: congruence rules may now have frees as head of term.
NEWS
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/FoldSet.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Summation.thy
src/Pure/meta_simplifier.ML
     1.1 --- a/NEWS	Wed Feb 26 14:26:18 2003 +0100
     1.2 +++ b/NEWS	Thu Feb 27 15:12:29 2003 +0100
     1.3 @@ -44,10 +44,11 @@
     1.4      where n is an integer. Thus you can force termination where previously
     1.5      the simplifier would diverge.
     1.6  
     1.7 +  - Accepts free variables as head terms in congruence rules.  Useful in Isar.
     1.8  
     1.9  * Pure: New flag for triggering if the overall goal of a proof state should
    1.10  be printed:
    1.11 -   PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
    1.12 +   PG menu: Isabelle/Isar -> Settings -> Show Main Goal
    1.13  (ML: Proof.show_main_goal).
    1.14  
    1.15  * Pure: You can find all matching introduction rules for subgoal 1, i.e. all
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Algebra/CRing.thy	Thu Feb 27 15:12:29 2003 +0100
     2.3 @@ -0,0 +1,278 @@
     2.4 +(*
     2.5 +  Title:     The algebraic hierarchy of rings
     2.6 +  Id:        $Id$
     2.7 +  Author:    Clemens Ballarin, started 9 December 1996
     2.8 +  Copyright: Clemens Ballarin
     2.9 +*)
    2.10 +
    2.11 +header {* The algebraic hierarchy of rings as axiomatic classes *}
    2.12 +
    2.13 +theory Ring = Group
    2.14 +
    2.15 +section {* The Algebraic Hierarchy of Rings *}
    2.16 +
    2.17 +subsection {* Basic Definitions *}
    2.18 +
    2.19 +record 'a ring = "'a group" +
    2.20 +  zero :: 'a ("\<zero>\<index>")
    2.21 +  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
    2.22 +  a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
    2.23 +
    2.24 +locale cring = abelian_monoid R +
    2.25 +  assumes a_abelian_group: "abelian_group (| carrier = carrier R,
    2.26 +      mult = add R, one = zero R, m_inv = a_inv R |)"
    2.27 +    and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
    2.28 +      ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
    2.29 +    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    2.30 +      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    2.31 +
    2.32 +ML {*
    2.33 +  thm "cring.l_distr"
    2.34 +*}
    2.35 +
    2.36 +(*
    2.37 +locale cring = struct R +
    2.38 +  assumes a_group: "abelian_group (| carrier = carrier R,
    2.39 +      mult = add R, one = zero R, m_inv = a_inv R |)"
    2.40 +    and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
    2.41 +      mult = mult R, one = one R |)"
    2.42 +    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    2.43 +      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    2.44 +
    2.45 +locale field = struct R +
    2.46 +  assumes a_group: "abelian_group (| carrier = carrier R,
    2.47 +      mult = add R, one = zero R, m_inv = a_inv R |)"
    2.48 +    and m_group: "monoid (| carrier = carrier R - {zero R},
    2.49 +      mult = mult R, one = one R |)"
    2.50 +    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    2.51 +      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    2.52 +*)
    2.53 +(*
    2.54 +  a_assoc:      "(a + b) + c = a + (b + c)"
    2.55 +  l_zero:       "0 + a = a"
    2.56 +  l_neg:        "(-a) + a = 0"
    2.57 +  a_comm:       "a + b = b + a"
    2.58 +
    2.59 +  m_assoc:      "(a * b) * c = a * (b * c)"
    2.60 +  l_one:        "1 * a = a"
    2.61 +
    2.62 +  l_distr:      "(a + b) * c = a * c + b * c"
    2.63 +
    2.64 +  m_comm:       "a * b = b * a"
    2.65 +
    2.66 +  -- {* Definition of derived operations *}
    2.67 +
    2.68 +  minus_def:    "a - b = a + (-b)"
    2.69 +  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
    2.70 +  divide_def:   "a / b = a * inverse b"
    2.71 +  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
    2.72 +*)
    2.73 +subsection {* Basic Facts *}
    2.74 +
    2.75 +lemma (in cring) a_magma [simp, intro]:
    2.76 +  "magma (| carrier = carrier R,
    2.77 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.78 +  using a_abelian_group by (simp only: abelian_group_def)
    2.79 +
    2.80 +lemma (in cring) a_l_one [simp, intro]:
    2.81 +  "l_one (| carrier = carrier R,
    2.82 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.83 +  using a_abelian_group by (simp only: abelian_group_def)
    2.84 +
    2.85 +lemma (in cring) a_abelian_group_parts [simp, intro]:
    2.86 +  "semigroup_axioms (| carrier = carrier R,
    2.87 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.88 +  "group_axioms (| carrier = carrier R,
    2.89 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.90 +  "abelian_semigroup_axioms (| carrier = carrier R,
    2.91 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.92 +  using a_abelian_group by (simp_all only: abelian_group_def)
    2.93 +
    2.94 +lemma (in cring) a_semigroup:
    2.95 +  "semigroup (| carrier = carrier R,
    2.96 +     mult = add R, one = zero R, m_inv = a_inv R |)"
    2.97 +  by (simp add: semigroup_def)
    2.98 +
    2.99 +lemma (in cring) a_group:
   2.100 +  "group (| carrier = carrier R,
   2.101 +     mult = add R, one = zero R, m_inv = a_inv R |)"
   2.102 +  by (simp add: group_def)
   2.103 +
   2.104 +lemma (in cring) a_abelian_semigroup:
   2.105 +  "abelian_semigroup (| carrier = carrier R,
   2.106 +     mult = add R, one = zero R, m_inv = a_inv R |)"
   2.107 +  by (simp add: abelian_semigroup_def)
   2.108 +
   2.109 +lemma (in cring) a_abelian_group:
   2.110 +  "abelian_group (| carrier = carrier R,
   2.111 +     mult = add R, one = zero R, m_inv = a_inv R |)"
   2.112 +  by (simp add: abelian_group_def)
   2.113 +
   2.114 +lemma (in cring) a_assoc:
   2.115 +  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   2.116 +  ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   2.117 +  using semigroup.m_assoc [OF a_semigroup]
   2.118 +  by simp
   2.119 +
   2.120 +lemma (in cring) l_zero:
   2.121 +  "x \<in> carrier R ==> \<zero> \<oplus> x = x"
   2.122 +  using l_one.l_one [OF a_l_one]
   2.123 +  by simp
   2.124 +
   2.125 +lemma (in cring) l_neg:
   2.126 +  "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
   2.127 +  using group.l_inv [OF a_group]
   2.128 +  by simp
   2.129 +
   2.130 +lemma (in cring) a_comm:
   2.131 +  "[| x \<in> carrier R; y \<in> carrier R |]
   2.132 +  ==> x \<oplus> y = y \<oplus> x"
   2.133 +  using abelian_semigroup.m_comm [OF a_abelian_semigroup]
   2.134 +  by simp
   2.135 +
   2.136 +
   2.137 +
   2.138 +
   2.139 +qed
   2.140 +
   2.141 +  l_zero:       "0 + a = a"
   2.142 +  l_neg:        "(-a) + a = 0"
   2.143 +  a_comm:       "a + b = b + a"
   2.144 +
   2.145 +  m_assoc:      "(a * b) * c = a * (b * c)"
   2.146 +  l_one:        "1 * a = a"
   2.147 +
   2.148 +  l_distr:      "(a + b) * c = a * c + b * c"
   2.149 +
   2.150 +  m_comm:       "a * b = b * a"
   2.151 +text {* Normaliser for Commutative Rings *}
   2.152 +
   2.153 +use "order.ML"
   2.154 +
   2.155 +method_setup ring =
   2.156 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
   2.157 +  {* computes distributive normal form in rings *}
   2.158 +
   2.159 +subsection {* Rings and the summation operator *}
   2.160 +
   2.161 +(* Basic facts --- move to HOL!!! *)
   2.162 +
   2.163 +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
   2.164 +by simp
   2.165 +
   2.166 +lemma natsum_Suc [simp]:
   2.167 +  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
   2.168 +by (simp add: atMost_Suc)
   2.169 +
   2.170 +lemma natsum_Suc2:
   2.171 +  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
   2.172 +proof (induct n)
   2.173 +  case 0 show ?case by simp
   2.174 +next
   2.175 +  case Suc thus ?case by (simp add: assoc) 
   2.176 +qed
   2.177 +
   2.178 +lemma natsum_cong [cong]:
   2.179 +  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
   2.180 +        setsum f {..j} = setsum g {..k}"
   2.181 +by (induct j) auto
   2.182 +
   2.183 +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
   2.184 +by (induct n) simp_all
   2.185 +
   2.186 +lemma natsum_add [simp]:
   2.187 +  "!!f::nat=>'a::plus_ac0.
   2.188 +   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
   2.189 +by (induct n) (simp_all add: plus_ac0)
   2.190 +
   2.191 +(* Facts specific to rings *)
   2.192 +
   2.193 +instance ring < plus_ac0
   2.194 +proof
   2.195 +  fix x y z
   2.196 +  show "(x::'a::ring) + y = y + x" by (rule a_comm)
   2.197 +  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
   2.198 +  show "0 + (x::'a::ring) = x" by (rule l_zero)
   2.199 +qed
   2.200 +
   2.201 +ML {*
   2.202 +  local
   2.203 +    val lhss = 
   2.204 +        [read_cterm (sign_of (the_context ()))
   2.205 +                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
   2.206 +	 read_cterm (sign_of (the_context ()))
   2.207 +                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
   2.208 +	 read_cterm (sign_of (the_context ()))
   2.209 +                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
   2.210 +	 read_cterm (sign_of (the_context ()))
   2.211 +                    ("- ?t::'a::ring", TVar (("'z", 0), []))
   2.212 +	];
   2.213 +    fun proc sg _ t = 
   2.214 +      let val rew = Tactic.prove sg [] []
   2.215 +            (HOLogic.mk_Trueprop
   2.216 +              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
   2.217 +                (fn _ => simp_tac ring_ss 1)
   2.218 +            |> mk_meta_eq;
   2.219 +          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
   2.220 +      in if t' aconv u 
   2.221 +        then None
   2.222 +        else Some rew 
   2.223 +    end;
   2.224 +  in
   2.225 +    val ring_simproc = mk_simproc "ring" lhss proc;
   2.226 +  end;
   2.227 +*}
   2.228 +
   2.229 +ML_setup {* Addsimprocs [ring_simproc] *}
   2.230 +
   2.231 +lemma natsum_ldistr:
   2.232 +  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
   2.233 +by (induct n) simp_all
   2.234 +
   2.235 +lemma natsum_rdistr:
   2.236 +  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
   2.237 +by (induct n) simp_all
   2.238 +
   2.239 +subsection {* Integral Domains *}
   2.240 +
   2.241 +declare one_not_zero [simp]
   2.242 +
   2.243 +lemma zero_not_one [simp]:
   2.244 +  "0 ~= (1::'a::domain)" 
   2.245 +by (rule not_sym) simp
   2.246 +
   2.247 +lemma integral_iff: (* not by default a simp rule! *)
   2.248 +  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
   2.249 +proof
   2.250 +  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
   2.251 +next
   2.252 +  assume "a = 0 | b = 0" then show "a * b = 0" by auto
   2.253 +qed
   2.254 +
   2.255 +(*
   2.256 +lemma "(a::'a::ring) - (a - b) = b" apply simp
   2.257 + simproc seems to fail on this example (fixed with new term order)
   2.258 +*)
   2.259 +(*
   2.260 +lemma bug: "(b::'a::ring) - (b - a) = a" by simp
   2.261 +   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
   2.262 +*)
   2.263 +lemma m_lcancel:
   2.264 +  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
   2.265 +proof
   2.266 +  assume eq: "a * b = a * c"
   2.267 +  then have "a * (b - c) = 0" by simp
   2.268 +  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
   2.269 +  with prem have "b - c = 0" by auto 
   2.270 +  then have "b = b - (b - c)" by simp 
   2.271 +  also have "b - (b - c) = c" by simp
   2.272 +  finally show "b = c" .
   2.273 +next
   2.274 +  assume "b = c" then show "a * b = a * c" by simp
   2.275 +qed
   2.276 +
   2.277 +lemma m_rcancel:
   2.278 +  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
   2.279 +by (simp add: m_lcancel)
   2.280 +
   2.281 +end
     3.1 --- a/src/HOL/Algebra/FoldSet.thy	Wed Feb 26 14:26:18 2003 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,297 +0,0 @@
     3.4 -(*  Title:      Summation Operator for Abelian Groups
     3.5 -    ID:         $Id$
     3.6 -    Author:     Clemens Ballarin, started 19 November 2002
     3.7 -
     3.8 -This file is largely based on HOL/Finite_Set.thy.
     3.9 -*)
    3.10 -
    3.11 -header {* Summation Operator *}
    3.12 -
    3.13 -theory FoldSet = Main:
    3.14 -
    3.15 -(* Instantiation of LC from Finite_Set.thy is not possible,
    3.16 -   because here we have explicit typing rules like x : carrier G.
    3.17 -   We introduce an explicit argument for the domain D *)
    3.18 -
    3.19 -consts
    3.20 -  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    3.21 -
    3.22 -inductive "foldSetD D f e"
    3.23 -  intros
    3.24 -    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    3.25 -    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    3.26 -                      (insert x A, f x y) : foldSetD D f e"
    3.27 -
    3.28 -inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    3.29 -
    3.30 -constdefs
    3.31 -  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    3.32 -  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    3.33 -
    3.34 -lemma foldSetD_closed:
    3.35 -  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    3.36 -      |] ==> z : D";
    3.37 -  by (erule foldSetD.elims) auto
    3.38 -
    3.39 -lemma Diff1_foldSetD:
    3.40 -  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    3.41 -   (A, f x y) : foldSetD D f e"
    3.42 -  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    3.43 -   apply auto
    3.44 -  done
    3.45 -
    3.46 -lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    3.47 -  by (induct set: foldSetD) auto
    3.48 -
    3.49 -lemma finite_imp_foldSetD:
    3.50 -  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    3.51 -   EX x. (A, x) : foldSetD D f e"
    3.52 -proof (induct set: Finites)
    3.53 -  case empty then show ?case by auto
    3.54 -next
    3.55 -  case (insert F x)
    3.56 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    3.57 -  with insert have "y : D" by (auto dest: foldSetD_closed)
    3.58 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    3.59 -    by (intro foldSetD.intros) auto
    3.60 -  then show ?case ..
    3.61 -qed
    3.62 -
    3.63 -subsection {* Left-commutative operations *}
    3.64 -
    3.65 -locale LCD =
    3.66 -  fixes B :: "'b set"
    3.67 -  and D :: "'a set"
    3.68 -  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    3.69 -  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    3.70 -  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    3.71 -
    3.72 -lemma (in LCD) foldSetD_closed [dest]:
    3.73 -  "(A, z) : foldSetD D f e ==> z : D";
    3.74 -  by (erule foldSetD.elims) auto
    3.75 -
    3.76 -lemma (in LCD) Diff1_foldSetD:
    3.77 -  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    3.78 -   (A, f x y) : foldSetD D f e"
    3.79 -  apply (subgoal_tac "x : B")
    3.80 -  prefer 2 apply fast
    3.81 -  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    3.82 -   apply auto
    3.83 -  done
    3.84 -
    3.85 -lemma (in LCD) foldSetD_imp_finite [simp]:
    3.86 -  "(A, x) : foldSetD D f e ==> finite A"
    3.87 -  by (induct set: foldSetD) auto
    3.88 -
    3.89 -lemma (in LCD) finite_imp_foldSetD:
    3.90 -  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
    3.91 -proof (induct set: Finites)
    3.92 -  case empty then show ?case by auto
    3.93 -next
    3.94 -  case (insert F x)
    3.95 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    3.96 -  with insert have "y : D" by auto
    3.97 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    3.98 -    by (intro foldSetD.intros) auto
    3.99 -  then show ?case ..
   3.100 -qed
   3.101 -
   3.102 -lemma (in LCD) foldSetD_determ_aux:
   3.103 -  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   3.104 -    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   3.105 -  apply (induct n)
   3.106 -   apply (auto simp add: less_Suc_eq)
   3.107 -  apply (erule foldSetD.cases)
   3.108 -   apply blast
   3.109 -  apply (erule foldSetD.cases)
   3.110 -   apply blast
   3.111 -  apply clarify
   3.112 -  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   3.113 -  apply (erule rev_mp)
   3.114 -  apply (simp add: less_Suc_eq_le)
   3.115 -  apply (rule impI)
   3.116 -  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   3.117 -   apply (subgoal_tac "Aa = Ab")
   3.118 -    prefer 2 apply (blast elim!: equalityE)
   3.119 -   apply blast
   3.120 -  txt {* case @{prop "xa \<notin> xb"}. *}
   3.121 -  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   3.122 -   prefer 2 apply (blast elim!: equalityE)
   3.123 -  apply clarify
   3.124 -  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   3.125 -   prefer 2 apply blast
   3.126 -  apply (subgoal_tac "card Aa <= card Ab")
   3.127 -   prefer 2
   3.128 -   apply (rule Suc_le_mono [THEN subst])
   3.129 -   apply (simp add: card_Suc_Diff1)
   3.130 -  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
   3.131 -  apply (blast intro: foldSetD_imp_finite finite_Diff)
   3.132 -(* new subgoal from finite_imp_foldSetD *)
   3.133 -    apply best (* blast doesn't seem to solve this *)
   3.134 -   apply assumption
   3.135 -  apply (frule (1) Diff1_foldSetD)
   3.136 -(* new subgoal from Diff1_foldSetD *)
   3.137 -    apply best
   3.138 -(*
   3.139 -apply (best del: foldSetD_closed elim: foldSetD_closed)
   3.140 -    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
   3.141 -    prefer 3 apply assumption apply (rule e_closed)
   3.142 -    apply (rule f_closed) apply force apply assumption
   3.143 -*)
   3.144 -  apply (subgoal_tac "ya = f xb x")
   3.145 -   prefer 2
   3.146 -(* new subgoal to make IH applicable *) 
   3.147 -  apply (subgoal_tac "Aa <= B")
   3.148 -   prefer 2 apply best
   3.149 -   apply (blast del: equalityCE)
   3.150 -  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   3.151 -   prefer 2 apply simp
   3.152 -  apply (subgoal_tac "yb = f xa x")
   3.153 -   prefer 2 
   3.154 -(*   apply (drule_tac x = xa in Diff1_foldSetD)
   3.155 -     apply assumption
   3.156 -     apply (rule f_closed) apply best apply (rule foldSetD_closed)
   3.157 -     prefer 3 apply assumption apply (rule e_closed)
   3.158 -     apply (rule f_closed) apply best apply assumption
   3.159 -*)
   3.160 -   apply (blast del: equalityCE dest: Diff1_foldSetD)
   3.161 -   apply (simp (no_asm_simp))
   3.162 -   apply (rule left_commute)
   3.163 -   apply assumption apply best apply best
   3.164 - done
   3.165 -
   3.166 -lemma (in LCD) foldSetD_determ:
   3.167 -  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   3.168 -   ==> y = x"
   3.169 -  by (blast intro: foldSetD_determ_aux [rule_format])
   3.170 -
   3.171 -lemma (in LCD) foldD_equality:
   3.172 -  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   3.173 -  by (unfold foldD_def) (blast intro: foldSetD_determ)
   3.174 -
   3.175 -lemma foldD_empty [simp]:
   3.176 -  "e : D ==> foldD D f e {} = e"
   3.177 -  by (unfold foldD_def) blast
   3.178 -
   3.179 -lemma (in LCD) foldD_insert_aux:
   3.180 -  "[| x ~: A; x : B; e : D; A <= B |] ==>
   3.181 -    ((insert x A, v) : foldSetD D f e) =
   3.182 -    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   3.183 -  apply auto
   3.184 -  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   3.185 -   apply (fastsimp dest: foldSetD_imp_finite)
   3.186 -(* new subgoal by finite_imp_foldSetD *)
   3.187 -    apply assumption
   3.188 -    apply assumption
   3.189 -  apply (blast intro: foldSetD_determ)
   3.190 -  done
   3.191 -
   3.192 -lemma (in LCD) foldD_insert:
   3.193 -    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   3.194 -     foldD D f e (insert x A) = f x (foldD D f e A)"
   3.195 -  apply (unfold foldD_def)
   3.196 -  apply (simp add: foldD_insert_aux)
   3.197 -  apply (rule the_equality)
   3.198 -  apply (auto intro: finite_imp_foldSetD
   3.199 -    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
   3.200 -  done
   3.201 -
   3.202 -lemma (in LCD) foldD_closed [simp]:
   3.203 -  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   3.204 -proof (induct set: Finites)
   3.205 -  case empty then show ?case by (simp add: foldD_empty)
   3.206 -next
   3.207 -  case insert then show ?case by (simp add: foldD_insert)
   3.208 -qed
   3.209 -
   3.210 -lemma (in LCD) foldD_commute:
   3.211 -  "[| finite A; x : B; e : D; A <= B |] ==>
   3.212 -   f x (foldD D f e A) = foldD D f (f x e) A"
   3.213 -  apply (induct set: Finites)
   3.214 -   apply simp
   3.215 -  apply (auto simp add: left_commute foldD_insert)
   3.216 -  done
   3.217 -
   3.218 -lemma Int_mono2:
   3.219 -  "[| A <= C; B <= C |] ==> A Int B <= C"
   3.220 -  by blast
   3.221 -
   3.222 -lemma (in LCD) foldD_nest_Un_Int:
   3.223 -  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   3.224 -   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   3.225 -  apply (induct set: Finites)
   3.226 -   apply simp
   3.227 -  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
   3.228 -    Int_mono2 Un_subset_iff)
   3.229 -  done
   3.230 -
   3.231 -lemma (in LCD) foldD_nest_Un_disjoint:
   3.232 -  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   3.233 -    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   3.234 -  by (simp add: foldD_nest_Un_Int)
   3.235 -
   3.236 --- {* Delete rules to do with @{text foldSetD} relation. *}
   3.237 -
   3.238 -declare foldSetD_imp_finite [simp del]
   3.239 -  empty_foldSetDE [rule del]
   3.240 -  foldSetD.intros [rule del]
   3.241 -declare (in LCD)
   3.242 -  foldSetD_closed [rule del]
   3.243 -
   3.244 -subsection {* Commutative monoids *}
   3.245 -
   3.246 -text {*
   3.247 -  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   3.248 -  instead of @{text "'b => 'a => 'a"}.
   3.249 -*}
   3.250 -
   3.251 -locale ACeD =
   3.252 -  fixes D :: "'a set"
   3.253 -    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   3.254 -    and e :: 'a
   3.255 -  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   3.256 -    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   3.257 -    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   3.258 -    and e_closed [simp]: "e : D"
   3.259 -    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   3.260 -
   3.261 -lemma (in ACeD) left_commute:
   3.262 -  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   3.263 -proof -
   3.264 -  assume D: "x : D" "y : D" "z : D"
   3.265 -  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   3.266 -  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   3.267 -  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   3.268 -  finally show ?thesis .
   3.269 -qed
   3.270 -
   3.271 -lemmas (in ACeD) AC = assoc commute left_commute
   3.272 -
   3.273 -lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   3.274 -proof -
   3.275 -  assume D: "x : D"
   3.276 -  have "x \<cdot> e = x" by (rule ident)
   3.277 -  with D show ?thesis by (simp add: commute)
   3.278 -qed
   3.279 -
   3.280 -lemma (in ACeD) foldD_Un_Int:
   3.281 -  "[| finite A; finite B; A <= D; B <= D |] ==>
   3.282 -    foldD D f e A \<cdot> foldD D f e B =
   3.283 -    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   3.284 -  apply (induct set: Finites)
   3.285 -   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   3.286 -(* left_commute is required to show premise of LCD.intro *)
   3.287 -  apply (simp add: AC insert_absorb Int_insert_left
   3.288 -    LCD.foldD_insert [OF LCD.intro [of D]]
   3.289 -    LCD.foldD_closed [OF LCD.intro [of D]]
   3.290 -    Int_mono2 Un_subset_iff)
   3.291 -  done
   3.292 -
   3.293 -lemma (in ACeD) foldD_Un_disjoint:
   3.294 -  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   3.295 -    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   3.296 -  by (simp add: foldD_Un_Int
   3.297 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   3.298 -
   3.299 -end
   3.300 -
     4.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 26 14:26:18 2003 +0100
     4.2 +++ b/src/HOL/Algebra/Group.thy	Thu Feb 27 15:12:29 2003 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  header {* Algebraic Structures up to Abelian Groups *}
     4.6  
     4.7 -theory Group = FuncSet + FoldSet:
     4.8 +theory Group = FuncSet:
     4.9  
    4.10  text {*
    4.11    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    4.12 @@ -20,6 +20,14 @@
    4.13  
    4.14  subsection {* Definitions *}
    4.15  
    4.16 +(* The following may be unnecessary. *)
    4.17 +text {*
    4.18 +  We write groups additively.  This simplifies notation for rings.
    4.19 +  All rings have an additive inverse, only fields have a
    4.20 +  multiplicative one.  This definitions reduces the need for
    4.21 +  qualifiers.
    4.22 +*}
    4.23 +
    4.24  record 'a semigroup =
    4.25    carrier :: "'a set"
    4.26    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    4.27 @@ -401,278 +409,4 @@
    4.28  
    4.29  locale abelian_group = abelian_monoid + group
    4.30  
    4.31 -subsection {* Products over Finite Sets *}
    4.32 -
    4.33 -locale finite_prod = abelian_monoid + var prod +
    4.34 -  defines "prod == (%f A. if finite A
    4.35 -      then foldD (carrier G) (op \<otimes> o f) \<one> A
    4.36 -      else arbitrary)"
    4.37 -
    4.38 -(* TODO: nice syntax for the summation operator inside the locale
    4.39 -   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
    4.40 -
    4.41 -ML_setup {* 
    4.42 -
    4.43 -Context.>> (fn thy => (simpset_ref_of thy :=
    4.44 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    4.45 -
    4.46 -lemma (in finite_prod) prod_empty [simp]: 
    4.47 -  "prod f {} = \<one>"
    4.48 -  by (simp add: prod_def)
    4.49 -
    4.50 -ML_setup {* 
    4.51 -
    4.52 -Context.>> (fn thy => (simpset_ref_of thy :=
    4.53 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    4.54 -
    4.55 -declare funcsetI [intro]
    4.56 -  funcset_mem [dest]
    4.57 -
    4.58 -lemma (in finite_prod) prod_insert [simp]:
    4.59 -  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
    4.60 -   prod f (insert a F) = f a \<otimes> prod f F"
    4.61 -  apply (rule trans)
    4.62 -  apply (simp add: prod_def)
    4.63 -  apply (rule trans)
    4.64 -  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
    4.65 -    apply simp
    4.66 -    apply (rule m_lcomm)
    4.67 -      apply fast apply fast apply assumption
    4.68 -    apply (fastsimp intro: m_closed)
    4.69 -    apply simp+ apply fast
    4.70 -  apply (auto simp add: prod_def)
    4.71 -  done
    4.72 -
    4.73 -lemma (in finite_prod) prod_one:
    4.74 -  "finite A ==> prod (%i. \<one>) A = \<one>"
    4.75 -proof (induct set: Finites)
    4.76 -  case empty show ?case by simp
    4.77 -next
    4.78 -  case (insert A a)
    4.79 -  have "(%i. \<one>) \<in> A -> carrier G" by auto
    4.80 -  with insert show ?case by simp
    4.81 -qed
    4.82 -
    4.83 -(*
    4.84 -lemma prod_eq_0_iff [simp]:
    4.85 -    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
    4.86 -  by (induct set: Finites) auto
    4.87 -
    4.88 -lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
    4.89 -  apply (case_tac "finite A")
    4.90 -   prefer 2 apply (simp add: prod_def)
    4.91 -  apply (erule rev_mp)
    4.92 -  apply (erule finite_induct)
    4.93 -   apply auto
    4.94 -  done
    4.95 -
    4.96 -lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
    4.97 -*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
    4.98 -(*
    4.99 -  by (induct set: Finites) auto
   4.100 -*)
   4.101 -
   4.102 -lemma (in finite_prod) prod_closed:
   4.103 -  fixes A
   4.104 -  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   4.105 -  shows "prod f A \<in> carrier G"
   4.106 -using fin f
   4.107 -proof induct
   4.108 -  case empty show ?case by simp
   4.109 -next
   4.110 -  case (insert A a)
   4.111 -  then have a: "f a \<in> carrier G" by fast
   4.112 -  from insert have A: "f \<in> A -> carrier G" by fast
   4.113 -  from insert A a show ?case by simp
   4.114 -qed
   4.115 -
   4.116 -lemma funcset_Int_left [simp, intro]:
   4.117 -  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   4.118 -  by fast
   4.119 -
   4.120 -lemma funcset_Un_left [iff]:
   4.121 -  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   4.122 -  by fast
   4.123 -
   4.124 -lemma (in finite_prod) prod_Un_Int:
   4.125 -  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   4.126 -   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
   4.127 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   4.128 -proof (induct set: Finites)
   4.129 -  case empty then show ?case by (simp add: prod_closed)
   4.130 -next
   4.131 -  case (insert A a)
   4.132 -  then have a: "g a \<in> carrier G" by fast
   4.133 -  from insert have A: "g \<in> A -> carrier G" by fast
   4.134 -  from insert A a show ?case
   4.135 -    by (simp add: ac Int_insert_left insert_absorb prod_closed
   4.136 -          Int_mono2 Un_subset_iff) 
   4.137 -qed
   4.138 -
   4.139 -lemma (in finite_prod) prod_Un_disjoint:
   4.140 -  "[| finite A; finite B; A Int B = {};
   4.141 -      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   4.142 -   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
   4.143 -  apply (subst prod_Un_Int [symmetric])
   4.144 -    apply (auto simp add: prod_closed)
   4.145 -  done
   4.146 -
   4.147 -(*
   4.148 -lemma prod_UN_disjoint:
   4.149 -  fixes f :: "'a => 'b::plus_ac0"
   4.150 -  shows
   4.151 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   4.152 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   4.153 -      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
   4.154 -  apply (induct set: Finites)
   4.155 -   apply simp
   4.156 -  apply atomize
   4.157 -  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   4.158 -   prefer 2 apply blast
   4.159 -  apply (subgoal_tac "A x Int UNION F A = {}")
   4.160 -   prefer 2 apply blast
   4.161 -  apply (simp add: prod_Un_disjoint)
   4.162 -  done
   4.163 -*)
   4.164 -
   4.165 -lemma (in finite_prod) prod_addf:
   4.166 -  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   4.167 -   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
   4.168 -proof (induct set: Finites)
   4.169 -  case empty show ?case by simp
   4.170 -next
   4.171 -  case (insert A a) then
   4.172 -  have fA: "f : A -> carrier G" by fast
   4.173 -  from insert have fa: "f a : carrier G" by fast
   4.174 -  from insert have gA: "g : A -> carrier G" by fast
   4.175 -  from insert have ga: "g a : carrier G" by fast
   4.176 -  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   4.177 -  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   4.178 -    by (simp add: Pi_def)
   4.179 -  show ?case  (* check if all simps are really necessary *)
   4.180 -    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   4.181 -qed
   4.182 -
   4.183 -(*
   4.184 -lemma prod_Un: "finite A ==> finite B ==>
   4.185 -    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
   4.186 -  -- {* For the natural numbers, we have subtraction. *}
   4.187 -  apply (subst prod_Un_Int [symmetric])
   4.188 -    apply auto
   4.189 -  done
   4.190 -
   4.191 -lemma prod_diff1: "(prod f (A - {a}) :: nat) =
   4.192 -    (if a:A then prod f A - f a else prod f A)"
   4.193 -  apply (case_tac "finite A")
   4.194 -   prefer 2 apply (simp add: prod_def)
   4.195 -  apply (erule finite_induct)
   4.196 -   apply (auto simp add: insert_Diff_if)
   4.197 -  apply (drule_tac a = a in mk_disjoint_insert)
   4.198 -  apply auto
   4.199 -  done
   4.200 -*)
   4.201 -
   4.202 -lemma (in finite_prod) prod_cong:
   4.203 -  "[| A = B; g : B -> carrier G;
   4.204 -      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   4.205 -proof -
   4.206 -  assume prems: "A = B" "g : B -> carrier G"
   4.207 -    "!!i. i : B ==> f i = g i"
   4.208 -  show ?thesis
   4.209 -  proof (cases "finite B")
   4.210 -    case True
   4.211 -    then have "!!A. [| A = B; g : B -> carrier G;
   4.212 -      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
   4.213 -    proof induct
   4.214 -      case empty thus ?case by simp
   4.215 -    next
   4.216 -      case (insert B x)
   4.217 -      then have "prod f A = prod f (insert x B)" by simp
   4.218 -      also from insert have "... = f x \<otimes> prod f B"
   4.219 -      proof (intro prod_insert)
   4.220 -	show "finite B" .
   4.221 -      next
   4.222 -	show "x ~: B" .
   4.223 -      next
   4.224 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   4.225 -	  "g \<in> insert x B \<rightarrow> carrier G"
   4.226 -	thus "f : B -> carrier G" by fastsimp
   4.227 -      next
   4.228 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   4.229 -	  "g \<in> insert x B \<rightarrow> carrier G"
   4.230 -	thus "f x \<in> carrier G" by fastsimp
   4.231 -      qed
   4.232 -      also from insert have "... = g x \<otimes> prod g B" by fastsimp
   4.233 -      also from insert have "... = prod g (insert x B)"
   4.234 -      by (intro prod_insert [THEN sym]) auto
   4.235 -      finally show ?case .
   4.236 -    qed
   4.237 -    with prems show ?thesis by simp
   4.238 -  next
   4.239 -    case False with prems show ?thesis by (simp add: prod_def)
   4.240 -  qed
   4.241 -qed
   4.242 -
   4.243 -lemma (in finite_prod) prod_cong1 [cong]:
   4.244 -  "[| A = B; !!i. i : B ==> f i = g i;
   4.245 -      g : B -> carrier G = True |] ==> prod f A = prod g B"
   4.246 -  by (rule prod_cong) fast+
   4.247 -
   4.248 -text {*Usually, if this rule causes a failed congruence proof error,
   4.249 -   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   4.250 -   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
   4.251 -
   4.252 -declare funcsetI [rule del]
   4.253 -  funcset_mem [rule del]
   4.254 -
   4.255 -subsection {* Summation over the integer interval @{term "{..n}"} *}
   4.256 -
   4.257 -text {*
   4.258 -  For technical reasons (locales) a new locale where the index set is
   4.259 -  restricted to @{term "nat"} is necessary.
   4.260 -*}
   4.261 -
   4.262 -locale finite_prod_nat = finite_prod +
   4.263 -  assumes "False ==> prod f (A::nat set) = prod f A"
   4.264 -
   4.265 -lemma (in finite_prod_nat) natSum_0 [simp]:
   4.266 -  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
   4.267 -by (simp add: Pi_def)
   4.268 -
   4.269 -lemma (in finite_prod_nat) natsum_Suc [simp]:
   4.270 -  "f : {..Suc n} -> carrier G ==>
   4.271 -   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
   4.272 -by (simp add: Pi_def atMost_Suc)
   4.273 -
   4.274 -lemma (in finite_prod_nat) natsum_Suc2:
   4.275 -  "f : {..Suc n} -> carrier G ==>
   4.276 -   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
   4.277 -proof (induct n)
   4.278 -  case 0 thus ?case by (simp add: Pi_def)
   4.279 -next
   4.280 -  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
   4.281 -qed
   4.282 -
   4.283 -lemma (in finite_prod_nat) natsum_zero [simp]:
   4.284 -  "prod (%i. \<one>) {..n::nat} = \<one>"
   4.285 -by (induct n) (simp_all add: Pi_def)
   4.286 -
   4.287 -lemma (in finite_prod_nat) natsum_add [simp]:
   4.288 -  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   4.289 -   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
   4.290 -by (induct n) (simp_all add: ac Pi_def prod_closed)
   4.291 -
   4.292 -thm setsum_cong
   4.293 -
   4.294 -ML_setup {* 
   4.295 -
   4.296 -Context.>> (fn thy => (simpset_ref_of thy :=
   4.297 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   4.298 -
   4.299 -lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
   4.300 -apply simp done
   4.301 -
   4.302 -lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"
   4.303 -apply (simp add: Pi_def)
   4.304 -
   4.305  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Algebra/Summation.thy	Thu Feb 27 15:12:29 2003 +0100
     5.3 @@ -0,0 +1,584 @@
     5.4 +(*  Title:      Summation Operator for Abelian Groups
     5.5 +    ID:         $Id$
     5.6 +    Author:     Clemens Ballarin, started 19 November 2002
     5.7 +
     5.8 +This file is largely based on HOL/Finite_Set.thy.
     5.9 +*)
    5.10 +
    5.11 +theory FoldSet = Group:
    5.12 +
    5.13 +section {* Summation operator *}
    5.14 +
    5.15 +(* Instantiation of LC from Finite_Set.thy is not possible,
    5.16 +   because here we have explicit typing rules like x : carrier G.
    5.17 +   We introduce an explicit argument for the domain D *)
    5.18 +
    5.19 +consts
    5.20 +  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
    5.21 +
    5.22 +inductive "foldSetD D f e"
    5.23 +  intros
    5.24 +    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    5.25 +    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    5.26 +                      (insert x A, f x y) : foldSetD D f e"
    5.27 +
    5.28 +inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    5.29 +
    5.30 +constdefs
    5.31 +  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    5.32 +  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    5.33 +
    5.34 +lemma foldSetD_closed:
    5.35 +  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    5.36 +      |] ==> z : D";
    5.37 +  by (erule foldSetD.elims) auto
    5.38 +
    5.39 +lemma Diff1_foldSetD:
    5.40 +  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    5.41 +   (A, f x y) : foldSetD D f e"
    5.42 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    5.43 +   apply auto
    5.44 +  done
    5.45 +
    5.46 +lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    5.47 +  by (induct set: foldSetD) auto
    5.48 +
    5.49 +lemma finite_imp_foldSetD:
    5.50 +  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    5.51 +   EX x. (A, x) : foldSetD D f e"
    5.52 +proof (induct set: Finites)
    5.53 +  case empty then show ?case by auto
    5.54 +next
    5.55 +  case (insert F x)
    5.56 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    5.57 +  with insert have "y : D" by (auto dest: foldSetD_closed)
    5.58 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    5.59 +    by (intro foldSetD.intros) auto
    5.60 +  then show ?case ..
    5.61 +qed
    5.62 +
    5.63 +subsection {* Left-commutative operations *}
    5.64 +
    5.65 +locale LCD =
    5.66 +  fixes B :: "'b set"
    5.67 +  and D :: "'a set"
    5.68 +  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    5.69 +  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    5.70 +  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    5.71 +
    5.72 +lemma (in LCD) foldSetD_closed [dest]:
    5.73 +  "(A, z) : foldSetD D f e ==> z : D";
    5.74 +  by (erule foldSetD.elims) auto
    5.75 +
    5.76 +lemma (in LCD) Diff1_foldSetD:
    5.77 +  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    5.78 +   (A, f x y) : foldSetD D f e"
    5.79 +  apply (subgoal_tac "x : B")
    5.80 +  prefer 2 apply fast
    5.81 +  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    5.82 +   apply auto
    5.83 +  done
    5.84 +
    5.85 +lemma (in LCD) foldSetD_imp_finite [simp]:
    5.86 +  "(A, x) : foldSetD D f e ==> finite A"
    5.87 +  by (induct set: foldSetD) auto
    5.88 +
    5.89 +lemma (in LCD) finite_imp_foldSetD:
    5.90 +  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
    5.91 +proof (induct set: Finites)
    5.92 +  case empty then show ?case by auto
    5.93 +next
    5.94 +  case (insert F x)
    5.95 +  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    5.96 +  with insert have "y : D" by auto
    5.97 +  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    5.98 +    by (intro foldSetD.intros) auto
    5.99 +  then show ?case ..
   5.100 +qed
   5.101 +
   5.102 +lemma (in LCD) foldSetD_determ_aux:
   5.103 +  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   5.104 +    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   5.105 +  apply (induct n)
   5.106 +   apply (auto simp add: less_Suc_eq)
   5.107 +  apply (erule foldSetD.cases)
   5.108 +   apply blast
   5.109 +  apply (erule foldSetD.cases)
   5.110 +   apply blast
   5.111 +  apply clarify
   5.112 +  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   5.113 +  apply (erule rev_mp)
   5.114 +  apply (simp add: less_Suc_eq_le)
   5.115 +  apply (rule impI)
   5.116 +  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   5.117 +   apply (subgoal_tac "Aa = Ab")
   5.118 +    prefer 2 apply (blast elim!: equalityE)
   5.119 +   apply blast
   5.120 +  txt {* case @{prop "xa \<notin> xb"}. *}
   5.121 +  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   5.122 +   prefer 2 apply (blast elim!: equalityE)
   5.123 +  apply clarify
   5.124 +  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   5.125 +   prefer 2 apply blast
   5.126 +  apply (subgoal_tac "card Aa <= card Ab")
   5.127 +   prefer 2
   5.128 +   apply (rule Suc_le_mono [THEN subst])
   5.129 +   apply (simp add: card_Suc_Diff1)
   5.130 +  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
   5.131 +  apply (blast intro: foldSetD_imp_finite finite_Diff)
   5.132 +(* new subgoal from finite_imp_foldSetD *)
   5.133 +    apply best (* blast doesn't seem to solve this *)
   5.134 +   apply assumption
   5.135 +  apply (frule (1) Diff1_foldSetD)
   5.136 +(* new subgoal from Diff1_foldSetD *)
   5.137 +    apply best
   5.138 +(*
   5.139 +apply (best del: foldSetD_closed elim: foldSetD_closed)
   5.140 +    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
   5.141 +    prefer 3 apply assumption apply (rule e_closed)
   5.142 +    apply (rule f_closed) apply force apply assumption
   5.143 +*)
   5.144 +  apply (subgoal_tac "ya = f xb x")
   5.145 +   prefer 2
   5.146 +(* new subgoal to make IH applicable *) 
   5.147 +  apply (subgoal_tac "Aa <= B")
   5.148 +   prefer 2 apply best
   5.149 +   apply (blast del: equalityCE)
   5.150 +  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   5.151 +   prefer 2 apply simp
   5.152 +  apply (subgoal_tac "yb = f xa x")
   5.153 +   prefer 2 
   5.154 +(*   apply (drule_tac x = xa in Diff1_foldSetD)
   5.155 +     apply assumption
   5.156 +     apply (rule f_closed) apply best apply (rule foldSetD_closed)
   5.157 +     prefer 3 apply assumption apply (rule e_closed)
   5.158 +     apply (rule f_closed) apply best apply assumption
   5.159 +*)
   5.160 +   apply (blast del: equalityCE dest: Diff1_foldSetD)
   5.161 +   apply (simp (no_asm_simp))
   5.162 +   apply (rule left_commute)
   5.163 +   apply assumption apply best apply best
   5.164 + done
   5.165 +
   5.166 +lemma (in LCD) foldSetD_determ:
   5.167 +  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   5.168 +   ==> y = x"
   5.169 +  by (blast intro: foldSetD_determ_aux [rule_format])
   5.170 +
   5.171 +lemma (in LCD) foldD_equality:
   5.172 +  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   5.173 +  by (unfold foldD_def) (blast intro: foldSetD_determ)
   5.174 +
   5.175 +lemma foldD_empty [simp]:
   5.176 +  "e : D ==> foldD D f e {} = e"
   5.177 +  by (unfold foldD_def) blast
   5.178 +
   5.179 +lemma (in LCD) foldD_insert_aux:
   5.180 +  "[| x ~: A; x : B; e : D; A <= B |] ==>
   5.181 +    ((insert x A, v) : foldSetD D f e) =
   5.182 +    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   5.183 +  apply auto
   5.184 +  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   5.185 +   apply (fastsimp dest: foldSetD_imp_finite)
   5.186 +(* new subgoal by finite_imp_foldSetD *)
   5.187 +    apply assumption
   5.188 +    apply assumption
   5.189 +  apply (blast intro: foldSetD_determ)
   5.190 +  done
   5.191 +
   5.192 +lemma (in LCD) foldD_insert:
   5.193 +    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   5.194 +     foldD D f e (insert x A) = f x (foldD D f e A)"
   5.195 +  apply (unfold foldD_def)
   5.196 +  apply (simp add: foldD_insert_aux)
   5.197 +  apply (rule the_equality)
   5.198 +  apply (auto intro: finite_imp_foldSetD
   5.199 +    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
   5.200 +  done
   5.201 +
   5.202 +lemma (in LCD) foldD_closed [simp]:
   5.203 +  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   5.204 +proof (induct set: Finites)
   5.205 +  case empty then show ?case by (simp add: foldD_empty)
   5.206 +next
   5.207 +  case insert then show ?case by (simp add: foldD_insert)
   5.208 +qed
   5.209 +
   5.210 +lemma (in LCD) foldD_commute:
   5.211 +  "[| finite A; x : B; e : D; A <= B |] ==>
   5.212 +   f x (foldD D f e A) = foldD D f (f x e) A"
   5.213 +  apply (induct set: Finites)
   5.214 +   apply simp
   5.215 +  apply (auto simp add: left_commute foldD_insert)
   5.216 +  done
   5.217 +
   5.218 +lemma Int_mono2:
   5.219 +  "[| A <= C; B <= C |] ==> A Int B <= C"
   5.220 +  by blast
   5.221 +
   5.222 +lemma (in LCD) foldD_nest_Un_Int:
   5.223 +  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   5.224 +   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   5.225 +  apply (induct set: Finites)
   5.226 +   apply simp
   5.227 +  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
   5.228 +    Int_mono2 Un_subset_iff)
   5.229 +  done
   5.230 +
   5.231 +lemma (in LCD) foldD_nest_Un_disjoint:
   5.232 +  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   5.233 +    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   5.234 +  by (simp add: foldD_nest_Un_Int)
   5.235 +
   5.236 +-- {* Delete rules to do with @{text foldSetD} relation. *}
   5.237 +
   5.238 +declare foldSetD_imp_finite [simp del]
   5.239 +  empty_foldSetDE [rule del]
   5.240 +  foldSetD.intros [rule del]
   5.241 +declare (in LCD)
   5.242 +  foldSetD_closed [rule del]
   5.243 +
   5.244 +subsection {* Commutative monoids *}
   5.245 +
   5.246 +text {*
   5.247 +  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
   5.248 +  instead of @{text "'b => 'a => 'a"}.
   5.249 +*}
   5.250 +
   5.251 +locale ACeD =
   5.252 +  fixes D :: "'a set"
   5.253 +    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   5.254 +    and e :: 'a
   5.255 +  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   5.256 +    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   5.257 +    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   5.258 +    and e_closed [simp]: "e : D"
   5.259 +    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   5.260 +
   5.261 +lemma (in ACeD) left_commute:
   5.262 +  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   5.263 +proof -
   5.264 +  assume D: "x : D" "y : D" "z : D"
   5.265 +  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   5.266 +  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   5.267 +  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   5.268 +  finally show ?thesis .
   5.269 +qed
   5.270 +
   5.271 +lemmas (in ACeD) AC = assoc commute left_commute
   5.272 +
   5.273 +lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   5.274 +proof -
   5.275 +  assume D: "x : D"
   5.276 +  have "x \<cdot> e = x" by (rule ident)
   5.277 +  with D show ?thesis by (simp add: commute)
   5.278 +qed
   5.279 +
   5.280 +lemma (in ACeD) foldD_Un_Int:
   5.281 +  "[| finite A; finite B; A <= D; B <= D |] ==>
   5.282 +    foldD D f e A \<cdot> foldD D f e B =
   5.283 +    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   5.284 +  apply (induct set: Finites)
   5.285 +   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
   5.286 +(* left_commute is required to show premise of LCD.intro *)
   5.287 +  apply (simp add: AC insert_absorb Int_insert_left
   5.288 +    LCD.foldD_insert [OF LCD.intro [of D]]
   5.289 +    LCD.foldD_closed [OF LCD.intro [of D]]
   5.290 +    Int_mono2 Un_subset_iff)
   5.291 +  done
   5.292 +
   5.293 +lemma (in ACeD) foldD_Un_disjoint:
   5.294 +  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   5.295 +    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   5.296 +  by (simp add: foldD_Un_Int
   5.297 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   5.298 +
   5.299 +subsection {* A Product Operator for Finite Sets *}
   5.300 +
   5.301 +text {*
   5.302 +  Definition of product (or summation, if the monoid is written addivitively)
   5.303 +  operator.
   5.304 +*}
   5.305 +
   5.306 +locale finite_prod = abelian_monoid + var prod +
   5.307 +  defines "prod == (%f A. if finite A
   5.308 +      then foldD (carrier G) (op \<otimes> o f) \<one> A
   5.309 +      else arbitrary)"
   5.310 +
   5.311 +(* TODO: nice syntax for the summation operator inside the locale
   5.312 +   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
   5.313 +
   5.314 +ML_setup {* 
   5.315 +
   5.316 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.317 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.318 +
   5.319 +lemma (in finite_prod) prod_empty [simp]: 
   5.320 +  "prod f {} = \<one>"
   5.321 +  by (simp add: prod_def)
   5.322 +
   5.323 +ML_setup {* 
   5.324 +
   5.325 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.326 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   5.327 +
   5.328 +declare funcsetI [intro]
   5.329 +  funcset_mem [dest]
   5.330 +
   5.331 +lemma (in finite_prod) prod_insert [simp]:
   5.332 +  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
   5.333 +   prod f (insert a F) = f a \<otimes> prod f F"
   5.334 +  apply (rule trans)
   5.335 +  apply (simp add: prod_def)
   5.336 +  apply (rule trans)
   5.337 +  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
   5.338 +    apply simp
   5.339 +    apply (rule m_lcomm)
   5.340 +      apply fast apply fast apply assumption
   5.341 +    apply (fastsimp intro: m_closed)
   5.342 +    apply simp+ apply fast
   5.343 +  apply (auto simp add: prod_def)
   5.344 +  done
   5.345 +
   5.346 +lemma (in finite_prod) prod_one:
   5.347 +  "finite A ==> prod (%i. \<one>) A = \<one>"
   5.348 +proof (induct set: Finites)
   5.349 +  case empty show ?case by simp
   5.350 +next
   5.351 +  case (insert A a)
   5.352 +  have "(%i. \<one>) \<in> A -> carrier G" by auto
   5.353 +  with insert show ?case by simp
   5.354 +qed
   5.355 +
   5.356 +(*
   5.357 +lemma prod_eq_0_iff [simp]:
   5.358 +    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
   5.359 +  by (induct set: Finites) auto
   5.360 +
   5.361 +lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
   5.362 +  apply (case_tac "finite A")
   5.363 +   prefer 2 apply (simp add: prod_def)
   5.364 +  apply (erule rev_mp)
   5.365 +  apply (erule finite_induct)
   5.366 +   apply auto
   5.367 +  done
   5.368 +
   5.369 +lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
   5.370 +*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
   5.371 +(*
   5.372 +  by (induct set: Finites) auto
   5.373 +*)
   5.374 +
   5.375 +lemma (in finite_prod) prod_closed:
   5.376 +  fixes A
   5.377 +  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   5.378 +  shows "prod f A \<in> carrier G"
   5.379 +using fin f
   5.380 +proof induct
   5.381 +  case empty show ?case by simp
   5.382 +next
   5.383 +  case (insert A a)
   5.384 +  then have a: "f a \<in> carrier G" by fast
   5.385 +  from insert have A: "f \<in> A -> carrier G" by fast
   5.386 +  from insert A a show ?case by simp
   5.387 +qed
   5.388 +
   5.389 +lemma funcset_Int_left [simp, intro]:
   5.390 +  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
   5.391 +  by fast
   5.392 +
   5.393 +lemma funcset_Un_left [iff]:
   5.394 +  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   5.395 +  by fast
   5.396 +
   5.397 +lemma (in finite_prod) prod_Un_Int:
   5.398 +  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
   5.399 +   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
   5.400 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   5.401 +proof (induct set: Finites)
   5.402 +  case empty then show ?case by (simp add: prod_closed)
   5.403 +next
   5.404 +  case (insert A a)
   5.405 +  then have a: "g a \<in> carrier G" by fast
   5.406 +  from insert have A: "g \<in> A -> carrier G" by fast
   5.407 +  from insert A a show ?case
   5.408 +    by (simp add: ac Int_insert_left insert_absorb prod_closed
   5.409 +          Int_mono2 Un_subset_iff) 
   5.410 +qed
   5.411 +
   5.412 +lemma (in finite_prod) prod_Un_disjoint:
   5.413 +  "[| finite A; finite B; A Int B = {};
   5.414 +      g \<in> A -> carrier G; g \<in> B -> carrier G |]
   5.415 +   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
   5.416 +  apply (subst prod_Un_Int [symmetric])
   5.417 +    apply (auto simp add: prod_closed)
   5.418 +  done
   5.419 +
   5.420 +(*
   5.421 +lemma prod_UN_disjoint:
   5.422 +  fixes f :: "'a => 'b::plus_ac0"
   5.423 +  shows
   5.424 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   5.425 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   5.426 +      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
   5.427 +  apply (induct set: Finites)
   5.428 +   apply simp
   5.429 +  apply atomize
   5.430 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   5.431 +   prefer 2 apply blast
   5.432 +  apply (subgoal_tac "A x Int UNION F A = {}")
   5.433 +   prefer 2 apply blast
   5.434 +  apply (simp add: prod_Un_disjoint)
   5.435 +  done
   5.436 +*)
   5.437 +
   5.438 +lemma (in finite_prod) prod_addf:
   5.439 +  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
   5.440 +   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
   5.441 +proof (induct set: Finites)
   5.442 +  case empty show ?case by simp
   5.443 +next
   5.444 +  case (insert A a) then
   5.445 +  have fA: "f : A -> carrier G" by fast
   5.446 +  from insert have fa: "f a : carrier G" by fast
   5.447 +  from insert have gA: "g : A -> carrier G" by fast
   5.448 +  from insert have ga: "g a : carrier G" by fast
   5.449 +  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
   5.450 +  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   5.451 +    by (simp add: Pi_def)
   5.452 +  show ?case  (* check if all simps are really necessary *)
   5.453 +    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
   5.454 +qed
   5.455 +
   5.456 +(*
   5.457 +lemma prod_Un: "finite A ==> finite B ==>
   5.458 +    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
   5.459 +  apply (subst prod_Un_Int [symmetric])
   5.460 +    apply auto
   5.461 +  done
   5.462 +
   5.463 +lemma prod_diff1: "(prod f (A - {a}) :: nat) =
   5.464 +    (if a:A then prod f A - f a else prod f A)"
   5.465 +  apply (case_tac "finite A")
   5.466 +   prefer 2 apply (simp add: prod_def)
   5.467 +  apply (erule finite_induct)
   5.468 +   apply (auto simp add: insert_Diff_if)
   5.469 +  apply (drule_tac a = a in mk_disjoint_insert)
   5.470 +  apply auto
   5.471 +  done
   5.472 +*)
   5.473 +
   5.474 +text {*
   5.475 +  Congruence rule.  The simplifier requires the rule to be in this form.
   5.476 +*}
   5.477 +(*
   5.478 +lemma (in finite_prod) prod_cong [cong]:
   5.479 +  "[| A = B; !!i. i \<in> B ==> f i = g i;
   5.480 +      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
   5.481 +*)
   5.482 +lemma (in finite_prod) prod_cong:
   5.483 +  "[| A = B; g \<in> B -> carrier G;
   5.484 +      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
   5.485 +
   5.486 +proof -
   5.487 +  assume prems: "A = B"
   5.488 +    "!!i. i \<in> B ==> f i = g i"
   5.489 +    "g \<in> B -> carrier G"
   5.490 +  show ?thesis
   5.491 +  proof (cases "finite B")
   5.492 +    case True
   5.493 +    then have "!!A. [| A = B; g \<in> B -> carrier G;
   5.494 +      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
   5.495 +    proof induct
   5.496 +      case empty thus ?case by simp
   5.497 +    next
   5.498 +      case (insert B x)
   5.499 +      then have "prod f A = prod f (insert x B)" by simp
   5.500 +      also from insert have "... = f x \<otimes> prod f B"
   5.501 +      proof (intro prod_insert)
   5.502 +	show "finite B" .
   5.503 +      next
   5.504 +	show "x \<notin> B" .
   5.505 +      next
   5.506 +	assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   5.507 +	  "g \<in> insert x B \<rightarrow> carrier G"
   5.508 +	thus "f \<in> B -> carrier G" by fastsimp
   5.509 +      next
   5.510 +	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   5.511 +	  "g \<in> insert x B \<rightarrow> carrier G"
   5.512 +	thus "f x \<in> carrier G" by fastsimp
   5.513 +      qed
   5.514 +      also from insert have "... = g x \<otimes> prod g B" by fastsimp
   5.515 +      also from insert have "... = prod g (insert x B)"
   5.516 +      by (intro prod_insert [THEN sym]) auto
   5.517 +      finally show ?case .
   5.518 +    qed
   5.519 +    with prems show ?thesis by simp
   5.520 +  next
   5.521 +    case False with prems show ?thesis by (simp add: prod_def)
   5.522 +  qed
   5.523 +qed
   5.524 +
   5.525 +lemma (in finite_prod) prod_cong1 [cong]:
   5.526 +  "[| A = B; !!i. i \<in> B ==> f i = g i;
   5.527 +      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
   5.528 +  by (rule prod_cong) fast+
   5.529 +
   5.530 +text {*
   5.531 +   Usually, if this rule causes a failed congruence proof error,
   5.532 +   the reason is that the premise @{text "g \<in> B -> carrier G"} could not
   5.533 +   be shown. Adding @{thm [source] Pi_def} to the simpset is often useful.
   5.534 +*}
   5.535 +
   5.536 +declare funcsetI [rule del]
   5.537 +  funcset_mem [rule del]
   5.538 +
   5.539 +subsection {* Summation over the integer interval @{term "{..n}"} *}
   5.540 +
   5.541 +text {*
   5.542 +  A new locale where the index set is restricted to @{term "nat"} is
   5.543 +  necessary, because currently locales demand types in theorems to be as
   5.544 +  general as in the locale's definition.
   5.545 +*}
   5.546 +
   5.547 +locale finite_prod_nat = finite_prod +
   5.548 +  assumes "False ==> prod f (A::nat set) = prod f A"
   5.549 +
   5.550 +lemma (in finite_prod_nat) natSum_0 [simp]:
   5.551 +  "f \<in> {0::nat} -> carrier G ==> prod f {..0} = f 0"
   5.552 +by (simp add: Pi_def)
   5.553 +
   5.554 +lemma (in finite_prod_nat) natsum_Suc [simp]:
   5.555 +  "f \<in> {..Suc n} -> carrier G ==>
   5.556 +   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
   5.557 +by (simp add: Pi_def atMost_Suc)
   5.558 +
   5.559 +lemma (in finite_prod_nat) natsum_Suc2:
   5.560 +  "f \<in> {..Suc n} -> carrier G ==>
   5.561 +   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
   5.562 +proof (induct n)
   5.563 +  case 0 thus ?case by (simp add: Pi_def)
   5.564 +next
   5.565 +  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
   5.566 +qed
   5.567 +
   5.568 +lemma (in finite_prod_nat) natsum_zero [simp]:
   5.569 +  "prod (%i. \<one>) {..n::nat} = \<one>"
   5.570 +by (induct n) (simp_all add: Pi_def)
   5.571 +
   5.572 +lemma (in finite_prod_nat) natsum_add [simp]:
   5.573 +  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
   5.574 +   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
   5.575 +by (induct n) (simp_all add: ac Pi_def prod_closed)
   5.576 +
   5.577 +ML_setup {* 
   5.578 +
   5.579 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.580 +  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   5.581 +
   5.582 +ML_setup {* 
   5.583 +
   5.584 +Context.>> (fn thy => (simpset_ref_of thy :=
   5.585 +  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
   5.586 +
   5.587 +end
     6.1 --- a/src/Pure/meta_simplifier.ML	Wed Feb 26 14:26:18 2003 +0100
     6.2 +++ b/src/Pure/meta_simplifier.ML	Thu Feb 27 15:12:29 2003 +0100
     6.3 @@ -404,13 +404,19 @@
     6.4    is_full_cong_prems prems (xs ~~ ys)
     6.5  end
     6.6  
     6.7 +fun cong_name (Const (a, _)) = Some a
     6.8 +  | cong_name (Free (a, _)) = Some ("Free: " ^ a)
     6.9 +  | cong_name _ = None;
    6.10 +
    6.11  fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
    6.12    let
    6.13      val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
    6.14        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    6.15  (*   val lhs = Pattern.eta_contract lhs; *)
    6.16 -    val (a, _) = dest_Const (head_of (term_of lhs)) handle TERM _ =>
    6.17 -      raise SIMPLIFIER ("Congruence must start with a constant", thm);
    6.18 +    val a = (case cong_name (head_of (term_of lhs)) of
    6.19 +        Some a => a
    6.20 +      | None =>
    6.21 +        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm));
    6.22      val (alist,weak) = congs
    6.23      val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
    6.24             ("Overwriting congruence rule for " ^ quote a);
    6.25 @@ -429,8 +435,10 @@
    6.26      val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
    6.27        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    6.28  (*   val lhs = Pattern.eta_contract lhs; *)
    6.29 -    val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
    6.30 -      raise SIMPLIFIER ("Congruence must start with a constant", thm);
    6.31 +    val a = (case cong_name (head_of lhs) of
    6.32 +        Some a => a
    6.33 +      | None =>
    6.34 +        raise SIMPLIFIER ("Congruence must start with a constant", thm));
    6.35      val (alist,_) = congs
    6.36      val alist2 = filter (fn (x,_)=> x<>a) alist
    6.37      val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
    6.38 @@ -780,8 +788,8 @@
    6.39                             | None => None))
    6.40                       end
    6.41                     val (h, ts) = strip_comb t
    6.42 -               in case h of
    6.43 -                    Const(a, _) =>
    6.44 +               in case cong_name h of
    6.45 +                    Some a =>
    6.46                        (case assoc_string (fst congs, a) of
    6.47                           None => appc ()
    6.48                         | Some cong =>