reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping

--- a/src/HOL/Codatatype/BNF_Comp.thy	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Comp.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -12,7 +12,6 @@
 uses
   "Tools/bnf_comp_tactics.ML"
   "Tools/bnf_comp.ML"
-  "Tools/bnf_fp_util.ML"
 begin
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Codatatype/BNF_FP.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Composition of bounded natural functors.
+*)
+
+header {* Composition of Bounded Natural Functors *}
+
+theory BNF_FP
+imports BNF_Comp BNF_Wrap
+keywords
+  "defaults"
+uses
+  "Tools/bnf_fp_util.ML"
+  "Tools/bnf_fp_sugar_tactics.ML"
+  "Tools/bnf_fp_sugar.ML"
+begin
+
+end

--- a/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -8,9 +8,10 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_Comp
+imports BNF_FP
 keywords
-  "codata_raw" :: thy_decl
+  "codata_raw" :: thy_decl and
+  "codata" :: thy_decl
 uses
   "Tools/bnf_gfp_util.ML"
   "Tools/bnf_gfp_tactics.ML"

--- a/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -8,9 +8,10 @@
 header {* Least Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_LFP
-imports BNF_Comp
+imports BNF_FP
 keywords
-  "data_raw" :: thy_decl
+  "data_raw" :: thy_decl and
+  "data" :: thy_decl
 uses
   "Tools/bnf_lfp_util.ML"
   "Tools/bnf_lfp_tactics.ML"

--- a/src/HOL/Codatatype/Codatatype.thy	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -10,14 +10,7 @@
 header {* The (Co)datatype Package *}
 
 theory Codatatype
-imports BNF_LFP BNF_GFP BNF_Wrap
-keywords
-  "data" :: thy_decl and
-  "codata" :: thy_decl and
-  "defaults"
-uses
-  "Tools/bnf_fp_sugar_tactics.ML"
-  "Tools/bnf_fp_sugar.ML"
+imports BNF_LFP BNF_GFP
 begin
 
 end

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 05:03:18 2012 +0200
@@ -8,9 +8,19 @@
 signature BNF_FP_SUGAR =
 sig
   val datatyp: bool ->
+    (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 * thm list *
+         thm list) * local_theory) ->
     bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
       (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
     local_theory -> local_theory
+  val parse_datatype_cmd: bool ->
+    (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 * thm list *
+         thm list) * local_theory) ->
+    (local_theory -> local_theory) parser
 end;
 
 structure BNF_FP_Sugar : BNF_FP_SUGAR =
@@ -20,8 +30,6 @@
 open BNF_Wrap
 open BNF_Def
 open BNF_FP_Util
-open BNF_LFP
-open BNF_GFP
 open BNF_FP_Sugar_Tactics
 
 val caseN = "case";
@@ -79,7 +87,6 @@
   if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
 
 fun type_args_constrained_of (((cAs, _), _), _) = cAs;
-val type_args_of = map fst o type_args_constrained_of;
 fun type_binder_of (((_, b), _), _) = b;
 fun mixfix_of ((_, mx), _) = mx;
 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
@@ -90,7 +97,7 @@
 fun defaults_of ((_, ds), _) = ds;
 fun ctr_mixfix_of (_, mx) = mx;
 
-fun define_datatype prepare_constraint prepare_typ prepare_term lfp (no_dests, specs)
+fun define_datatype prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
     no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
@@ -148,7 +155,7 @@
     val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
     val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
 
-    val (Ass as As :: _) :: fake_ctr_Tsss =
+    val (As :: _) :: fake_ctr_Tsss =
       burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
 
     val _ = (case duplicates (op =) unsorted_As of [] => ()
@@ -178,8 +185,7 @@
 
     val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
         fp_iter_thms, fp_rec_thms), lthy)) =
-      fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs
-        no_defs_lthy0;
+      fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
 
     val add_nested_bnf_names =
       let
@@ -694,7 +700,7 @@
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       (if lfp then "" else "co") ^ "datatype"));
   in
