respect order of/additional type variables supplied by the user in fixed point constructions;

--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy	Thu Sep 06 16:06:22 2012 +0200
@@ -53,15 +53,10 @@
    and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
    and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
-codata_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
-       and in_here: 'B = "'b \<times> 'a + 'c"
-
-(* FIXME
 codata ('a, 'b, 'c) some_killing =
   SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
- and ('a, 'b, 'c) in_here =
+   and ('a, 'b, 'c) in_here =
   IH1 'b 'a | IH2 'c
-*)
 
 codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
 and in_here': 'c = "'d + 'e"
@@ -69,7 +64,7 @@
 codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
 and in_here'': 'c = "'d \<times> 'b + 'e"
 
-codata_raw less_killing: 'a = "'b \<Rightarrow> 'c"
+codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
 
 codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
 
@@ -95,6 +90,14 @@
    and ('c, 'e, 'g) ind_wit =
        IW1 | IW2 'c
 
+codata ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
+codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+
+codata 'a dead_foo = A
+(* FIXME: handle unknown type constructors using DEADID?
+codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+*)
+
 (* SLOW, MEMORY-HUNGRY
 codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
    and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"

--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 06 16:06:22 2012 +0200
@@ -51,15 +51,10 @@
  and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
  and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
-data_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
-     and in_here: 'B = "'b \<times> 'a + 'c"
-
-(* FIXME
 data ('a, 'b, 'c) some_killing =
   SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
  and ('a, 'b, 'c) in_here =
   IH1 'b 'a | IH2 'c
-*)
 
 data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b
 data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
@@ -150,4 +145,11 @@
  and s8 = S8 nat
 *)
 
+data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
+data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+
+data 'a dead_foo = A
+(* FIXME: handle unknown type constructors using DEADID?
+data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+*)
 end

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 06 16:06:22 2012 +0200
@@ -23,7 +23,7 @@
     (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
     (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
   val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
-    BNF_Def.BNF * local_theory
+    (BNF_Def.BNF * typ list) * local_theory
 end;
 
 structure BNF_Comp : BNF_COMP =
@@ -656,6 +656,7 @@
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
     val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
     val params = fold Term.add_tfreesT Ds [];
+    val deads = map TFree params;
 
     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
       lthy
@@ -666,7 +667,7 @@
     val phi = Proof_Context.export_morphism lthy lthy';
 
     val bnf_bd' = mk_dir_image bnf_bd
-      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params)))
+      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
 
     val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
     val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
@@ -701,8 +702,8 @@
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
-        ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
+    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
+      ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
 
     val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
     val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
@@ -723,7 +724,7 @@
       |> map (fn (thmN, thms) =>
         ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   in
-    (bnf', lthy' |> Local_Theory.notes notes |> snd)
+    ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
   end;
 
 fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 06 16:06:22 2012 +0200
@@ -103,12 +103,12 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
-    BNF_Def.BNF list -> local_theory -> 'a) ->
+  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
+    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
     local_theory -> 'a
-  val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
-    BNF_Def.BNF list -> local_theory -> 'a) ->
+  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
+    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list * (string list * string list) -> local_theory -> 'a
 end;
 
@@ -272,10 +272,12 @@
 
 (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
    also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
-fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
-  (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
+fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
+    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
+  | fp_sort lhss (SOME resBs) Ass =
+    (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
   let
     val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
     fun qualify i bind =
@@ -286,8 +288,8 @@
       end;
 
     val Ass = map (map dest_TFree) livess;
-    val resDs = fold (subtract (op =)) Ass resBs;
-    val Ds = fold (fold Term.add_tfreesT) deadss resDs;
+    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
+    val Ds = fold (fold Term.add_tfreesT) deadss [];
 
     val _ = (case Library.inter (op =) Ds lhss of [] => ()
       | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
@@ -300,12 +302,13 @@
 
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
-    val (bnfs'', lthy'') =
-      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy';
+    val ((bnfs'', deadss), lthy'') =
+      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
+      |>> split_list;
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
+    val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
@@ -316,25 +319,25 @@
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
-    val sort = fp_sort lhss;
+    val sort = fp_sort lhss (SOME resBs);
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
         (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
-    val sort = fp_sort lhss;
+    val sort = fp_sort lhss NONE;
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => fn rawT =>
         (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
-        bs raw_bnfs (empty_unfold, lthy));
+      bs raw_bnfs (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 end;

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 06 16:06:22 2012 +0200
@@ -9,8 +9,8 @@
 
 signature BNF_GFP =
 sig
-  val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
-    BNF_Def.BNF list -> local_theory ->
+  val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
+    typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
@@ -53,7 +53,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all bnfs have the same lives*)
-fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
+fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -66,8 +66,7 @@
 
     (* TODO: check if m, n etc are sane *)
 
-    val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
-    val deads = fold (union (op =)) Dss (map TFree resDs);
+    val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
@@ -92,8 +91,16 @@
     val Css' = replicate n allCs';
 
     (* typs *)
+    val dead_poss =
+      (case resBs of
+        NONE => map SOME deads @ replicate m NONE
+      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+    fun mk_param NONE passive = (hd passive, tl passive)
+      | mk_param (SOME a) passive = (a, passive);
+    val mk_params = fold_map mk_param dead_poss #> fst;
+
     fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
-    val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
+    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
     val FTsAs = mk_FTs allAs;
     val FTsBs = mk_FTs allBs;
     val FTsCs = mk_FTs allCs;
@@ -1912,7 +1919,7 @@
     (*transforms defined frees into consts*)
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_unfs passive =
-      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
+      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
         Morphism.term phi) unf_frees;
     val unfs = mk_unfs passiveAs;
     val unf's = mk_unfs passiveBs;

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 06 16:06:22 2012 +0200
@@ -8,8 +8,8 @@
 
 signature BNF_LFP =
 sig
-  val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
-    BNF_Def.BNF list -> local_theory ->
+  val bnf_lfp:  mixfix list -> (string * sort) list option -> binding list ->
+    typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
@@ -24,7 +24,7 @@
 open BNF_LFP_Tactics
 
 (*all bnfs have the same lives*)
-fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
+fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val live = live_of_bnf (hd bnfs);
@@ -35,8 +35,7 @@
 
     (* TODO: check if m, n etc are sane *)
 
-    val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
-    val deads = fold (union (op =)) Dss (map TFree resDs);
+    val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
@@ -58,8 +57,16 @@
     val Css' = replicate n allCs';
 
     (* typs *)
+    val dead_poss =
+      (case resBs of
+        NONE => map SOME deads @ replicate m NONE
+      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+    fun mk_param NONE passive = (hd passive, tl passive)
+      | mk_param (SOME a) passive = (a, passive);
+    val mk_params = fold_map mk_param dead_poss #> fst;
+
     fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
-    val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
+    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
     val FTsAs = mk_FTs allAs;
     val FTsBs = mk_FTs allBs;
     val FTsCs = mk_FTs allCs;
@@ -1019,7 +1026,7 @@
     (*transforms defined frees into consts*)
     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_flds passive =
-      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
+      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
         Morphism.term phi) fld_frees;
     val flds = mk_flds passiveAs;
     val fld's = mk_flds passiveBs;