1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Jan 09 15:49:19 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jan 09 16:40:50 2014 +0100
     1.3 @@ -1920,14 +1920,12 @@
     1.4  
     1.5  text {*
     1.6  \noindent
     1.7 -Fortunately, it is easy to prove the following lemma, where the corecursive call
     1.8 -is moved inside the lazy list constructor, thereby eliminating the need for
     1.9 -@{const lmap}:
    1.10 +A more natural syntax, also supported by Isabelle, is to move corecursive calls
    1.11 +under constructors:
    1.12  *}
    1.13  
    1.14 -    lemma tree\<^sub>i\<^sub>i_of_stream_alt:
    1.15 +    primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
    1.16        "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
    1.17 -    by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
    1.18  
    1.19  text {*
    1.20  The next example illustrates corecursion through functions, which is a bit

     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 15:49:19 2014 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 16:40:50 2014 +0100
     2.3 @@ -78,6 +78,7 @@
     2.4  type corec_spec =
     2.5    {corec: term,
     2.6     disc_exhausts: thm list,
     2.7 +   nested_maps: thm list,
     2.8     nested_map_idents: thm list,
     2.9     nested_map_comps: thm list,
    2.10     ctr_specs: corec_ctr_spec list};
    2.11 @@ -279,23 +280,37 @@
    2.12      fun massage_call bound_Ts U T =
    2.13        massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
    2.14          if has_call t then
    2.15 -          (case t of
    2.16 -            Const (@{const_name prod_case}, _) $ t' =>
    2.17 -            let
    2.18 -              val U' = curried_type U;
    2.19 -              val T' = curried_type T;
    2.20 -            in
    2.21 -              Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
    2.22 -            end
    2.23 -          | t1 $ t2 =>
    2.24 -            (if has_call t2 then
    2.25 -              massage_mutual_call bound_Ts U T t
    2.26 -            else
    2.27 -              massage_map bound_Ts U T t1 $ t2
    2.28 -              handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
    2.29 -          | Abs (s, T', t') =>
    2.30 -            Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
    2.31 -          | _ => massage_mutual_call bound_Ts U T t)
    2.32 +          (case U of
    2.33 +            Type (s, Us) =>
    2.34 +            (case try (dest_ctr ctxt s) t of
    2.35 +              SOME (f, args) =>
    2.36 +              let
    2.37 +                val typof = curry fastype_of1 bound_Ts;
    2.38 +                val f' = mk_ctr Us f
    2.39 +                val f'_T = typof f';
    2.40 +                val arg_Ts = map typof args;
    2.41 +              in
    2.42 +                Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
    2.43 +              end
    2.44 +            | NONE =>
    2.45 +              (case t of
    2.46 +                Const (@{const_name prod_case}, _) $ t' =>
    2.47 +                let
    2.48 +                  val U' = curried_type U;
    2.49 +                  val T' = curried_type T;
    2.50 +                in
    2.51 +                  Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
    2.52 +                end
    2.53 +              | t1 $ t2 =>
    2.54 +                (if has_call t2 then
    2.55 +                  massage_mutual_call bound_Ts U T t
    2.56 +                else
    2.57 +                  massage_map bound_Ts U T t1 $ t2
    2.58 +                  handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
    2.59 +              | Abs (s, T', t') =>
    2.60 +                Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
    2.61 +              | _ => massage_mutual_call bound_Ts U T t))
    2.62 +          | _ => ill_formed_corec_call ctxt t)
    2.63          else
    2.64            build_map_Inl (T, U) $ t) bound_Ts;
    2.65  
    2.66 @@ -355,6 +370,12 @@
    2.67        end)
    2.68    | _ => not_codatatype ctxt res_T);
    2.69  
    2.70 +fun map_thms_of_typ ctxt (Type (s, _)) =
    2.71 +    (case fp_sugar_of ctxt s of
    2.72 +      SOME {index, mapss, ...} => nth mapss index
    2.73 +    | NONE => [])
    2.74 +  | map_thms_of_typ _ _ = [];
    2.75 +
    2.76  fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
    2.77    let
    2.78      val thy = Proof_Context.theory_of lthy;
    2.79 @@ -447,6 +468,7 @@
    2.80          p_is q_isss f_isss f_Tsss =
    2.81        {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
    2.82         disc_exhausts = #disc_exhausts (nth ctr_sugars index),
    2.83 +       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    2.84         nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
    2.85         nested_map_comps = map map_comp_of_bnf nested_bnfs,
    2.86         ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
    2.87 @@ -1047,8 +1069,8 @@
    2.88                  |> single
    2.89              end;
    2.90  
    2.91 -        fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec)
    2.92 -            (disc_eqns : coeqn_data_disc list) excludesss
    2.93 +        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
    2.94 +              : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
    2.95              ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) =
    2.96            let
    2.97              val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs;
    2.98 @@ -1068,8 +1090,8 @@
    2.99                |> curry Logic.list_all (map dest_Free fun_args);
   2.100              val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
   2.101            in
   2.102 -            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
   2.103 -              nested_map_comps sel_corec k m excludesss
   2.104 +            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
   2.105 +              nested_map_idents nested_map_comps sel_corec k m excludesss
   2.106              |> K |> Goal.prove_sorry lthy [] [] goal
   2.107              |> Thm.close_derivation
   2.108              |> pair sel

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 15:49:19 2014 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 16:40:50 2014 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4    val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     3.5      thm list -> int list -> thm list -> thm option -> tactic
     3.6    val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
     3.7 -    thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
     3.8 +    thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
     3.9  end;
    3.10  
    3.11  structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
    3.12 @@ -122,8 +122,8 @@
    3.13        fun_discss) THEN'
    3.14      rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
    3.15  
    3.16 -fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m
    3.17 -    exclsss =
    3.18 +fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
    3.19 +    m exclsss =
    3.20    prelude_tac ctxt defs (fun_sel RS trans) THEN
    3.21    cases_tac ctxt k m exclsss THEN
    3.22    HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
    3.23 @@ -133,8 +133,8 @@
    3.24      Splitter.split_tac (split_if :: splits) ORELSE'
    3.25      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    3.26      etac notE THEN' atac ORELSE'
    3.27 -    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
    3.28 -       (@{thms fst_conv snd_conv id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
    3.29 +    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def
    3.30 +       sum.cases} @ mapsx @ map_comps @ map_idents)))));
    3.31  
    3.32  fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
    3.33    HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'