tuned;

--- a/src/HOL/NatArith.thy	Thu Jul 04 15:06:46 2002 +0200
+++ b/src/HOL/NatArith.thy	Thu Jul 04 16:48:21 2002 +0200
@@ -1,38 +1,59 @@
 (*  Title:      HOL/NatArith.thy
     ID:         $Id$
+    Author:     Tobias Nipkow and Markus Wenzel
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
 
-Setup arithmetic proof procedures.
-*)
+header {* More arithmetic on natural numbers *}
 
 theory NatArith = Nat
 files "arith_data.ML":
 
 setup arith_setup
 
+
 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
 apply (simp add: less_eq reflcl_trancl [symmetric]
             del: reflcl_trancl)
-by arith
+apply arith
+done
 
-(*elimination of `-' on nat*)
 lemma nat_diff_split:
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
-  by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
+    -- {* elimination of @{text -} on @{text nat} *}
+  by (cases "a<b" rule: case_split)
+    (auto simp add: diff_is_0_eq [THEN iffD2])
 
-(*elimination of `-' on nat in assumptions*)
 lemma nat_diff_split_asm:
     "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
+    -- {* elimination of @{text -} on @{text nat} in assumptions *}
   by (simp split: nat_diff_split)
 
 ML {*
  val nat_diff_split = thm "nat_diff_split";
  val nat_diff_split_asm = thm "nat_diff_split_asm";
 
-(* TODO: use this for force_tac in Provers/clasip.ML *)
 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
-*}
+*} (* TODO: use arith_tac for force_tac in Provers/clasip.ML *)
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
 
+subsubsection {* Generic summation indexed over natural numbers *}
+
+consts
+  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
+primrec
+  "Summation f 0 = 0"
+  "Summation f (Suc n) = Summation f n + f n"
+
+syntax
+  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
+translations
+  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
+
+theorem Summation_step:
+    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
+  by (induct n) simp_all
+
 end

--- a/src/HOL/PreList.thy	Thu Jul 04 15:06:46 2002 +0200
+++ b/src/HOL/PreList.thy	Thu Jul 04 16:48:21 2002 +0200
@@ -19,22 +19,4 @@
 (*belongs to theory Wellfounded_Recursion*)
 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
 
-
-(* generic summation indexed over nat *)
-
-consts
-  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
-primrec
-  "Summation f 0 = 0"
-  "Summation f (Suc n) = Summation f n + f n"
-
-syntax
-  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
-translations
-  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
-
-theorem Summation_step:
-    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
-  by (induct n) simp_all
-
 end