-    (timer; lthy')
+    timer; lthy'
   end;
 
 val datatyp = define_datatype (K I) (K I) (K I);
@@ -717,12 +723,6 @@
 
 val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
 
-val _ =
-  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
-    (parse_datatype >> datatype_cmd true);
-
-val _ =
-  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
-    (parse_datatype >> datatype_cmd false);
+fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct;
 
 end;

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 05:03:18 2012 +0200
@@ -352,7 +352,7 @@
 
     val timer = time (timer "FP construction in total");
   in
-    (bnfs'', res)
+    timer; (bnfs'', res)
   end;
 
 fun fp_bnf construct bs mixfixes resBs eqs lthy =

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 05:03:18 2012 +0200
@@ -22,6 +22,7 @@
 open BNF_Util
 open BNF_Tactics
 open BNF_FP_Util
+open BNF_FP_Sugar
 open BNF_GFP_Util
 open BNF_GFP_Tactics
 
@@ -49,7 +50,7 @@
      (I, nth flds i $ (Term.list_comb (snd (nth (nth witss i) nwit),
        map (snd o tree_to_fld_wit vars flds witss) subtrees)));
 
-fun tree_to_coind_wits _ (Leaf j) = []
+fun tree_to_coind_wits _ (Leaf _) = []
   | tree_to_coind_wits lwitss (Node ((i, nwit, I), subtrees)) =
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
@@ -147,7 +148,6 @@
     val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
     val sum_bdT = fst (dest_relT (fastype_of sum_bd));
-    val witss = map wits_of_bnf bnfs;
 
     val emptys = map (fn T => HOLogic.mk_set T []) passiveAs;
     val Zeros = map (fn empty =>
@@ -272,7 +272,6 @@
     val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
     val in_mono'_thms = map (fn thm =>
       (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
-    val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
 
     val map_arg_cong_thms =
       let
@@ -1860,7 +1859,6 @@
     val prodTs = map (HOLogic.mk_prodT o `I) Ts;
     val prodFTs = mk_FTs (passiveAs @ prodTs);
     val FTs_setss = mk_setss (passiveAs @ Ts);
-    val FTs'_setss = mk_setss (passiveBs @ Ts);
     val prodFT_setss = mk_setss (passiveAs @ prodTs);
     val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs;
     val map_FT_nths = map2 (fn Ds =>
@@ -2318,13 +2316,13 @@
         val XTs = mk_Ts passiveXs;
         val YTs = mk_Ts passiveYs;
 
-        val (((((((((((((((((((((fs, fs'), (fs_copy, fs'_copy)), (gs, gs')), us),
+        val ((((((((((((((((((((fs, fs'), fs_copy), gs), us),
           (Jys, Jys')), (Jys_copy, Jys'_copy)), set_induct_phiss), JRs), Jphis),
-          B1s), B2s), AXs), Xs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
+          B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
           names_lthy) = names_lthy
           |> mk_Frees' "f" fTs
-          ||>> mk_Frees' "f" fTs
-          ||>> mk_Frees' "g" gTs
+          ||>> mk_Frees "f" fTs
+          ||>> mk_Frees "g" gTs
           ||>> mk_Frees "u" uTs
           ||>> mk_Frees' "b" Ts'
           ||>> mk_Frees' "b" Ts'
@@ -2334,7 +2332,6 @@
           ||>> mk_Frees "B1" B1Ts
           ||>> mk_Frees "B2" B2Ts
           ||>> mk_Frees "A" AXTs
-          ||>> mk_Frees "x" XTs
           ||>> mk_Frees "f1" f1Ts
           ||>> mk_Frees "f2" f2Ts
           ||>> mk_Frees "p1" p1Ts
@@ -2414,7 +2411,7 @@
               |> Thm.close_derivation)
           end;
 
-        val (map_unique_thms, map_unique_thm) =
+        val map_unique_thm =
           let
             fun mk_prem u map unf unf' =
               mk_Trueprop_eq (HOLogic.mk_comp (unf', u),
@@ -2423,12 +2420,11 @@
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
-            val unique = Skip_Proof.prove lthy [] []
+          in
+            Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
               (mk_map_unique_tac coiter_unique_thm map_comps)
-              |> Thm.close_derivation;
-          in
-            `split_conj_thm unique
+              |> Thm.close_derivation
           end;
 
         val timer = time (timer "map functions for the new codatatypes");
@@ -2437,11 +2433,6 @@
 
         val timer = time (timer "bounds for the new codatatypes");
 
-        fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T);
-        val setsss = map (mk_setss o mk_set_Ts) passiveAs;
-        val map_setss = map (fn T => map2 (fn Ds =>
-          mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs;
-
         val setss_by_bnf = map (fn i => map2 (mk_hset unfs i) ls passiveAs) ks;
         val setss_by_bnf' = map (fn i => map2 (mk_hset unf's i) ls passiveBs) ks;
         val setss_by_range = transpose setss_by_bnf;
@@ -2778,11 +2769,11 @@
           end;
 
         val nat_witss =
-          map3 (fn i => fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
+          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
             (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
             |> map (fn (I, wit) =>
               (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
-          ks Dss bnfs;
+          Dss bnfs;
 
         val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
 
@@ -2969,7 +2960,7 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd
+        timer; lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd
       end;
 
       val common_notes =
@@ -3006,9 +2997,14 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points of BNF equations"
+  Outer_Syntax.local_theory @{command_spec "codata_raw"}
+    "define BNF-based coinductive datatypes (low-level)"
     (Parse.and_list1
       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
       (snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list));
 
+val _ =
+  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
+    (parse_datatype_cmd false bnf_gfp);
+
 end;

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 05:03:18 2012 +0200
@@ -21,6 +21,7 @@
 open BNF_Util
 open BNF_Tactics
 open BNF_FP_Util
+open BNF_FP_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
@@ -1118,8 +1119,8 @@
         `split_conj_thm unique_mor
       end;
 
-    val (iter_unique_thms, iter_unique_thm) =
-      `split_conj_thm (mk_conjIN n RS
+    val iter_unique_thms =
+      split_conj_thm (mk_conjIN n RS
         (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
 
     val iter_fld_thms =
@@ -1791,7 +1792,7 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
+        timer; lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
       end;
 
       val common_notes =
@@ -1821,9 +1822,14 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations"
+  Outer_Syntax.local_theory @{command_spec "data_raw"}
+    "define BNF-based inductive datatypes (low-level)"
     (Parse.and_list1
       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
       (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
 
+val _ =
+  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
+    (parse_datatype_cmd true bnf_lfp);
+
 end;