src/HOL/Tools/function_package/fundef_package.ML
changeset 22498 62cdd4b3e96b
parent 22325 be61bd159a99
child 22623 5fcee5b319a2
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:56 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:57 2007 +0100
     1.3 @@ -10,13 +10,13 @@
     1.4  signature FUNDEF_PACKAGE =
     1.5  sig
     1.6      val add_fundef :  (string * string option * mixfix) list
     1.7 -                      -> ((bstring * Attrib.src list) * (string * bool) list) list list
     1.8 +                      -> ((bstring * Attrib.src list) * (string * bool)) list 
     1.9                        -> FundefCommon.fundef_config
    1.10                        -> local_theory
    1.11                        -> string * Proof.state
    1.12  
    1.13      val add_fundef_i:  (string * typ option * mixfix) list
    1.14 -                       -> ((bstring * Attrib.src list) * (term * bool) list) list list
    1.15 +                       -> ((bstring * Attrib.src list) * (term * bool)) list
    1.16                         -> FundefCommon.fundef_config
    1.17                         -> local_theory
    1.18                         -> string * Proof.state
    1.19 @@ -47,15 +47,15 @@
    1.20      in xs ~~ f ys end
    1.21  
    1.22  fun restore_spec_structure reps spec =
    1.23 -    (burrow o burrow_snd o burrow o K) reps spec
    1.24 +    (burrow_snd o burrow o K) reps spec
    1.25  
    1.26  fun add_simps fixes spec sort label moreatts simps lthy =
    1.27      let
    1.28        val fnames = map (fst o fst) fixes
    1.29  
    1.30        val (saved_spec_simps, lthy) =
    1.31 -        fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
    1.32 -      val saved_simps = flat (map snd (flat saved_spec_simps))
    1.33 +        fold_map note_theorem (restore_spec_structure simps spec) lthy
    1.34 +      val saved_simps = flat (map snd saved_spec_simps)
    1.35  
    1.36        val simps_by_f = sort saved_simps
    1.37  
    1.38 @@ -99,21 +99,21 @@
    1.39  
    1.40  fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
    1.41      let
    1.42 -      val eqnss = map (map (apsnd (map fst))) eqnss_flags
    1.43 -      val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
    1.44 +      val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
    1.45 +      val eqns = map (apsnd (single o fst)) eqnss_flags
    1.46  
    1.47        val ((fixes, _), ctxt') = prep fixspec [] lthy
    1.48 -      val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
    1.49 -                     |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
    1.50 -                     |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
    1.51 -                     |> (burrow o burrow_snd o burrow)
    1.52 -                          (FundefSplit.split_some_equations lthy)
    1.53 -                     |> map (map (apsnd flat))
    1.54 +
    1.55 +      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
    1.56 +                         |> apsnd the_single
    1.57 +
    1.58 +      val spec = map prep_eqn eqns
    1.59 +                     |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
    1.60 +                     |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts))
    1.61      in
    1.62        ((fixes, spec), ctxt')
    1.63      end
    1.64  
    1.65 -
    1.66  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    1.67      let
    1.68        val FundefConfig {sequential, default, tailrec, ...} = config
    1.69 @@ -122,8 +122,7 @@
    1.70  
    1.71        val defname = mk_defname fixes
    1.72  
    1.73 -      val t_eqns = spec
    1.74 -                     |> flat |> map snd |> flat (* flatten external structure *)
    1.75 +      val t_eqns = spec |> map snd |> flat (* flatten external structure *)
    1.76  
    1.77        val ((goalstate, cont, sort_cont), lthy) =
    1.78            FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
    1.79 @@ -225,26 +224,13 @@
    1.80  
    1.81  local structure P = OuterParse and K = OuterKeyword in
    1.82  
    1.83 -
    1.84 -
    1.85 -fun or_list1 s = P.enum1 "|" s
    1.86 -
    1.87 -val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    1.88 -
    1.89 -val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    1.90 -val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
    1.91 -val statements_ow = or_list1 statement_ow
    1.92 -
    1.93 -
    1.94  val functionP =
    1.95    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.96 -  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.97 -     >> (fn (((config, target), fixes), statements) =>
    1.98 -            Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
    1.99 +  (fundef_parser default_config
   1.100 +     >> (fn ((config, fixes), statements) =>
   1.101 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd)
   1.102              #> Toplevel.print));
   1.103  
   1.104 -
   1.105 -
   1.106  val terminationP =
   1.107    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   1.108    (P.opt_target -- Scan.option P.name
   1.109 @@ -252,7 +238,6 @@
   1.110             Toplevel.print o
   1.111             Toplevel.local_theory_to_proof target (setup_termination_proof name)));
   1.112  
   1.113 -
   1.114  val _ = OuterSyntax.add_parsers [functionP];
   1.115  val _ = OuterSyntax.add_parsers [terminationP];
   1.116  val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];