# HG changeset patch
# User panny
# Date 1381517257 -7200
# Node ID 07a8145aaebaacd01ab92f1ea11b26d030ef88a8
# Parent  92c5bd3b342dabc19159f70333cd0b18ed10ac8f
pass the right theorems to tactic

diff -r 92c5bd3b342d -r 07a8145aaeba src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 16:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 11 20:47:37 2013 +0200
@@ -962,10 +962,8 @@
                 |> single
             end;
 
-        fun prove_code disc_eqns sel_eqns ctr_alist
-            {distincts, sel_splits, sel_split_asms, ctr_specs, ...} =
-(* FIXME doesn't work reliably yet *)
-[](*          let
+        fun prove_code disc_eqns sel_eqns ctr_alist {ctr_specs, ...} =
+          let
             val (fun_name, fun_T, fun_args, maybe_rhs) =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
                find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
@@ -975,16 +973,14 @@
 
             val maybe_rhs' = if is_some maybe_rhs then maybe_rhs else
               let
-                fun prove_code_ctr {ctr, disc, sels, ...} =
+                fun prove_code_ctr {ctr, sels, ...} =
                   if not (exists (equal ctr o fst) ctr_alist) then NONE else
                     let
-                      val (fun_name, fun_T, fun_args, prems) =
+                      val prems =
                         (find_first (equal ctr o #ctr) disc_eqns,
                          find_first (equal ctr o #ctr) sel_eqns)
-                        |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x))
-                        ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, []))
+                        |>> Option.map #prems ||> Option.map #prems
                         |> the o merge_options;
-                      val m = length prems;
                       val t =
                         filter (equal ctr o #ctr) sel_eqns
                         |> fst o finds ((op =) o apsnd #sel) sels
@@ -1005,26 +1001,32 @@
               let
                 val rhs = the maybe_rhs';
                 val bound_Ts = List.rev (map fastype_of fun_args);
-                val rhs' = expand_corec_code_rhs lthy has_call bound_Ts rhs;
-                val cond_ctrs = fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts rhs' [];
+                val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
+                val cond_ctrs =
+                  fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
                 val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
                 val ms = map (Logic.count_prems o prop_of) ctr_thms;
-                val (t', t) = (rhs', rhs)
+                val (raw_t, t) = (raw_rhs, rhs)
                   |> pairself
                     (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
                       map Bound (length fun_args - 1 downto 0)))
                     #> HOLogic.mk_Trueprop
                     #> curry Logic.list_all (map dest_Free fun_args));
-                val discIs = map #discI ctr_specs;
-                val raw_code = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
+                val (distincts, discIs, sel_splits, sel_split_asms) =
+                  case_thms_of_term lthy bound_Ts raw_rhs;
+
+                val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms
-                  |> K |> Goal.prove lthy [] [] t';
+                  |> K |> Goal.prove lthy [] [] raw_t;
+val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
               in
-                mk_primcorec_code_of_raw_code_tac sel_splits raw_code
+                mk_primcorec_code_of_raw_code_tac sel_splits raw_code_thm
                 |> K |> Goal.prove lthy [] [] t
+|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
                 |> single
               end
-          end;*)
+handle ERROR s => (warning s; []) (*###*)
+          end;
 
         val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;
diff -r 92c5bd3b342d -r 07a8145aaeba src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 11 16:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 11 20:47:37 2013 +0200
@@ -49,9 +49,6 @@
      nested_maps: thm list,
      nested_map_idents: thm list,
      nested_map_comps: thm list,
-     distincts: thm list,
-     sel_splits: thm list,
-     sel_split_asms: thm list,
      ctr_specs: corec_ctr_spec list}
 
   val s_not: term -> term
@@ -134,9 +131,6 @@
    nested_maps: thm list,
    nested_map_idents: thm list,
    nested_map_comps: thm list,
-   distincts: thm list,
-   sel_splits: thm list,
-   sel_split_asms: thm list,
    ctr_specs: corec_ctr_spec list};
 
 val id_def = @{thm id_def};
@@ -658,9 +652,6 @@
        nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
        nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
-       distincts = #distincts (nth ctr_sugars index),
-       sel_splits = #sel_splits (nth ctr_sugars index),
-       sel_split_asms = #sel_split_asms (nth ctr_sugars index),
        ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
          disc_coitersss sel_coiterssss};
   in