# HG changeset patch
# User ballarin
# Date 1046355149 -3600
# Node ID 12b2ffbe543a0b2035d9d305bd2d9b63cf9d677a
# Parent  4d50cf8ea3d7fd90475613e123651e3a9811f7ad
Change to meta simplifier: congruence rules may now have frees as head of term.

diff -r 4d50cf8ea3d7 -r 12b2ffbe543a NEWS
--- a/NEWS	Wed Feb 26 14:26:18 2003 +0100
+++ b/NEWS	Thu Feb 27 15:12:29 2003 +0100
@@ -44,10 +44,11 @@
     where n is an integer. Thus you can force termination where previously
     the simplifier would diverge.
 
+  - Accepts free variables as head terms in congruence rules.  Useful in Isar.
 
 * Pure: New flag for triggering if the overall goal of a proof state should
 be printed:
-   PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
+   PG menu: Isabelle/Isar -> Settings -> Show Main Goal
 (ML: Proof.show_main_goal).
 
 * Pure: You can find all matching introduction rules for subgoal 1, i.e. all
diff -r 4d50cf8ea3d7 -r 12b2ffbe543a src/HOL/Algebra/CRing.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/CRing.thy	Thu Feb 27 15:12:29 2003 +0100
@@ -0,0 +1,278 @@
+(*
+  Title:     The algebraic hierarchy of rings
+  Id:        $Id$
+  Author:    Clemens Ballarin, started 9 December 1996
+  Copyright: Clemens Ballarin
+*)
+
+header {* The algebraic hierarchy of rings as axiomatic classes *}
+
+theory Ring = Group
+
+section {* The Algebraic Hierarchy of Rings *}
+
+subsection {* Basic Definitions *}
+
+record 'a ring = "'a group" +
+  zero :: 'a ("\<zero>\<index>")
+  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
+  a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
+
+locale cring = abelian_monoid R +
+  assumes a_abelian_group: "abelian_group (| carrier = carrier R,
+      mult = add R, one = zero R, m_inv = a_inv R |)"
+    and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
+      ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
+    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
+
+ML {*
+  thm "cring.l_distr"
+*}
+
+(*
+locale cring = struct R +
+  assumes a_group: "abelian_group (| carrier = carrier R,
+      mult = add R, one = zero R, m_inv = a_inv R |)"
+    and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
+      mult = mult R, one = one R |)"
+    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
+
+locale field = struct R +
+  assumes a_group: "abelian_group (| carrier = carrier R,
+      mult = add R, one = zero R, m_inv = a_inv R |)"
+    and m_group: "monoid (| carrier = carrier R - {zero R},
+      mult = mult R, one = one R |)"
+    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+      ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
+*)
+(*
+  a_assoc:      "(a + b) + c = a + (b + c)"
+  l_zero:       "0 + a = a"
+  l_neg:        "(-a) + a = 0"
+  a_comm:       "a + b = b + a"
+
+  m_assoc:      "(a * b) * c = a * (b * c)"
+  l_one:        "1 * a = a"
+
+  l_distr:      "(a + b) * c = a * c + b * c"
+
+  m_comm:       "a * b = b * a"
+
+  -- {* Definition of derived operations *}
+
+  minus_def:    "a - b = a + (-b)"
+  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
+  divide_def:   "a / b = a * inverse b"
+  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
+*)
+subsection {* Basic Facts *}
+
+lemma (in cring) a_magma [simp, intro]:
+  "magma (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  using a_abelian_group by (simp only: abelian_group_def)
+
+lemma (in cring) a_l_one [simp, intro]:
+  "l_one (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  using a_abelian_group by (simp only: abelian_group_def)
+
+lemma (in cring) a_abelian_group_parts [simp, intro]:
+  "semigroup_axioms (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  "group_axioms (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  "abelian_semigroup_axioms (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  using a_abelian_group by (simp_all only: abelian_group_def)
+
+lemma (in cring) a_semigroup:
+  "semigroup (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  by (simp add: semigroup_def)
+
+lemma (in cring) a_group:
+  "group (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  by (simp add: group_def)
+
+lemma (in cring) a_abelian_semigroup:
+  "abelian_semigroup (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  by (simp add: abelian_semigroup_def)
+
+lemma (in cring) a_abelian_group:
+  "abelian_group (| carrier = carrier R,
+     mult = add R, one = zero R, m_inv = a_inv R |)"
+  by (simp add: abelian_group_def)
+
+lemma (in cring) a_assoc:
+  "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+  ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+  using semigroup.m_assoc [OF a_semigroup]
+  by simp
+
+lemma (in cring) l_zero:
+  "x \<in> carrier R ==> \<zero> \<oplus> x = x"
+  using l_one.l_one [OF a_l_one]
+  by simp
+
+lemma (in cring) l_neg:
+  "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
+  using group.l_inv [OF a_group]
+  by simp
+
+lemma (in cring) a_comm:
+  "[| x \<in> carrier R; y \<in> carrier R |]
+  ==> x \<oplus> y = y \<oplus> x"
+  using abelian_semigroup.m_comm [OF a_abelian_semigroup]
+  by simp
+
+
+
+
+qed
+
+  l_zero:       "0 + a = a"
+  l_neg:        "(-a) + a = 0"
+  a_comm:       "a + b = b + a"
+
+  m_assoc:      "(a * b) * c = a * (b * c)"
+  l_one:        "1 * a = a"
+
+  l_distr:      "(a + b) * c = a * c + b * c"
+
+  m_comm:       "a * b = b * a"
+text {* Normaliser for Commutative Rings *}
+
+use "order.ML"
+
+method_setup ring =
+  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
+  {* computes distributive normal form in rings *}
+
+subsection {* Rings and the summation operator *}
+
+(* Basic facts --- move to HOL!!! *)
+
+lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
+by simp
+
+lemma natsum_Suc [simp]:
+  "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
+by (simp add: atMost_Suc)
+
+lemma natsum_Suc2:
+  "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case Suc thus ?case by (simp add: assoc) 
+qed
+
+lemma natsum_cong [cong]:
+  "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
+        setsum f {..j} = setsum g {..k}"
+by (induct j) auto
+
+lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
+by (induct n) simp_all
+
+lemma natsum_add [simp]:
+  "!!f::nat=>'a::plus_ac0.
+   setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
+by (induct n) (simp_all add: plus_ac0)
+
+(* Facts specific to rings *)
+
+instance ring < plus_ac0
+proof
+  fix x y z
+  show "(x::'a::ring) + y = y + x" by (rule a_comm)
+  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
+  show "0 + (x::'a::ring) = x" by (rule l_zero)
+qed
+
+ML {*
+  local
+    val lhss = 
+        [read_cterm (sign_of (the_context ()))
+                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
+	 read_cterm (sign_of (the_context ()))
+                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
+	 read_cterm (sign_of (the_context ()))
+                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
+	 read_cterm (sign_of (the_context ()))
+                    ("- ?t::'a::ring", TVar (("'z", 0), []))
+	];
+    fun proc sg _ t = 
+      let val rew = Tactic.prove sg [] []
+            (HOLogic.mk_Trueprop
+              (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
+                (fn _ => simp_tac ring_ss 1)
+            |> mk_meta_eq;
+          val (t', u) = Logic.dest_equals (Thm.prop_of rew);
+      in if t' aconv u 
+        then None
+        else Some rew 
+    end;
+  in
+    val ring_simproc = mk_simproc "ring" lhss proc;
+  end;
+*}
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+lemma natsum_ldistr:
+  "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
+by (induct n) simp_all
+
+lemma natsum_rdistr:
+  "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
+by (induct n) simp_all
+
+subsection {* Integral Domains *}
+
+declare one_not_zero [simp]
+
+lemma zero_not_one [simp]:
+  "0 ~= (1::'a::domain)" 
+by (rule not_sym) simp
+
+lemma integral_iff: (* not by default a simp rule! *)
+  "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
+proof
+  assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
+next
+  assume "a = 0 | b = 0" then show "a * b = 0" by auto
+qed
+
+(*
+lemma "(a::'a::ring) - (a - b) = b" apply simp
+ simproc seems to fail on this example (fixed with new term order)
+*)
+(*
+lemma bug: "(b::'a::ring) - (b - a) = a" by simp
+   simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" 
+*)
+lemma m_lcancel:
+  assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
+proof
+  assume eq: "a * b = a * c"
+  then have "a * (b - c) = 0" by simp
+  then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
+  with prem have "b - c = 0" by auto 
+  then have "b = b - (b - c)" by simp 
+  also have "b - (b - c) = c" by simp
+  finally show "b = c" .
+next
+  assume "b = c" then show "a * b = a * c" by simp
+qed
+
+lemma m_rcancel:
+  "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
+by (simp add: m_lcancel)
+
+end
diff -r 4d50cf8ea3d7 -r 12b2ffbe543a src/HOL/Algebra/FoldSet.thy
--- a/src/HOL/Algebra/FoldSet.thy	Wed Feb 26 14:26:18 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(*  Title:      Summation Operator for Abelian Groups
-    ID:         $Id$
-    Author:     Clemens Ballarin, started 19 November 2002
-
-This file is largely based on HOL/Finite_Set.thy.
-*)
-
-header {* Summation Operator *}
-
-theory FoldSet = Main:
-
-(* Instantiation of LC from Finite_Set.thy is not possible,
-   because here we have explicit typing rules like x : carrier G.
-   We introduce an explicit argument for the domain D *)
-
-consts
-  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
-
-inductive "foldSetD D f e"
-  intros
-    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
-    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
-                      (insert x A, f x y) : foldSetD D f e"
-
-inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
-
-constdefs
-  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
-  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
-
-lemma foldSetD_closed:
-  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
-      |] ==> z : D";
-  by (erule foldSetD.elims) auto
-
-lemma Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
-   (A, f x y) : foldSetD D f e"
-  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
-   apply auto
-  done
-
-lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
-  by (induct set: foldSetD) auto
-
-lemma finite_imp_foldSetD:
-  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
-   EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
-  case empty then show ?case by auto
-next
-  case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by (auto dest: foldSetD_closed)
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
-    by (intro foldSetD.intros) auto
-  then show ?case ..
-qed
-
-subsection {* Left-commutative operations *}
-
-locale LCD =
-  fixes B :: "'b set"
-  and D :: "'a set"
-  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
-  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
-
-lemma (in LCD) foldSetD_closed [dest]:
-  "(A, z) : foldSetD D f e ==> z : D";
-  by (erule foldSetD.elims) auto
-
-lemma (in LCD) Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
-   (A, f x y) : foldSetD D f e"
-  apply (subgoal_tac "x : B")
-  prefer 2 apply fast
-  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
-   apply auto
-  done
-
-lemma (in LCD) foldSetD_imp_finite [simp]:
-  "(A, x) : foldSetD D f e ==> finite A"
-  by (induct set: foldSetD) auto
-
-lemma (in LCD) finite_imp_foldSetD:
-  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
-  case empty then show ?case by auto
-next
-  case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by auto
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
-    by (intro foldSetD.intros) auto
-  then show ?case ..
-qed
-
-lemma (in LCD) foldSetD_determ_aux:
-  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
-    (ALL y. (A, y) : foldSetD D f e --> y = x)"
-  apply (induct n)
-   apply (auto simp add: less_Suc_eq)
-  apply (erule foldSetD.cases)
-   apply blast
-  apply (erule foldSetD.cases)
-   apply blast
-  apply clarify
-  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
-  apply (erule rev_mp)
-  apply (simp add: less_Suc_eq_le)
-  apply (rule impI)
-  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
-   apply (subgoal_tac "Aa = Ab")
-    prefer 2 apply (blast elim!: equalityE)
-   apply blast
-  txt {* case @{prop "xa \<notin> xb"}. *}
-  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
-   prefer 2 apply (blast elim!: equalityE)
-  apply clarify
-  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
-   prefer 2 apply blast
-  apply (subgoal_tac "card Aa <= card Ab")
-   prefer 2
-   apply (rule Suc_le_mono [THEN subst])
-   apply (simp add: card_Suc_Diff1)
-  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
-  apply (blast intro: foldSetD_imp_finite finite_Diff)
-(* new subgoal from finite_imp_foldSetD *)
-    apply best (* blast doesn't seem to solve this *)
-   apply assumption
-  apply (frule (1) Diff1_foldSetD)
-(* new subgoal from Diff1_foldSetD *)
-    apply best
-(*
-apply (best del: foldSetD_closed elim: foldSetD_closed)
-    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
-    prefer 3 apply assumption apply (rule e_closed)
-    apply (rule f_closed) apply force apply assumption
-*)
-  apply (subgoal_tac "ya = f xb x")
-   prefer 2
-(* new subgoal to make IH applicable *) 
-  apply (subgoal_tac "Aa <= B")
-   prefer 2 apply best
-   apply (blast del: equalityCE)
-  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
-   prefer 2 apply simp
-  apply (subgoal_tac "yb = f xa x")
-   prefer 2 
-(*   apply (drule_tac x = xa in Diff1_foldSetD)
-     apply assumption
-     apply (rule f_closed) apply best apply (rule foldSetD_closed)
-     prefer 3 apply assumption apply (rule e_closed)
-     apply (rule f_closed) apply best apply assumption
-*)
-   apply (blast del: equalityCE dest: Diff1_foldSetD)
-   apply (simp (no_asm_simp))
-   apply (rule left_commute)
-   apply assumption apply best apply best
- done
-
-lemma (in LCD) foldSetD_determ:
-  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
-   ==> y = x"
-  by (blast intro: foldSetD_determ_aux [rule_format])
-
-lemma (in LCD) foldD_equality:
-  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
-  by (unfold foldD_def) (blast intro: foldSetD_determ)
-
-lemma foldD_empty [simp]:
-  "e : D ==> foldD D f e {} = e"
-  by (unfold foldD_def) blast
-
-lemma (in LCD) foldD_insert_aux:
-  "[| x ~: A; x : B; e : D; A <= B |] ==>
-    ((insert x A, v) : foldSetD D f e) =
-    (EX y. (A, y) : foldSetD D f e & v = f x y)"
-  apply auto
-  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
-   apply (fastsimp dest: foldSetD_imp_finite)
-(* new subgoal by finite_imp_foldSetD *)
-    apply assumption
-    apply assumption
-  apply (blast intro: foldSetD_determ)
-  done
-
-lemma (in LCD) foldD_insert:
-    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
-     foldD D f e (insert x A) = f x (foldD D f e A)"
-  apply (unfold foldD_def)
-  apply (simp add: foldD_insert_aux)
-  apply (rule the_equality)
-  apply (auto intro: finite_imp_foldSetD
-    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
-  done
-
-lemma (in LCD) foldD_closed [simp]:
-  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
-proof (induct set: Finites)
-  case empty then show ?case by (simp add: foldD_empty)
-next
-  case insert then show ?case by (simp add: foldD_insert)
-qed
-
-lemma (in LCD) foldD_commute:
-  "[| finite A; x : B; e : D; A <= B |] ==>
-   f x (foldD D f e A) = foldD D f (f x e) A"
-  apply (induct set: Finites)
-   apply simp
-  apply (auto simp add: left_commute foldD_insert)
-  done
-
-lemma Int_mono2:
-  "[| A <= C; B <= C |] ==> A Int B <= C"
-  by blast
-
-lemma (in LCD) foldD_nest_Un_Int:
-  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
-   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
-  apply (induct set: Finites)
-   apply simp
-  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
-    Int_mono2 Un_subset_iff)
-  done
-
-lemma (in LCD) foldD_nest_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
-    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
-  by (simp add: foldD_nest_Un_Int)
-
--- {* Delete rules to do with @{text foldSetD} relation. *}
-
-declare foldSetD_imp_finite [simp del]
-  empty_foldSetDE [rule del]
-  foldSetD.intros [rule del]
-declare (in LCD)
-  foldSetD_closed [rule del]
-
-subsection {* Commutative monoids *}
-
-text {*
-  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
-  instead of @{text "'b => 'a => 'a"}.
-*}
-
-locale ACeD =
-  fixes D :: "'a set"
-    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
-    and e :: 'a
-  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
-    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
-    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
-    and e_closed [simp]: "e : D"
-    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
-
-lemma (in ACeD) left_commute:
-  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-proof -
-  assume D: "x : D" "y : D" "z : D"
-  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
-  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
-  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
-  finally show ?thesis .
-qed
-
-lemmas (in ACeD) AC = assoc commute left_commute
-
-lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
-proof -
-  assume D: "x : D"
-  have "x \<cdot> e = x" by (rule ident)
-  with D show ?thesis by (simp add: commute)
-qed
-
-lemma (in ACeD) foldD_Un_Int:
-  "[| finite A; finite B; A <= D; B <= D |] ==>
-    foldD D f e A \<cdot> foldD D f e B =
-    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
-  apply (induct set: Finites)
-   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
-(* left_commute is required to show premise of LCD.intro *)
-  apply (simp add: AC insert_absorb Int_insert_left
-    LCD.foldD_insert [OF LCD.intro [of D]]
-    LCD.foldD_closed [OF LCD.intro [of D]]
-    Int_mono2 Un_subset_iff)
-  done
-
-lemma (in ACeD) foldD_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
-    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
-  by (simp add: foldD_Un_Int
-    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
-
-end
-
diff -r 4d50cf8ea3d7 -r 12b2ffbe543a src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Feb 26 14:26:18 2003 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Feb 27 15:12:29 2003 +0100
@@ -8,7 +8,7 @@
 
 header {* Algebraic Structures up to Abelian Groups *}
 
-theory Group = FuncSet + FoldSet:
+theory Group = FuncSet:
 
 text {*
   Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
@@ -20,6 +20,14 @@
 
 subsection {* Definitions *}
 
+(* The following may be unnecessary. *)
+text {*
+  We write groups additively.  This simplifies notation for rings.
+  All rings have an additive inverse, only fields have a
+  multiplicative one.  This definitions reduces the need for
+  qualifiers.
+*}
+
 record 'a semigroup =
   carrier :: "'a set"
   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
@@ -401,278 +409,4 @@
 
 locale abelian_group = abelian_monoid + group
 
-subsection {* Products over Finite Sets *}
-
-locale finite_prod = abelian_monoid + var prod +
-  defines "prod == (%f A. if finite A
-      then foldD (carrier G) (op \<otimes> o f) \<one> A
-      else arbitrary)"
-
-(* TODO: nice syntax for the summation operator inside the locale
-   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-lemma (in finite_prod) prod_empty [simp]: 
-  "prod f {} = \<one>"
-  by (simp add: prod_def)
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
-
-declare funcsetI [intro]
-  funcset_mem [dest]
-
-lemma (in finite_prod) prod_insert [simp]:
-  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
-   prod f (insert a F) = f a \<otimes> prod f F"
-  apply (rule trans)
-  apply (simp add: prod_def)
-  apply (rule trans)
-  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
-    apply simp
-    apply (rule m_lcomm)
-      apply fast apply fast apply assumption
-    apply (fastsimp intro: m_closed)
-    apply simp+ apply fast
-  apply (auto simp add: prod_def)
-  done
-
-lemma (in finite_prod) prod_one:
-  "finite A ==> prod (%i. \<one>) A = \<one>"
-proof (induct set: Finites)
-  case empty show ?case by simp
-next
-  case (insert A a)
-  have "(%i. \<one>) \<in> A -> carrier G" by auto
-  with insert show ?case by simp
-qed
-
-(*
-lemma prod_eq_0_iff [simp]:
-    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
-  by (induct set: Finites) auto
-
-lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: prod_def)
-  apply (erule rev_mp)
-  apply (erule finite_induct)
-   apply auto
-  done
-
-lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
-*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
-(*
-  by (induct set: Finites) auto
-*)
-
-lemma (in finite_prod) prod_closed:
-  fixes A
-  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
-  shows "prod f A \<in> carrier G"
-using fin f
-proof induct
-  case empty show ?case by simp
-next
-  case (insert A a)
-  then have a: "f a \<in> carrier G" by fast
-  from insert have A: "f \<in> A -> carrier G" by fast
-  from insert A a show ?case by simp
-qed
-
-lemma funcset_Int_left [simp, intro]:
-  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
-  by fast
-
-lemma funcset_Un_left [iff]:
-  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
-  by fast
-
-lemma (in finite_prod) prod_Un_Int:
-  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
-   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
-  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-proof (induct set: Finites)
-  case empty then show ?case by (simp add: prod_closed)
-next
-  case (insert A a)
-  then have a: "g a \<in> carrier G" by fast
-  from insert have A: "g \<in> A -> carrier G" by fast
-  from insert A a show ?case
-    by (simp add: ac Int_insert_left insert_absorb prod_closed
-          Int_mono2 Un_subset_iff) 
-qed
-
-lemma (in finite_prod) prod_Un_disjoint:
-  "[| finite A; finite B; A Int B = {};
-      g \<in> A -> carrier G; g \<in> B -> carrier G |]
-   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
-  apply (subst prod_Un_Int [symmetric])
-    apply (auto simp add: prod_closed)
-  done
-
-(*
-lemma prod_UN_disjoint:
-  fixes f :: "'a => 'b::plus_ac0"
-  shows
-    "finite I ==> (ALL i:I. finite (A i)) ==>
-        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
-  apply (induct set: Finites)
-   apply simp
-  apply atomize
-  apply (subgoal_tac "ALL i:F. x \<noteq> i")
-   prefer 2 apply blast
-  apply (subgoal_tac "A x Int UNION F A = {}")
-   prefer 2 apply blast
-  apply (simp add: prod_Un_disjoint)
-  done
-*)
-
-lemma (in finite_prod) prod_addf:
-  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
-   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
-proof (induct set: Finites)
-  case empty show ?case by simp
-next
-  case (insert A a) then
-  have fA: "f : A -> carrier G" by fast
-  from insert have fa: "f a : carrier G" by fast
-  from insert have gA: "g : A -> carrier G" by fast
-  from insert have ga: "g a : carrier G" by fast
-  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
-  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
-    by (simp add: Pi_def)
-  show ?case  (* check if all simps are really necessary *)
-    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
-qed
-
-(*
-lemma prod_Un: "finite A ==> finite B ==>
-    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
-  -- {* For the natural numbers, we have subtraction. *}
-  apply (subst prod_Un_Int [symmetric])
-    apply auto
-  done
-
-lemma prod_diff1: "(prod f (A - {a}) :: nat) =
-    (if a:A then prod f A - f a else prod f A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: prod_def)
-  apply (erule finite_induct)
-   apply (auto simp add: insert_Diff_if)
-  apply (drule_tac a = a in mk_disjoint_insert)
-  apply auto
-  done
-*)
-
-lemma (in finite_prod) prod_cong:
-  "[| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
-proof -
-  assume prems: "A = B" "g : B -> carrier G"
-    "!!i. i : B ==> f i = g i"
-  show ?thesis
-  proof (cases "finite B")
-    case True
-    then have "!!A. [| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> prod f A = prod g B"
-    proof induct
-      case empty thus ?case by simp
-    next
-      case (insert B x)
-      then have "prod f A = prod f (insert x B)" by simp
-      also from insert have "... = f x \<otimes> prod f B"
-      proof (intro prod_insert)
-	show "finite B" .
-      next
-	show "x ~: B" .
-      next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f : B -> carrier G" by fastsimp
-      next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f x \<in> carrier G" by fastsimp
-      qed
-      also from insert have "... = g x \<otimes> prod g B" by fastsimp
-      also from insert have "... = prod g (insert x B)"
-      by (intro prod_insert [THEN sym]) auto
-      finally show ?case .
-    qed
-    with prems show ?thesis by simp
-  next
-    case False with prems show ?thesis by (simp add: prod_def)
-  qed
-qed
-
-lemma (in finite_prod) prod_cong1 [cong]:
-  "[| A = B; !!i. i : B ==> f i = g i;
-      g : B -> carrier G = True |] ==> prod f A = prod g B"
-  by (rule prod_cong) fast+
-
-text {*Usually, if this rule causes a failed congruence proof error,
-   the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
-   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
-
-declare funcsetI [rule del]
-  funcset_mem [rule del]
-
-subsection {* Summation over the integer interval @{term "{..n}"} *}
-
-text {*
-  For technical reasons (locales) a new locale where the index set is
-  restricted to @{term "nat"} is necessary.
-*}
-
-locale finite_prod_nat = finite_prod +
-  assumes "False ==> prod f (A::nat set) = prod f A"
-
-lemma (in finite_prod_nat) natSum_0 [simp]:
-  "f : {0::nat} -> carrier G ==> prod f {..0} = f 0"
-by (simp add: Pi_def)
-
-lemma (in finite_prod_nat) natsum_Suc [simp]:
-  "f : {..Suc n} -> carrier G ==>
-   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
-by (simp add: Pi_def atMost_Suc)
-
-lemma (in finite_prod_nat) natsum_Suc2:
-  "f : {..Suc n} -> carrier G ==>
-   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
-proof (induct n)
-  case 0 thus ?case by (simp add: Pi_def)
-next
-  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
-qed
-
-lemma (in finite_prod_nat) natsum_zero [simp]:
-  "prod (%i. \<one>) {..n::nat} = \<one>"
-by (induct n) (simp_all add: Pi_def)
-
-lemma (in finite_prod_nat) natsum_add [simp]:
-  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
-   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
-by (induct n) (simp_all add: ac Pi_def prod_closed)
-
-thm setsum_cong
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-lemma "(\<Sum>i\<in>{..10::nat}. if i<=10 then 0 else 1) = (0::nat)"
-apply simp done
-
-lemma (in finite_prod_nat) "prod (%i. if i<=10 then \<one> else x) {..10} = \<one>"
-apply (simp add: Pi_def)
-
 end
diff -r 4d50cf8ea3d7 -r 12b2ffbe543a src/HOL/Algebra/Summation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Summation.thy	Thu Feb 27 15:12:29 2003 +0100
@@ -0,0 +1,584 @@
+(*  Title:      Summation Operator for Abelian Groups
+    ID:         $Id$
+    Author:     Clemens Ballarin, started 19 November 2002
+
+This file is largely based on HOL/Finite_Set.thy.
+*)
+
+theory FoldSet = Group:
+
+section {* Summation operator *}
+
+(* Instantiation of LC from Finite_Set.thy is not possible,
+   because here we have explicit typing rules like x : carrier G.
+   We introduce an explicit argument for the domain D *)
+
+consts
+  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
+
+inductive "foldSetD D f e"
+  intros
+    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
+    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
+                      (insert x A, f x y) : foldSetD D f e"
+
+inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
+
+constdefs
+  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
+
+lemma foldSetD_closed:
+  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
+      |] ==> z : D";
+  by (erule foldSetD.elims) auto
+
+lemma Diff1_foldSetD:
+  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
+   (A, f x y) : foldSetD D f e"
+  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+   apply auto
+  done
+
+lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
+  by (induct set: foldSetD) auto
+
+lemma finite_imp_foldSetD:
+  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
+   EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+  case empty then show ?case by auto
+next
+  case (insert F x)
+  then obtain y where y: "(F, y) : foldSetD D f e" by auto
+  with insert have "y : D" by (auto dest: foldSetD_closed)
+  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+    by (intro foldSetD.intros) auto
+  then show ?case ..
+qed
+
+subsection {* Left-commutative operations *}
+
+locale LCD =
+  fixes B :: "'b set"
+  and D :: "'a set"
+  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
+  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
+
+lemma (in LCD) foldSetD_closed [dest]:
+  "(A, z) : foldSetD D f e ==> z : D";
+  by (erule foldSetD.elims) auto
+
+lemma (in LCD) Diff1_foldSetD:
+  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
+   (A, f x y) : foldSetD D f e"
+  apply (subgoal_tac "x : B")
+  prefer 2 apply fast
+  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+   apply auto
+  done
+
+lemma (in LCD) foldSetD_imp_finite [simp]:
+  "(A, x) : foldSetD D f e ==> finite A"
+  by (induct set: foldSetD) auto
+
+lemma (in LCD) finite_imp_foldSetD:
+  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+  case empty then show ?case by auto
+next
+  case (insert F x)
+  then obtain y where y: "(F, y) : foldSetD D f e" by auto
+  with insert have "y : D" by auto
+  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+    by (intro foldSetD.intros) auto
+  then show ?case ..
+qed
+
+lemma (in LCD) foldSetD_determ_aux:
+  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
+    (ALL y. (A, y) : foldSetD D f e --> y = x)"
+  apply (induct n)
+   apply (auto simp add: less_Suc_eq)
+  apply (erule foldSetD.cases)
+   apply blast
+  apply (erule foldSetD.cases)
+   apply blast
+  apply clarify
+  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
+  apply (erule rev_mp)
+  apply (simp add: less_Suc_eq_le)
+  apply (rule impI)
+  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
+   apply (subgoal_tac "Aa = Ab")
+    prefer 2 apply (blast elim!: equalityE)
+   apply blast
+  txt {* case @{prop "xa \<notin> xb"}. *}
+  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
+   prefer 2 apply (blast elim!: equalityE)
+  apply clarify
+  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
+   prefer 2 apply blast
+  apply (subgoal_tac "card Aa <= card Ab")
+   prefer 2
+   apply (rule Suc_le_mono [THEN subst])
+   apply (simp add: card_Suc_Diff1)
+  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
+  apply (blast intro: foldSetD_imp_finite finite_Diff)
+(* new subgoal from finite_imp_foldSetD *)
+    apply best (* blast doesn't seem to solve this *)
+   apply assumption
+  apply (frule (1) Diff1_foldSetD)
+(* new subgoal from Diff1_foldSetD *)
+    apply best
+(*
+apply (best del: foldSetD_closed elim: foldSetD_closed)
+    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
+    prefer 3 apply assumption apply (rule e_closed)
+    apply (rule f_closed) apply force apply assumption
+*)
+  apply (subgoal_tac "ya = f xb x")
+   prefer 2
+(* new subgoal to make IH applicable *) 
+  apply (subgoal_tac "Aa <= B")
+   prefer 2 apply best
+   apply (blast del: equalityCE)
+  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
+   prefer 2 apply simp
+  apply (subgoal_tac "yb = f xa x")
+   prefer 2 
+(*   apply (drule_tac x = xa in Diff1_foldSetD)
+     apply assumption
+     apply (rule f_closed) apply best apply (rule foldSetD_closed)
+     prefer 3 apply assumption apply (rule e_closed)
+     apply (rule f_closed) apply best apply assumption
+*)
+   apply (blast del: equalityCE dest: Diff1_foldSetD)
+   apply (simp (no_asm_simp))
+   apply (rule left_commute)
+   apply assumption apply best apply best
+ done
+
+lemma (in LCD) foldSetD_determ:
+  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
+   ==> y = x"
+  by (blast intro: foldSetD_determ_aux [rule_format])
+
+lemma (in LCD) foldD_equality:
+  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
+  by (unfold foldD_def) (blast intro: foldSetD_determ)
+
+lemma foldD_empty [simp]:
+  "e : D ==> foldD D f e {} = e"
+  by (unfold foldD_def) blast
+
+lemma (in LCD) foldD_insert_aux:
+  "[| x ~: A; x : B; e : D; A <= B |] ==>
+    ((insert x A, v) : foldSetD D f e) =
+    (EX y. (A, y) : foldSetD D f e & v = f x y)"
+  apply auto
+  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
+   apply (fastsimp dest: foldSetD_imp_finite)
+(* new subgoal by finite_imp_foldSetD *)
+    apply assumption
+    apply assumption
+  apply (blast intro: foldSetD_determ)
+  done
+
+lemma (in LCD) foldD_insert:
+    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
+     foldD D f e (insert x A) = f x (foldD D f e A)"
+  apply (unfold foldD_def)
+  apply (simp add: foldD_insert_aux)
+  apply (rule the_equality)
+  apply (auto intro: finite_imp_foldSetD
+    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
+  done
+
+lemma (in LCD) foldD_closed [simp]:
+  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
+proof (induct set: Finites)
+  case empty then show ?case by (simp add: foldD_empty)
+next
+  case insert then show ?case by (simp add: foldD_insert)
+qed
+
+lemma (in LCD) foldD_commute:
+  "[| finite A; x : B; e : D; A <= B |] ==>
+   f x (foldD D f e A) = foldD D f (f x e) A"
+  apply (induct set: Finites)
+   apply simp
+  apply (auto simp add: left_commute foldD_insert)
+  done
+
+lemma Int_mono2:
+  "[| A <= C; B <= C |] ==> A Int B <= C"
+  by blast
+
+lemma (in LCD) foldD_nest_Un_Int:
+  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
+   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
+  apply (induct set: Finites)
+   apply simp
+  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
+    Int_mono2 Un_subset_iff)
+  done
+
+lemma (in LCD) foldD_nest_Un_disjoint:
+  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
+    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
+  by (simp add: foldD_nest_Un_Int)
+
+-- {* Delete rules to do with @{text foldSetD} relation. *}
+
+declare foldSetD_imp_finite [simp del]
+  empty_foldSetDE [rule del]
+  foldSetD.intros [rule del]
+declare (in LCD)
+  foldSetD_closed [rule del]
+
+subsection {* Commutative monoids *}
+
+text {*
+  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
+  instead of @{text "'b => 'a => 'a"}.
+*}
+
+locale ACeD =
+  fixes D :: "'a set"
+    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
+    and e :: 'a
+  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
+    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
+    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+    and e_closed [simp]: "e : D"
+    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
+
+lemma (in ACeD) left_commute:
+  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+proof -
+  assume D: "x : D" "y : D" "z : D"
+  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
+  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
+  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
+  finally show ?thesis .
+qed
+
+lemmas (in ACeD) AC = assoc commute left_commute
+
+lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
+proof -
+  assume D: "x : D"
+  have "x \<cdot> e = x" by (rule ident)
+  with D show ?thesis by (simp add: commute)
+qed
+
+lemma (in ACeD) foldD_Un_Int:
+  "[| finite A; finite B; A <= D; B <= D |] ==>
+    foldD D f e A \<cdot> foldD D f e B =
+    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
+  apply (induct set: Finites)
+   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
+(* left_commute is required to show premise of LCD.intro *)
+  apply (simp add: AC insert_absorb Int_insert_left
+    LCD.foldD_insert [OF LCD.intro [of D]]
+    LCD.foldD_closed [OF LCD.intro [of D]]
+    Int_mono2 Un_subset_iff)
+  done
+
+lemma (in ACeD) foldD_Un_disjoint:
+  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
+    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
+  by (simp add: foldD_Un_Int
+    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+
+subsection {* A Product Operator for Finite Sets *}
+
+text {*
+  Definition of product (or summation, if the monoid is written addivitively)
+  operator.
+*}
+
+locale finite_prod = abelian_monoid + var prod +
+  defines "prod == (%f A. if finite A
+      then foldD (carrier G) (op \<otimes> o f) \<one> A
+      else arbitrary)"
+
+(* TODO: nice syntax for the summation operator inside the locale
+   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
+
+ML_setup {* 
+
+Context.>> (fn thy => (simpset_ref_of thy :=
+  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+
+lemma (in finite_prod) prod_empty [simp]: 
+  "prod f {} = \<one>"
+  by (simp add: prod_def)
+
+ML_setup {* 
+
+Context.>> (fn thy => (simpset_ref_of thy :=
+  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+
+declare funcsetI [intro]
+  funcset_mem [dest]
+
+lemma (in finite_prod) prod_insert [simp]:
+  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
+   prod f (insert a F) = f a \<otimes> prod f F"
+  apply (rule trans)
+  apply (simp add: prod_def)
+  apply (rule trans)
+  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
+    apply simp
+    apply (rule m_lcomm)
+      apply fast apply fast apply assumption
+    apply (fastsimp intro: m_closed)
+    apply simp+ apply fast
+  apply (auto simp add: prod_def)
+  done
+
+lemma (in finite_prod) prod_one:
+  "finite A ==> prod (%i. \<one>) A = \<one>"
+proof (induct set: Finites)
+  case empty show ?case by simp
+next
+  case (insert A a)
+  have "(%i. \<one>) \<in> A -> carrier G" by auto
+  with insert show ?case by simp
+qed
+
+(*
+lemma prod_eq_0_iff [simp]:
+    "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))"
+  by (induct set: Finites) auto
+
+lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: prod_def)
+  apply (erule rev_mp)
+  apply (erule finite_induct)
+   apply auto
+  done
+
+lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A"
+*)  -- {* Could allow many @{text "card"} proofs to be simplified. *}
+(*
+  by (induct set: Finites) auto
+*)
+
+lemma (in finite_prod) prod_closed:
+  fixes A
+  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
+  shows "prod f A \<in> carrier G"
+using fin f
+proof induct
+  case empty show ?case by simp
+next
+  case (insert A a)
+  then have a: "f a \<in> carrier G" by fast
+  from insert have A: "f \<in> A -> carrier G" by fast
+  from insert A a show ?case by simp
+qed
+
+lemma funcset_Int_left [simp, intro]:
+  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
+  by fast
+
+lemma funcset_Un_left [iff]:
+  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
+  by fast
+
+lemma (in finite_prod) prod_Un_Int:
+  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+   prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B"
+  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+proof (induct set: Finites)
+  case empty then show ?case by (simp add: prod_closed)
+next
+  case (insert A a)
+  then have a: "g a \<in> carrier G" by fast
+  from insert have A: "g \<in> A -> carrier G" by fast
+  from insert A a show ?case
+    by (simp add: ac Int_insert_left insert_absorb prod_closed
+          Int_mono2 Un_subset_iff) 
+qed
+
+lemma (in finite_prod) prod_Un_disjoint:
+  "[| finite A; finite B; A Int B = {};
+      g \<in> A -> carrier G; g \<in> B -> carrier G |]
+   ==> prod g (A Un B) = prod g A \<otimes> prod g B"
+  apply (subst prod_Un_Int [symmetric])
+    apply (auto simp add: prod_closed)
+  done
+
+(*
+lemma prod_UN_disjoint:
+  fixes f :: "'a => 'b::plus_ac0"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I"
+  apply (induct set: Finites)
+   apply simp
+  apply atomize
+  apply (subgoal_tac "ALL i:F. x \<noteq> i")
+   prefer 2 apply blast
+  apply (subgoal_tac "A x Int UNION F A = {}")
+   prefer 2 apply blast
+  apply (simp add: prod_Un_disjoint)
+  done
+*)
+
+lemma (in finite_prod) prod_addf:
+  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+   prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)"
+proof (induct set: Finites)
+  case empty show ?case by simp
+next
+  case (insert A a) then
+  have fA: "f : A -> carrier G" by fast
+  from insert have fa: "f a : carrier G" by fast
+  from insert have gA: "g : A -> carrier G" by fast
+  from insert have ga: "g a : carrier G" by fast
+  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
+  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
+    by (simp add: Pi_def)
+  show ?case  (* check if all simps are really necessary *)
+    by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
+qed
+
+(*
+lemma prod_Un: "finite A ==> finite B ==>
+    (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)"
+  apply (subst prod_Un_Int [symmetric])
+    apply auto
+  done
+
+lemma prod_diff1: "(prod f (A - {a}) :: nat) =
+    (if a:A then prod f A - f a else prod f A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: prod_def)
+  apply (erule finite_induct)
+   apply (auto simp add: insert_Diff_if)
+  apply (drule_tac a = a in mk_disjoint_insert)
+  apply auto
+  done
+*)
+
+text {*
+  Congruence rule.  The simplifier requires the rule to be in this form.
+*}
+(*
+lemma (in finite_prod) prod_cong [cong]:
+  "[| A = B; !!i. i \<in> B ==> f i = g i;
+      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
+*)
+lemma (in finite_prod) prod_cong:
+  "[| A = B; g \<in> B -> carrier G;
+      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
+
+proof -
+  assume prems: "A = B"
+    "!!i. i \<in> B ==> f i = g i"
+    "g \<in> B -> carrier G"
+  show ?thesis
+  proof (cases "finite B")
+    case True
+    then have "!!A. [| A = B; g \<in> B -> carrier G;
+      !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B"
+    proof induct
+      case empty thus ?case by simp
+    next
+      case (insert B x)
+      then have "prod f A = prod f (insert x B)" by simp
+      also from insert have "... = f x \<otimes> prod f B"
+      proof (intro prod_insert)
+	show "finite B" .
+      next
+	show "x \<notin> B" .
+      next
+	assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+	  "g \<in> insert x B \<rightarrow> carrier G"
+	thus "f \<in> B -> carrier G" by fastsimp
+      next
+	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+	  "g \<in> insert x B \<rightarrow> carrier G"
+	thus "f x \<in> carrier G" by fastsimp
+      qed
+      also from insert have "... = g x \<otimes> prod g B" by fastsimp
+      also from insert have "... = prod g (insert x B)"
+      by (intro prod_insert [THEN sym]) auto
+      finally show ?case .
+    qed
+    with prems show ?thesis by simp
+  next
+    case False with prems show ?thesis by (simp add: prod_def)
+  qed
+qed
+
+lemma (in finite_prod) prod_cong1 [cong]:
+  "[| A = B; !!i. i \<in> B ==> f i = g i;
+      g \<in> B -> carrier G = True |] ==> prod f A = prod g B"
+  by (rule prod_cong) fast+
+
+text {*
+   Usually, if this rule causes a failed congruence proof error,
+   the reason is that the premise @{text "g \<in> B -> carrier G"} could not
+   be shown. Adding @{thm [source] Pi_def} to the simpset is often useful.
+*}
+
+declare funcsetI [rule del]
+  funcset_mem [rule del]
+
+subsection {* Summation over the integer interval @{term "{..n}"} *}
+
+text {*
+  A new locale where the index set is restricted to @{term "nat"} is
+  necessary, because currently locales demand types in theorems to be as
+  general as in the locale's definition.
+*}
+
+locale finite_prod_nat = finite_prod +
+  assumes "False ==> prod f (A::nat set) = prod f A"
+
+lemma (in finite_prod_nat) natSum_0 [simp]:
+  "f \<in> {0::nat} -> carrier G ==> prod f {..0} = f 0"
+by (simp add: Pi_def)
+
+lemma (in finite_prod_nat) natsum_Suc [simp]:
+  "f \<in> {..Suc n} -> carrier G ==>
+   prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})"
+by (simp add: Pi_def atMost_Suc)
+
+lemma (in finite_prod_nat) natsum_Suc2:
+  "f \<in> {..Suc n} -> carrier G ==>
+   prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)"
+proof (induct n)
+  case 0 thus ?case by (simp add: Pi_def)
+next
+  case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed)
+qed
+
+lemma (in finite_prod_nat) natsum_zero [simp]:
+  "prod (%i. \<one>) {..n::nat} = \<one>"
+by (induct n) (simp_all add: Pi_def)
+
+lemma (in finite_prod_nat) natsum_add [simp]:
+  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
+   prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}"
+by (induct n) (simp_all add: ac Pi_def prod_closed)
+
+ML_setup {* 
+
+Context.>> (fn thy => (simpset_ref_of thy :=
+  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+
+ML_setup {* 
+
+Context.>> (fn thy => (simpset_ref_of thy :=
+  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+
+end
diff -r 4d50cf8ea3d7 -r 12b2ffbe543a src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Feb 26 14:26:18 2003 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Feb 27 15:12:29 2003 +0100
@@ -404,13 +404,19 @@
   is_full_cong_prems prems (xs ~~ ys)
 end
 
+fun cong_name (Const (a, _)) = Some a
+  | cong_name (Free (a, _)) = Some ("Free: " ^ a)
+  | cong_name _ = None;
+
 fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
   let
     val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
 (*   val lhs = Pattern.eta_contract lhs; *)
-    val (a, _) = dest_Const (head_of (term_of lhs)) handle TERM _ =>
-      raise SIMPLIFIER ("Congruence must start with a constant", thm);
+    val a = (case cong_name (head_of (term_of lhs)) of
+        Some a => a
+      | None =>
+        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm));
     val (alist,weak) = congs
     val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
            ("Overwriting congruence rule for " ^ quote a);
@@ -429,8 +435,10 @@
     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
 (*   val lhs = Pattern.eta_contract lhs; *)
-    val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
-      raise SIMPLIFIER ("Congruence must start with a constant", thm);
+    val a = (case cong_name (head_of lhs) of
+        Some a => a
+      | None =>
+        raise SIMPLIFIER ("Congruence must start with a constant", thm));
     val (alist,_) = congs
     val alist2 = filter (fn (x,_)=> x<>a) alist
     val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
@@ -780,8 +788,8 @@
                            | None => None))
                      end
                    val (h, ts) = strip_comb t
-               in case h of
-                    Const(a, _) =>
+               in case cong_name h of
+                    Some a =>
                       (case assoc_string (fst congs, a) of
                          None => appc ()
                        | Some cong =>