moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
authorblanchet
Fri Aug 30 11:27:23 2013 +0200 (2013-08-30)
changeset 53303ae49b835ca01
parent 53302 98fdf6c34142
child 53304 cfef783090eb
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
src/HOL/BNF/BNF_FP_N2M.thy
src/HOL/BNF/BNF_FP_Rec_Sugar.thy
src/HOL/BNF/BNF_LFP_Compat.thy
src/HOL/BNF/Examples/Misc_Primrec.thy
src/HOL/BNF/Tools/bnf_fp_n2m.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/BNF_FP_N2M.thy	Fri Aug 30 11:27:23 2013 +0200
     1.3 @@ -0,0 +1,26 @@
     1.4 +(*  Title:      HOL/BNF/BNF_FP_N2M.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +    Copyright   2013
     1.8 +
     1.9 +Flattening of nested to mutual (co)recursion.
    1.10 +*)
    1.11 +
    1.12 +header {* Flattening of Nested to Mutual (Co)recursion *}
    1.13 +
    1.14 +theory BNF_FP_N2M
    1.15 +imports "~~/src/HOL/BNF/BNF_FP_Basic"
    1.16 +begin
    1.17 +
    1.18 +lemma eq_le_Grp_id_iff: "(op = \<le> BNF_Util.Grp (Collect R) id) = (All R)"
    1.19 +  unfolding Grp_def id_apply by blast
    1.20 +
    1.21 +lemma Grp_id_mono_subst: "(\<And>x y. BNF_Util.Grp P id x y \<Longrightarrow> BNF_Util.Grp Q id (f x) (f y)) \<equiv>
    1.22 +   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
    1.23 +  unfolding Grp_def by rule auto
    1.24 +
    1.25 +ML_file "Tools/bnf_fp_n2m_tactics.ML"
    1.26 +ML_file "Tools/bnf_fp_n2m.ML"
    1.27 +ML_file "Tools/bnf_fp_n2m_sugar.ML"
    1.28 +
    1.29 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/BNF/BNF_FP_Rec_Sugar.thy	Fri Aug 30 11:27:23 2013 +0200
     2.3 @@ -0,0 +1,34 @@
     2.4 +(*  Title:      HOL/BNF/BNF_FP_Rec_Sugar.thy
     2.5 +    Author:     Lorenz Panny, TU Muenchen
     2.6 +    Author:     Dmitriy Traytel, TU Muenchen
     2.7 +    Author:     Jasmin Blanchette, TU Muenchen
     2.8 +    Copyright   2013
     2.9 +
    2.10 +Recursor and corecursor sugar.
    2.11 +*)
    2.12 +
    2.13 +header {* Recursor and Corecursor Sugar *}
    2.14 +
    2.15 +theory BNF_FP_Rec_Sugar
    2.16 +imports BNF_FP_N2M
    2.17 +keywords
    2.18 +  "primrec_new" :: thy_decl and
    2.19 +  "primcorec" :: thy_goal and
    2.20 +  "sequential"
    2.21 +begin
    2.22 +
    2.23 +lemma if_if_True:
    2.24 +"(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
    2.25 + (if b then x else if b' then x' else f y')"
    2.26 +by simp
    2.27 +
    2.28 +lemma if_if_False:
    2.29 +"(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
    2.30 + (if b then f y else if b' then x' else f y')"
    2.31 +by simp
    2.32 +
    2.33 +ML_file "Tools/bnf_fp_rec_sugar_util.ML"
    2.34 +ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
    2.35 +ML_file "Tools/bnf_fp_rec_sugar.ML"
    2.36 +
    2.37 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/BNF/BNF_LFP_Compat.thy	Fri Aug 30 11:27:23 2013 +0200
     3.3 @@ -0,0 +1,18 @@
     3.4 +(*  Title:      HOL/BNF/BNF_LFP_Compat.thy
     3.5 +    Author:     Jasmin Blanchette, TU Muenchen
     3.6 +    Copyright   2013
     3.7 +
     3.8 +Compatibility layer with the old datatype package.
     3.9 +*)
    3.10 +
    3.11 +header {* Compatibility Layer with the Old Datatype Package *}
    3.12 +
    3.13 +theory BNF_LFP_Compat
    3.14 +imports BNF_FP_N2M
    3.15 +keywords
    3.16 +  "datatype_compat" :: thy_goal
    3.17 +begin
    3.18 +
    3.19 +ML_file "Tools/bnf_lfp_compat.ML"
    3.20 +
    3.21 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Fri Aug 30 11:27:23 2013 +0200
     4.3 @@ -0,0 +1,116 @@
     4.4 +(*  Title:      HOL/BNF/Examples/Misc_Primrec.thy
     4.5 +    Author:     Jasmin Blanchette, TU Muenchen
     4.6 +    Copyright   2013
     4.7 +
     4.8 +Miscellaneous primitive recursive function definitions.
     4.9 +*)
    4.10 +
    4.11 +header {* Miscellaneous Primitive Recursive Function Definitions *}
    4.12 +
    4.13 +theory Misc_Primrec
    4.14 +imports
    4.15 +  "~~/src/HOL/BNF/Examples/Misc_Datatype"
    4.16 +  "../BNF_FP_Rec_Sugar"
    4.17 +begin
    4.18 +
    4.19 +primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
    4.20 +  "nat_of_simple X1 = 1" |
    4.21 +  "nat_of_simple X2 = 2" |
    4.22 +  "nat_of_simple X3 = 2" |
    4.23 +  "nat_of_simple X4 = 4"
    4.24 +
    4.25 +primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where
    4.26 +  "simple_of_simple' (X1' _) = X1" |
    4.27 +  "simple_of_simple' (X2' _) = X2" |
    4.28 +  "simple_of_simple' (X3' _) = X3" |
    4.29 +  "simple_of_simple' (X4' _) = X4"
    4.30 +
    4.31 +primrec_new inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
    4.32 +  "inc_simple'' k (X1'' n i) = X1'' (n + k) (i + int k)" |
    4.33 +  "inc_simple'' _ X2'' = X2''"
    4.34 +
    4.35 +primrec_new myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
    4.36 +  "myapp MyNil ys = ys" |
    4.37 +  "myapp (MyCons x xs) ys = MyCons x (myapp xs ys)"
    4.38 +
    4.39 +primrec_new myrev :: "'a mylist \<Rightarrow> 'a mylist" where
    4.40 +  "myrev MyNil = MyNil" |
    4.41 +  "myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)"
    4.42 +
    4.43 +primrec_new shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
    4.44 +  "shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" |
    4.45 +  "shuffle_sp (SP2 a) = SP3 a" |
    4.46 +  "shuffle_sp (SP3 b) = SP4 b" |
    4.47 +  "shuffle_sp (SP4 c) = SP5 c" |
    4.48 +  "shuffle_sp (SP5 d) = SP2 d"
    4.49 +
    4.50 +primrec_new
    4.51 +  hf_size :: "hfset \<Rightarrow> nat"
    4.52 +where
    4.53 +  "hf_size (HFset X) = 1 + setsum id (fset (fmap hf_size X))"
    4.54 +
    4.55 +primrec_new rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
    4.56 +  "rename_lam f (Var s) = Var (f s)" |
    4.57 +  "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
    4.58 +  "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
    4.59 +  "rename_lam f (Let SL l) = Let (fmap (map_pair f (rename_lam f)) SL) (rename_lam f l)"
    4.60 +
    4.61 +primrec_new
    4.62 +  sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
    4.63 +  sum_i2 :: "'a I2 \<Rightarrow> 'a"
    4.64 +where
    4.65 +  "sum_i1 (I11 n i) = n + sum_i1 i" |
    4.66 +  "sum_i1 (I12 n i) = n + sum_i2 i" |
    4.67 +  "sum_i2 I21 = 0" |
    4.68 +  "sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
    4.69 +
    4.70 +primrec_new forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
    4.71 +  "forest_of_mylist MyNil = FNil" |
    4.72 +  "forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
    4.73 +
    4.74 +primrec_new mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
    4.75 +  "mylist_of_forest FNil = MyNil" |
    4.76 +  "mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)"
    4.77 +
    4.78 +definition frev :: "'a forest \<Rightarrow> 'a forest" where
    4.79 +  "frev = forest_of_mylist o myrev o mylist_of_forest"
    4.80 +
    4.81 +primrec_new
    4.82 +  mirror_tree :: "'a tree \<Rightarrow> 'a tree" and
    4.83 +  mirror_forest :: "'a forest \<Rightarrow> 'a forest"
    4.84 +where
    4.85 +  "mirror_tree TEmpty = TEmpty" |
    4.86 +  "mirror_tree (TNode x ts) = TNode x (mirror_forest ts)" |
    4.87 +  "mirror_forest FNil = FNil" |
    4.88 +  "mirror_forest (FCons t ts) = frev (FCons (mirror_tree t) (mirror_forest ts))"
    4.89 +
    4.90 +primrec_new
    4.91 +  mylist_of_tree' :: "'a tree' \<Rightarrow> 'a mylist" and
    4.92 +  mylist_of_branch :: "'a branch \<Rightarrow> 'a mylist"
    4.93 +where
    4.94 +  "mylist_of_tree' TEmpty' = MyNil" |
    4.95 +  "mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
    4.96 +  "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
    4.97 +
    4.98 +primrec_new
    4.99 +  is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
   4.100 +  is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
   4.101 +  is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"
   4.102 +where
   4.103 +  "is_ground_exp (Term t) \<longleftrightarrow> is_ground_trm t" |
   4.104 +  "is_ground_exp (Sum t e) \<longleftrightarrow> is_ground_trm t \<and> is_ground_exp e" |
   4.105 +  "is_ground_trm (Factor f) \<longleftrightarrow> is_ground_factor f" |
   4.106 +  "is_ground_trm (Prod f t) \<longleftrightarrow> is_ground_factor f \<and> is_ground_trm t" |
   4.107 +  "is_ground_factor (C _) \<longleftrightarrow> True" |
   4.108 +  "is_ground_factor (V _) \<longleftrightarrow> False" |
   4.109 +  "is_ground_factor (Paren e) \<longleftrightarrow> is_ground_exp e"
   4.110 +
   4.111 +primrec_new map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   4.112 +  "map_ftreeA f (FTLeaf x) = FTLeaf (f x)" |
   4.113 +  "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f o g)"
   4.114 +
   4.115 +primrec_new map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
   4.116 +  "map_ftreeB f (FTLeaf x) = FTLeaf (f x)" |
   4.117 +  "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f o g o the_inv f)"
   4.118 +
   4.119 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 11:27:23 2013 +0200
     5.3 @@ -0,0 +1,384 @@
     5.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_n2m.ML
     5.5 +    Author:     Dmitriy Traytel, TU Muenchen
     5.6 +    Copyright   2013
     5.7 +
     5.8 +Flattening of nested to mutual (co)recursion.
     5.9 +*)
    5.10 +
    5.11 +signature BNF_FP_N2M =
    5.12 +sig
    5.13 +  val construct_mutualized_fp: BNF_FP_Util.fp_kind  -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
    5.14 +    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    5.15 +    local_theory -> BNF_FP_Util.fp_result * local_theory
    5.16 +end;
    5.17 +
    5.18 +structure BNF_FP_N2M : BNF_FP_N2M =
    5.19 +struct
    5.20 +
    5.21 +open BNF_Def
    5.22 +open BNF_Util
    5.23 +open BNF_FP_Util
    5.24 +open BNF_FP_Def_Sugar
    5.25 +open BNF_Tactics
    5.26 +open BNF_FP_N2M_Tactics
    5.27 +
    5.28 +fun force_typ ctxt T =
    5.29 +  map_types Type_Infer.paramify_vars 
    5.30 +  #> Type.constraint T
    5.31 +  #> Syntax.check_term ctxt
    5.32 +  #> singleton (Variable.polymorphic ctxt);
    5.33 +
    5.34 +fun mk_prod_map f g =
    5.35 +  let
    5.36 +    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    5.37 +    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    5.38 +  in
    5.39 +    Const (@{const_name map_pair},
    5.40 +      fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    5.41 +  end;
    5.42 +
    5.43 +fun mk_sum_map f g =
    5.44 +  let
    5.45 +    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    5.46 +    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    5.47 +  in
    5.48 +    Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    5.49 +  end;
    5.50 +
    5.51 +fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
    5.52 +  let
    5.53 +    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
    5.54 +
    5.55 +    val n = length bnfs;
    5.56 +    val deads = fold (union (op =)) Dss resDs;
    5.57 +    val As = subtract (op =) deads (map TFree resBs);
    5.58 +    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    5.59 +    val m = length As;
    5.60 +    val live = m + n;
    5.61 +    val ((Xs, Bs), names_lthy) = names_lthy
    5.62 +      |> mk_TFrees n
    5.63 +      ||>> mk_TFrees m;
    5.64 +    val allAs = As @ Xs;
    5.65 +    val phiTs = map2 mk_pred2T As Bs;
    5.66 +    val theta = As ~~ Bs;
    5.67 +    val fpTs' = map (Term.typ_subst_atomic theta) fpTs;
    5.68 +    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
    5.69 +
    5.70 +    fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
    5.71 +    fun co_swap pair = fp_case fp I swap pair;
    5.72 +    val dest_co_algT = co_swap o dest_funT;
    5.73 +    val co_alg_argT = fp_case fp range_type domain_type;
    5.74 +    val co_alg_funT = fp_case fp domain_type range_type;
    5.75 +    val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
    5.76 +    val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
    5.77 +    val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    5.78 +    val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    5.79 +    val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    5.80 +
    5.81 +    val ((ctors, dtors), (xtor's, xtors)) =
    5.82 +      let
    5.83 +        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
    5.84 +        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
    5.85 +      in
    5.86 +        ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
    5.87 +      end;
    5.88 +
    5.89 +    val xTs = map (domain_type o fastype_of) xtors;
    5.90 +    val yTs = map (domain_type o fastype_of) xtor's;
    5.91 +
    5.92 +    val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
    5.93 +      |> mk_Frees' "R" phiTs
    5.94 +      ||>> mk_Frees "S" pre_phiTs
    5.95 +      ||>> mk_Frees "x" xTs
    5.96 +      ||>> mk_Frees "y" yTs;
    5.97 +
    5.98 +    val fp_bnfs = steal #bnfs;
    5.99 +    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
   5.100 +    val pre_bnfss = map #pre_bnfs fp_sugars;
   5.101 +    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
   5.102 +    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
   5.103 +    val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
   5.104 +
   5.105 +    fun abstract t =
   5.106 +      let val Ts = Term.add_frees t [];
   5.107 +      in fold_rev Term.absfree (filter (member op = Ts) phis') t end;
   5.108 +
   5.109 +    val rels =
   5.110 +      let
   5.111 +        fun find_rel T As Bs = fp_nesty_bnfss
   5.112 +          |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
   5.113 +          |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
   5.114 +          |> Option.map (fn bnf =>
   5.115 +            let val live = live_of_bnf bnf;
   5.116 +            in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
   5.117 +          |> the_default (HOLogic.eq_const T, 0);
   5.118 +
   5.119 +        fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
   5.120 +              let
   5.121 +                val (rel, live) = find_rel T Ts Us;
   5.122 +                val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
   5.123 +                val rels = map2 mk_rel Ts' Us';
   5.124 +              in
   5.125 +                Term.list_comb (rel, rels)
   5.126 +              end
   5.127 +          | mk_rel (T as TFree _) _ = nth phis (find_index (curry op = T) As)
   5.128 +          | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
   5.129 +      in
   5.130 +        map2 (abstract oo mk_rel) fpTs fpTs'
   5.131 +      end;
   5.132 +
   5.133 +    val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
   5.134 +
   5.135 +    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
   5.136 +    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
   5.137 +      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
   5.138 +
   5.139 +    val rel_defs = map rel_def_of_bnf bnfs;
   5.140 +    val rel_monos = map rel_mono_of_bnf bnfs;
   5.141 +
   5.142 +    val rel_xtor_co_induct_thm =
   5.143 +      mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's
   5.144 +        (mk_rel_xtor_co_induct_tactic fp rel_xtor_co_inducts rel_defs rel_monos) lthy;
   5.145 +
   5.146 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
   5.147 +    val map_id0s = no_refl (map map_id0_of_bnf bnfs);
   5.148 +
   5.149 +    val xtor_co_induct_thm =
   5.150 +      (case fp of
   5.151 +        Least_FP =>
   5.152 +          let
   5.153 +            val (Ps, names_lthy) = names_lthy
   5.154 +              |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
   5.155 +            fun mk_Grp_id P =
   5.156 +              let val T = domain_type (fastype_of P);
   5.157 +              in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   5.158 +            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   5.159 +          in
   5.160 +            cterm_instantiate_pos cts rel_xtor_co_induct_thm
   5.161 +            |> singleton (Proof_Context.export names_lthy lthy)
   5.162 +            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
   5.163 +            |> funpow n (fn thm => thm RS spec)
   5.164 +            |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
   5.165 +            |> unfold_thms lthy @{thms Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)}
   5.166 +            |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
   5.167 +               atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
   5.168 +            |> unfold_thms lthy (maps set_defs_of_bnf bnfs)
   5.169 +          end
   5.170 +      | Greatest_FP =>
   5.171 +          let
   5.172 +            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
   5.173 +          in
   5.174 +            cterm_instantiate_pos cts rel_xtor_co_induct_thm
   5.175 +            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
   5.176 +            |> funpow (2 * n) (fn thm => thm RS spec)
   5.177 +            |> Conv.fconv_rule Object_Logic.atomize
   5.178 +            |> funpow n (fn thm => thm RS mp)
   5.179 +          end);
   5.180 +
   5.181 +    val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
   5.182 +    val fold_pre_deads_only_Ts = map2 (fn Ds => mk_T_of_bnf Ds (replicate live dummyT)) Dss bnfs;
   5.183 +    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   5.184 +    val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
   5.185 +
   5.186 +    val fold_strTs = map2 mk_co_algT fold_preTs Xs;
   5.187 +    val rec_strTs = map2 mk_co_algT rec_preTs Xs;
   5.188 +    val resTs = map2 mk_co_algT fpTs Xs;
   5.189 +
   5.190 +    val (((fold_strs, fold_strs'), (rec_strs, rec_strs')), names_lthy) = names_lthy
   5.191 +      |> mk_Frees' "s" fold_strTs
   5.192 +      ||>> mk_Frees' "s" rec_strTs;
   5.193 +
   5.194 +    val co_iters = steal #xtor_co_iterss;
   5.195 +    val ns = map (length o #pre_bnfs) fp_sugars;
   5.196 +    fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
   5.197 +      | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
   5.198 +      | substT _ T = T;
   5.199 +    fun force_iter is_rec i TU TU_rec raw_iters =
   5.200 +      let
   5.201 +        val approx_fold = un_fold_of raw_iters
   5.202 +          |> force_typ names_lthy
   5.203 +            (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
   5.204 +        val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
   5.205 +        val js = find_indices Type.could_unify
   5.206 +          TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
   5.207 +        val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
   5.208 +        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
   5.209 +      in
   5.210 +        force_typ names_lthy (Tpats ---> TU) iter
   5.211 +      end;
   5.212 +
   5.213 +    fun mk_iter b_opt is_rec iters lthy TU =
   5.214 +      let
   5.215 +        val x = co_alg_argT TU;
   5.216 +        val i = find_index (fn T => x = T) Xs;
   5.217 +        val TUiter =
   5.218 +          (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
   5.219 +            NONE => nth co_iters i
   5.220 +              |> force_iter is_rec i
   5.221 +                (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
   5.222 +                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
   5.223 +          | SOME f => f);
   5.224 +        val TUs = binder_fun_types (fastype_of TUiter);
   5.225 +        val iter_preTs = if is_rec then rec_preTs else fold_preTs;
   5.226 +        val iter_strs = if is_rec then rec_strs else fold_strs;
   5.227 +        fun mk_s TU' =
   5.228 +          let
   5.229 +            val i = find_index (fn T => co_alg_argT TU' = T) Xs;
   5.230 +            val sF = co_alg_funT TU'; 
   5.231 +            val F = nth iter_preTs i;
   5.232 +            val s = nth iter_strs i;
   5.233 +          in
   5.234 +            (if sF = F then s
   5.235 +            else
   5.236 +              let
   5.237 +                val smapT = replicate live dummyT ---> mk_co_algT sF F;
   5.238 +                fun hidden_to_unit t =
   5.239 +                  Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
   5.240 +                val smap = map_of_bnf (nth bnfs i)
   5.241 +                  |> force_typ names_lthy smapT
   5.242 +                  |> hidden_to_unit;
   5.243 +                val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
   5.244 +                fun mk_smap_arg TU =              
   5.245 +                  (if domain_type TU = range_type TU then
   5.246 +                    HOLogic.id_const (domain_type TU)
   5.247 +                  else if is_rec then
   5.248 +                    let
   5.249 +                      val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
   5.250 +                      val T = mk_co_algT TY U;
   5.251 +                    in
   5.252 +                      (case try (force_typ lthy T o build_map lthy co_proj1_const o dest_funT) T of
   5.253 +                        SOME f => mk_co_product f
   5.254 +                          (fst (fst (mk_iter NONE is_rec iters lthy (mk_co_algT TY X))))
   5.255 +                      | NONE => mk_map_co_product
   5.256 +                          (build_map lthy co_proj1_const
   5.257 +                            (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
   5.258 +                          (HOLogic.id_const X))
   5.259 +                    end
   5.260 +                  else
   5.261 +                    fst (fst (mk_iter NONE is_rec iters lthy TU)))
   5.262 +                val smap_args = map mk_smap_arg smap_argTs;
   5.263 +              in
   5.264 +                HOLogic.mk_comp (co_swap (s, Term.list_comb (smap, smap_args)))
   5.265 +              end)
   5.266 +          end;
   5.267 +        val t = Term.list_comb (TUiter, map mk_s TUs);
   5.268 +      in
   5.269 +        (case b_opt of
   5.270 +          NONE => ((t, Drule.dummy_thm), lthy)
   5.271 +        | SOME b => Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), 
   5.272 +            fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd)
   5.273 +      end;
   5.274 +
   5.275 +    fun mk_iters is_rec name lthy =
   5.276 +      fold2 (fn TU => fn b => fn ((iters, defs), lthy) =>
   5.277 +        mk_iter (SOME b) is_rec iters lthy TU |>> (fn (f, d) => (f :: iters, d :: defs)))
   5.278 +      resTs (map (Binding.suffix_name ("_" ^ name)) bs) (([], []), lthy)
   5.279 +      |>> apfst rev o apsnd rev;
   5.280 +    val foldN = fp_case fp ctor_foldN dtor_unfoldN;
   5.281 +    val recN = fp_case fp ctor_recN dtor_corecN;
   5.282 +    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, lthy_old)) =
   5.283 +      lthy
   5.284 +      |> mk_iters false foldN
   5.285 +      ||>> mk_iters true recN
   5.286 +      ||> `(Local_Theory.restore);
   5.287 +
   5.288 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   5.289 +
   5.290 +    val un_folds = map (Morphism.term phi) raw_un_folds;
   5.291 +    val co_recs = map (Morphism.term phi) raw_co_recs;
   5.292 +
   5.293 +    val (xtor_un_fold_thms, xtor_co_rec_thms) =
   5.294 +      let
   5.295 +        val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
   5.296 +        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
   5.297 +        val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
   5.298 +        val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
   5.299 +        val pre_fold_maps =
   5.300 +          map2 (fn Ds => fn bnf =>
   5.301 +            Term.list_comb (uncurry (mk_map_of_bnf Ds) fold_mapTs bnf,
   5.302 +              map HOLogic.id_const As @ folds))
   5.303 +          Dss bnfs;
   5.304 +        val pre_rec_maps =
   5.305 +          map2 (fn Ds => fn bnf =>
   5.306 +            Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
   5.307 +              map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
   5.308 +          Dss bnfs;
   5.309 +
   5.310 +        fun mk_goals f xtor s smap =
   5.311 +          ((f, xtor), (s, smap))
   5.312 +          |> pairself (HOLogic.mk_comp o co_swap)
   5.313 +          |> HOLogic.mk_eq;
   5.314 +
   5.315 +        val fold_goals = map4 mk_goals folds xtors fold_strs pre_fold_maps
   5.316 +        val rec_goals = map4 mk_goals recs xtors rec_strs pre_rec_maps;
   5.317 +
   5.318 +        fun mk_thms ss goals tac =
   5.319 +          Library.foldr1 HOLogic.mk_conj goals
   5.320 +          |> HOLogic.mk_Trueprop
   5.321 +          |> fold_rev Logic.all ss
   5.322 +          |> (fn goal => Goal.prove_sorry lthy [] [] goal tac)
   5.323 +          |> Thm.close_derivation
   5.324 +          |> Morphism.thm phi
   5.325 +          |> split_conj_thm
   5.326 +          |> map (fn thm => thm RS @{thm comp_eq_dest});
   5.327 +
   5.328 +        val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   5.329 +        val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   5.330 +
   5.331 +        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
   5.332 +        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
   5.333 +
   5.334 +        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
   5.335 +        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
   5.336 +        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
   5.337 +
   5.338 +        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
   5.339 +        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
   5.340 +        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
   5.341 +        val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
   5.342 +          @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
   5.343 +        val rec_thms = fold_thms @ fp_case fp
   5.344 +          @{thms fst_convol map_pair_o_convol convol_o}
   5.345 +          @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
   5.346 +        val map_thms = no_refl (maps (fn bnf =>
   5.347 +          [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
   5.348 +
   5.349 +        fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
   5.350 +          unfold_thms_tac ctxt
   5.351 +            (flat [thms, defs, pre_map_defs, fp_pre_map_defs, xtor_thms, o_map_thms, map_thms]) THEN
   5.352 +          CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   5.353 +
   5.354 +        val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
   5.355 +        val rec_tac = mk_tac raw_co_rec_defs fp_rec_o_maps fp_xtor_co_recs rec_thms;
   5.356 +      in
   5.357 +        (mk_thms fold_strs fold_goals fold_tac, mk_thms rec_strs rec_goals rec_tac)
   5.358 +      end;
   5.359 +
   5.360 +    (* These results are half broken. This is deliberate. We care only about those fields that are
   5.361 +       used by "primrec_new", "primcorec", and "datatype_compat". *)
   5.362 +    val fp_res =
   5.363 +      ({Ts = fpTs,
   5.364 +        bnfs = steal #bnfs,
   5.365 +        dtors = dtors,
   5.366 +        ctors = ctors,
   5.367 +        xtor_co_iterss = transpose [un_folds, co_recs],
   5.368 +        xtor_co_induct = xtor_co_induct_thm,
   5.369 +        dtor_ctors = steal #dtor_ctors (*too general types*),
   5.370 +        ctor_dtors = steal #ctor_dtors (*too general types*),
   5.371 +        ctor_injects = steal #ctor_injects (*too general types*),
   5.372 +        dtor_injects = steal #dtor_injects (*too general types*),
   5.373 +        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
   5.374 +        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
   5.375 +        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
   5.376 +        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
   5.377 +        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
   5.378 +        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   5.379 +       |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
   5.380 +(**
   5.381 +    val _ = fp_res |> @{make_string} |> tracing
   5.382 +**)
   5.383 +  in
   5.384 +    (fp_res, lthy)
   5.385 +  end
   5.386 +
   5.387 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Fri Aug 30 11:27:23 2013 +0200
     6.3 @@ -0,0 +1,261 @@
     6.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +    Copyright   2013
     6.7 +
     6.8 +Suggared flattening of nested to mutual (co)recursion.
     6.9 +*)
    6.10 +
    6.11 +signature BNF_FP_N2M_SUGAR =
    6.12 +sig
    6.13 +  val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
    6.14 +    (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
    6.15 +    local_theory -> (bool * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
    6.16 +  val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
    6.17 +    (term * term list list) list list -> term list list list list
    6.18 +  val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
    6.19 +    (term -> int list) -> ((term * term list list) list) list -> local_theory ->
    6.20 +    (bool * typ list * int list * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
    6.21 +end;
    6.22 +
    6.23 +structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
    6.24 +struct
    6.25 +
    6.26 +open BNF_Util
    6.27 +open BNF_Def
    6.28 +open BNF_Ctr_Sugar
    6.29 +open BNF_FP_Util
    6.30 +open BNF_FP_Def_Sugar
    6.31 +open BNF_FP_N2M
    6.32 +
    6.33 +val n2mN = "n2m_"
    6.34 +
    6.35 +(* TODO: test with sort constraints on As *)
    6.36 +(* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    6.37 +   as deads? *)
    6.38 +fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0
    6.39 +    no_defs_lthy0 =
    6.40 +  (* TODO: Also check whether there's any lost recursion? *)
    6.41 +  if mutualize orelse has_duplicates (op =) fpTs then
    6.42 +    let
    6.43 +      val thy = Proof_Context.theory_of no_defs_lthy0;
    6.44 +
    6.45 +      val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
    6.46 +
    6.47 +      fun heterogeneous_call t = error ("Heterogeneous recursive call: " ^ qsotm t);
    6.48 +      fun incompatible_calls t1 t2 =
    6.49 +        error ("Incompatible recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
    6.50 +
    6.51 +      val b_names = map Binding.name_of bs;
    6.52 +      val fp_b_names = map base_name_of_typ fpTs;
    6.53 +
    6.54 +      val nn = length fpTs;
    6.55 +
    6.56 +      fun target_ctr_sugar_of_fp_sugar fpT {T, index, ctr_sugars, ...} =
    6.57 +        let
    6.58 +          val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    6.59 +          val phi = Morphism.term_morphism (Term.subst_TVars rho);
    6.60 +        in
    6.61 +          morph_ctr_sugar phi (nth ctr_sugars index)
    6.62 +        end;
    6.63 +
    6.64 +      val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
    6.65 +      val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
    6.66 +
    6.67 +      val ctrss = map #ctrs ctr_sugars0;
    6.68 +      val ctr_Tss = map (map fastype_of) ctrss;
    6.69 +
    6.70 +      val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
    6.71 +      val As = map TFree As';
    6.72 +
    6.73 +      val ((Cs, Xs), no_defs_lthy) =
    6.74 +        no_defs_lthy0
    6.75 +        |> fold Variable.declare_typ As
    6.76 +        |> mk_TFrees nn
    6.77 +        ||>> variant_tfrees fp_b_names;
    6.78 +
    6.79 +      (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to
    6.80 +           'list = unit + 'a list
    6.81 +         instead of
    6.82 +           'list = unit + 'list
    6.83 +         resulting in a simpler (co)induction rule and (co)recursor. *)
    6.84 +      fun freeze_fp_default (T as Type (s, Ts)) =
    6.85 +          (case find_index (curry (op =) T) fpTs of
    6.86 +            ~1 => Type (s, map freeze_fp_default Ts)
    6.87 +          | kk => nth Xs kk)
    6.88 +        | freeze_fp_default T = T;
    6.89 +
    6.90 +      fun get_indices_checked call =
    6.91 +        (case get_indices call of
    6.92 +          _ :: _ :: _ => heterogeneous_call call
    6.93 +        | kks => kks);
    6.94 +
    6.95 +      fun freeze_fp calls (T as Type (s, Ts)) =
    6.96 +          (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
    6.97 +            [] =>
    6.98 +            (case union (op = o pairself fst)
    6.99 +                (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
   6.100 +              [] => T |> not lose_co_rec ? freeze_fp_default
   6.101 +            | [(kk, _)] => nth Xs kk
   6.102 +            | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
   6.103 +          | callss =>
   6.104 +            Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
   6.105 +              (transpose callss)) Ts))
   6.106 +        | freeze_fp _ T = T;
   6.107 +
   6.108 +      val ctr_Tsss = map (map binder_types) ctr_Tss;
   6.109 +      val ctrXs_Tsss = map2 (map2 (map2 freeze_fp)) callssss ctr_Tsss;
   6.110 +      val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
   6.111 +      val Ts = map (body_type o hd) ctr_Tss;
   6.112 +
   6.113 +      val ns = map length ctr_Tsss;
   6.114 +      val kss = map (fn n => 1 upto n) ns;
   6.115 +      val mss = map (map length) ctr_Tsss;
   6.116 +
   6.117 +      val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
   6.118 +
   6.119 +      val base_fp_names = Name.variant_list [] fp_b_names;
   6.120 +      val fp_bs = map2 (fn b_name => fn base_fp_name =>
   6.121 +          Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
   6.122 +        b_names base_fp_names;
   6.123 +
   6.124 +      val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
   6.125 +             dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
   6.126 +        fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
   6.127 +
   6.128 +      val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
   6.129 +      val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
   6.130 +
   6.131 +      val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
   6.132 +        mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
   6.133 +
   6.134 +      fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
   6.135 +
   6.136 +      val ((co_iterss, co_iter_defss), lthy) =
   6.137 +        fold_map2 (fn b =>
   6.138 +          (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
   6.139 +           else define_coiters [unfoldN, corecN] (the coiters_args_types))
   6.140 +            (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
   6.141 +        |>> split_list;
   6.142 +
   6.143 +      val rho = tvar_subst thy Ts fpTs;
   6.144 +      val ctr_sugar_phi =
   6.145 +        Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
   6.146 +          (Morphism.term_morphism (Term.subst_TVars rho));
   6.147 +      val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
   6.148 +
   6.149 +      val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
   6.150 +
   6.151 +      val (co_inducts, un_fold_thmss, co_rec_thmss) =
   6.152 +        if fp = Least_FP then
   6.153 +          derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
   6.154 +            xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
   6.155 +            co_iterss co_iter_defss lthy
   6.156 +          |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
   6.157 +            ([induct], fold_thmss, rec_thmss))
   6.158 +        else
   6.159 +          derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
   6.160 +            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
   6.161 +            ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
   6.162 +          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
   6.163 +            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
   6.164 +
   6.165 +      val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   6.166 +
   6.167 +      fun mk_target_fp_sugar (kk, T) =
   6.168 +        {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   6.169 +         nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   6.170 +         ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
   6.171 +         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
   6.172 +        |> morph_fp_sugar phi;
   6.173 +    in
   6.174 +      ((true, map_index mk_target_fp_sugar fpTs), lthy)
   6.175 +    end
   6.176 +  else
   6.177 +    (* TODO: reorder hypotheses and predicates in (co)induction rules? *)
   6.178 +    ((false, fp_sugars0), no_defs_lthy0);
   6.179 +
   6.180 +fun indexify_callsss fp_sugar callsss =
   6.181 +  let
   6.182 +    val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
   6.183 +    fun do_ctr ctr =
   6.184 +      (case AList.lookup Term.aconv_untyped callsss ctr of
   6.185 +        NONE => replicate (num_binder_types (fastype_of ctr)) []
   6.186 +      | SOME callss => map (map Envir.beta_eta_contract) callss);
   6.187 +  in
   6.188 +    map do_ctr ctrs
   6.189 +  end;
   6.190 +
   6.191 +fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
   6.192 +
   6.193 +fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
   6.194 +  let
   6.195 +    val qsoty = quote o Syntax.string_of_typ lthy;
   6.196 +    val qsotys = space_implode " or " o map qsoty;
   6.197 +
   6.198 +    fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
   6.199 +    fun not_co_datatype (T as Type (s, _)) =
   6.200 +        if fp = Least_FP andalso
   6.201 +           is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
   6.202 +          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
   6.203 +        else
   6.204 +          not_co_datatype0 T
   6.205 +      | not_co_datatype T = not_co_datatype0 T;
   6.206 +    fun not_mutually_nested_rec Ts1 Ts2 =
   6.207 +      error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^
   6.208 +        qsotys Ts2);
   6.209 +
   6.210 +    val perm_actual_Ts as Type (_, ty_args0) :: _ =
   6.211 +      sort (int_ord o pairself Term.size_of_typ) actual_Ts;
   6.212 +
   6.213 +    fun check_enrich_with_mutuals _ [] = []
   6.214 +      | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) =
   6.215 +        (case fp_sugar_of lthy T_name of
   6.216 +          SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) =>
   6.217 +          if fp = fp' then
   6.218 +            let
   6.219 +              val mutual_Ts = map (fn Type (s, _) => Type (s, ty_args)) Ts';
   6.220 +              val _ =
   6.221 +                seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
   6.222 +                not_mutually_nested_rec mutual_Ts seen;
   6.223 +              val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
   6.224 +            in
   6.225 +              mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
   6.226 +            end
   6.227 +          else
   6.228 +            not_co_datatype T
   6.229 +        | NONE => not_co_datatype T)
   6.230 +      | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
   6.231 +
   6.232 +    val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
   6.233 +
   6.234 +    val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
   6.235 +    val Ts = actual_Ts @ missing_Ts;
   6.236 +
   6.237 +    val nn = length Ts;
   6.238 +    val kks = 0 upto nn - 1;
   6.239 +
   6.240 +    val common_name = mk_common_name (map Binding.name_of actual_bs);
   6.241 +    val bs = pad_list (Binding.name common_name) nn actual_bs;
   6.242 +
   6.243 +    fun permute xs = permute_like (op =) Ts perm_Ts xs;
   6.244 +    fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
   6.245 +
   6.246 +    val perm_bs = permute bs;
   6.247 +    val perm_kks = permute kks;
   6.248 +    val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
   6.249 +
   6.250 +    val mutualize = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
   6.251 +    val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0;
   6.252 +
   6.253 +    val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
   6.254 +
   6.255 +    val ((nontriv, perm_fp_sugars), lthy) =
   6.256 +      mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
   6.257 +        perm_fp_sugars0 lthy;
   6.258 +
   6.259 +    val fp_sugars = unpermute perm_fp_sugars;
   6.260 +  in
   6.261 +    ((nontriv, missing_Ts, perm_kks, fp_sugars), lthy)
   6.262 +  end;
   6.263 +
   6.264 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML	Fri Aug 30 11:27:23 2013 +0200
     7.3 @@ -0,0 +1,41 @@
     7.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
     7.5 +    Author:     Dmitriy Traytel, TU Muenchen
     7.6 +    Copyright   2013
     7.7 +
     7.8 +Tactics for mutualization of nested (co)datatypes.
     7.9 +*)
    7.10 +
    7.11 +signature BNF_FP_N2M_TACTICS =
    7.12 +sig
    7.13 +  val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list ->
    7.14 +    {prems: thm list, context: Proof.context} -> tactic
    7.15 +end;
    7.16 +
    7.17 +structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
    7.18 +struct
    7.19 +
    7.20 +open BNF_Util
    7.21 +open BNF_FP_Util
    7.22 +
    7.23 +fun mk_rel_xtor_co_induct_tactic fp co_inducts rel_defs rel_monos
    7.24 +  {context = ctxt, prems = raw_C_IHs} =
    7.25 +  let
    7.26 +    val unfolds = map (fn def => unfold_thms ctxt (id_apply :: no_reflexive [def])) rel_defs;
    7.27 +    val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
    7.28 +    val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
    7.29 +    val C_IH_monos =
    7.30 +      map3 (fn C_IH => fn mono => fn unfold =>
    7.31 +        (mono RSN (2, @{thm rev_predicate2D}), C_IH)
    7.32 +        |> fp = Greatest_FP ? swap
    7.33 +        |> op RS
    7.34 +        |> unfold)
    7.35 +      folded_C_IHs rel_monos unfolds;
    7.36 +  in
    7.37 +    HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI})
    7.38 +      (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
    7.39 +         REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
    7.40 +           rtac @{thm order_refl}, atac, resolve_tac co_inducts])))
    7.41 +    co_inducts)
    7.42 +  end;
    7.43 +
    7.44 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 11:27:23 2013 +0200
     8.3 @@ -0,0 +1,744 @@
     8.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar.ML
     8.5 +    Author:     Lorenz Panny, TU Muenchen
     8.6 +    Copyright   2013
     8.7 +
     8.8 +Recursor and corecursor sugar.
     8.9 +*)
    8.10 +
    8.11 +signature BNF_FP_REC_SUGAR =
    8.12 +sig
    8.13 +  val add_primrec_cmd: (binding * string option * mixfix) list ->
    8.14 +    (Attrib.binding * string) list -> local_theory -> local_theory;
    8.15 +end;
    8.16 +
    8.17 +(* TODO:
    8.18 +     - error handling for indirect calls
    8.19 +*)
    8.20 +
    8.21 +structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
    8.22 +struct
    8.23 +
    8.24 +open BNF_Util
    8.25 +open BNF_FP_Util
    8.26 +open BNF_FP_Rec_Sugar_Util
    8.27 +open BNF_FP_Rec_Sugar_Tactics
    8.28 +
    8.29 +exception Primrec_Error of string * term list;
    8.30 +
    8.31 +fun primrec_error str = raise Primrec_Error (str, []);
    8.32 +fun primrec_error_eqn str eqn = raise Primrec_Error (str, [eqn]);
    8.33 +fun primrec_error_eqns str eqns = raise Primrec_Error (str, eqns);
    8.34 +
    8.35 +fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
    8.36 +
    8.37 +val simp_attrs = @{attributes [simp]};
    8.38 +
    8.39 +
    8.40 +type eqn_data = {
    8.41 +  fun_name: string,
    8.42 +  rec_type: typ,
    8.43 +  ctr: term,
    8.44 +  ctr_args: term list,
    8.45 +  left_args: term list,
    8.46 +  right_args: term list,
    8.47 +  res_type: typ,
    8.48 +  rhs_term: term,
    8.49 +  user_eqn: term
    8.50 +};
    8.51 +
    8.52 +fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
    8.53 +  |> fold (K (fn u => Abs ("", dummyT, u))) (0 upto n);
    8.54 +
    8.55 +fun dissect_eqn lthy fun_names eqn' =
    8.56 +  let
    8.57 +    val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
    8.58 +        strip_qnt_body @{const_name all} eqn') |> HOLogic.dest_Trueprop
    8.59 +        handle TERM _ =>
    8.60 +          primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
    8.61 +    val (lhs, rhs) = HOLogic.dest_eq eqn
    8.62 +        handle TERM _ =>
    8.63 +          primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
    8.64 +    val (fun_name, args) = strip_comb lhs
    8.65 +      |>> (fn x => if is_Free x then fst (dest_Free x)
    8.66 +          else primrec_error_eqn "malformed function equation (does not start with free)" eqn);
    8.67 +    val (left_args, rest) = take_prefix is_Free args;
    8.68 +    val (nonfrees, right_args) = take_suffix is_Free rest;
    8.69 +    val _ = length nonfrees = 1 orelse if length nonfrees = 0 then
    8.70 +      primrec_error_eqn "constructor pattern missing in left-hand side" eqn else
    8.71 +      primrec_error_eqn "more than one non-variable argument in left-hand side" eqn;
    8.72 +    val _ = member (op =) fun_names fun_name orelse
    8.73 +      primrec_error_eqn "malformed function equation (does not start with function name)" eqn
    8.74 +
    8.75 +    val (ctr, ctr_args) = strip_comb (the_single nonfrees);
    8.76 +    val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse
    8.77 +      primrec_error_eqn "partially applied constructor in pattern" eqn;
    8.78 +    val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse
    8.79 +      primrec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^
    8.80 +        "\" in left-hand side") eqn end;
    8.81 +    val _ = forall is_Free ctr_args orelse
    8.82 +      primrec_error_eqn "non-primitive pattern in left-hand side" eqn;
    8.83 +    val _ =
    8.84 +      let val b = fold_aterms (fn x as Free (v, _) =>
    8.85 +        if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso
    8.86 +        not (member (op =) fun_names v) andalso
    8.87 +        not (Variable.is_fixed lthy v)) then cons x else I | _ => I) rhs []
    8.88 +      in
    8.89 +        null b orelse
    8.90 +        primrec_error_eqn ("extra variable(s) in right-hand side: " ^
    8.91 +          commas (map (Syntax.string_of_term lthy) b)) eqn
    8.92 +      end;
    8.93 +  in
    8.94 +    {fun_name = fun_name,
    8.95 +     rec_type = body_type (type_of ctr),
    8.96 +     ctr = ctr,
    8.97 +     ctr_args = ctr_args,
    8.98 +     left_args = left_args,
    8.99 +     right_args = right_args,
   8.100 +     res_type = map fastype_of (left_args @ right_args) ---> fastype_of rhs,
   8.101 +     rhs_term = rhs,
   8.102 +     user_eqn = eqn'}
   8.103 +  end;
   8.104 +
   8.105 +(* substitutes (f ls x rs) by (y ls rs) for all f: get_idx f \<ge> 0, (x,y) \<in> substs *)
   8.106 +fun subst_direct_calls get_idx get_ctr_pos substs = 
   8.107 +  let
   8.108 +    fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
   8.109 +      | subst t =
   8.110 +        let
   8.111 +          val (f, args) = strip_comb t;
   8.112 +          val idx = get_idx f;
   8.113 +          val ctr_pos  = if idx >= 0 then get_ctr_pos idx else ~1;
   8.114 +        in
   8.115 +          if idx < 0 then
   8.116 +            list_comb (f, map subst args)
   8.117 +          else if ctr_pos >= length args then
   8.118 +            primrec_error_eqn "too few arguments in recursive call" t
   8.119 +          else
   8.120 +            let
   8.121 +              val (key, repl) = the (find_first (equal (nth args ctr_pos) o fst) substs)
   8.122 +                handle Option.Option => primrec_error_eqn
   8.123 +                  "recursive call not directly applied to constructor argument" t;
   8.124 +            in
   8.125 +              remove (op =) key args |> map subst |> curry list_comb repl
   8.126 +            end
   8.127 +        end
   8.128 +  in subst end;
   8.129 +
   8.130 +(* FIXME get rid of funs_data or get_indices *)
   8.131 +fun rewrite_map_arg funs_data get_indices y rec_type res_type =
   8.132 +  let
   8.133 +    val pT = HOLogic.mk_prodT (rec_type, res_type);
   8.134 +    val fstx = fst_const pT;
   8.135 +    val sndx = snd_const pT;
   8.136 +
   8.137 +    val SOME ({fun_name, left_args, ...} :: _) =
   8.138 +      find_first (equal rec_type o #rec_type o hd) funs_data;
   8.139 +    val ctr_pos = length left_args;
   8.140 +
   8.141 +    fun subst _ d (t as Bound d') = t |> d = d' ? curry (op $) fstx
   8.142 +      | subst l d (Abs (v, T, b)) = Abs (v, if d < 0 then pT else T, subst l (d + 1) b)
   8.143 +      | subst l d t =
   8.144 +        let val (u, vs) = strip_comb t in
   8.145 +          if try (fst o dest_Free) u = SOME fun_name then
   8.146 +            if l andalso length vs = ctr_pos then
   8.147 +              list_comb (sndx |> permute_args ctr_pos, vs)
   8.148 +            else if length vs <= ctr_pos then
   8.149 +              primrec_error_eqn "too few arguments in recursive call" t
   8.150 +            else if nth vs ctr_pos |> member (op =) [y, Bound d] then
   8.151 +              list_comb (sndx $ nth vs ctr_pos, nth_drop ctr_pos vs |> map (subst false d))
   8.152 +            else
   8.153 +              primrec_error_eqn "recursive call not directly applied to constructor argument" t
   8.154 +          else if try (fst o dest_Const) u = SOME @{const_name comp} then
   8.155 +            (hd vs |> get_indices |> null orelse
   8.156 +              primrec_error_eqn "recursive call not directly applied to constructor argument" t;
   8.157 +            list_comb
   8.158 +              (u |> map_types (strip_type #>> (fn Ts => Ts
   8.159 +                   |> nth_map (length Ts - 1) (K pT)
   8.160 +                   |> nth_map (length Ts - 2) (strip_type #>> nth_map 0 (K pT) #> (op --->)))
   8.161 +                 #> (op --->)),
   8.162 +              nth_map 1 (subst l d) vs))
   8.163 +          else
   8.164 +            list_comb (u, map (subst false d) vs)
   8.165 +        end
   8.166 +  in
   8.167 +    subst true ~1
   8.168 +  end;
   8.169 +
   8.170 +(* FIXME get rid of funs_data or get_indices *)
   8.171 +fun subst_indirect_call lthy funs_data get_indices (y, y') =
   8.172 +  let
   8.173 +    fun massage massage_map_arg bound_Ts =
   8.174 +      massage_indirect_rec_call lthy (not o null o get_indices) massage_map_arg bound_Ts y y';
   8.175 +    fun subst bound_Ts (t as _ $ _) =
   8.176 +        let
   8.177 +          val (f', args') = strip_comb t;
   8.178 +          val fun_arg_idx = find_index (exists_subterm (not o null o get_indices)) args';
   8.179 +          val arg_idx = find_index (exists_subterm (equal y)) args';
   8.180 +          val (f, args) = chop (arg_idx + 1) args' |>> curry list_comb f';
   8.181 +          val _ = fun_arg_idx < 0 orelse arg_idx >= 0 orelse
   8.182 +            primrec_error_eqn "recursive call not applied to constructor argument" t;
   8.183 +        in
   8.184 +          if fun_arg_idx <> arg_idx andalso fun_arg_idx >= 0 then
   8.185 +            if nth args' arg_idx = y then
   8.186 +              list_comb (massage (rewrite_map_arg funs_data get_indices y) bound_Ts f, args)
   8.187 +            else
   8.188 +              primrec_error_eqn "recursive call not directly applied to constructor argument" f
   8.189 +          else
   8.190 +            list_comb (f', map (subst bound_Ts) args')
   8.191 +        end
   8.192 +      | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
   8.193 +      | subst bound_Ts t = t |> t = y ? massage (K I |> K) bound_Ts;
   8.194 +  in subst [] end;
   8.195 +
   8.196 +fun build_rec_arg lthy get_indices funs_data ctr_spec maybe_eqn_data =
   8.197 +  if is_some maybe_eqn_data then
   8.198 +    let
   8.199 +      val eqn_data = the maybe_eqn_data;
   8.200 +      val t = #rhs_term eqn_data;
   8.201 +      val ctr_args = #ctr_args eqn_data;
   8.202 +
   8.203 +      val calls = #calls ctr_spec;
   8.204 +      val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2 | _ => 1)) calls 0;
   8.205 +
   8.206 +      val no_calls' = tag_list 0 calls
   8.207 +        |> map_filter (try (apsnd (fn No_Rec n => n | Direct_Rec (n, _) => n)));
   8.208 +      val direct_calls' = tag_list 0 calls
   8.209 +        |> map_filter (try (apsnd (fn Direct_Rec (_, n) => n)));
   8.210 +      val indirect_calls' = tag_list 0 calls
   8.211 +        |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
   8.212 +
   8.213 +      fun make_direct_type T = dummyT; (* FIXME? *)
   8.214 +
   8.215 +      val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
   8.216 +
   8.217 +      fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
   8.218 +        let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
   8.219 +          if is_some maybe_res_type
   8.220 +          then HOLogic.mk_prodT (T, the maybe_res_type)
   8.221 +          else make_indirect_type T end))
   8.222 +        | make_indirect_type T = T;
   8.223 +
   8.224 +      val args = replicate n_args ("", dummyT)
   8.225 +        |> Term.rename_wrt_term t
   8.226 +        |> map Free
   8.227 +        |> fold (fn (ctr_arg_idx, arg_idx) =>
   8.228 +            nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
   8.229 +          no_calls'
   8.230 +        |> fold (fn (ctr_arg_idx, arg_idx) =>
   8.231 +            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_direct_type)))
   8.232 +          direct_calls'
   8.233 +        |> fold (fn (ctr_arg_idx, arg_idx) =>
   8.234 +            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_indirect_type)))
   8.235 +          indirect_calls';
   8.236 +
   8.237 +      val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls';
   8.238 +      val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls';
   8.239 +
   8.240 +      val get_idx = (fn Free (v, _) => find_index (equal v o #fun_name o hd) funs_data | _ => ~1);
   8.241 +
   8.242 +      val t' = t
   8.243 +        |> fold (subst_indirect_call lthy funs_data get_indices) indirect_calls
   8.244 +        |> subst_direct_calls get_idx (length o #left_args o hd o nth funs_data) direct_calls;
   8.245 +
   8.246 +      val abstractions = map dest_Free (args @ #left_args eqn_data @ #right_args eqn_data);
   8.247 +    in
   8.248 +      t' |> fold_rev absfree abstractions
   8.249 +    end
   8.250 +  else Const (@{const_name undefined}, dummyT)
   8.251 +
   8.252 +fun build_defs lthy bs funs_data rec_specs get_indices =
   8.253 +  let
   8.254 +    val n_funs = length funs_data;
   8.255 +
   8.256 +    val ctr_spec_eqn_data_list' =
   8.257 +      (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data
   8.258 +      |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
   8.259 +          ##> (fn x => null x orelse
   8.260 +            primrec_error_eqns "excess equations in definition" (map #rhs_term x)) #> fst);
   8.261 +    val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse
   8.262 +      primrec_error_eqns ("multiple equations for constructor") (map #user_eqn x));
   8.263 +
   8.264 +    val ctr_spec_eqn_data_list =
   8.265 +      ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
   8.266 +
   8.267 +    val recs = take n_funs rec_specs |> map #recx;
   8.268 +    val rec_args = ctr_spec_eqn_data_list
   8.269 +      |> sort ((op <) o pairself (#offset o fst) |> make_ord)
   8.270 +      |> map (uncurry (build_rec_arg lthy get_indices funs_data) o apsnd (try the_single));
   8.271 +    val ctr_poss = map (fn x =>
   8.272 +      if length (distinct ((op =) o pairself (length o #left_args)) x) <> 1 then
   8.273 +        primrec_error ("inconstant constructor pattern position for function " ^
   8.274 +          quote (#fun_name (hd x)))
   8.275 +      else
   8.276 +        hd x |> #left_args |> length) funs_data;
   8.277 +  in
   8.278 +    (recs, ctr_poss)
   8.279 +    |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
   8.280 +    |> Syntax.check_terms lthy
   8.281 +    |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
   8.282 +  end;
   8.283 +
   8.284 +fun find_rec_calls get_indices eqn_data =
   8.285 +  let
   8.286 +    fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg
   8.287 +      | find (t as _ $ _) ctr_arg =
   8.288 +        let
   8.289 +          val (f', args') = strip_comb t;
   8.290 +          val n = find_index (equal ctr_arg) args';
   8.291 +        in
   8.292 +          if n < 0 then
   8.293 +            find f' ctr_arg @ maps (fn x => find x ctr_arg) args'
   8.294 +          else
   8.295 +            let val (f, args) = chop n args' |>> curry list_comb f' in
   8.296 +              if exists_subterm (not o null o get_indices) f then
   8.297 +                f :: maps (fn x => find x ctr_arg) args
   8.298 +              else
   8.299 +                find f ctr_arg @ maps (fn x => find x ctr_arg) args
   8.300 +            end
   8.301 +        end
   8.302 +      | find _ _ = [];
   8.303 +  in
   8.304 +    map (find (#rhs_term eqn_data)) (#ctr_args eqn_data)
   8.305 +    |> (fn [] => NONE | callss => SOME (#ctr eqn_data, callss))
   8.306 +  end;
   8.307 +
   8.308 +fun add_primrec fixes specs lthy =
   8.309 +  let
   8.310 +    val bs = map (fst o fst) fixes;
   8.311 +    val fun_names = map Binding.name_of bs;
   8.312 +    val eqns_data = map (snd #> dissect_eqn lthy fun_names) specs;
   8.313 +    val funs_data = eqns_data
   8.314 +      |> partition_eq ((op =) o pairself #fun_name)
   8.315 +      |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
   8.316 +      |> map (fn (x, y) => the_single y handle List.Empty =>
   8.317 +          primrec_error ("missing equations for function " ^ quote x));
   8.318 +
   8.319 +    fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes
   8.320 +      |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
   8.321 +      |> map_filter I;
   8.322 +
   8.323 +    val arg_Ts = map (#rec_type o hd) funs_data;
   8.324 +    val res_Ts = map (#res_type o hd) funs_data;
   8.325 +    val callssss = funs_data
   8.326 +      |> map (partition_eq ((op =) o pairself #ctr))
   8.327 +      |> map (maps (map_filter (find_rec_calls get_indices)));
   8.328 +
   8.329 +    val ((nontriv, rec_specs, _, induct_thm, induct_thms), lthy') =
   8.330 +      rec_specs_of bs arg_Ts res_Ts get_indices callssss lthy;
   8.331 +
   8.332 +    val actual_nn = length funs_data;
   8.333 +
   8.334 +    val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
   8.335 +      map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
   8.336 +        primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
   8.337 +          " is not a constructor in left-hand side") user_eqn) eqns_data end;
   8.338 +
   8.339 +    val defs = build_defs lthy' bs funs_data rec_specs get_indices;
   8.340 +
   8.341 +    fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
   8.342 +        lthy =
   8.343 +      let
   8.344 +        val fun_name = #fun_name (hd fun_data);
   8.345 +        val def_thms = map (snd o snd) def_thms';
   8.346 +        val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
   8.347 +          |> fst
   8.348 +          |> map_filter (try (fn (x, [y]) =>
   8.349 +            (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
   8.350 +          |> map (fn (user_eqn, num_extra_args, rec_thm) =>
   8.351 +            mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
   8.352 +            |> K |> Goal.prove lthy [] [] user_eqn)
   8.353 +
   8.354 +        val notes =
   8.355 +          [(inductN, if actual_nn > 1 then [induct_thm] else [], []),
   8.356 +           (simpsN, simp_thms, simp_attrs)]
   8.357 +          |> filter_out (null o #2)
   8.358 +          |> map (fn (thmN, thms, attrs) =>
   8.359 +            ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]));
   8.360 +      in
   8.361 +        lthy |> Local_Theory.notes notes
   8.362 +      end;
   8.363 +
   8.364 +    val common_name = mk_common_name fun_names;
   8.365 +
   8.366 +    val common_notes =
   8.367 +      [(inductN, if nontriv andalso actual_nn > 1 then [induct_thm] else [], [])]
   8.368 +      |> filter_out (null o #2)
   8.369 +      |> map (fn (thmN, thms, attrs) =>
   8.370 +        ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
   8.371 +  in
   8.372 +    lthy'
   8.373 +    |> fold_map Local_Theory.define defs
   8.374 +    |-> (fn def_thms' => fold_map3 (prove def_thms') (take actual_nn rec_specs)
   8.375 +      (take actual_nn induct_thms) funs_data)
   8.376 +    |> snd
   8.377 +    |> Local_Theory.notes common_notes |> snd
   8.378 +  end;
   8.379 +
   8.380 +fun add_primrec_cmd raw_fixes raw_specs lthy =
   8.381 +  let
   8.382 +    val _ = let val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) in null d orelse
   8.383 +      primrec_error ("duplicate function name(s): " ^ commas d) end;
   8.384 +    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
   8.385 +  in
   8.386 +    add_primrec fixes specs lthy
   8.387 +      handle ERROR str => primrec_error str
   8.388 +  end
   8.389 +  handle Primrec_Error (str, eqns) =>
   8.390 +    if null eqns
   8.391 +    then error ("primrec_new error:\n  " ^ str)
   8.392 +    else error ("primrec_new error:\n  " ^ str ^ "\nin\n  " ^
   8.393 +      space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
   8.394 +
   8.395 +
   8.396 +val _ = Outer_Syntax.local_theory
   8.397 +  @{command_spec "primrec_new"}
   8.398 +  "define primitive recursive functions"
   8.399 +  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
   8.400 +
   8.401 +
   8.402 +
   8.403 +
   8.404 +
   8.405 +
   8.406 +
   8.407 +
   8.408 +
   8.409 +
   8.410 +
   8.411 +
   8.412 +
   8.413 +
   8.414 +
   8.415 +
   8.416 +type co_eqn_data_dtr_disc = {
   8.417 +  fun_name: string,
   8.418 +  ctr_no: int,
   8.419 +  cond: term,
   8.420 +  user_eqn: term
   8.421 +};
   8.422 +type co_eqn_data_dtr_sel = {
   8.423 +  fun_name: string,
   8.424 +  ctr_no: int,
   8.425 +  sel_no: int,
   8.426 +  fun_args: term list,
   8.427 +  rhs_term: term,
   8.428 +  user_eqn: term
   8.429 +};
   8.430 +datatype co_eqn_data =
   8.431 +  Dtr_Disc of co_eqn_data_dtr_disc |
   8.432 +  Dtr_Sel of co_eqn_data_dtr_sel
   8.433 +
   8.434 +fun co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps =
   8.435 +  let
   8.436 +    fun find_subterm p = let (* FIXME \<exists>? *)
   8.437 +      fun f (t as u $ v) =
   8.438 +        fold_rev (curry merge_options) [if p t then SOME t else NONE, f u, f v] NONE
   8.439 +        | f t = if p t then SOME t else NONE
   8.440 +      in f end;
   8.441 +
   8.442 +    val fun_name = imp_rhs
   8.443 +      |> perhaps (try HOLogic.dest_not)
   8.444 +      |> `(try (fst o dest_Free o head_of o snd o dest_comb))
   8.445 +      ||> (try (fst o dest_Free o head_of o fst o HOLogic.dest_eq))
   8.446 +      |> the o merge_options;
   8.447 +    val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
   8.448 +      handle Option.Option => primrec_error_eqn "malformed discriminator equation" imp_rhs;
   8.449 +
   8.450 +    val discs = #ctr_specs corec_spec |> map #disc;
   8.451 +    val ctrs = #ctr_specs corec_spec |> map #ctr;
   8.452 +    val n_ctrs = length ctrs;
   8.453 +    val not_disc = head_of imp_rhs = @{term Not};
   8.454 +    val _ = not_disc andalso n_ctrs <> 2 andalso
   8.455 +      primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" imp_rhs;
   8.456 +    val disc = find_subterm (member (op =) discs o head_of) imp_rhs;
   8.457 +    val eq_ctr0 = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd)
   8.458 +        |> (fn SOME t => let val n = find_index (equal t) ctrs in
   8.459 +          if n >= 0 then SOME n else NONE end | _ => NONE);
   8.460 +    val _ = is_some disc orelse is_some eq_ctr0 orelse
   8.461 +      primrec_error_eqn "no discriminator in equation" imp_rhs;
   8.462 +    val ctr_no' =
   8.463 +      if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs;
   8.464 +    val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
   8.465 +    val fun_args = if is_none disc
   8.466 +      then imp_rhs |> perhaps (try HOLogic.dest_not) |> HOLogic.dest_eq |> fst |> strip_comb |> snd
   8.467 +      else the disc |> the_single o snd o strip_comb
   8.468 +        |> (fn t => if try (fst o dest_Free o head_of) t = SOME fun_name
   8.469 +          then snd (strip_comb t) else []);
   8.470 +
   8.471 +    val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
   8.472 +    val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
   8.473 +    val catch_all = try (fst o dest_Free o the_single) imp_lhs' = SOME Name.uu_;
   8.474 +    val matched_conds = filter (equal fun_name o fst) matched_conds_ps |> map snd;
   8.475 +    val imp_lhs = mk_conjs imp_lhs';
   8.476 +    val cond =
   8.477 +      if catch_all then
   8.478 +        if null matched_conds then fold_rev absfree (map dest_Free fun_args) @{const True} else
   8.479 +          (strip_abs_vars (hd matched_conds),
   8.480 +            mk_disjs (map strip_abs_body matched_conds) |> HOLogic.mk_not)
   8.481 +          |-> fold_rev (fn (v, T) => fn u => Abs (v, T, u))
   8.482 +      else if sequential then
   8.483 +        HOLogic.mk_conj (HOLogic.mk_not (mk_disjs (map strip_abs_body matched_conds)), imp_lhs)
   8.484 +        |> fold_rev absfree (map dest_Free fun_args)
   8.485 +      else
   8.486 +        imp_lhs |> fold_rev absfree (map dest_Free fun_args);
   8.487 +    val matched_cond =
   8.488 +      if sequential then fold_rev absfree (map dest_Free fun_args) imp_lhs else cond;
   8.489 +
   8.490 +    val matched_conds_ps' = if catch_all
   8.491 +      then (fun_name, cond) :: filter (not_equal fun_name o fst) matched_conds_ps
   8.492 +      else (fun_name, matched_cond) :: matched_conds_ps;
   8.493 +  in
   8.494 +    (Dtr_Disc {
   8.495 +      fun_name = fun_name,
   8.496 +      ctr_no = ctr_no,
   8.497 +      cond = cond,
   8.498 +      user_eqn = eqn'
   8.499 +    }, matched_conds_ps')
   8.500 +  end;
   8.501 +
   8.502 +fun co_dissect_eqn_sel fun_name_corec_spec_list eqn' eqn =
   8.503 +  let
   8.504 +    val (lhs, rhs) = HOLogic.dest_eq eqn
   8.505 +      handle TERM _ =>
   8.506 +        primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
   8.507 +    val sel = head_of lhs;
   8.508 +    val (fun_name, fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst (fst o dest_Free)
   8.509 +      handle TERM _ =>
   8.510 +        primrec_error_eqn "malformed selector argument in left-hand side" eqn;
   8.511 +    val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
   8.512 +      handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn;
   8.513 +    val ((ctr_spec, ctr_no), sel) = #ctr_specs corec_spec
   8.514 +      |> the o get_index (try (the o find_first (equal sel) o #sels))
   8.515 +      |>> `(nth (#ctr_specs corec_spec));
   8.516 +    val sel_no = find_index (equal sel) (#sels ctr_spec);
   8.517 +  in
   8.518 +    Dtr_Sel {
   8.519 +      fun_name = fun_name,
   8.520 +      ctr_no = ctr_no,
   8.521 +      sel_no = sel_no,
   8.522 +      fun_args = fun_args,
   8.523 +      rhs_term = rhs,
   8.524 +      user_eqn = eqn'
   8.525 +    }
   8.526 +  end;
   8.527 +
   8.528 +fun co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps =
   8.529 +  let 
   8.530 +    val (lhs, rhs) = HOLogic.dest_eq imp_rhs;
   8.531 +    val fun_name = head_of lhs |> fst o dest_Free;
   8.532 +    val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name);
   8.533 +    val (ctr, ctr_args) = strip_comb rhs;
   8.534 +    val ctr_spec = the (find_first (equal ctr o #ctr) (#ctr_specs corec_spec))
   8.535 +      handle Option.Option => primrec_error_eqn "not a constructor" ctr;
   8.536 +    val disc_imp_rhs = betapply (#disc ctr_spec, lhs);
   8.537 +    val (eqn_data_disc, matched_conds_ps') = co_dissect_eqn_disc
   8.538 +        sequential fun_name_corec_spec_list eqn' imp_lhs' disc_imp_rhs matched_conds_ps;
   8.539 +
   8.540 +    val sel_imp_rhss = (#sels ctr_spec ~~ ctr_args)
   8.541 +      |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
   8.542 +
   8.543 +val _ = warning ("reduced\n    " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n    \<cdot> " ^
   8.544 + Syntax.string_of_term @{context} disc_imp_rhs ^ "\n    \<cdot> " ^
   8.545 + space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
   8.546 +
   8.547 +    val eqns_data_sel =
   8.548 +      map (co_dissect_eqn_sel fun_name_corec_spec_list @{const True}(*###*)) sel_imp_rhss;
   8.549 +  in
   8.550 +    (eqn_data_disc :: eqns_data_sel, matched_conds_ps')
   8.551 +  end;
   8.552 +
   8.553 +fun co_dissect_eqn sequential fun_name_corec_spec_list eqn' matched_conds_ps =
   8.554 +  let
   8.555 +    val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
   8.556 +        strip_qnt_body @{const_name all} eqn')
   8.557 +        handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
   8.558 +    val (imp_lhs', imp_rhs) =
   8.559 +      (map HOLogic.dest_Trueprop (Logic.strip_imp_prems eqn),
   8.560 +       HOLogic.dest_Trueprop (Logic.strip_imp_concl eqn));
   8.561 +
   8.562 +    val head = imp_rhs
   8.563 +      |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
   8.564 +      |> head_of;
   8.565 +
   8.566 +    val maybe_rhs = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq);
   8.567 +
   8.568 +    val fun_names = map fst fun_name_corec_spec_list;
   8.569 +    val discs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #disc;
   8.570 +    val sels = maps (#ctr_specs o snd) fun_name_corec_spec_list |> maps #sels;
   8.571 +    val ctrs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #ctr;
   8.572 +  in
   8.573 +    if member (op =) discs head orelse
   8.574 +      is_some maybe_rhs andalso
   8.575 +        member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then
   8.576 +      co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps
   8.577 +      |>> single
   8.578 +    else if member (op =) sels head then
   8.579 +      ([co_dissect_eqn_sel fun_name_corec_spec_list eqn' imp_rhs], matched_conds_ps)
   8.580 +    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
   8.581 +      co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps
   8.582 +    else
   8.583 +      primrec_error_eqn "malformed function equation" eqn
   8.584 +  end;
   8.585 +
   8.586 +fun build_corec_args_discs ctr_specs disc_eqns =
   8.587 +  let
   8.588 +    val conds = map #cond disc_eqns;
   8.589 +    val args =
   8.590 +      if length ctr_specs = 1 then []
   8.591 +      else if length disc_eqns = length ctr_specs then
   8.592 +        fst (split_last conds)
   8.593 +      else if length disc_eqns = length ctr_specs - 1 then
   8.594 +        let val n = 0 upto length ctr_specs - 1
   8.595 +            |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) (*###*) in
   8.596 +          if n = length ctr_specs - 1 then
   8.597 +            conds
   8.598 +          else
   8.599 +            split_last conds
   8.600 +            ||> (fn t => fold_rev absfree (strip_abs_vars t) (strip_abs_body t |> HOLogic.mk_not))
   8.601 +            |>> chop n
   8.602 +            |> (fn ((l, r), x) => l @ (x :: r))
   8.603 +        end
   8.604 +      else
   8.605 +        0 upto length ctr_specs - 1
   8.606 +        |> map (fn idx => find_first (equal idx o #ctr_no) disc_eqns
   8.607 +          |> Option.map #cond
   8.608 +          |> the_default (Const (@{const_name undefined}, dummyT)))
   8.609 +        |> fst o split_last;
   8.610 +    fun finish t =
   8.611 +      let val n = length (fastype_of t |> binder_types) in
   8.612 +        if t = Const (@{const_name undefined}, dummyT) then t
   8.613 +        else if n = 0 then Abs (Name.uu_, @{typ unit}, t)
   8.614 +        else if n = 1 then t
   8.615 +        else Const (@{const_name prod_case}, dummyT) $ t
   8.616 +      end;
   8.617 +  in
   8.618 +    map finish args
   8.619 +  end;
   8.620 +
   8.621 +fun build_corec_args_sel sel_eqns ctr_spec =
   8.622 +  let
   8.623 +    (* FIXME *)
   8.624 +    val n_args = fold (curry (op +)) (map (fn Direct_Corec _ => 3 | _ => 1) (#calls ctr_spec)) 0;
   8.625 +  in
   8.626 +    replicate n_args (Const (@{const_name undefined}, dummyT))
   8.627 +  end;
   8.628 +
   8.629 +fun co_build_defs lthy sequential bs arg_Tss fun_name_corec_spec_list eqns_data =
   8.630 +  let
   8.631 +    val fun_names = map Binding.name_of bs;
   8.632 +
   8.633 +(*    fun group _ [] = [] (* FIXME \<exists>? *)
   8.634 +      | group eq (x :: xs) =
   8.635 +        let val (xs', ys) = List.partition (eq x) xs in (x :: xs') :: group eq ys end;*)
   8.636 +    val disc_eqnss = map_filter (try (fn Dtr_Disc x => x)) eqns_data
   8.637 +      |> partition_eq ((op =) o pairself #fun_name)
   8.638 +      |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
   8.639 +      |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
   8.640 +
   8.641 +    val _ = disc_eqnss |> map (fn x =>
   8.642 +      let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse
   8.643 +        primrec_error_eqns "excess discriminator equations in definition"
   8.644 +          (maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end);
   8.645 +
   8.646 +val _ = warning ("disc_eqnss:\n    \<cdot> " ^ space_implode "\n    \<cdot> " (map @{make_string} disc_eqnss));
   8.647 +
   8.648 +    val sel_eqnss = map_filter (try (fn Dtr_Sel x => x)) eqns_data
   8.649 +      |> partition_eq ((op =) o pairself #fun_name)
   8.650 +      |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
   8.651 +      |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
   8.652 +
   8.653 +val _ = warning ("sel_eqnss:\n    \<cdot> " ^ space_implode "\n    \<cdot> " (map @{make_string} sel_eqnss));
   8.654 +
   8.655 +    fun splice (xs :: xss) (ys :: yss) = xs @ ys @ splice xss yss (* FIXME \<exists>? *)
   8.656 +      | splice xss yss = flat xss @ flat yss;
   8.657 +    val corecs = map (#corec o snd) fun_name_corec_spec_list;
   8.658 +    val corec_args = (map snd fun_name_corec_spec_list ~~ disc_eqnss ~~ sel_eqnss)
   8.659 +      |> maps (fn (({ctr_specs, ...}, disc_eqns), sel_eqns) =>
   8.660 +        splice (build_corec_args_discs ctr_specs disc_eqns |> map single)
   8.661 +          (map (build_corec_args_sel sel_eqns) ctr_specs));
   8.662 +
   8.663 +val _ = warning ("corecursor arguments:\n    \<cdot> " ^
   8.664 + space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) corec_args));
   8.665 +
   8.666 +    fun uneq_pairs_rev xs = xs (* FIXME \<exists>? *)
   8.667 +      |> these o try (split_last #> (fn (ys, y) => uneq_pairs_rev ys @ map (pair y) ys));
   8.668 +    val proof_obligations = if sequential then [] else
   8.669 +      maps (uneq_pairs_rev o map #cond) disc_eqnss
   8.670 +      |> map (fn (x, y) => ((strip_abs_body x, strip_abs_body y), strip_abs_vars x))
   8.671 +      |> map (apfst (apsnd HOLogic.mk_not #> pairself HOLogic.mk_Trueprop
   8.672 +        #> apfst (curry (op $) @{const ==>}) #> (op $)))
   8.673 +      |> map (fn (t, abs_vars) => fold_rev (fn (v, T) => fn u =>
   8.674 +          Const (@{const_name all}, (T --> @{typ prop}) --> @{typ prop}) $
   8.675 +            Abs (v, T, u)) abs_vars t);
   8.676 +
   8.677 +    fun currys Ts t = if length Ts <= 1 then t else
   8.678 +      t $ foldr1 (fn (u, v) => HOLogic.pair_const dummyT dummyT $ u $ v)
   8.679 +        (length Ts - 1 downto 0 |> map Bound)
   8.680 +      |> fold_rev (fn T => fn u => Abs ("", T, u)) Ts;
   8.681 +  in
   8.682 +    map (list_comb o rpair corec_args) corecs
   8.683 +    |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
   8.684 +    |> map2 currys arg_Tss
   8.685 +    |> Syntax.check_terms lthy
   8.686 +    |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
   8.687 +    |> rpair proof_obligations
   8.688 +  end;
   8.689 +
   8.690 +fun add_primcorec sequential fixes specs lthy =
   8.691 +  let
   8.692 +    val bs = map (fst o fst) fixes;
   8.693 +    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
   8.694 +
   8.695 +    (* copied from primrec_new *)
   8.696 +    fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes
   8.697 +      |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
   8.698 +      |> map_filter I;
   8.699 +
   8.700 +    val callssss = []; (* FIXME *)
   8.701 +
   8.702 +    val ((nontriv, corec_specs, _, coinduct_thm, strong_co_induct_thm, coinduct_thmss,
   8.703 +          strong_coinduct_thmss), lthy') =
   8.704 +      corec_specs_of bs arg_Ts res_Ts get_indices callssss lthy;
   8.705 +
   8.706 +    val fun_names = map Binding.name_of bs;
   8.707 +
   8.708 +    val fun_name_corec_spec_list = (fun_names ~~ res_Ts, corec_specs)
   8.709 +      |> uncurry (finds (fn ((v, T), {corec, ...}) => T = body_type (fastype_of corec))) |> fst
   8.710 +      |> map (apfst fst #> apsnd the_single); (*###*)
   8.711 +
   8.712 +    val (eqns_data, _) =
   8.713 +      fold_map (co_dissect_eqn sequential fun_name_corec_spec_list) (map snd specs) []
   8.714 +      |>> flat;
   8.715 +
   8.716 +    val (defs, proof_obligations) =
   8.717 +      co_build_defs lthy' sequential bs (map (binder_types o snd o fst) fixes)
   8.718 +        fun_name_corec_spec_list eqns_data;
   8.719 +  in
   8.720 +    lthy'
   8.721 +    |> fold_map Local_Theory.define defs |> snd
   8.722 +    |> Proof.theorem NONE (K I) [map (rpair []) proof_obligations]
   8.723 +    |> Proof.refine (Method.primitive_text I)
   8.724 +    |> Seq.hd
   8.725 +  end
   8.726 +
   8.727 +fun add_primcorec_cmd seq (raw_fixes, raw_specs) lthy =
   8.728 +  let
   8.729 +    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
   8.730 +  in
   8.731 +    add_primcorec seq fixes specs lthy
   8.732 +    handle ERROR str => primrec_error str
   8.733 +  end
   8.734 +  handle Primrec_Error (str, eqns) =>
   8.735 +    if null eqns
   8.736 +    then error ("primcorec error:\n  " ^ str)
   8.737 +    else error ("primcorec error:\n  " ^ str ^ "\nin\n  " ^
   8.738 +      space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
   8.739 +
   8.740 +val _ = Outer_Syntax.local_theory_to_proof
   8.741 +  @{command_spec "primcorec"}
   8.742 +  "define primitive corecursive functions"
   8.743 +  (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
   8.744 +    uncurry add_primcorec_cmd);
   8.745 +
   8.746 +end;
   8.747 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Fri Aug 30 11:27:23 2013 +0200
     9.3 @@ -0,0 +1,66 @@
     9.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
     9.5 +    Author:     Jasmin Blanchette, TU Muenchen
     9.6 +    Copyright   2013
     9.7 +
     9.8 +Tactics for recursor and corecursor sugar.
     9.9 +*)
    9.10 +
    9.11 +signature BNF_FP_REC_SUGAR_TACTICS =
    9.12 +sig
    9.13 +  val mk_primcorec_taut_tac: Proof.context -> tactic
    9.14 +  val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    9.15 +    tactic
    9.16 +  val mk_primcorec_dtr_to_ctr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
    9.17 +  val mk_primcorec_eq_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    9.18 +    thm list -> thm list -> thm list -> tactic
    9.19 +  val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
    9.20 +end;
    9.21 +
    9.22 +structure BNF_FP_Rec_Sugar_Tactics : BNF_FP_REC_SUGAR_TACTICS =
    9.23 +struct
    9.24 +
    9.25 +open BNF_Util
    9.26 +open BNF_Tactics
    9.27 +
    9.28 +fun mk_primrec_tac ctxt num_extra_args map_id's map_comps fun_defs recx =
    9.29 +  unfold_thms_tac ctxt fun_defs THEN
    9.30 +  HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
    9.31 +  unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_id's) THEN
    9.32 +  HEADGOAL (rtac refl);
    9.33 +
    9.34 +fun mk_primcorec_taut_tac ctxt =
    9.35 +  HEADGOAL (etac FalseE) ORELSE
    9.36 +  unfold_thms_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not not_False_eq_True} THEN
    9.37 +  HEADGOAL (SOLVE o REPEAT o (atac ORELSE' resolve_tac @{thms disjI1 disjI2 conjI TrueI}));
    9.38 +
    9.39 +fun mk_primcorec_same_case_tac m =
    9.40 +  HEADGOAL (if m = 0 then rtac TrueI
    9.41 +    else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
    9.42 +
    9.43 +fun mk_primcorec_different_case_tac ctxt excl =
    9.44 +  unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
    9.45 +  HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_taut_tac ctxt));
    9.46 +
    9.47 +fun mk_primcorec_cases_tac ctxt k m exclsss =
    9.48 +  let val n = length exclsss in
    9.49 +    EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
    9.50 +        | [excl] => mk_primcorec_different_case_tac ctxt excl)
    9.51 +      (take k (nth exclsss (k - 1))))
    9.52 +  end;
    9.53 +
    9.54 +fun mk_primcorec_prelude ctxt defs thm =
    9.55 +  unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt @{thms split};
    9.56 +
    9.57 +fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
    9.58 +  mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
    9.59 +
    9.60 +fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_id's map_comps =
    9.61 +  mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
    9.62 +  unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
    9.63 +    maps @ map_comps @ map_id's) THEN HEADGOAL (rtac refl);
    9.64 +
    9.65 +fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
    9.66 +  HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
    9.67 +  unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
    9.68 +
    9.69 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Aug 30 11:27:23 2013 +0200
    10.3 @@ -0,0 +1,437 @@
    10.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
    10.5 +    Author:     Lorenz Panny, TU Muenchen
    10.6 +    Author:     Jasmin Blanchette, TU Muenchen
    10.7 +    Copyright   2013
    10.8 +
    10.9 +Library for recursor and corecursor sugar.
   10.10 +*)
   10.11 +
   10.12 +signature BNF_FP_REC_SUGAR_UTIL =
   10.13 +sig
   10.14 +  datatype rec_call =
   10.15 +    No_Rec of int |
   10.16 +    Direct_Rec of int (*before*) * int (*after*) |
   10.17 +    Indirect_Rec of int
   10.18 +
   10.19 +  datatype corec_call =
   10.20 +    Dummy_No_Corec of int |
   10.21 +    No_Corec of int |
   10.22 +    Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
   10.23 +    Indirect_Corec of int
   10.24 +
   10.25 +  type rec_ctr_spec =
   10.26 +    {ctr: term,
   10.27 +     offset: int,
   10.28 +     calls: rec_call list,
   10.29 +     rec_thm: thm}
   10.30 +
   10.31 +  type corec_ctr_spec =
   10.32 +    {ctr: term,
   10.33 +     disc: term,
   10.34 +     sels: term list,
   10.35 +     pred: int option,
   10.36 +     calls: corec_call list,
   10.37 +     corec_thm: thm}
   10.38 +
   10.39 +  type rec_spec =
   10.40 +    {recx: term,
   10.41 +     nested_map_id's: thm list,
   10.42 +     nested_map_comps: thm list,
   10.43 +     ctr_specs: rec_ctr_spec list}
   10.44 +
   10.45 +  type corec_spec =
   10.46 +    {corec: term,
   10.47 +     ctr_specs: corec_ctr_spec list}
   10.48 +
   10.49 +  val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
   10.50 +    typ list -> term -> term -> term -> term
   10.51 +  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
   10.52 +    typ list -> typ -> term -> term
   10.53 +  val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
   10.54 +    (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
   10.55 +  val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
   10.56 +    ((term * term list list) list) list -> local_theory ->
   10.57 +    (bool * rec_spec list * typ list * thm * thm list) * local_theory
   10.58 +  val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
   10.59 +    ((term * term list list) list) list -> local_theory ->
   10.60 +    (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
   10.61 +end;
   10.62 +
   10.63 +structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
   10.64 +struct
   10.65 +
   10.66 +open BNF_Util
   10.67 +open BNF_Def
   10.68 +open BNF_Ctr_Sugar
   10.69 +open BNF_FP_Util
   10.70 +open BNF_FP_Def_Sugar
   10.71 +open BNF_FP_N2M_Sugar
   10.72 +
   10.73 +datatype rec_call =
   10.74 +  No_Rec of int |
   10.75 +  Direct_Rec of int * int |
   10.76 +  Indirect_Rec of int;
   10.77 +
   10.78 +datatype corec_call =
   10.79 +  Dummy_No_Corec of int |
   10.80 +  No_Corec of int |
   10.81 +  Direct_Corec of int * int * int |
   10.82 +  Indirect_Corec of int;
   10.83 +
   10.84 +type rec_ctr_spec =
   10.85 +  {ctr: term,
   10.86 +   offset: int,
   10.87 +   calls: rec_call list,
   10.88 +   rec_thm: thm};
   10.89 +
   10.90 +type corec_ctr_spec =
   10.91 +  {ctr: term,
   10.92 +   disc: term,
   10.93 +   sels: term list,
   10.94 +   pred: int option,
   10.95 +   calls: corec_call list,
   10.96 +   corec_thm: thm};
   10.97 +
   10.98 +type rec_spec =
   10.99 +  {recx: term,
  10.100 +   nested_map_id's: thm list,
  10.101 +   nested_map_comps: thm list,
  10.102 +   ctr_specs: rec_ctr_spec list};
  10.103 +
  10.104 +type corec_spec =
  10.105 +  {corec: term,
  10.106 +   ctr_specs: corec_ctr_spec list};
  10.107 +
  10.108 +val id_def = @{thm id_def};
  10.109 +
  10.110 +exception AINT_NO_MAP of term;
  10.111 +
  10.112 +fun ill_formed_rec_call ctxt t =
  10.113 +  error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
  10.114 +fun ill_formed_corec_call ctxt t =
  10.115 +  error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
  10.116 +fun invalid_map ctxt t =
  10.117 +  error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
  10.118 +fun unexpected_rec_call ctxt t =
  10.119 +  error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
  10.120 +fun unexpected_corec_call ctxt t =
  10.121 +  error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
  10.122 +
  10.123 +fun factor_out_types ctxt massage destU U T =
  10.124 +  (case try destU U of
  10.125 +    SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
  10.126 +  | NONE => invalid_map ctxt);
  10.127 +
  10.128 +fun map_flattened_map_args ctxt s map_args fs =
  10.129 +  let
  10.130 +    val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
  10.131 +    val flat_fs' = map_args flat_fs;
  10.132 +  in
  10.133 +    permute_like (op aconv) flat_fs fs flat_fs'
  10.134 +  end;
  10.135 +
  10.136 +fun massage_indirect_rec_call ctxt has_call massage_unapplied_direct_call bound_Ts y y' =
  10.137 +  let
  10.138 +    val typof = curry fastype_of1 bound_Ts;
  10.139 +    val build_map_fst = build_map ctxt (fst_const o fst);
  10.140 +
  10.141 +    val yT = typof y;
  10.142 +    val yU = typof y';
  10.143 +
  10.144 +    fun y_of_y' () = build_map_fst (yU, yT) $ y';
  10.145 +    val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
  10.146 +
  10.147 +    fun check_and_massage_unapplied_direct_call U T t =
  10.148 +      if has_call t then
  10.149 +        factor_out_types ctxt massage_unapplied_direct_call HOLogic.dest_prodT U T t
  10.150 +      else
  10.151 +        HOLogic.mk_comp (t, build_map_fst (U, T));
  10.152 +
  10.153 +    fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
  10.154 +        (case try (dest_map ctxt s) t of
  10.155 +          SOME (map0, fs) =>
  10.156 +          let
  10.157 +            val Type (_, ran_Ts) = range_type (typof t);
  10.158 +            val map' = mk_map (length fs) Us ran_Ts map0;
  10.159 +            val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
  10.160 +          in
  10.161 +            list_comb (map', fs')
  10.162 +          end
  10.163 +        | NONE => raise AINT_NO_MAP t)
  10.164 +      | massage_map _ _ t = raise AINT_NO_MAP t
  10.165 +    and massage_map_or_map_arg U T t =
  10.166 +      if T = U then
  10.167 +        if has_call t then unexpected_rec_call ctxt t else t
  10.168 +      else
  10.169 +        massage_map U T t
  10.170 +        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
  10.171 +
  10.172 +    fun massage_call (t as t1 $ t2) =
  10.173 +        if t2 = y then
  10.174 +          massage_map yU yT (elim_y t1) $ y'
  10.175 +          handle AINT_NO_MAP t' => invalid_map ctxt t'
  10.176 +        else
  10.177 +          ill_formed_rec_call ctxt t
  10.178 +      | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
  10.179 +  in
  10.180 +    massage_call o Envir.beta_eta_contract
  10.181 +  end;
  10.182 +
  10.183 +fun massage_let_and_if ctxt has_call massage_rec massage_else U T t =
  10.184 +  (case Term.strip_comb t of
  10.185 +    (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
  10.186 +  | (Const (@{const_name If}, _), arg :: args) =>
  10.187 +    if has_call arg then unexpected_corec_call ctxt arg
  10.188 +    else list_comb (If_const U $ arg, map (massage_rec U T) args)
  10.189 +  | _ => massage_else U T t);
  10.190 +
  10.191 +fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
  10.192 +  let
  10.193 +    val typof = curry fastype_of1 bound_Ts;
  10.194 +
  10.195 +    fun massage_call U T =
  10.196 +      massage_let_and_if ctxt has_call massage_call massage_direct_call U T;
  10.197 +  in
  10.198 +    massage_call res_U (typof t) (Envir.beta_eta_contract t)
  10.199 +  end;
  10.200 +
  10.201 +fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
  10.202 +  let
  10.203 +    val typof = curry fastype_of1 bound_Ts;
  10.204 +    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o fst);
  10.205 +
  10.206 +    fun check_and_massage_direct_call U T t =
  10.207 +      if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
  10.208 +      else build_map_Inl (U, T) $ t;
  10.209 +
  10.210 +    fun check_and_massage_unapplied_direct_call U T t =
  10.211 +      let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
  10.212 +        Term.lambda var (check_and_massage_direct_call U T (t $ var))
  10.213 +      end;
  10.214 +
  10.215 +    fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
  10.216 +        (case try (dest_map ctxt s) t of
  10.217 +          SOME (map0, fs) =>
  10.218 +          let
  10.219 +            val Type (_, dom_Ts) = domain_type (typof t);
  10.220 +            val map' = mk_map (length fs) dom_Ts Us map0;
  10.221 +            val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
  10.222 +          in
  10.223 +            list_comb (map', fs')
  10.224 +          end
  10.225 +        | NONE => raise AINT_NO_MAP t)
  10.226 +      | massage_map _ _ t = raise AINT_NO_MAP t
  10.227 +    and massage_map_or_map_arg U T t =
  10.228 +      if T = U then
  10.229 +        if has_call t then unexpected_corec_call ctxt t else t
  10.230 +      else
  10.231 +        massage_map U T t
  10.232 +        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
  10.233 +
  10.234 +    fun massage_call U T =
  10.235 +      massage_let_and_if ctxt has_call massage_call
  10.236 +        (fn U => fn T => fn t =>
  10.237 +            (case U of
  10.238 +              Type (s, Us) =>
  10.239 +              (case try (dest_ctr ctxt s) t of
  10.240 +                SOME (f, args) =>
  10.241 +                let val f' = mk_ctr Us f in
  10.242 +                  list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
  10.243 +                end
  10.244 +              | NONE =>
  10.245 +                (case t of
  10.246 +                  t1 $ t2 =>
  10.247 +                  if has_call t2 then
  10.248 +                    check_and_massage_direct_call U T t
  10.249 +                  else
  10.250 +                    massage_map U T t1 $ t2
  10.251 +                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t
  10.252 +                | _ => check_and_massage_direct_call U T t))
  10.253 +            | _ => ill_formed_corec_call ctxt t))
  10.254 +        U T
  10.255 +  in
  10.256 +    massage_call res_U (typof t) (Envir.beta_eta_contract t)
  10.257 +  end;
  10.258 +
  10.259 +fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
  10.260 +fun indexedd xss = fold_map indexed xss;
  10.261 +fun indexeddd xsss = fold_map indexedd xsss;
  10.262 +fun indexedddd xssss = fold_map indexeddd xssss;
  10.263 +
  10.264 +fun find_index_eq hs h = find_index (curry (op =) h) hs;
  10.265 +
  10.266 +val lose_co_rec = false (*FIXME: try true?*);
  10.267 +
  10.268 +fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
  10.269 +  let
  10.270 +    val thy = Proof_Context.theory_of lthy;
  10.271 +
  10.272 +    val ((nontriv, missing_arg_Ts, perm0_kks,
  10.273 +          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
  10.274 +            co_inducts = [induct_thm], ...} :: _), lthy') =
  10.275 +      nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
  10.276 +
  10.277 +    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
  10.278 +
  10.279 +    val indices = map #index fp_sugars;
  10.280 +    val perm_indices = map #index perm_fp_sugars;
  10.281 +
  10.282 +    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
  10.283 +    val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
  10.284 +    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
  10.285 +
  10.286 +    val nn0 = length arg_Ts;
  10.287 +    val nn = length perm_fpTs;
  10.288 +    val kks = 0 upto nn - 1;
  10.289 +    val perm_ns = map length perm_ctr_Tsss;
  10.290 +    val perm_mss = map (map length) perm_ctr_Tsss;
  10.291 +
  10.292 +    val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
  10.293 +      perm_fp_sugars;
  10.294 +    val perm_fun_arg_Tssss = mk_iter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of ctor_iters1);
  10.295 +
  10.296 +    fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
  10.297 +    fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
  10.298 +
  10.299 +    val induct_thms = unpermute0 (conj_dests nn induct_thm);
  10.300 +
  10.301 +    val fpTs = unpermute perm_fpTs;
  10.302 +    val Cs = unpermute perm_Cs;
  10.303 +
  10.304 +    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
  10.305 +    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
  10.306 +
  10.307 +    val substA = Term.subst_TVars As_rho;
  10.308 +    val substAT = Term.typ_subst_TVars As_rho;
  10.309 +    val substCT = Term.typ_subst_TVars Cs_rho;
  10.310 +
  10.311 +    val perm_Cs' = map substCT perm_Cs;
  10.312 +
  10.313 +    fun offset_of_ctr 0 _ = 0
  10.314 +      | offset_of_ctr n ({ctrs, ...} :: ctr_sugars) =
  10.315 +        length ctrs + offset_of_ctr (n - 1) ctr_sugars;
  10.316 +
  10.317 +    fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
  10.318 +      | call_of [i, i'] _ = Direct_Rec (i, i');
  10.319 +
  10.320 +    fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
  10.321 +      let
  10.322 +        val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
  10.323 +        val fun_arg_hs = flat_rec_arg_args fun_arg_hss;
  10.324 +        val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss;
  10.325 +      in
  10.326 +        {ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss,
  10.327 +         rec_thm = rec_thm}
  10.328 +      end;
  10.329 +
  10.330 +    fun mk_ctr_specs index ctr_sugars iter_thmsss =
  10.331 +      let
  10.332 +        val ctrs = #ctrs (nth ctr_sugars index);
  10.333 +        val rec_thmss = co_rec_of (nth iter_thmsss index);
  10.334 +        val k = offset_of_ctr index ctr_sugars;
  10.335 +        val n = length ctrs;
  10.336 +      in
  10.337 +        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
  10.338 +      end;
  10.339 +
  10.340 +    fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
  10.341 +      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
  10.342 +       nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
  10.343 +       nested_map_comps = map map_comp_of_bnf nested_bnfs,
  10.344 +       ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
  10.345 +  in
  10.346 +    ((nontriv, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy')
  10.347 +  end;
  10.348 +
  10.349 +fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
  10.350 +  let
  10.351 +    val thy = Proof_Context.theory_of lthy;
  10.352 +
  10.353 +    val ((nontriv, missing_res_Ts, perm0_kks,
  10.354 +          fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
  10.355 +          co_inducts = coinduct_thms, ...} :: _), lthy') =
  10.356 +      nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
  10.357 +
  10.358 +    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
  10.359 +
  10.360 +    val indices = map #index fp_sugars;
  10.361 +    val perm_indices = map #index perm_fp_sugars;
  10.362 +
  10.363 +    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
  10.364 +    val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
  10.365 +    val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
  10.366 +
  10.367 +    val nn0 = length res_Ts;
  10.368 +    val nn = length perm_fpTs;
  10.369 +    val kks = 0 upto nn - 1;
  10.370 +    val perm_ns = map length perm_ctr_Tsss;
  10.371 +    val perm_mss = map (map length) perm_ctr_Tsss;
  10.372 +
  10.373 +    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
  10.374 +      of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
  10.375 +    val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
  10.376 +      mk_coiter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of dtor_coiters1);
  10.377 +
  10.378 +    val (perm_p_hss, h) = indexedd perm_p_Tss 0;
  10.379 +    val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
  10.380 +    val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
  10.381 +
  10.382 +    val fun_arg_hs =
  10.383 +      flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
  10.384 +
  10.385 +    fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
  10.386 +    fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
  10.387 +
  10.388 +    val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
  10.389 +
  10.390 +    val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
  10.391 +    val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
  10.392 +    val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
  10.393 +
  10.394 +    val f_Tssss = unpermute perm_f_Tssss;
  10.395 +    val fpTs = unpermute perm_fpTs;
  10.396 +    val Cs = unpermute perm_Cs;
  10.397 +
  10.398 +    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
  10.399 +    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
  10.400 +
  10.401 +    val substA = Term.subst_TVars As_rho;
  10.402 +    val substAT = Term.typ_subst_TVars As_rho;
  10.403 +    val substCT = Term.typ_subst_TVars Cs_rho;
  10.404 +
  10.405 +    val perm_Cs' = map substCT perm_Cs;
  10.406 +
  10.407 +    fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
  10.408 +        (if exists_subtype_in Cs T then Indirect_Corec
  10.409 +         else if nullary then Dummy_No_Corec
  10.410 +         else No_Corec) g_i
  10.411 +      | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
  10.412 +
  10.413 +    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
  10.414 +      let val nullary = not (can dest_funT (fastype_of ctr)) in
  10.415 +        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
  10.416 +         calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
  10.417 +      end;
  10.418 +
  10.419 +    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss =
  10.420 +      let
  10.421 +        val ctrs = #ctrs (nth ctr_sugars index);
  10.422 +        val discs = #discs (nth ctr_sugars index);
  10.423 +        val selss = #selss (nth ctr_sugars index);
  10.424 +        val p_ios = map SOME p_is @ [NONE];
  10.425 +        val corec_thmss = co_rec_of (nth coiter_thmsss index);
  10.426 +      in
  10.427 +        map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
  10.428 +      end;
  10.429 +
  10.430 +    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
  10.431 +        p_is q_isss f_isss f_Tsss =
  10.432 +      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
  10.433 +       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
  10.434 +  in
  10.435 +    ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
  10.436 +      co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
  10.437 +      strong_co_induct_of coinduct_thmss), lthy')
  10.438 +  end;
  10.439 +
  10.440 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Fri Aug 30 11:27:23 2013 +0200
    11.3 @@ -0,0 +1,140 @@
    11.4 +(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML
    11.5 +    Author:     Jasmin Blanchette, TU Muenchen
    11.6 +    Copyright   2013
    11.7 +
    11.8 +Compatibility layer with the old datatype package.
    11.9 +*)
   11.10 +
   11.11 +signature BNF_LFP_COMPAT =
   11.12 +sig
   11.13 +  val datatype_compat_cmd : string list -> local_theory -> local_theory
   11.14 +end;
   11.15 +
   11.16 +structure BNF_LFP_Compat : BNF_LFP_COMPAT =
   11.17 +struct
   11.18 +
   11.19 +open BNF_Util
   11.20 +open BNF_FP_Util
   11.21 +open BNF_FP_Def_Sugar
   11.22 +open BNF_FP_N2M_Sugar
   11.23 +
   11.24 +fun dtyp_of_typ _ (TFree a) = Datatype_Aux.DtTFree a
   11.25 +  | dtyp_of_typ recTs (T as Type (s, Ts)) =
   11.26 +    (case find_index (curry (op =) T) recTs of
   11.27 +      ~1 => Datatype_Aux.DtType (s, map (dtyp_of_typ recTs) Ts)
   11.28 +    | kk => Datatype_Aux.DtRec kk);
   11.29 +
   11.30 +val compatN = "compat_";
   11.31 +
   11.32 +(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
   11.33 +fun datatype_compat_cmd raw_fpT_names lthy =
   11.34 +  let
   11.35 +    val thy = Proof_Context.theory_of lthy;
   11.36 +
   11.37 +    fun not_datatype s = error (quote s ^ " is not a new-style datatype");
   11.38 +    fun not_mutually_recursive ss =
   11.39 +      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
   11.40 +
   11.41 +    val (fpT_names as fpT_name1 :: _) =
   11.42 +      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
   11.43 +
   11.44 +    val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS;
   11.45 +
   11.46 +    val (unsorted_As, _) = lthy |> mk_TFrees (length Ss);
   11.47 +    val As = map2 resort_tfree Ss unsorted_As;
   11.48 +
   11.49 +    fun lfp_sugar_of s =
   11.50 +      (case fp_sugar_of lthy s of
   11.51 +        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
   11.52 +      | _ => not_datatype s);
   11.53 +
   11.54 +    val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
   11.55 +    val fpT_names' = map (fst o dest_Type) fpTs0;
   11.56 +
   11.57 +    val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
   11.58 +
   11.59 +    val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
   11.60 +
   11.61 +    fun add_nested_types_of (T as Type (s, _)) seen =
   11.62 +      if member (op =) seen T orelse s = @{type_name fun} then
   11.63 +        seen
   11.64 +      else
   11.65 +        (case try lfp_sugar_of s of
   11.66 +          SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
   11.67 +          let
   11.68 +            val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
   11.69 +            val substT = Term.typ_subst_TVars rho;
   11.70 +
   11.71 +            val mutual_Ts = map substT mutual_Ts0;
   11.72 +
   11.73 +            fun add_interesting_subtypes (U as Type (s, Us)) =
   11.74 +                (case filter (exists_subtype_in mutual_Ts) Us of [] => I
   11.75 +                | Us' => insert (op =) U #> fold add_interesting_subtypes Us')
   11.76 +              | add_interesting_subtypes _ = I;
   11.77 +
   11.78 +            val ctrs = maps #ctrs ctr_sugars;
   11.79 +            val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =);
   11.80 +            val subTs = fold add_interesting_subtypes ctr_Ts [];
   11.81 +          in
   11.82 +            fold add_nested_types_of subTs (seen @ mutual_Ts)
   11.83 +          end
   11.84 +        | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
   11.85 +            " not associated with new-style datatype (cf. \"datatype_new\")"));
   11.86 +
   11.87 +    val Ts = add_nested_types_of fpT1 [];
   11.88 +    val bs = map (Binding.name o prefix compatN o base_name_of_typ) Ts;
   11.89 +    val nn_fp = length fpTs;
   11.90 +    val nn = length Ts;
   11.91 +    val get_indices = K [];
   11.92 +    val fp_sugars0 =
   11.93 +      if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
   11.94 +    val callssss = pad_and_indexify_calls fp_sugars0 nn [];
   11.95 +    val has_nested = nn > nn_fp;
   11.96 +
   11.97 +    val ((_, fp_sugars), lthy) =
   11.98 +      mutualize_fp_sugars false has_nested Least_FP bs Ts get_indices callssss fp_sugars0 lthy;
   11.99 +
  11.100 +    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
  11.101 +      fp_sugars;
  11.102 +    val inducts = conj_dests nn induct;
  11.103 +
  11.104 +    val frozen_Ts = map Type.legacy_freeze_type Ts;
  11.105 +    val mk_dtyp = dtyp_of_typ frozen_Ts;
  11.106 +
  11.107 +    fun mk_ctr_descr (Const (s, T)) =
  11.108 +      (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));
  11.109 +    fun mk_typ_descr index (Type (T_name, Ts)) {ctrs, ...} =
  11.110 +      (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));
  11.111 +
  11.112 +    val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;
  11.113 +    val recs = map (fst o dest_Const o co_rec_of) co_iterss;
  11.114 +    val rec_thms = flat (map co_rec_of iter_thmsss);
  11.115 +
  11.116 +    fun mk_info {T = Type (T_name0, _), index, ...} =
  11.117 +      let
  11.118 +        val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
  11.119 +          split, split_asm, ...} = nth ctr_sugars index;
  11.120 +      in
  11.121 +        (T_name0,
  11.122 +         {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
  11.123 +         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
  11.124 +         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
  11.125 +         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
  11.126 +         split_asm = split_asm})
  11.127 +      end;
  11.128 +
  11.129 +    val infos = map mk_info (take nn_fp fp_sugars);
  11.130 +
  11.131 +    val register_and_interpret =
  11.132 +      Datatype_Data.register infos
  11.133 +      #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)
  11.134 +  in
  11.135 +    Local_Theory.raw_theory register_and_interpret lthy
  11.136 +  end;
  11.137 +
  11.138 +val _ =
  11.139 +  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
  11.140 +    "register a new-style datatype as an old-style datatype"
  11.141 +    (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
  11.142 +
  11.143 +end;