moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
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;