# HG changeset patch
# User blanchet
# Date 1382002073 -7200
# Node ID b26baa7f82625610e1e5ec290e446d4f7a281bde
# Parent  a22ded8a7f7db80c023cedd924c10ccde4114ac9
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")

diff -r a22ded8a7f7d -r b26baa7f8262 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 10:29:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 11:27:53 2013 +0200
@@ -25,6 +25,11 @@
      calls: rec_call list,
      rec_thm: thm}
 
+  type basic_corec_ctr_spec =
+    {ctr: term,
+     disc: term,
+     sels: term list}
+
   type corec_ctr_spec =
     {ctr: term,
      disc: term,
@@ -75,6 +80,7 @@
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
+  val basic_corec_specs_of: Proof.context -> typ -> basic_corec_ctr_spec list
   val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
@@ -107,6 +113,11 @@
    calls: rec_call list,
    rec_thm: thm};
 
+type basic_corec_ctr_spec =
+  {ctr: term,
+   disc: term,
+   sels: term list};
+
 type corec_ctr_spec =
   {ctr: term,
    disc: term,
@@ -137,6 +148,8 @@
 
 exception AINT_NO_MAP of term;
 
+fun not_codatatype ctxt T =
+  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
 fun ill_formed_rec_call ctxt t =
   error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
 fun ill_formed_corec_call ctxt t =
@@ -487,10 +500,10 @@
 
     val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
-    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
+    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
 
     val nn0 = length arg_Ts;
-    val nn = length perm_fpTs;
+    val nn = length perm_lfpTs;
     val kks = 0 upto nn - 1;
     val perm_ns = map length perm_ctr_Tsss;
     val perm_mss = map (map length) perm_ctr_Tsss;
@@ -505,10 +518,10 @@
 
     val induct_thms = unpermute0 (conj_dests nn induct_thm);
 
-    val fpTs = unpermute perm_fpTs;
+    val lfpTs = unpermute perm_lfpTs;
     val Cs = unpermute perm_Cs;
 
-    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
+    val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
 
     val substA = Term.subst_TVars As_rho;
@@ -555,6 +568,24 @@
      lthy')
   end;
 
+fun basic_corec_specs_of ctxt res_T =
+  (case res_T of
+    Type (T_name, _) =>
+    (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
+      NONE => not_codatatype ctxt res_T
+    | SOME {ctrs, discs, selss, ...} =>
+      let
+        val thy = Proof_Context.theory_of ctxt;
+        val gfpT = body_type (fastype_of (hd ctrs));
+        val As_rho = tvar_subst thy [gfpT] [res_T];
+        val substA = Term.subst_TVars As_rho;
+
+        fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
+      in
+        map3 mk_spec ctrs discs selss
+      end)
+  | _ => not_codatatype ctxt res_T);
+
 fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -571,10 +602,10 @@
 
     val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
-    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
+    val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
 
     val nn0 = length res_Ts;
-    val nn = length perm_fpTs;
+    val nn = length perm_gfpTs;
     val kks = 0 upto nn - 1;
     val perm_ns = map length perm_ctr_Tsss;
 
@@ -600,10 +631,10 @@
     val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
 
     val f_Tssss = unpermute perm_f_Tssss;
-    val fpTs = unpermute perm_fpTs;
+    val gfpTs = unpermute perm_gfpTs;
     val Cs = unpermute perm_Cs;
 
-    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
+    val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts;
     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
 
     val substA = Term.subst_TVars As_rho;