1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 16:31:23 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 20:47:37 2013 +0200
     1.3 @@ -962,10 +962,8 @@
     1.4                  |> single
     1.5              end;
     1.6  
     1.7 -        fun prove_code disc_eqns sel_eqns ctr_alist
     1.8 -            {distincts, sel_splits, sel_split_asms, ctr_specs, ...} =
     1.9 -(* FIXME doesn't work reliably yet *)
    1.10 -[](*          let
    1.11 +        fun prove_code disc_eqns sel_eqns ctr_alist {ctr_specs, ...} =
    1.12 +          let
    1.13              val (fun_name, fun_T, fun_args, maybe_rhs) =
    1.14                (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
    1.15                 find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
    1.16 @@ -975,16 +973,14 @@
    1.17  
    1.18              val maybe_rhs' = if is_some maybe_rhs then maybe_rhs else
    1.19                let
    1.20 -                fun prove_code_ctr {ctr, disc, sels, ...} =
    1.21 +                fun prove_code_ctr {ctr, sels, ...} =
    1.22                    if not (exists (equal ctr o fst) ctr_alist) then NONE else
    1.23                      let
    1.24 -                      val (fun_name, fun_T, fun_args, prems) =
    1.25 +                      val prems =
    1.26                          (find_first (equal ctr o #ctr) disc_eqns,
    1.27                           find_first (equal ctr o #ctr) sel_eqns)
    1.28 -                        |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x))
    1.29 -                        ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, []))
    1.30 +                        |>> Option.map #prems ||> Option.map #prems
    1.31                          |> the o merge_options;
    1.32 -                      val m = length prems;
    1.33                        val t =
    1.34                          filter (equal ctr o #ctr) sel_eqns
    1.35                          |> fst o finds ((op =) o apsnd #sel) sels
    1.36 @@ -1005,26 +1001,32 @@
    1.37                let
    1.38                  val rhs = the maybe_rhs';
    1.39                  val bound_Ts = List.rev (map fastype_of fun_args);
    1.40 -                val rhs' = expand_corec_code_rhs lthy has_call bound_Ts rhs;
    1.41 -                val cond_ctrs = fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts rhs' [];
    1.42 +                val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
    1.43 +                val cond_ctrs =
    1.44 +                  fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
    1.45                  val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
    1.46                  val ms = map (Logic.count_prems o prop_of) ctr_thms;
    1.47 -                val (t', t) = (rhs', rhs)
    1.48 +                val (raw_t, t) = (raw_rhs, rhs)
    1.49                    |> pairself
    1.50                      (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
    1.51                        map Bound (length fun_args - 1 downto 0)))
    1.52                      #> HOLogic.mk_Trueprop
    1.53                      #> curry Logic.list_all (map dest_Free fun_args));
    1.54 -                val discIs = map #discI ctr_specs;
    1.55 -                val raw_code = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
    1.56 +                val (distincts, discIs, sel_splits, sel_split_asms) =
    1.57 +                  case_thms_of_term lthy bound_Ts raw_rhs;
    1.58 +
    1.59 +                val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
    1.60                      sel_split_asms ms ctr_thms
    1.61 -                  |> K |> Goal.prove lthy [] [] t';
    1.62 +                  |> K |> Goal.prove lthy [] [] raw_t;
    1.63 +val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
    1.64                in
    1.65 -                mk_primcorec_code_of_raw_code_tac sel_splits raw_code
    1.66 +                mk_primcorec_code_of_raw_code_tac sel_splits raw_code_thm
    1.67                  |> K |> Goal.prove lthy [] [] t
    1.68 +|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
    1.69                  |> single
    1.70                end
    1.71 -          end;*)
    1.72 +handle ERROR s => (warning s; []) (*###*)
    1.73 +          end;
    1.74  
    1.75          val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
    1.76          val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;