moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_FP_N2M.thy Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,26 @@
+(* Title: HOL/BNF/BNF_FP_N2M.thy
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Flattening of nested to mutual (co)recursion.
+*)
+
+header {* Flattening of Nested to Mutual (Co)recursion *}
+
+theory BNF_FP_N2M
+imports "~~/src/HOL/BNF/BNF_FP_Basic"
+begin
+
+lemma eq_le_Grp_id_iff: "(op = \<le> BNF_Util.Grp (Collect R) id) = (All R)"
+ unfolding Grp_def id_apply by blast
+
+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>
+ (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
+ unfolding Grp_def by rule auto
+
+ML_file "Tools/bnf_fp_n2m_tactics.ML"
+ML_file "Tools/bnf_fp_n2m.ML"
+ML_file "Tools/bnf_fp_n2m_sugar.ML"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_FP_Rec_Sugar.thy Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,34 @@
+(* Title: HOL/BNF/BNF_FP_Rec_Sugar.thy
+ Author: Lorenz Panny, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Recursor and corecursor sugar.
+*)
+
+header {* Recursor and Corecursor Sugar *}
+
+theory BNF_FP_Rec_Sugar
+imports BNF_FP_N2M
+keywords
+ "primrec_new" :: thy_decl and
+ "primcorec" :: thy_goal and
+ "sequential"
+begin
+
+lemma if_if_True:
+"(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
+ (if b then x else if b' then x' else f y')"
+by simp
+
+lemma if_if_False:
+"(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
+ (if b then f y else if b' then x' else f y')"
+by simp
+
+ML_file "Tools/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_rec_sugar.ML"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_LFP_Compat.thy Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,18 @@
+(* Title: HOL/BNF/BNF_LFP_Compat.thy
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Compatibility layer with the old datatype package.
+*)
+
+header {* Compatibility Layer with the Old Datatype Package *}
+
+theory BNF_LFP_Compat
+imports BNF_FP_N2M
+keywords
+ "datatype_compat" :: thy_goal
+begin
+
+ML_file "Tools/bnf_lfp_compat.ML"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Misc_Primrec.thy Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,116 @@
+(* Title: HOL/BNF/Examples/Misc_Primrec.thy
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Miscellaneous primitive recursive function definitions.
+*)
+
+header {* Miscellaneous Primitive Recursive Function Definitions *}
+
+theory Misc_Primrec
+imports
+ "~~/src/HOL/BNF/Examples/Misc_Datatype"
+ "../BNF_FP_Rec_Sugar"
+begin
+
+primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
+ "nat_of_simple X1 = 1" |
+ "nat_of_simple X2 = 2" |
+ "nat_of_simple X3 = 2" |
+ "nat_of_simple X4 = 4"
+
+primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where
+ "simple_of_simple' (X1' _) = X1" |
+ "simple_of_simple' (X2' _) = X2" |
+ "simple_of_simple' (X3' _) = X3" |
+ "simple_of_simple' (X4' _) = X4"
+
+primrec_new inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
+ "inc_simple'' k (X1'' n i) = X1'' (n + k) (i + int k)" |
+ "inc_simple'' _ X2'' = X2''"
+
+primrec_new myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
+ "myapp MyNil ys = ys" |
+ "myapp (MyCons x xs) ys = MyCons x (myapp xs ys)"
+
+primrec_new myrev :: "'a mylist \<Rightarrow> 'a mylist" where
+ "myrev MyNil = MyNil" |
+ "myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)"
+
+primrec_new shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
+ "shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" |
+ "shuffle_sp (SP2 a) = SP3 a" |
+ "shuffle_sp (SP3 b) = SP4 b" |
+ "shuffle_sp (SP4 c) = SP5 c" |
+ "shuffle_sp (SP5 d) = SP2 d"
+
+primrec_new
+ hf_size :: "hfset \<Rightarrow> nat"
+where
+ "hf_size (HFset X) = 1 + setsum id (fset (fmap hf_size X))"
+
+primrec_new rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
+ "rename_lam f (Var s) = Var (f s)" |
+ "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
+ "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
+ "rename_lam f (Let SL l) = Let (fmap (map_pair f (rename_lam f)) SL) (rename_lam f l)"
+
+primrec_new
+ sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
+ sum_i2 :: "'a I2 \<Rightarrow> 'a"
+where
+ "sum_i1 (I11 n i) = n + sum_i1 i" |
+ "sum_i1 (I12 n i) = n + sum_i2 i" |
+ "sum_i2 I21 = 0" |
+ "sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
+
+primrec_new forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
+ "forest_of_mylist MyNil = FNil" |
+ "forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
+
+primrec_new mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
+ "mylist_of_forest FNil = MyNil" |
+ "mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)"
+
+definition frev :: "'a forest \<Rightarrow> 'a forest" where
+ "frev = forest_of_mylist o myrev o mylist_of_forest"
+
+primrec_new
+ mirror_tree :: "'a tree \<Rightarrow> 'a tree" and
+ mirror_forest :: "'a forest \<Rightarrow> 'a forest"
+where
+ "mirror_tree TEmpty = TEmpty" |
+ "mirror_tree (TNode x ts) = TNode x (mirror_forest ts)" |
+ "mirror_forest FNil = FNil" |
+ "mirror_forest (FCons t ts) = frev (FCons (mirror_tree t) (mirror_forest ts))"
+
+primrec_new
+ mylist_of_tree' :: "'a tree' \<Rightarrow> 'a mylist" and
+ mylist_of_branch :: "'a branch \<Rightarrow> 'a mylist"
+where
+ "mylist_of_tree' TEmpty' = MyNil" |
+ "mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
+ "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
+
+primrec_new
+ is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
+ is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
+ is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"
+where
+ "is_ground_exp (Term t) \<longleftrightarrow> is_ground_trm t" |
+ "is_ground_exp (Sum t e) \<longleftrightarrow> is_ground_trm t \<and> is_ground_exp e" |
+ "is_ground_trm (Factor f) \<longleftrightarrow> is_ground_factor f" |
+ "is_ground_trm (Prod f t) \<longleftrightarrow> is_ground_factor f \<and> is_ground_trm t" |
+ "is_ground_factor (C _) \<longleftrightarrow> True" |
+ "is_ground_factor (V _) \<longleftrightarrow> False" |
+ "is_ground_factor (Paren e) \<longleftrightarrow> is_ground_exp e"
+
+primrec_new map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+ "map_ftreeA f (FTLeaf x) = FTLeaf (f x)" |
+ "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f o g)"
+
+primrec_new map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
+ "map_ftreeB f (FTLeaf x) = FTLeaf (f x)" |
+ "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f o g o the_inv f)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,384 @@
+(* Title: HOL/BNF/Tools/bnf_fp_n2m.ML
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2013
+
+Flattening of nested to mutual (co)recursion.
+*)
+
+signature BNF_FP_N2M =
+sig
+ val construct_mutualized_fp: BNF_FP_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
+ binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+ local_theory -> BNF_FP_Util.fp_result * local_theory
+end;
+
+structure BNF_FP_N2M : BNF_FP_N2M =
+struct
+
+open BNF_Def
+open BNF_Util
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+open BNF_Tactics
+open BNF_FP_N2M_Tactics
+
+fun force_typ ctxt T =
+ map_types Type_Infer.paramify_vars
+ #> Type.constraint T
+ #> Syntax.check_term ctxt
+ #> singleton (Variable.polymorphic ctxt);
+
+fun mk_prod_map f g =
+ let
+ val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
+ val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
+ in
+ Const (@{const_name map_pair},
+ fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
+ end;
+
+fun mk_sum_map f g =
+ let
+ val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
+ val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
+ in
+ Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
+ end;
+
+fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
+ let
+ fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
+
+ val n = length bnfs;
+ val deads = fold (union (op =)) Dss resDs;
+ val As = subtract (op =) deads (map TFree resBs);
+ val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
+ val m = length As;
+ val live = m + n;
+ val ((Xs, Bs), names_lthy) = names_lthy
+ |> mk_TFrees n
+ ||>> mk_TFrees m;
+ val allAs = As @ Xs;
+ val phiTs = map2 mk_pred2T As Bs;
+ val theta = As ~~ Bs;
+ val fpTs' = map (Term.typ_subst_atomic theta) fpTs;
+ val pre_phiTs = map2 mk_pred2T fpTs fpTs';
+
+ fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
+ fun co_swap pair = fp_case fp I swap pair;
+ val dest_co_algT = co_swap o dest_funT;
+ val co_alg_argT = fp_case fp range_type domain_type;
+ val co_alg_funT = fp_case fp domain_type range_type;
+ val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
+ val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
+ val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
+ val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
+ val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
+
+ val ((ctors, dtors), (xtor's, xtors)) =
+ let
+ val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
+ val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
+ in
+ ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
+ end;
+
+ val xTs = map (domain_type o fastype_of) xtors;
+ val yTs = map (domain_type o fastype_of) xtor's;
+
+ val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
+ |> mk_Frees' "R" phiTs
+ ||>> mk_Frees "S" pre_phiTs
+ ||>> mk_Frees "x" xTs
+ ||>> mk_Frees "y" yTs;
+
+ val fp_bnfs = steal #bnfs;
+ val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
+ val pre_bnfss = map #pre_bnfs fp_sugars;
+ val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
+ val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
+ val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
+
+ fun abstract t =
+ let val Ts = Term.add_frees t [];
+ in fold_rev Term.absfree (filter (member op = Ts) phis') t end;
+
+ val rels =
+ let
+ fun find_rel T As Bs = fp_nesty_bnfss
+ |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
+ |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
+ |> Option.map (fn bnf =>
+ let val live = live_of_bnf bnf;
+ in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
+ |> the_default (HOLogic.eq_const T, 0);
+
+ fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
+ let
+ val (rel, live) = find_rel T Ts Us;
+ val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
+ val rels = map2 mk_rel Ts' Us';
+ in
+ Term.list_comb (rel, rels)
+ end
+ | mk_rel (T as TFree _) _ = nth phis (find_index (curry op = T) As)
+ | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
+ in
+ map2 (abstract oo mk_rel) fpTs fpTs'
+ end;
+
+ val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
+
+ val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
+ val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
+ |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
+
+ val rel_defs = map rel_def_of_bnf bnfs;
+ val rel_monos = map rel_mono_of_bnf bnfs;
+
+ val rel_xtor_co_induct_thm =
+ mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's
+ (mk_rel_xtor_co_induct_tactic fp rel_xtor_co_inducts rel_defs rel_monos) lthy;
+
+ val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
+ val map_id0s = no_refl (map map_id0_of_bnf bnfs);
+
+ val xtor_co_induct_thm =
+ (case fp of
+ Least_FP =>
+ let
+ val (Ps, names_lthy) = names_lthy
+ |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
+ fun mk_Grp_id P =
+ let val T = domain_type (fastype_of P);
+ in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
+ val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
+ in
+ cterm_instantiate_pos cts rel_xtor_co_induct_thm
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
+ |> funpow n (fn thm => thm RS spec)
+ |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
+ |> unfold_thms lthy @{thms Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)}
+ |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
+ atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
+ |> unfold_thms lthy (maps set_defs_of_bnf bnfs)
+ end
+ | Greatest_FP =>
+ let
+ val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
+ in
+ cterm_instantiate_pos cts rel_xtor_co_induct_thm
+ |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
+ |> funpow (2 * n) (fn thm => thm RS spec)
+ |> Conv.fconv_rule Object_Logic.atomize
+ |> funpow n (fn thm => thm RS mp)
+ end);
+
+ val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
+ val fold_pre_deads_only_Ts = map2 (fn Ds => mk_T_of_bnf Ds (replicate live dummyT)) Dss bnfs;
+ val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
+ val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
+
+ val fold_strTs = map2 mk_co_algT fold_preTs Xs;
+ val rec_strTs = map2 mk_co_algT rec_preTs Xs;
+ val resTs = map2 mk_co_algT fpTs Xs;
+
+ val (((fold_strs, fold_strs'), (rec_strs, rec_strs')), names_lthy) = names_lthy
+ |> mk_Frees' "s" fold_strTs
+ ||>> mk_Frees' "s" rec_strTs;
+
+ val co_iters = steal #xtor_co_iterss;
+ val ns = map (length o #pre_bnfs) fp_sugars;
+ fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
+ | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
+ | substT _ T = T;
+ fun force_iter is_rec i TU TU_rec raw_iters =
+ let
+ val approx_fold = un_fold_of raw_iters
+ |> force_typ names_lthy
+ (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
+ val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
+ val js = find_indices Type.could_unify
+ TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
+ val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
+ val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
+ in
+ force_typ names_lthy (Tpats ---> TU) iter
+ end;
+
+ fun mk_iter b_opt is_rec iters lthy TU =
+ let
+ val x = co_alg_argT TU;
+ val i = find_index (fn T => x = T) Xs;
+ val TUiter =
+ (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
+ NONE => nth co_iters i
+ |> force_iter is_rec i
+ (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
+ (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+ | SOME f => f);
+ val TUs = binder_fun_types (fastype_of TUiter);
+ val iter_preTs = if is_rec then rec_preTs else fold_preTs;
+ val iter_strs = if is_rec then rec_strs else fold_strs;
+ fun mk_s TU' =
+ let
+ val i = find_index (fn T => co_alg_argT TU' = T) Xs;
+ val sF = co_alg_funT TU';
+ val F = nth iter_preTs i;
+ val s = nth iter_strs i;
+ in
+ (if sF = F then s
+ else
+ let
+ val smapT = replicate live dummyT ---> mk_co_algT sF F;
+ fun hidden_to_unit t =
+ Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
+ val smap = map_of_bnf (nth bnfs i)
+ |> force_typ names_lthy smapT
+ |> hidden_to_unit;
+ val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
+ fun mk_smap_arg TU =
+ (if domain_type TU = range_type TU then
+ HOLogic.id_const (domain_type TU)
+ else if is_rec then
+ let
+ val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
+ val T = mk_co_algT TY U;
+ in
+ (case try (force_typ lthy T o build_map lthy co_proj1_const o dest_funT) T of
+ SOME f => mk_co_product f
+ (fst (fst (mk_iter NONE is_rec iters lthy (mk_co_algT TY X))))
+ | NONE => mk_map_co_product
+ (build_map lthy co_proj1_const
+ (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
+ (HOLogic.id_const X))
+ end
+ else
+ fst (fst (mk_iter NONE is_rec iters lthy TU)))
+ val smap_args = map mk_smap_arg smap_argTs;
+ in
+ HOLogic.mk_comp (co_swap (s, Term.list_comb (smap, smap_args)))
+ end)
+ end;
+ val t = Term.list_comb (TUiter, map mk_s TUs);
+ in
+ (case b_opt of
+ NONE => ((t, Drule.dummy_thm), lthy)
+ | SOME b => Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []),
+ fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd)
+ end;
+
+ fun mk_iters is_rec name lthy =
+ fold2 (fn TU => fn b => fn ((iters, defs), lthy) =>
+ mk_iter (SOME b) is_rec iters lthy TU |>> (fn (f, d) => (f :: iters, d :: defs)))
+ resTs (map (Binding.suffix_name ("_" ^ name)) bs) (([], []), lthy)
+ |>> apfst rev o apsnd rev;
+ val foldN = fp_case fp ctor_foldN dtor_unfoldN;
+ val recN = fp_case fp ctor_recN dtor_corecN;
+ val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, lthy_old)) =
+ lthy
+ |> mk_iters false foldN
+ ||>> mk_iters true recN
+ ||> `(Local_Theory.restore);
+
+ val phi = Proof_Context.export_morphism lthy_old lthy;
+
+ val un_folds = map (Morphism.term phi) raw_un_folds;
+ val co_recs = map (Morphism.term phi) raw_co_recs;
+
+ val (xtor_un_fold_thms, xtor_co_rec_thms) =
+ let
+ val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
+ val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
+ val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
+ val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
+ val pre_fold_maps =
+ map2 (fn Ds => fn bnf =>
+ Term.list_comb (uncurry (mk_map_of_bnf Ds) fold_mapTs bnf,
+ map HOLogic.id_const As @ folds))
+ Dss bnfs;
+ val pre_rec_maps =
+ map2 (fn Ds => fn bnf =>
+ Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
+ map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
+ Dss bnfs;
+
+ fun mk_goals f xtor s smap =
+ ((f, xtor), (s, smap))
+ |> pairself (HOLogic.mk_comp o co_swap)
+ |> HOLogic.mk_eq;
+
+ val fold_goals = map4 mk_goals folds xtors fold_strs pre_fold_maps
+ val rec_goals = map4 mk_goals recs xtors rec_strs pre_rec_maps;
+
+ fun mk_thms ss goals tac =
+ Library.foldr1 HOLogic.mk_conj goals
+ |> HOLogic.mk_Trueprop
+ |> fold_rev Logic.all ss
+ |> (fn goal => Goal.prove_sorry lthy [] [] goal tac)
+ |> Thm.close_derivation
+ |> Morphism.thm phi
+ |> split_conj_thm
+ |> map (fn thm => thm RS @{thm comp_eq_dest});
+
+ val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
+ val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
+
+ val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
+ val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
+
+ val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
+ val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
+ val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
+
+ val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
+ val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
+ val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
+ val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
+ @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
+ val rec_thms = fold_thms @ fp_case fp
+ @{thms fst_convol map_pair_o_convol convol_o}
+ @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
+ val map_thms = no_refl (maps (fn bnf =>
+ [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
+
+ fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt
+ (flat [thms, defs, pre_map_defs, fp_pre_map_defs, xtor_thms, o_map_thms, map_thms]) THEN
+ CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
+
+ val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
+ val rec_tac = mk_tac raw_co_rec_defs fp_rec_o_maps fp_xtor_co_recs rec_thms;
+ in
+ (mk_thms fold_strs fold_goals fold_tac, mk_thms rec_strs rec_goals rec_tac)
+ end;
+
+ (* These results are half broken. This is deliberate. We care only about those fields that are
+ used by "primrec_new", "primcorec", and "datatype_compat". *)
+ val fp_res =
+ ({Ts = fpTs,
+ bnfs = steal #bnfs,
+ dtors = dtors,
+ ctors = ctors,
+ xtor_co_iterss = transpose [un_folds, co_recs],
+ xtor_co_induct = xtor_co_induct_thm,
+ dtor_ctors = steal #dtor_ctors (*too general types*),
+ ctor_dtors = steal #ctor_dtors (*too general types*),
+ ctor_injects = steal #ctor_injects (*too general types*),
+ dtor_injects = steal #dtor_injects (*too general types*),
+ xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
+ xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
+ xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
+ xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
+ xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
+ rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
+ |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
+(**
+ val _ = fp_res |> @{make_string} |> tracing
+**)
+ in
+ (fp_res, lthy)
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,261 @@
+(* Title: HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Suggared flattening of nested to mutual (co)recursion.
+*)
+
+signature BNF_FP_N2M_SUGAR =
+sig
+ val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
+ (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
+ local_theory -> (bool * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
+ val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int ->
+ (term * term list list) list list -> term list list list list
+ val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
+ (term -> int list) -> ((term * term list list) list) list -> local_theory ->
+ (bool * typ list * int list * BNF_FP_Def_Sugar.fp_sugar list) * local_theory
+end;
+
+structure BNF_FP_N2M_Sugar : BNF_FP_N2M_SUGAR =
+struct
+
+open BNF_Util
+open BNF_Def
+open BNF_Ctr_Sugar
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+open BNF_FP_N2M
+
+val n2mN = "n2m_"
+
+(* TODO: test with sort constraints on As *)
+(* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
+ as deads? *)
+fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0
+ no_defs_lthy0 =
+ (* TODO: Also check whether there's any lost recursion? *)
+ if mutualize orelse has_duplicates (op =) fpTs then
+ let
+ val thy = Proof_Context.theory_of no_defs_lthy0;
+
+ val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
+
+ fun heterogeneous_call t = error ("Heterogeneous recursive call: " ^ qsotm t);
+ fun incompatible_calls t1 t2 =
+ error ("Incompatible recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
+
+ val b_names = map Binding.name_of bs;
+ val fp_b_names = map base_name_of_typ fpTs;
+
+ val nn = length fpTs;
+
+ fun target_ctr_sugar_of_fp_sugar fpT {T, index, ctr_sugars, ...} =
+ let
+ val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
+ val phi = Morphism.term_morphism (Term.subst_TVars rho);
+ in
+ morph_ctr_sugar phi (nth ctr_sugars index)
+ end;
+
+ val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
+ val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
+
+ val ctrss = map #ctrs ctr_sugars0;
+ val ctr_Tss = map (map fastype_of) ctrss;
+
+ val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
+ val As = map TFree As';
+
+ val ((Cs, Xs), no_defs_lthy) =
+ no_defs_lthy0
+ |> fold Variable.declare_typ As
+ |> mk_TFrees nn
+ ||>> variant_tfrees fp_b_names;
+
+ (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to
+ 'list = unit + 'a list
+ instead of
+ 'list = unit + 'list
+ resulting in a simpler (co)induction rule and (co)recursor. *)
+ fun freeze_fp_default (T as Type (s, Ts)) =
+ (case find_index (curry (op =) T) fpTs of
+ ~1 => Type (s, map freeze_fp_default Ts)
+ | kk => nth Xs kk)
+ | freeze_fp_default T = T;
+
+ fun get_indices_checked call =
+ (case get_indices call of
+ _ :: _ :: _ => heterogeneous_call call
+ | kks => kks);
+
+ fun freeze_fp calls (T as Type (s, Ts)) =
+ (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
+ [] =>
+ (case union (op = o pairself fst)
+ (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
+ [] => T |> not lose_co_rec ? freeze_fp_default
+ | [(kk, _)] => nth Xs kk
+ | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
+ | callss =>
+ Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
+ (transpose callss)) Ts))
+ | freeze_fp _ T = T;
+
+ val ctr_Tsss = map (map binder_types) ctr_Tss;
+ val ctrXs_Tsss = map2 (map2 (map2 freeze_fp)) callssss ctr_Tsss;
+ val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
+ val Ts = map (body_type o hd) ctr_Tss;
+
+ val ns = map length ctr_Tsss;
+ val kss = map (fn n => 1 upto n) ns;
+ val mss = map (map length) ctr_Tsss;
+
+ val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
+
+ val base_fp_names = Name.variant_list [] fp_b_names;
+ val fp_bs = map2 (fn b_name => fn base_fp_name =>
+ Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
+ b_names base_fp_names;
+
+ val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
+ dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
+ fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
+
+ val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
+ val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+
+ val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
+ mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
+
+ fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
+
+ val ((co_iterss, co_iter_defss), lthy) =
+ fold_map2 (fn b =>
+ (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
+ else define_coiters [unfoldN, corecN] (the coiters_args_types))
+ (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
+ |>> split_list;
+
+ val rho = tvar_subst thy Ts fpTs;
+ val ctr_sugar_phi =
+ Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
+ (Morphism.term_morphism (Term.subst_TVars rho));
+ val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
+
+ val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
+
+ val (co_inducts, un_fold_thmss, co_rec_thmss) =
+ if fp = Least_FP then
+ derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
+ xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
+ co_iterss co_iter_defss lthy
+ |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
+ ([induct], fold_thmss, rec_thmss))
+ else
+ derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
+ dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
+ ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
+ |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
+ (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
+
+ val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
+
+ fun mk_target_fp_sugar (kk, T) =
+ {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
+ nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
+ ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
+ co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
+ |> morph_fp_sugar phi;
+ in
+ ((true, map_index mk_target_fp_sugar fpTs), lthy)
+ end
+ else
+ (* TODO: reorder hypotheses and predicates in (co)induction rules? *)
+ ((false, fp_sugars0), no_defs_lthy0);
+
+fun indexify_callsss fp_sugar callsss =
+ let
+ val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
+ fun do_ctr ctr =
+ (case AList.lookup Term.aconv_untyped callsss ctr of
+ NONE => replicate (num_binder_types (fastype_of ctr)) []
+ | SOME callss => map (map Envir.beta_eta_contract) callss);
+ in
+ map do_ctr ctrs
+ end;
+
+fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list [];
+
+fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
+ let
+ val qsoty = quote o Syntax.string_of_typ lthy;
+ val qsotys = space_implode " or " o map qsoty;
+
+ fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
+ fun not_co_datatype (T as Type (s, _)) =
+ if fp = Least_FP andalso
+ is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
+ error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
+ else
+ not_co_datatype0 T
+ | not_co_datatype T = not_co_datatype0 T;
+ fun not_mutually_nested_rec Ts1 Ts2 =
+ error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^
+ qsotys Ts2);
+
+ val perm_actual_Ts as Type (_, ty_args0) :: _ =
+ sort (int_ord o pairself Term.size_of_typ) actual_Ts;
+
+ fun check_enrich_with_mutuals _ [] = []
+ | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) =
+ (case fp_sugar_of lthy T_name of
+ SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) =>
+ if fp = fp' then
+ let
+ val mutual_Ts = map (fn Type (s, _) => Type (s, ty_args)) Ts';
+ val _ =
+ seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse
+ not_mutually_nested_rec mutual_Ts seen;
+ val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts;
+ in
+ mutual_Ts @ check_enrich_with_mutuals (seen @ T :: seen') Ts'
+ end
+ else
+ not_co_datatype T
+ | NONE => not_co_datatype T)
+ | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
+
+ val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
+
+ val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
+ val Ts = actual_Ts @ missing_Ts;
+
+ val nn = length Ts;
+ val kks = 0 upto nn - 1;
+
+ val common_name = mk_common_name (map Binding.name_of actual_bs);
+ val bs = pad_list (Binding.name common_name) nn actual_bs;
+
+ fun permute xs = permute_like (op =) Ts perm_Ts xs;
+ fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
+
+ val perm_bs = permute bs;
+ val perm_kks = permute kks;
+ val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
+
+ val mutualize = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts;
+ val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0;
+
+ val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
+
+ val ((nontriv, perm_fp_sugars), lthy) =
+ mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss
+ perm_fp_sugars0 lthy;
+
+ val fp_sugars = unpermute perm_fp_sugars;
+ in
+ ((nontriv, missing_Ts, perm_kks, fp_sugars), lthy)
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,41 @@
+(* Title: HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2013
+
+Tactics for mutualization of nested (co)datatypes.
+*)
+
+signature BNF_FP_N2M_TACTICS =
+sig
+ val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
+end;
+
+structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
+struct
+
+open BNF_Util
+open BNF_FP_Util
+
+fun mk_rel_xtor_co_induct_tactic fp co_inducts rel_defs rel_monos
+ {context = ctxt, prems = raw_C_IHs} =
+ let
+ val unfolds = map (fn def => unfold_thms ctxt (id_apply :: no_reflexive [def])) rel_defs;
+ val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
+ val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
+ val C_IH_monos =
+ map3 (fn C_IH => fn mono => fn unfold =>
+ (mono RSN (2, @{thm rev_predicate2D}), C_IH)
+ |> fp = Greatest_FP ? swap
+ |> op RS
+ |> unfold)
+ folded_C_IHs rel_monos unfolds;
+ in
+ HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI})
+ (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
+ REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
+ rtac @{thm order_refl}, atac, resolve_tac co_inducts])))
+ co_inducts)
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,744 @@
+(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar.ML
+ Author: Lorenz Panny, TU Muenchen
+ Copyright 2013
+
+Recursor and corecursor sugar.
+*)
+
+signature BNF_FP_REC_SUGAR =
+sig
+ val add_primrec_cmd: (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> local_theory -> local_theory;
+end;
+
+(* TODO:
+ - error handling for indirect calls
+*)
+
+structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
+struct
+
+open BNF_Util
+open BNF_FP_Util
+open BNF_FP_Rec_Sugar_Util
+open BNF_FP_Rec_Sugar_Tactics
+
+exception Primrec_Error of string * term list;
+
+fun primrec_error str = raise Primrec_Error (str, []);
+fun primrec_error_eqn str eqn = raise Primrec_Error (str, [eqn]);
+fun primrec_error_eqns str eqns = raise Primrec_Error (str, eqns);
+
+fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
+
+val simp_attrs = @{attributes [simp]};
+
+
+type eqn_data = {
+ fun_name: string,
+ rec_type: typ,
+ ctr: term,
+ ctr_args: term list,
+ left_args: term list,
+ right_args: term list,
+ res_type: typ,
+ rhs_term: term,
+ user_eqn: term
+};
+
+fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
+ |> fold (K (fn u => Abs ("", dummyT, u))) (0 upto n);
+
+fun dissect_eqn lthy fun_names eqn' =
+ let
+ val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
+ strip_qnt_body @{const_name all} eqn') |> HOLogic.dest_Trueprop
+ handle TERM _ =>
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
+ val (lhs, rhs) = HOLogic.dest_eq eqn
+ handle TERM _ =>
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
+ val (fun_name, args) = strip_comb lhs
+ |>> (fn x => if is_Free x then fst (dest_Free x)
+ else primrec_error_eqn "malformed function equation (does not start with free)" eqn);
+ val (left_args, rest) = take_prefix is_Free args;
+ val (nonfrees, right_args) = take_suffix is_Free rest;
+ val _ = length nonfrees = 1 orelse if length nonfrees = 0 then
+ primrec_error_eqn "constructor pattern missing in left-hand side" eqn else
+ primrec_error_eqn "more than one non-variable argument in left-hand side" eqn;
+ val _ = member (op =) fun_names fun_name orelse
+ primrec_error_eqn "malformed function equation (does not start with function name)" eqn
+
+ val (ctr, ctr_args) = strip_comb (the_single nonfrees);
+ val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse
+ primrec_error_eqn "partially applied constructor in pattern" eqn;
+ val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse
+ primrec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^
+ "\" in left-hand side") eqn end;
+ val _ = forall is_Free ctr_args orelse
+ primrec_error_eqn "non-primitive pattern in left-hand side" eqn;
+ val _ =
+ let val b = fold_aterms (fn x as Free (v, _) =>
+ if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso
+ not (member (op =) fun_names v) andalso
+ not (Variable.is_fixed lthy v)) then cons x else I | _ => I) rhs []
+ in
+ null b orelse
+ primrec_error_eqn ("extra variable(s) in right-hand side: " ^
+ commas (map (Syntax.string_of_term lthy) b)) eqn
+ end;
+ in
+ {fun_name = fun_name,
+ rec_type = body_type (type_of ctr),
+ ctr = ctr,
+ ctr_args = ctr_args,
+ left_args = left_args,
+ right_args = right_args,
+ res_type = map fastype_of (left_args @ right_args) ---> fastype_of rhs,
+ rhs_term = rhs,
+ user_eqn = eqn'}
+ end;
+
+(* substitutes (f ls x rs) by (y ls rs) for all f: get_idx f \<ge> 0, (x,y) \<in> substs *)
+fun subst_direct_calls get_idx get_ctr_pos substs =
+ let
+ fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
+ | subst t =
+ let
+ val (f, args) = strip_comb t;
+ val idx = get_idx f;
+ val ctr_pos = if idx >= 0 then get_ctr_pos idx else ~1;
+ in
+ if idx < 0 then
+ list_comb (f, map subst args)
+ else if ctr_pos >= length args then
+ primrec_error_eqn "too few arguments in recursive call" t
+ else
+ let
+ val (key, repl) = the (find_first (equal (nth args ctr_pos) o fst) substs)
+ handle Option.Option => primrec_error_eqn
+ "recursive call not directly applied to constructor argument" t;
+ in
+ remove (op =) key args |> map subst |> curry list_comb repl
+ end
+ end
+ in subst end;
+
+(* FIXME get rid of funs_data or get_indices *)
+fun rewrite_map_arg funs_data get_indices y rec_type res_type =
+ let
+ val pT = HOLogic.mk_prodT (rec_type, res_type);
+ val fstx = fst_const pT;
+ val sndx = snd_const pT;
+
+ val SOME ({fun_name, left_args, ...} :: _) =
+ find_first (equal rec_type o #rec_type o hd) funs_data;
+ val ctr_pos = length left_args;
+
+ fun subst _ d (t as Bound d') = t |> d = d' ? curry (op $) fstx
+ | subst l d (Abs (v, T, b)) = Abs (v, if d < 0 then pT else T, subst l (d + 1) b)
+ | subst l d t =
+ let val (u, vs) = strip_comb t in
+ if try (fst o dest_Free) u = SOME fun_name then
+ if l andalso length vs = ctr_pos then
+ list_comb (sndx |> permute_args ctr_pos, vs)
+ else if length vs <= ctr_pos then
+ primrec_error_eqn "too few arguments in recursive call" t
+ else if nth vs ctr_pos |> member (op =) [y, Bound d] then
+ list_comb (sndx $ nth vs ctr_pos, nth_drop ctr_pos vs |> map (subst false d))
+ else
+ primrec_error_eqn "recursive call not directly applied to constructor argument" t
+ else if try (fst o dest_Const) u = SOME @{const_name comp} then
+ (hd vs |> get_indices |> null orelse
+ primrec_error_eqn "recursive call not directly applied to constructor argument" t;
+ list_comb
+ (u |> map_types (strip_type #>> (fn Ts => Ts
+ |> nth_map (length Ts - 1) (K pT)
+ |> nth_map (length Ts - 2) (strip_type #>> nth_map 0 (K pT) #> (op --->)))
+ #> (op --->)),
+ nth_map 1 (subst l d) vs))
+ else
+ list_comb (u, map (subst false d) vs)
+ end
+ in
+ subst true ~1
+ end;
+
+(* FIXME get rid of funs_data or get_indices *)
+fun subst_indirect_call lthy funs_data get_indices (y, y') =
+ let
+ fun massage massage_map_arg bound_Ts =
+ massage_indirect_rec_call lthy (not o null o get_indices) massage_map_arg bound_Ts y y';
+ fun subst bound_Ts (t as _ $ _) =
+ let
+ val (f', args') = strip_comb t;
+ val fun_arg_idx = find_index (exists_subterm (not o null o get_indices)) args';
+ val arg_idx = find_index (exists_subterm (equal y)) args';
+ val (f, args) = chop (arg_idx + 1) args' |>> curry list_comb f';
+ val _ = fun_arg_idx < 0 orelse arg_idx >= 0 orelse
+ primrec_error_eqn "recursive call not applied to constructor argument" t;
+ in
+ if fun_arg_idx <> arg_idx andalso fun_arg_idx >= 0 then
+ if nth args' arg_idx = y then
+ list_comb (massage (rewrite_map_arg funs_data get_indices y) bound_Ts f, args)
+ else
+ primrec_error_eqn "recursive call not directly applied to constructor argument" f
+ else
+ list_comb (f', map (subst bound_Ts) args')
+ end
+ | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
+ | subst bound_Ts t = t |> t = y ? massage (K I |> K) bound_Ts;
+ in subst [] end;
+
+fun build_rec_arg lthy get_indices funs_data ctr_spec maybe_eqn_data =
+ if is_some maybe_eqn_data then
+ let
+ val eqn_data = the maybe_eqn_data;
+ val t = #rhs_term eqn_data;
+ val ctr_args = #ctr_args eqn_data;
+
+ val calls = #calls ctr_spec;
+ val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2 | _ => 1)) calls 0;
+
+ val no_calls' = tag_list 0 calls
+ |> map_filter (try (apsnd (fn No_Rec n => n | Direct_Rec (n, _) => n)));
+ val direct_calls' = tag_list 0 calls
+ |> map_filter (try (apsnd (fn Direct_Rec (_, n) => n)));
+ val indirect_calls' = tag_list 0 calls
+ |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
+
+ fun make_direct_type T = dummyT; (* FIXME? *)
+
+ val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
+
+ fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
+ let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
+ if is_some maybe_res_type
+ then HOLogic.mk_prodT (T, the maybe_res_type)
+ else make_indirect_type T end))
+ | make_indirect_type T = T;
+
+ val args = replicate n_args ("", dummyT)
+ |> Term.rename_wrt_term t
+ |> map Free
+ |> fold (fn (ctr_arg_idx, arg_idx) =>
+ nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
+ no_calls'
+ |> fold (fn (ctr_arg_idx, arg_idx) =>
+ nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_direct_type)))
+ direct_calls'
+ |> fold (fn (ctr_arg_idx, arg_idx) =>
+ nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_indirect_type)))
+ indirect_calls';
+
+ val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls';
+ val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls';
+
+ val get_idx = (fn Free (v, _) => find_index (equal v o #fun_name o hd) funs_data | _ => ~1);
+
+ val t' = t
+ |> fold (subst_indirect_call lthy funs_data get_indices) indirect_calls
+ |> subst_direct_calls get_idx (length o #left_args o hd o nth funs_data) direct_calls;
+
+ val abstractions = map dest_Free (args @ #left_args eqn_data @ #right_args eqn_data);
+ in
+ t' |> fold_rev absfree abstractions
+ end
+ else Const (@{const_name undefined}, dummyT)
+
+fun build_defs lthy bs funs_data rec_specs get_indices =
+ let
+ val n_funs = length funs_data;
+
+ val ctr_spec_eqn_data_list' =
+ (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data
+ |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
+ ##> (fn x => null x orelse
+ primrec_error_eqns "excess equations in definition" (map #rhs_term x)) #> fst);
+ val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse
+ primrec_error_eqns ("multiple equations for constructor") (map #user_eqn x));
+
+ val ctr_spec_eqn_data_list =
+ ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
+
+ val recs = take n_funs rec_specs |> map #recx;
+ val rec_args = ctr_spec_eqn_data_list
+ |> sort ((op <) o pairself (#offset o fst) |> make_ord)
+ |> map (uncurry (build_rec_arg lthy get_indices funs_data) o apsnd (try the_single));
+ val ctr_poss = map (fn x =>
+ if length (distinct ((op =) o pairself (length o #left_args)) x) <> 1 then
+ primrec_error ("inconstant constructor pattern position for function " ^
+ quote (#fun_name (hd x)))
+ else
+ hd x |> #left_args |> length) funs_data;
+ in
+ (recs, ctr_poss)
+ |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
+ |> Syntax.check_terms lthy
+ |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
+ end;
+
+fun find_rec_calls get_indices eqn_data =
+ let
+ fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg
+ | find (t as _ $ _) ctr_arg =
+ let
+ val (f', args') = strip_comb t;
+ val n = find_index (equal ctr_arg) args';
+ in
+ if n < 0 then
+ find f' ctr_arg @ maps (fn x => find x ctr_arg) args'
+ else
+ let val (f, args) = chop n args' |>> curry list_comb f' in
+ if exists_subterm (not o null o get_indices) f then
+ f :: maps (fn x => find x ctr_arg) args
+ else
+ find f ctr_arg @ maps (fn x => find x ctr_arg) args
+ end
+ end
+ | find _ _ = [];
+ in
+ map (find (#rhs_term eqn_data)) (#ctr_args eqn_data)
+ |> (fn [] => NONE | callss => SOME (#ctr eqn_data, callss))
+ end;
+
+fun add_primrec fixes specs lthy =
+ let
+ val bs = map (fst o fst) fixes;
+ val fun_names = map Binding.name_of bs;
+ val eqns_data = map (snd #> dissect_eqn lthy fun_names) specs;
+ val funs_data = eqns_data
+ |> partition_eq ((op =) o pairself #fun_name)
+ |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
+ |> map (fn (x, y) => the_single y handle List.Empty =>
+ primrec_error ("missing equations for function " ^ quote x));
+
+ fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes
+ |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
+ |> map_filter I;
+
+ val arg_Ts = map (#rec_type o hd) funs_data;
+ val res_Ts = map (#res_type o hd) funs_data;
+ val callssss = funs_data
+ |> map (partition_eq ((op =) o pairself #ctr))
+ |> map (maps (map_filter (find_rec_calls get_indices)));
+
+ val ((nontriv, rec_specs, _, induct_thm, induct_thms), lthy') =
+ rec_specs_of bs arg_Ts res_Ts get_indices callssss lthy;
+
+ val actual_nn = length funs_data;
+
+ val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
+ map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
+ primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
+ " is not a constructor in left-hand side") user_eqn) eqns_data end;
+
+ val defs = build_defs lthy' bs funs_data rec_specs get_indices;
+
+ fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
+ lthy =
+ let
+ val fun_name = #fun_name (hd fun_data);
+ val def_thms = map (snd o snd) def_thms';
+ val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
+ |> fst
+ |> map_filter (try (fn (x, [y]) =>
+ (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
+ |> map (fn (user_eqn, num_extra_args, rec_thm) =>
+ mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
+ |> K |> Goal.prove lthy [] [] user_eqn)
+
+ val notes =
+ [(inductN, if actual_nn > 1 then [induct_thm] else [], []),
+ (simpsN, simp_thms, simp_attrs)]
+ |> filter_out (null o #2)
+ |> map (fn (thmN, thms, attrs) =>
+ ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]));
+ in
+ lthy |> Local_Theory.notes notes
+ end;
+
+ val common_name = mk_common_name fun_names;
+
+ val common_notes =
+ [(inductN, if nontriv andalso actual_nn > 1 then [induct_thm] else [], [])]
+ |> filter_out (null o #2)
+ |> map (fn (thmN, thms, attrs) =>
+ ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
+ in
+ lthy'
+ |> fold_map Local_Theory.define defs
+ |-> (fn def_thms' => fold_map3 (prove def_thms') (take actual_nn rec_specs)
+ (take actual_nn induct_thms) funs_data)
+ |> snd
+ |> Local_Theory.notes common_notes |> snd
+ end;
+
+fun add_primrec_cmd raw_fixes raw_specs lthy =
+ let
+ val _ = let val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) in null d orelse
+ primrec_error ("duplicate function name(s): " ^ commas d) end;
+ val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
+ in
+ add_primrec fixes specs lthy
+ handle ERROR str => primrec_error str
+ end
+ handle Primrec_Error (str, eqns) =>
+ if null eqns
+ then error ("primrec_new error:\n " ^ str)
+ else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^
+ space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns))
+
+
+val _ = Outer_Syntax.local_theory
+ @{command_spec "primrec_new"}
+ "define primitive recursive functions"
+ (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+type co_eqn_data_dtr_disc = {
+ fun_name: string,
+ ctr_no: int,
+ cond: term,
+ user_eqn: term
+};
+type co_eqn_data_dtr_sel = {
+ fun_name: string,
+ ctr_no: int,
+ sel_no: int,
+ fun_args: term list,
+ rhs_term: term,
+ user_eqn: term
+};
+datatype co_eqn_data =
+ Dtr_Disc of co_eqn_data_dtr_disc |
+ Dtr_Sel of co_eqn_data_dtr_sel
+
+fun co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps =
+ let
+ fun find_subterm p = let (* FIXME \<exists>? *)
+ fun f (t as u $ v) =
+ fold_rev (curry merge_options) [if p t then SOME t else NONE, f u, f v] NONE
+ | f t = if p t then SOME t else NONE
+ in f end;
+
+ val fun_name = imp_rhs
+ |> perhaps (try HOLogic.dest_not)
+ |> `(try (fst o dest_Free o head_of o snd o dest_comb))
+ ||> (try (fst o dest_Free o head_of o fst o HOLogic.dest_eq))
+ |> the o merge_options;
+ val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
+ handle Option.Option => primrec_error_eqn "malformed discriminator equation" imp_rhs;
+
+ val discs = #ctr_specs corec_spec |> map #disc;
+ val ctrs = #ctr_specs corec_spec |> map #ctr;
+ val n_ctrs = length ctrs;
+ val not_disc = head_of imp_rhs = @{term Not};
+ val _ = not_disc andalso n_ctrs <> 2 andalso
+ primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" imp_rhs;
+ val disc = find_subterm (member (op =) discs o head_of) imp_rhs;
+ val eq_ctr0 = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd)
+ |> (fn SOME t => let val n = find_index (equal t) ctrs in
+ if n >= 0 then SOME n else NONE end | _ => NONE);
+ val _ = is_some disc orelse is_some eq_ctr0 orelse
+ primrec_error_eqn "no discriminator in equation" imp_rhs;
+ val ctr_no' =
+ if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs;
+ val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
+ val fun_args = if is_none disc
+ then imp_rhs |> perhaps (try HOLogic.dest_not) |> HOLogic.dest_eq |> fst |> strip_comb |> snd
+ else the disc |> the_single o snd o strip_comb
+ |> (fn t => if try (fst o dest_Free o head_of) t = SOME fun_name
+ then snd (strip_comb t) else []);
+
+ val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
+ val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
+ val catch_all = try (fst o dest_Free o the_single) imp_lhs' = SOME Name.uu_;
+ val matched_conds = filter (equal fun_name o fst) matched_conds_ps |> map snd;
+ val imp_lhs = mk_conjs imp_lhs';
+ val cond =
+ if catch_all then
+ if null matched_conds then fold_rev absfree (map dest_Free fun_args) @{const True} else
+ (strip_abs_vars (hd matched_conds),
+ mk_disjs (map strip_abs_body matched_conds) |> HOLogic.mk_not)
+ |-> fold_rev (fn (v, T) => fn u => Abs (v, T, u))
+ else if sequential then
+ HOLogic.mk_conj (HOLogic.mk_not (mk_disjs (map strip_abs_body matched_conds)), imp_lhs)
+ |> fold_rev absfree (map dest_Free fun_args)
+ else
+ imp_lhs |> fold_rev absfree (map dest_Free fun_args);
+ val matched_cond =
+ if sequential then fold_rev absfree (map dest_Free fun_args) imp_lhs else cond;
+
+ val matched_conds_ps' = if catch_all
+ then (fun_name, cond) :: filter (not_equal fun_name o fst) matched_conds_ps
+ else (fun_name, matched_cond) :: matched_conds_ps;
+ in
+ (Dtr_Disc {
+ fun_name = fun_name,
+ ctr_no = ctr_no,
+ cond = cond,
+ user_eqn = eqn'
+ }, matched_conds_ps')
+ end;
+
+fun co_dissect_eqn_sel fun_name_corec_spec_list eqn' eqn =
+ let
+ val (lhs, rhs) = HOLogic.dest_eq eqn
+ handle TERM _ =>
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
+ val sel = head_of lhs;
+ val (fun_name, fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst (fst o dest_Free)
+ handle TERM _ =>
+ primrec_error_eqn "malformed selector argument in left-hand side" eqn;
+ val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
+ handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn;
+ val ((ctr_spec, ctr_no), sel) = #ctr_specs corec_spec
+ |> the o get_index (try (the o find_first (equal sel) o #sels))
+ |>> `(nth (#ctr_specs corec_spec));
+ val sel_no = find_index (equal sel) (#sels ctr_spec);
+ in
+ Dtr_Sel {
+ fun_name = fun_name,
+ ctr_no = ctr_no,
+ sel_no = sel_no,
+ fun_args = fun_args,
+ rhs_term = rhs,
+ user_eqn = eqn'
+ }
+ end;
+
+fun co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps =
+ let
+ val (lhs, rhs) = HOLogic.dest_eq imp_rhs;
+ val fun_name = head_of lhs |> fst o dest_Free;
+ val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name);
+ val (ctr, ctr_args) = strip_comb rhs;
+ val ctr_spec = the (find_first (equal ctr o #ctr) (#ctr_specs corec_spec))
+ handle Option.Option => primrec_error_eqn "not a constructor" ctr;
+ val disc_imp_rhs = betapply (#disc ctr_spec, lhs);
+ val (eqn_data_disc, matched_conds_ps') = co_dissect_eqn_disc
+ sequential fun_name_corec_spec_list eqn' imp_lhs' disc_imp_rhs matched_conds_ps;
+
+ val sel_imp_rhss = (#sels ctr_spec ~~ ctr_args)
+ |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
+
+val _ = warning ("reduced\n " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n \<cdot> " ^
+ Syntax.string_of_term @{context} disc_imp_rhs ^ "\n \<cdot> " ^
+ space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
+
+ val eqns_data_sel =
+ map (co_dissect_eqn_sel fun_name_corec_spec_list @{const True}(*###*)) sel_imp_rhss;
+ in
+ (eqn_data_disc :: eqns_data_sel, matched_conds_ps')
+ end;
+
+fun co_dissect_eqn sequential fun_name_corec_spec_list eqn' matched_conds_ps =
+ let
+ val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
+ strip_qnt_body @{const_name all} eqn')
+ handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
+ val (imp_lhs', imp_rhs) =
+ (map HOLogic.dest_Trueprop (Logic.strip_imp_prems eqn),
+ HOLogic.dest_Trueprop (Logic.strip_imp_concl eqn));
+
+ val head = imp_rhs
+ |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
+ |> head_of;
+
+ val maybe_rhs = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq);
+
+ val fun_names = map fst fun_name_corec_spec_list;
+ val discs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #disc;
+ val sels = maps (#ctr_specs o snd) fun_name_corec_spec_list |> maps #sels;
+ val ctrs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #ctr;
+ in
+ if member (op =) discs head orelse
+ is_some maybe_rhs andalso
+ member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then
+ co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps
+ |>> single
+ else if member (op =) sels head then
+ ([co_dissect_eqn_sel fun_name_corec_spec_list eqn' imp_rhs], matched_conds_ps)
+ else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
+ co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds_ps
+ else
+ primrec_error_eqn "malformed function equation" eqn
+ end;
+
+fun build_corec_args_discs ctr_specs disc_eqns =
+ let
+ val conds = map #cond disc_eqns;
+ val args =
+ if length ctr_specs = 1 then []
+ else if length disc_eqns = length ctr_specs then
+ fst (split_last conds)
+ else if length disc_eqns = length ctr_specs - 1 then
+ let val n = 0 upto length ctr_specs - 1
+ |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) (*###*) in
+ if n = length ctr_specs - 1 then
+ conds
+ else
+ split_last conds
+ ||> (fn t => fold_rev absfree (strip_abs_vars t) (strip_abs_body t |> HOLogic.mk_not))
+ |>> chop n
+ |> (fn ((l, r), x) => l @ (x :: r))
+ end
+ else
+ 0 upto length ctr_specs - 1
+ |> map (fn idx => find_first (equal idx o #ctr_no) disc_eqns
+ |> Option.map #cond
+ |> the_default (Const (@{const_name undefined}, dummyT)))
+ |> fst o split_last;
+ fun finish t =
+ let val n = length (fastype_of t |> binder_types) in
+ if t = Const (@{const_name undefined}, dummyT) then t
+ else if n = 0 then Abs (Name.uu_, @{typ unit}, t)
+ else if n = 1 then t
+ else Const (@{const_name prod_case}, dummyT) $ t
+ end;
+ in
+ map finish args
+ end;
+
+fun build_corec_args_sel sel_eqns ctr_spec =
+ let
+ (* FIXME *)
+ val n_args = fold (curry (op +)) (map (fn Direct_Corec _ => 3 | _ => 1) (#calls ctr_spec)) 0;
+ in
+ replicate n_args (Const (@{const_name undefined}, dummyT))
+ end;
+
+fun co_build_defs lthy sequential bs arg_Tss fun_name_corec_spec_list eqns_data =
+ let
+ val fun_names = map Binding.name_of bs;
+
+(* fun group _ [] = [] (* FIXME \<exists>? *)
+ | group eq (x :: xs) =
+ let val (xs', ys) = List.partition (eq x) xs in (x :: xs') :: group eq ys end;*)
+ val disc_eqnss = map_filter (try (fn Dtr_Disc x => x)) eqns_data
+ |> partition_eq ((op =) o pairself #fun_name)
+ |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
+ |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
+
+ val _ = disc_eqnss |> map (fn x =>
+ let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse
+ primrec_error_eqns "excess discriminator equations in definition"
+ (maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end);
+
+val _ = warning ("disc_eqnss:\n \<cdot> " ^ space_implode "\n \<cdot> " (map @{make_string} disc_eqnss));
+
+ val sel_eqnss = map_filter (try (fn Dtr_Sel x => x)) eqns_data
+ |> partition_eq ((op =) o pairself #fun_name)
+ |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
+ |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
+
+val _ = warning ("sel_eqnss:\n \<cdot> " ^ space_implode "\n \<cdot> " (map @{make_string} sel_eqnss));
+
+ fun splice (xs :: xss) (ys :: yss) = xs @ ys @ splice xss yss (* FIXME \<exists>? *)
+ | splice xss yss = flat xss @ flat yss;
+ val corecs = map (#corec o snd) fun_name_corec_spec_list;
+ val corec_args = (map snd fun_name_corec_spec_list ~~ disc_eqnss ~~ sel_eqnss)
+ |> maps (fn (({ctr_specs, ...}, disc_eqns), sel_eqns) =>
+ splice (build_corec_args_discs ctr_specs disc_eqns |> map single)
+ (map (build_corec_args_sel sel_eqns) ctr_specs));
+
+val _ = warning ("corecursor arguments:\n \<cdot> " ^
+ space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) corec_args));
+
+ fun uneq_pairs_rev xs = xs (* FIXME \<exists>? *)
+ |> these o try (split_last #> (fn (ys, y) => uneq_pairs_rev ys @ map (pair y) ys));
+ val proof_obligations = if sequential then [] else
+ maps (uneq_pairs_rev o map #cond) disc_eqnss
+ |> map (fn (x, y) => ((strip_abs_body x, strip_abs_body y), strip_abs_vars x))
+ |> map (apfst (apsnd HOLogic.mk_not #> pairself HOLogic.mk_Trueprop
+ #> apfst (curry (op $) @{const ==>}) #> (op $)))
+ |> map (fn (t, abs_vars) => fold_rev (fn (v, T) => fn u =>
+ Const (@{const_name all}, (T --> @{typ prop}) --> @{typ prop}) $
+ Abs (v, T, u)) abs_vars t);
+
+ fun currys Ts t = if length Ts <= 1 then t else
+ t $ foldr1 (fn (u, v) => HOLogic.pair_const dummyT dummyT $ u $ v)
+ (length Ts - 1 downto 0 |> map Bound)
+ |> fold_rev (fn T => fn u => Abs ("", T, u)) Ts;
+ in
+ map (list_comb o rpair corec_args) corecs
+ |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
+ |> map2 currys arg_Tss
+ |> Syntax.check_terms lthy
+ |> map2 (fn b => fn t => ((b, NoSyn), ((Binding.map_name Thm.def_name b, []), t))) bs
+ |> rpair proof_obligations
+ end;
+
+fun add_primcorec sequential fixes specs lthy =
+ let
+ val bs = map (fst o fst) fixes;
+ val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
+
+ (* copied from primrec_new *)
+ fun get_indices t = map (fst #>> Binding.name_of #> Free) fixes
+ |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
+ |> map_filter I;
+
+ val callssss = []; (* FIXME *)
+
+ val ((nontriv, corec_specs, _, coinduct_thm, strong_co_induct_thm, coinduct_thmss,
+ strong_coinduct_thmss), lthy') =
+ corec_specs_of bs arg_Ts res_Ts get_indices callssss lthy;
+
+ val fun_names = map Binding.name_of bs;
+
+ val fun_name_corec_spec_list = (fun_names ~~ res_Ts, corec_specs)
+ |> uncurry (finds (fn ((v, T), {corec, ...}) => T = body_type (fastype_of corec))) |> fst
+ |> map (apfst fst #> apsnd the_single); (*###*)
+
+ val (eqns_data, _) =
+ fold_map (co_dissect_eqn sequential fun_name_corec_spec_list) (map snd specs) []
+ |>> flat;
+
+ val (defs, proof_obligations) =
+ co_build_defs lthy' sequential bs (map (binder_types o snd o fst) fixes)
+ fun_name_corec_spec_list eqns_data;
+ in
+ lthy'
+ |> fold_map Local_Theory.define defs |> snd
+ |> Proof.theorem NONE (K I) [map (rpair []) proof_obligations]
+ |> Proof.refine (Method.primitive_text I)
+ |> Seq.hd
+ end
+
+fun add_primcorec_cmd seq (raw_fixes, raw_specs) lthy =
+ let
+ val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
+ in
+ add_primcorec seq fixes specs lthy
+ handle ERROR str => primrec_error str
+ end
+ handle Primrec_Error (str, eqns) =>
+ if null eqns
+ then error ("primcorec error:\n " ^ str)
+ else error ("primcorec error:\n " ^ str ^ "\nin\n " ^
+ space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns))
+
+val _ = Outer_Syntax.local_theory_to_proof
+ @{command_spec "primcorec"}
+ "define primitive corecursive functions"
+ (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
+ uncurry add_primcorec_cmd);
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,66 @@
+(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Tactics for recursor and corecursor sugar.
+*)
+
+signature BNF_FP_REC_SUGAR_TACTICS =
+sig
+ val mk_primcorec_taut_tac: Proof.context -> tactic
+ val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
+ tactic
+ val mk_primcorec_dtr_to_ctr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
+ val mk_primcorec_eq_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
+ thm list -> thm list -> thm list -> tactic
+ val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
+end;
+
+structure BNF_FP_Rec_Sugar_Tactics : BNF_FP_REC_SUGAR_TACTICS =
+struct
+
+open BNF_Util
+open BNF_Tactics
+
+fun mk_primrec_tac ctxt num_extra_args map_id's map_comps fun_defs recx =
+ unfold_thms_tac ctxt fun_defs THEN
+ HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
+ unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_id's) THEN
+ HEADGOAL (rtac refl);
+
+fun mk_primcorec_taut_tac ctxt =
+ HEADGOAL (etac FalseE) ORELSE
+ unfold_thms_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not not_False_eq_True} THEN
+ HEADGOAL (SOLVE o REPEAT o (atac ORELSE' resolve_tac @{thms disjI1 disjI2 conjI TrueI}));
+
+fun mk_primcorec_same_case_tac m =
+ HEADGOAL (if m = 0 then rtac TrueI
+ else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
+
+fun mk_primcorec_different_case_tac ctxt excl =
+ unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
+ HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_taut_tac ctxt));
+
+fun mk_primcorec_cases_tac ctxt k m exclsss =
+ let val n = length exclsss in
+ EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
+ | [excl] => mk_primcorec_different_case_tac ctxt excl)
+ (take k (nth exclsss (k - 1))))
+ end;
+
+fun mk_primcorec_prelude ctxt defs thm =
+ unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt @{thms split};
+
+fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
+ mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
+
+fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_id's map_comps =
+ mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
+ unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
+ maps @ map_comps @ map_id's) THEN HEADGOAL (rtac refl);
+
+fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
+ HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
+ unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,437 @@
+(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
+ Author: Lorenz Panny, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Library for recursor and corecursor sugar.
+*)
+
+signature BNF_FP_REC_SUGAR_UTIL =
+sig
+ datatype rec_call =
+ No_Rec of int |
+ Direct_Rec of int (*before*) * int (*after*) |
+ Indirect_Rec of int
+
+ datatype corec_call =
+ Dummy_No_Corec of int |
+ No_Corec of int |
+ Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
+ Indirect_Corec of int
+
+ type rec_ctr_spec =
+ {ctr: term,
+ offset: int,
+ calls: rec_call list,
+ rec_thm: thm}
+
+ type corec_ctr_spec =
+ {ctr: term,
+ disc: term,
+ sels: term list,
+ pred: int option,
+ calls: corec_call list,
+ corec_thm: thm}
+
+ type rec_spec =
+ {recx: term,
+ nested_map_id's: thm list,
+ nested_map_comps: thm list,
+ ctr_specs: rec_ctr_spec list}
+
+ type corec_spec =
+ {corec: term,
+ ctr_specs: corec_ctr_spec list}
+
+ val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+ typ list -> term -> term -> term -> term
+ val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+ typ list -> typ -> term -> term
+ val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
+ (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
+ val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
+ ((term * term list list) list) list -> local_theory ->
+ (bool * rec_spec list * typ list * thm * thm list) * local_theory
+ val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
+ ((term * term list list) list) list -> local_theory ->
+ (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
+end;
+
+structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
+struct
+
+open BNF_Util
+open BNF_Def
+open BNF_Ctr_Sugar
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+open BNF_FP_N2M_Sugar
+
+datatype rec_call =
+ No_Rec of int |
+ Direct_Rec of int * int |
+ Indirect_Rec of int;
+
+datatype corec_call =
+ Dummy_No_Corec of int |
+ No_Corec of int |
+ Direct_Corec of int * int * int |
+ Indirect_Corec of int;
+
+type rec_ctr_spec =
+ {ctr: term,
+ offset: int,
+ calls: rec_call list,
+ rec_thm: thm};
+
+type corec_ctr_spec =
+ {ctr: term,
+ disc: term,
+ sels: term list,
+ pred: int option,
+ calls: corec_call list,
+ corec_thm: thm};
+
+type rec_spec =
+ {recx: term,
+ nested_map_id's: thm list,
+ nested_map_comps: thm list,
+ ctr_specs: rec_ctr_spec list};
+
+type corec_spec =
+ {corec: term,
+ ctr_specs: corec_ctr_spec list};
+
+val id_def = @{thm id_def};
+
+exception AINT_NO_MAP of term;
+
+fun ill_formed_rec_call ctxt t =
+ error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun ill_formed_corec_call ctxt t =
+ error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun invalid_map ctxt t =
+ error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
+fun unexpected_rec_call ctxt t =
+ error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun unexpected_corec_call ctxt t =
+ error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
+
+fun factor_out_types ctxt massage destU U T =
+ (case try destU U of
+ SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
+ | NONE => invalid_map ctxt);
+
+fun map_flattened_map_args ctxt s map_args fs =
+ let
+ val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
+ val flat_fs' = map_args flat_fs;
+ in
+ permute_like (op aconv) flat_fs fs flat_fs'
+ end;
+
+fun massage_indirect_rec_call ctxt has_call massage_unapplied_direct_call bound_Ts y y' =
+ let
+ val typof = curry fastype_of1 bound_Ts;
+ val build_map_fst = build_map ctxt (fst_const o fst);
+
+ val yT = typof y;
+ val yU = typof y';
+
+ fun y_of_y' () = build_map_fst (yU, yT) $ y';
+ val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
+
+ fun check_and_massage_unapplied_direct_call U T t =
+ if has_call t then
+ factor_out_types ctxt massage_unapplied_direct_call HOLogic.dest_prodT U T t
+ else
+ HOLogic.mk_comp (t, build_map_fst (U, T));
+
+ fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
+ (case try (dest_map ctxt s) t of
+ SOME (map0, fs) =>
+ let
+ val Type (_, ran_Ts) = range_type (typof t);
+ val map' = mk_map (length fs) Us ran_Ts map0;
+ val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
+ in
+ list_comb (map', fs')
+ end
+ | NONE => raise AINT_NO_MAP t)
+ | massage_map _ _ t = raise AINT_NO_MAP t
+ and massage_map_or_map_arg U T t =
+ if T = U then
+ if has_call t then unexpected_rec_call ctxt t else t
+ else
+ massage_map U T t
+ handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+
+ fun massage_call (t as t1 $ t2) =
+ if t2 = y then
+ massage_map yU yT (elim_y t1) $ y'
+ handle AINT_NO_MAP t' => invalid_map ctxt t'
+ else
+ ill_formed_rec_call ctxt t
+ | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
+ in
+ massage_call o Envir.beta_eta_contract
+ end;
+
+fun massage_let_and_if ctxt has_call massage_rec massage_else U T t =
+ (case Term.strip_comb t of
+ (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
+ | (Const (@{const_name If}, _), arg :: args) =>
+ if has_call arg then unexpected_corec_call ctxt arg
+ else list_comb (If_const U $ arg, map (massage_rec U T) args)
+ | _ => massage_else U T t);
+
+fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
+ let
+ val typof = curry fastype_of1 bound_Ts;
+
+ fun massage_call U T =
+ massage_let_and_if ctxt has_call massage_call massage_direct_call U T;
+ in
+ massage_call res_U (typof t) (Envir.beta_eta_contract t)
+ end;
+
+fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
+ let
+ val typof = curry fastype_of1 bound_Ts;
+ val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o fst);
+
+ fun check_and_massage_direct_call U T t =
+ if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
+ else build_map_Inl (U, T) $ t;
+
+ fun check_and_massage_unapplied_direct_call U T t =
+ let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
+ Term.lambda var (check_and_massage_direct_call U T (t $ var))
+ end;
+
+ fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
+ (case try (dest_map ctxt s) t of
+ SOME (map0, fs) =>
+ let
+ val Type (_, dom_Ts) = domain_type (typof t);
+ val map' = mk_map (length fs) dom_Ts Us map0;
+ val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
+ in
+ list_comb (map', fs')
+ end
+ | NONE => raise AINT_NO_MAP t)
+ | massage_map _ _ t = raise AINT_NO_MAP t
+ and massage_map_or_map_arg U T t =
+ if T = U then
+ if has_call t then unexpected_corec_call ctxt t else t
+ else
+ massage_map U T t
+ handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+
+ fun massage_call U T =
+ massage_let_and_if ctxt has_call massage_call
+ (fn U => fn T => fn t =>
+ (case U of
+ Type (s, Us) =>
+ (case try (dest_ctr ctxt s) t of
+ SOME (f, args) =>
+ let val f' = mk_ctr Us f in
+ list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
+ end
+ | NONE =>
+ (case t of
+ t1 $ t2 =>
+ if has_call t2 then
+ check_and_massage_direct_call U T t
+ else
+ massage_map U T t1 $ t2
+ handle AINT_NO_MAP _ => check_and_massage_direct_call U T t
+ | _ => check_and_massage_direct_call U T t))
+ | _ => ill_formed_corec_call ctxt t))
+ U T
+ in
+ massage_call res_U (typof t) (Envir.beta_eta_contract t)
+ end;
+
+fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
+fun indexedd xss = fold_map indexed xss;
+fun indexeddd xsss = fold_map indexedd xsss;
+fun indexedddd xssss = fold_map indexeddd xssss;
+
+fun find_index_eq hs h = find_index (curry (op =) h) hs;
+
+val lose_co_rec = false (*FIXME: try true?*);
+
+fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+
+ val ((nontriv, missing_arg_Ts, perm0_kks,
+ fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
+ co_inducts = [induct_thm], ...} :: _), lthy') =
+ nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy;
+
+ val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+
+ val indices = map #index fp_sugars;
+ val perm_indices = map #index perm_fp_sugars;
+
+ val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+ val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
+ val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
+
+ val nn0 = length arg_Ts;
+ val nn = length perm_fpTs;
+ val kks = 0 upto nn - 1;
+ val perm_ns = map length perm_ctr_Tsss;
+ val perm_mss = map (map length) perm_ctr_Tsss;
+
+ val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
+ perm_fp_sugars;
+ val perm_fun_arg_Tssss = mk_iter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of ctor_iters1);
+
+ fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
+ fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
+
+ val induct_thms = unpermute0 (conj_dests nn induct_thm);
+
+ val fpTs = unpermute perm_fpTs;
+ val Cs = unpermute perm_Cs;
+
+ val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
+ val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
+
+ val substA = Term.subst_TVars As_rho;
+ val substAT = Term.typ_subst_TVars As_rho;
+ val substCT = Term.typ_subst_TVars Cs_rho;
+
+ val perm_Cs' = map substCT perm_Cs;
+
+ fun offset_of_ctr 0 _ = 0
+ | offset_of_ctr n ({ctrs, ...} :: ctr_sugars) =
+ length ctrs + offset_of_ctr (n - 1) ctr_sugars;
+
+ fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
+ | call_of [i, i'] _ = Direct_Rec (i, i');
+
+ fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
+ let
+ val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
+ val fun_arg_hs = flat_rec_arg_args fun_arg_hss;
+ val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss;
+ in
+ {ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss,
+ rec_thm = rec_thm}
+ end;
+
+ fun mk_ctr_specs index ctr_sugars iter_thmsss =
+ let
+ val ctrs = #ctrs (nth ctr_sugars index);
+ val rec_thmss = co_rec_of (nth iter_thmsss index);
+ val k = offset_of_ctr index ctr_sugars;
+ val n = length ctrs;
+ in
+ map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
+ end;
+
+ fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
+ {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
+ nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
+ nested_map_comps = map map_comp_of_bnf nested_bnfs,
+ ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
+ in
+ ((nontriv, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy')
+ end;
+
+fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+
+ val ((nontriv, missing_res_Ts, perm0_kks,
+ fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
+ co_inducts = coinduct_thms, ...} :: _), lthy') =
+ nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
+
+ val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+
+ val indices = map #index fp_sugars;
+ val perm_indices = map #index perm_fp_sugars;
+
+ val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+ val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
+ val perm_fpTs = map (body_type o fastype_of o hd) perm_ctrss;
+
+ val nn0 = length res_Ts;
+ val nn = length perm_fpTs;
+ val kks = 0 upto nn - 1;
+ val perm_ns = map length perm_ctr_Tsss;
+ val perm_mss = map (map length) perm_ctr_Tsss;
+
+ val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
+ of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
+ val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
+ mk_coiter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of dtor_coiters1);
+
+ val (perm_p_hss, h) = indexedd perm_p_Tss 0;
+ val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
+ val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
+
+ val fun_arg_hs =
+ flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
+
+ fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
+ fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
+
+ val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
+
+ val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
+ val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
+ val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
+
+ val f_Tssss = unpermute perm_f_Tssss;
+ val fpTs = unpermute perm_fpTs;
+ val Cs = unpermute perm_Cs;
+
+ val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
+ val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
+
+ val substA = Term.subst_TVars As_rho;
+ val substAT = Term.typ_subst_TVars As_rho;
+ val substCT = Term.typ_subst_TVars Cs_rho;
+
+ val perm_Cs' = map substCT perm_Cs;
+
+ fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
+ (if exists_subtype_in Cs T then Indirect_Corec
+ else if nullary then Dummy_No_Corec
+ else No_Corec) g_i
+ | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
+
+ fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
+ let val nullary = not (can dest_funT (fastype_of ctr)) in
+ {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
+ calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
+ end;
+
+ fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss =
+ let
+ val ctrs = #ctrs (nth ctr_sugars index);
+ val discs = #discs (nth ctr_sugars index);
+ val selss = #selss (nth ctr_sugars index);
+ val p_ios = map SOME p_is @ [NONE];
+ val corec_thmss = co_rec_of (nth coiter_thmsss index);
+ in
+ map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
+ end;
+
+ fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
+ p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
+ ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
+ in
+ ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
+ co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
+ strong_co_induct_of coinduct_thmss), lthy')
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Fri Aug 30 11:27:23 2013 +0200
@@ -0,0 +1,140 @@
+(* Title: HOL/BNF/Tools/bnf_lfp_compat.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+Compatibility layer with the old datatype package.
+*)
+
+signature BNF_LFP_COMPAT =
+sig
+ val datatype_compat_cmd : string list -> local_theory -> local_theory
+end;
+
+structure BNF_LFP_Compat : BNF_LFP_COMPAT =
+struct
+
+open BNF_Util
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+open BNF_FP_N2M_Sugar
+
+fun dtyp_of_typ _ (TFree a) = Datatype_Aux.DtTFree a
+ | dtyp_of_typ recTs (T as Type (s, Ts)) =
+ (case find_index (curry (op =) T) recTs of
+ ~1 => Datatype_Aux.DtType (s, map (dtyp_of_typ recTs) Ts)
+ | kk => Datatype_Aux.DtRec kk);
+
+val compatN = "compat_";
+
+(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
+fun datatype_compat_cmd raw_fpT_names lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+
+ fun not_datatype s = error (quote s ^ " is not a new-style datatype");
+ fun not_mutually_recursive ss =
+ error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
+
+ val (fpT_names as fpT_name1 :: _) =
+ map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
+
+ val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS;
+
+ val (unsorted_As, _) = lthy |> mk_TFrees (length Ss);
+ val As = map2 resort_tfree Ss unsorted_As;
+
+ fun lfp_sugar_of s =
+ (case fp_sugar_of lthy s of
+ SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
+ | _ => not_datatype s);
+
+ val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
+ val fpT_names' = map (fst o dest_Type) fpTs0;
+
+ val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
+
+ val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
+
+ fun add_nested_types_of (T as Type (s, _)) seen =
+ if member (op =) seen T orelse s = @{type_name fun} then
+ seen
+ else
+ (case try lfp_sugar_of s of
+ SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
+ let
+ val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
+ val substT = Term.typ_subst_TVars rho;
+
+ val mutual_Ts = map substT mutual_Ts0;
+
+ fun add_interesting_subtypes (U as Type (s, Us)) =
+ (case filter (exists_subtype_in mutual_Ts) Us of [] => I
+ | Us' => insert (op =) U #> fold add_interesting_subtypes Us')
+ | add_interesting_subtypes _ = I;
+
+ val ctrs = maps #ctrs ctr_sugars;
+ val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =);
+ val subTs = fold add_interesting_subtypes ctr_Ts [];
+ in
+ fold add_nested_types_of subTs (seen @ mutual_Ts)
+ end
+ | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
+ " not associated with new-style datatype (cf. \"datatype_new\")"));
+
+ val Ts = add_nested_types_of fpT1 [];
+ val bs = map (Binding.name o prefix compatN o base_name_of_typ) Ts;
+ val nn_fp = length fpTs;
+ val nn = length Ts;
+ val get_indices = K [];
+ val fp_sugars0 =
+ if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
+ val callssss = pad_and_indexify_calls fp_sugars0 nn [];
+ val has_nested = nn > nn_fp;
+
+ val ((_, fp_sugars), lthy) =
+ mutualize_fp_sugars false has_nested Least_FP bs Ts get_indices callssss fp_sugars0 lthy;
+
+ val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
+ fp_sugars;
+ val inducts = conj_dests nn induct;
+
+ val frozen_Ts = map Type.legacy_freeze_type Ts;
+ val mk_dtyp = dtyp_of_typ frozen_Ts;
+
+ fun mk_ctr_descr (Const (s, T)) =
+ (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));
+ fun mk_typ_descr index (Type (T_name, Ts)) {ctrs, ...} =
+ (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));
+
+ val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;
+ val recs = map (fst o dest_Const o co_rec_of) co_iterss;
+ val rec_thms = flat (map co_rec_of iter_thmsss);
+
+ fun mk_info {T = Type (T_name0, _), index, ...} =
+ let
+ val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
+ split, split_asm, ...} = nth ctr_sugars index;
+ in
+ (T_name0,
+ {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
+ inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
+ rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+ case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+ split_asm = split_asm})
+ end;
+
+ val infos = map mk_info (take nn_fp fp_sugars);
+
+ val register_and_interpret =
+ Datatype_Data.register infos
+ #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)
+ in
+ Local_Theory.raw_theory register_and_interpret lthy
+ end;
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "datatype_compat"}
+ "register a new-style datatype as an old-style datatype"
+ (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
+
+end;