made function syntax strict, requiring | to separate equations; cleanup

--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 22 13:36:56 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 22 13:36:57 2007 +0100
@@ -9,27 +9,23 @@
 structure FundefCommon =
 struct
 
-(* Theory Dependencies *)
-val acc_const_name = "Accessible_Part.acc"
-
+(* Profiling *)
 val profile = ref false;
 
 fun PROFILE msg = if !profile then timeap_msg msg else I
 
+
+val acc_const_name = "Accessible_Part.acc"
 fun mk_acc domT R =
     Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
 
-(* FIXME, unused *)
 val function_name = suffix "C"
 val graph_name = suffix "_graph"
 val rel_name = suffix "_rel"
 val dom_name = suffix "_dom"
 
-val dest_rel_name = unsuffix "_rel"
-
 type depgraph = int IntGraph.T
 
-
 datatype ctx_tree 
   = Leaf of term
   | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
@@ -160,30 +156,38 @@
   | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
     FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } 
 
+fun target_of (FundefConfig {target, ...}) = target
 
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
+local 
+  structure P = OuterParse and K = OuterKeyword 
 
-val option_parser = (P.$$$ "sequential" >> K Sequential)
-               || ((P.reserved "default" |-- P.term) >> Default)
-               || (P.reserved "domintros" >> K DomIntros)
-               || (P.reserved "tailrec" >> K Tailrec)
-               || ((P.$$$ "in" |-- P.xname) >> Target)
+  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
+                       
+  val option_parser = (P.$$$ "sequential" >> K Sequential)
+                   || ((P.reserved "default" |-- P.term) >> Default)
+                   || (P.reserved "domintros" >> K DomIntros)
+                   || (P.reserved "tailrec" >> K Tailrec)
+                   || ((P.$$$ "in" |-- P.xname) >> Target)
 
-fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
+  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
                           >> (fn opts => fold apply_opt opts def)
 
+  fun pipe_list1 s = P.enum1 "|" s
+
+  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
+
+  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
+
+  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
+                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
+
+  val statements_ow = pipe_list1 statement_ow
+in
+  fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
 end
 
-
-
-
-
 end
 
-
-
 (* Common Abbreviations *)
 
 structure FundefAbbrev =
@@ -191,32 +195,13 @@
 
 fun implies_elim_swp x y = implies_elim y x
 
-(* Some HOL things frequently used *)
+(* HOL abbreviations *)
 val boolT = HOLogic.boolT
 val mk_prod = HOLogic.mk_prod
-val mk_mem = HOLogic.mk_mem
 val mk_eq = HOLogic.mk_eq
 val eq_const = HOLogic.eq_const
 val Trueprop = HOLogic.mk_Trueprop
-
 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
-fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
-
-fun mk_subset T A B = 
-    let val sT = HOLogic.mk_setT T
-    in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
-
-
-(* with explicit types: Needed with loose bounds *)
-fun mk_relmemT xT yT (x,y) R = 
-    let 
-  val pT = HOLogic.mk_prodT (xT, yT)
-  val RT = HOLogic.mk_setT pT
-    in
-  Const ("op :", [pT, RT] ---> boolT)
-        $ (HOLogic.pair_const xT yT $ x $ y)
-        $ R
-    end
 
 fun free_to_var (Free (v,T)) = Var ((v,0),T)
   | free_to_var _ = raise Match

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Mar 22 13:36:56 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Mar 22 13:36:57 2007 +0100
@@ -181,25 +181,18 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-
-fun or_list1 s = P.enum1 "|" s
-val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
-val statements_ow = or_list1 statement_ow
-
-
-fun fun_cmd fixes statements lthy =
+fun fun_cmd config fixes statements lthy =
     lthy
-      |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
+      |> FundefPackage.add_fundef fixes statements config
       ||> by_pat_completeness_simp
       |-> termination_by_lexicographic_order
 
 
 val funP =
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
-  ((P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
-     >> (fn ((target, fixes), statements) =>
-            (Toplevel.local_theory target (fun_cmd fixes statements))));
+  (fundef_parser FundefCommon.fun_config
+     >> (fn ((config, fixes), statements) =>
+            (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements))));
 
 val _ = OuterSyntax.add_parsers [funP];
 end

--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:56 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:57 2007 +0100
@@ -10,13 +10,13 @@
 signature FUNDEF_PACKAGE =
 sig
     val add_fundef :  (string * string option * mixfix) list
-                      -> ((bstring * Attrib.src list) * (string * bool) list) list list
+                      -> ((bstring * Attrib.src list) * (string * bool)) list 
                       -> FundefCommon.fundef_config
                       -> local_theory
                       -> string * Proof.state
 
     val add_fundef_i:  (string * typ option * mixfix) list
-                       -> ((bstring * Attrib.src list) * (term * bool) list) list list
+                       -> ((bstring * Attrib.src list) * (term * bool)) list
                        -> FundefCommon.fundef_config
                        -> local_theory
                        -> string * Proof.state
@@ -47,15 +47,15 @@
     in xs ~~ f ys end
 
 fun restore_spec_structure reps spec =
-    (burrow o burrow_snd o burrow o K) reps spec
+    (burrow_snd o burrow o K) reps spec
 
 fun add_simps fixes spec sort label moreatts simps lthy =
     let
       val fnames = map (fst o fst) fixes
 
       val (saved_spec_simps, lthy) =
-        fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
-      val saved_simps = flat (map snd (flat saved_spec_simps))
+        fold_map note_theorem (restore_spec_structure simps spec) lthy
+      val saved_simps = flat (map snd saved_spec_simps)
 
       val simps_by_f = sort saved_simps
 
@@ -99,21 +99,21 @@
 
 fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
     let
-      val eqnss = map (map (apsnd (map fst))) eqnss_flags
-      val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
+      val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
+      val eqns = map (apsnd (single o fst)) eqnss_flags
 
       val ((fixes, _), ctxt') = prep fixspec [] lthy
-      val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
-                     |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
-                     |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
-                     |> (burrow o burrow_snd o burrow)
-                          (FundefSplit.split_some_equations lthy)
-                     |> map (map (apsnd flat))
+
+      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
+                         |> apsnd the_single
+
+      val spec = map prep_eqn eqns
+                     |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
+                     |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts))
     in
       ((fixes, spec), ctxt')
     end
 
-
 fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
     let
       val FundefConfig {sequential, default, tailrec, ...} = config
@@ -122,8 +122,7 @@
 
       val defname = mk_defname fixes
 
-      val t_eqns = spec
-                     |> flat |> map snd |> flat (* flatten external structure *)
+      val t_eqns = spec |> map snd |> flat (* flatten external structure *)
 
       val ((goalstate, cont, sort_cont), lthy) =
           FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
@@ -225,26 +224,13 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-
-
-fun or_list1 s = P.enum1 "|" s
-
-val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
-
-val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
-val statements_ow = or_list1 statement_ow
-
-
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
-     >> (fn (((config, target), fixes), statements) =>
-            Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
+  (fundef_parser default_config
+     >> (fn ((config, fixes), statements) =>
+            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd)
             #> Toplevel.print));
 
-
-
 val terminationP =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   (P.opt_target -- Scan.option P.name
@@ -252,7 +238,6 @@
            Toplevel.print o
            Toplevel.local_theory_to_proof target (setup_termination_proof name)));
 
-
 val _ = OuterSyntax.add_parsers [functionP];
 val _ = OuterSyntax.add_parsers [terminationP];
 val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];