1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 17:54:09 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 18:07:09 2013 +0200
     1.3 @@ -1877,7 +1877,7 @@
     1.4  constructor view:
     1.5  *}
     1.6  
     1.7 -    primcorec_notyet
     1.8 +    primcorec
     1.9        random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
    1.10      where
    1.11        "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
    1.12 @@ -1987,19 +1987,18 @@
    1.13  constructors:
    1.14  *}
    1.15  
    1.16 -    primcorec_notyet
    1.17 +    primcorec
    1.18        random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
    1.19      where
    1.20        "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" |
    1.21        "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
    1.22        "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
    1.23        "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
    1.24 -      "cont (random_process s f n) = random_process s f (f n)" (* of Skip FIXME *) |
    1.25 +      "cont (random_process s f n) = random_process s f (f n)" of Skip |
    1.26        "prefix (random_process s f n) = shd s" |
    1.27 -      "cont (random_process s f n) = random_process (stl s) f (f n)" (* of Action FIXME *) |
    1.28 +      "cont (random_process s f n) = random_process (stl s) f (f n)" of Action |
    1.29        "left (random_process s f n) = random_process (every_snd s) f (f n)" |
    1.30 -      "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" (*<*)
    1.31 -(*>*)
    1.32 +      "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
    1.33  
    1.34  text {*
    1.35  \noindent

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Sep 24 17:54:09 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Sep 24 18:07:09 2013 +0200
     2.3 @@ -10,11 +10,11 @@
     2.4    val add_primrec_cmd: (binding * string option * mixfix) list ->
     2.5      (Attrib.binding * string) list -> local_theory -> local_theory;
     2.6    val add_primcorecursive_cmd: bool ->
     2.7 -    (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context ->
     2.8 -    Proof.state
     2.9 +    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
    2.10 +    Proof.context -> Proof.state
    2.11    val add_primcorec_cmd: bool ->
    2.12 -    (binding * string option * mixfix) list * (Attrib.binding * string) list -> local_theory ->
    2.13 -    local_theory
    2.14 +    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
    2.15 +    local_theory -> local_theory
    2.16  end;
    2.17  
    2.18  structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
    2.19 @@ -479,7 +479,7 @@
    2.20      }, matchedsss')
    2.21    end;
    2.22  
    2.23 -fun co_dissect_eqn_sel fun_names corec_specs eqn' eqn =
    2.24 +fun co_dissect_eqn_sel fun_names corec_specs eqn' of_spec eqn =
    2.25    let
    2.26      val (lhs, rhs) = HOLogic.dest_eq eqn
    2.27        handle TERM _ =>
    2.28 @@ -490,9 +490,11 @@
    2.29          primrec_error_eqn "malformed selector argument in left-hand side" eqn;
    2.30      val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name)
    2.31        handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn;
    2.32 -    val (ctr_spec, sel) = #ctr_specs corec_spec
    2.33 -      |> the o get_index (try (the o find_first (equal sel) o #sels))
    2.34 -      |>> nth (#ctr_specs corec_spec);
    2.35 +    val ctr_spec =
    2.36 +      if is_some of_spec
    2.37 +      then the (find_first (equal (the of_spec) o #ctr) (#ctr_specs corec_spec))
    2.38 +      else #ctr_specs corec_spec |> filter (exists (equal sel) o #sels) |> the_single
    2.39 +        handle List.Empty => primrec_error_eqn "ambiguous selector - use \"of\"" eqn;
    2.40      val user_eqn = drop_All eqn';
    2.41    in
    2.42      Sel {
    2.43 @@ -529,12 +531,12 @@
    2.44   space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
    2.45  
    2.46      val eqns_data_sel =
    2.47 -      map (co_dissect_eqn_sel fun_names corec_specs eqn') sel_imp_rhss;
    2.48 +      map (co_dissect_eqn_sel fun_names corec_specs eqn' (SOME ctr)) sel_imp_rhss;
    2.49    in
    2.50      (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss')
    2.51    end;
    2.52  
    2.53 -fun co_dissect_eqn sequential fun_names corec_specs eqn' matchedsss =
    2.54 +fun co_dissect_eqn sequential fun_names corec_specs eqn' of_spec matchedsss =
    2.55    let
    2.56      val eqn = drop_All eqn'
    2.57        handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
    2.58 @@ -557,7 +559,7 @@
    2.59        co_dissect_eqn_disc sequential fun_names corec_specs imp_prems imp_rhs matchedsss
    2.60        |>> single
    2.61      else if member (op =) sels head then
    2.62 -      ([co_dissect_eqn_sel fun_names corec_specs eqn' imp_rhs], matchedsss)
    2.63 +      ([co_dissect_eqn_sel fun_names corec_specs eqn' of_spec imp_rhs], matchedsss)
    2.64      else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
    2.65        co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedsss
    2.66      else
    2.67 @@ -693,7 +695,7 @@
    2.68        chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
    2.69      end;
    2.70  
    2.71 -fun add_primcorec simple sequential fixes specs lthy =
    2.72 +fun add_primcorec simple sequential fixes specs of_specs lthy =
    2.73    let
    2.74      val (bs, mxs) = map_split (apfst fst) fixes;
    2.75      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
    2.76 @@ -708,9 +710,9 @@
    2.77      val fun_names = map Binding.name_of bs;
    2.78      val corec_specs = take actual_nn corec_specs'; (*###*)
    2.79  
    2.80 -    val (eqns_data, _) =
    2.81 -      fold_map (co_dissect_eqn sequential fun_names corec_specs) (map snd specs) []
    2.82 -      |>> flat;
    2.83 +    val eqns_data =
    2.84 +      fold_map2 (co_dissect_eqn sequential fun_names corec_specs) (map snd specs) of_specs []
    2.85 +      |> flat o fst;
    2.86  
    2.87      val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
    2.88        |> partition_eq ((op =) o pairself #fun_name)
    2.89 @@ -820,7 +822,7 @@
    2.90                  ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, []))
    2.91                  |> the o merge_options;
    2.92                val m = length prems;
    2.93 -              val t = sel_eqns
    2.94 +              val t = filter (equal ctr o #ctr) sel_eqns
    2.95                  |> fst o finds ((op =) o apsnd #sel) sels
    2.96                  |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
    2.97                  |> curry list_comb ctr
    2.98 @@ -899,11 +901,12 @@
    2.99        |> rpair NONE o SOME
   2.100    end;
   2.101  
   2.102 -fun add_primcorec_ursive_cmd simple seq (raw_fixes, raw_specs) lthy =
   2.103 +fun add_primcorec_ursive_cmd simple seq (raw_fixes, raw_specs') lthy =
   2.104    let
   2.105 -    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
   2.106 +    val (raw_specs, of_specs) = split_list raw_specs' ||> map (Option.map (Syntax.read_term lthy));
   2.107 +    val ((fixes, specs), _) = Specification.read_spec raw_fixes raw_specs lthy;
   2.108    in
   2.109 -    add_primcorec simple seq fixes specs lthy
   2.110 +    add_primcorec simple seq fixes specs of_specs lthy
   2.111      handle ERROR str => primrec_error str
   2.112    end
   2.113    handle Primrec_Error (str, eqns) =>

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Sep 24 17:54:09 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Sep 24 18:07:09 2013 +0200
     3.3 @@ -2921,14 +2921,17 @@
     3.4  
     3.5  val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
     3.6  
     3.7 +val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
     3.8 +  (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
     3.9 +
    3.10  val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
    3.11    "define primitive corecursive functions"
    3.12    ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    3.13 -    (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorecursive_cmd);
    3.14 +    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
    3.15  
    3.16  val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
    3.17    "define primitive corecursive functions"
    3.18    ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    3.19 -    (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
    3.20 +    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
    3.21  
    3.22  end;