author ballarin Thu Feb 27 15:12:29 2003 +0100 (2003-02-27) changeset 13835 12b2ffbe543a parent 13834 4d50cf8ea3d7 child 13836 6d0392fc6dc5
Change to meta simplifier: congruence rules may now have frees as head of term.
 NEWS file | annotate | diff | revisions src/HOL/Algebra/CRing.thy file | annotate | diff | revisions src/HOL/Algebra/FoldSet.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/Summation.thy file | annotate | diff | revisions src/Pure/meta_simplifier.ML file | annotate | diff | revisions
```     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 =>
```