--- a/src/Pure/Isar/locale.ML	Thu Jul 04 15:06:46 2002 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 04 16:48:21 2002 +0200
@@ -75,8 +75,6 @@
   Defines of ((string * 'att list) * ('term * 'term list)) list |
   Notes of ((string * 'att list) * ('fact * 'att list) list) list;
 
-datatype fact_kind = Assume | Define | Note;
-
 datatype expr =
   Locale of string |
   Rename of expr * string option list |
@@ -409,21 +407,16 @@
 
 local
 
-fun activate_elem (ctxt, Fixes fixes) =
-      (ctxt |> ProofContext.add_fixes fixes, [])
+fun activate_elem (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, [])
   | activate_elem (ctxt, Assumes asms) =
       ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms))
       |> ProofContext.assume_i ProofContext.export_assume asms
-      |> apsnd (map (pair Assume))
   | activate_elem (ctxt, Defines defs) =
       ctxt |> ProofContext.assume_i ProofContext.export_def
         (map (fn ((name, atts), (t, ps)) =>
           let val (c, t') = ProofContext.cert_def ctxt t
           in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs)
-      |> apsnd (map (pair Define))
-  | activate_elem (ctxt, Notes facts) =
-      ctxt |> ProofContext.have_thmss_i facts
-      |> apsnd (map (pair Note));
+  | activate_elem (ctxt, Notes facts) = ctxt |> ProofContext.have_thmss_i facts;
 
 fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt =>
   foldl_map activate_elem (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
@@ -444,7 +437,7 @@
 
 fun apply_facts name (ctxt, facts) =
   let val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((name, []), [Notes facts])])
-  in (ctxt', map (#2 o #2) facts') end;
+  in (ctxt', map #2 facts') end;
 
 end;
 
@@ -713,7 +706,7 @@
 fun gen_facts prep_locale thy name =
   let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
     |> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] [];
-  in flat (map (#2 o #2) facts) end;
+  in flat (map #2 facts) end;
 
 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
   let
@@ -790,48 +783,6 @@
 
 (** define locales **)
 
-(* add_locale(_i) *)
-
-local
-
-fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy =
-  let
-    val sign = Theory.sign_of thy;
-    val name = Sign.full_name sign bname;
-    val _ = conditional (is_some (get_locale thy name)) (fn () =>
-      error ("Duplicate definition of locale " ^ quote name));
-
-    val thy_ctxt = ProofContext.init thy;
-    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
-        (int_ext_text, ext_text)) = prep_ctxt raw_import raw_body thy_ctxt;
-
-    val import_parms = params_of import_elemss;
-    val body_parms = params_of body_elemss;
-    val all_parms = import_parms @ body_parms;
-
-    (* FIXME *)
-    val ((_, spec), defs) = int_ext_text;
-    val ((xs, _), _) = int_ext_text;
-    val xs' = all_parms |> mapfilter (fn (p, _) =>
-      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
-
-    val import = prep_expr sign raw_import;
-    val elems = flat (map snd body_elemss);
-  in
-    thy
-    |> declare_locale name
-    |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
-        ((xs', spec), defs) (all_parms, map fst body_parms))
-  end;
-
-in
-
-val add_locale = gen_add_locale read_context intern_expr;
-val add_locale_i = gen_add_locale cert_context (K I);
-
-end;
-
-
 (* store results *)
 
 local
@@ -892,6 +843,48 @@
 end;
 
 
+(* add_locale(_i) *)
+
+local
+
+fun gen_add_locale prep_ctxt prep_expr bname raw_import raw_body thy =
+  let
+    val sign = Theory.sign_of thy;
+    val name = Sign.full_name sign bname;
+    val _ = conditional (is_some (get_locale thy name)) (fn () =>
+      error ("Duplicate definition of locale " ^ quote name));
+
+    val thy_ctxt = ProofContext.init thy;
+    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
+        (int_ext_text, ext_text)) = prep_ctxt raw_import raw_body thy_ctxt;
+
+    val import_parms = params_of import_elemss;
+    val body_parms = params_of body_elemss;
+    val all_parms = import_parms @ body_parms;
+
+    (* FIXME *)
+    val ((_, spec), defs) = int_ext_text;
+    val ((xs, _), _) = int_ext_text;
+    val xs' = all_parms |> mapfilter (fn (p, _) =>
+      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
+
+    val import = prep_expr sign raw_import;
+    val elems = flat (map snd body_elemss);
+  in
+    thy
+    |> declare_locale name
+    |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
+        ((xs', spec), defs) (all_parms, map fst body_parms))
+  end;
+
+in
+
+val add_locale = gen_add_locale read_context intern_expr;
+val add_locale_i = gen_add_locale cert_context (K I);
+
+end;
+
+
 
 (** locale theory setup **)
 

--- a/src/Pure/Isar/proof.ML	Thu Jul 04 15:06:46 2002 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 04 16:48:21 2002 +0200
@@ -249,7 +249,7 @@
 val reset_facts = put_facts None;
 
 fun these_factss (state, named_factss) =
-  state |> put_facts (Some (flat (map #2 named_factss)));
+  state |> put_facts (Some (flat (map snd named_factss)));
 
 
 (* goal *)