# HG changeset patch # User wenzelm # Date 1377863192 -7200 # Node ID d0e4c8f73541cba65ccf6c3c5c7f850ebf3c7d6a # Parent a1cf42366ceaba327f35f5d9c865bfa71be81357# Parent d8ad101cc6849e04ce2df8ab96b2750aa0f483e9 merged diff -r d8ad101cc684 -r d0e4c8f73541 CONTRIBUTORS --- a/CONTRIBUTORS Fri Aug 30 13:45:57 2013 +0200 +++ b/CONTRIBUTORS Fri Aug 30 13:46:32 2013 +0200 @@ -6,8 +6,12 @@ Contributions to this Isabelle version -------------------------------------- +* Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM + Various improvements to BNF-based (co)datatype package, including a + "primrec_new" command and a compatibility layer. + * Summer 2013: Christian Sternagel, JAIST - Improved support for adhoc overloading of constants, including + Improved support for ad hoc overloading of constants, including documentation and examples. * May 2013: Florian Haftmann, TUM diff -r d8ad101cc684 -r d0e4c8f73541 NEWS --- a/NEWS Fri Aug 30 13:45:57 2013 +0200 +++ b/NEWS Fri Aug 30 13:46:32 2013 +0200 @@ -164,7 +164,7 @@ *** HOL *** -* Improved support for adhoc overloading of constants (see also +* Improved support for ad hoc overloading of constants (see also isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy). * Attibute 'code': 'code' now declares concrete and abstract code @@ -179,6 +179,20 @@ See the isar-ref manual for syntax diagrams, and the HOL theories for examples. +* HOL/BNF: + - Various improvements to BNF-based (co)datatype package, including a + "primrec_new" command, a "datatype_new_compat" command, and + documentation. See "datatypes.pdf" for details. + - Renamed keywords: + data ~> datatype_new + codata ~> codatatype + bnf_def ~> bnf + - Renamed many generated theorems, including + map_comp' ~> map_comp + map_id' ~> map_id + set_map' ~> set_map +IMCOMPATIBILITY. + * Library/Polynomial.thy: - Use lifting for primitive definitions. - Explicit conversions from and to lists of coefficients, used for @@ -189,7 +203,7 @@ poly_eq_iff ~> poly_eq_poly_eq_iff poly_ext ~> poly_eqI expand_poly_eq ~> poly_eq_iff -IMCOMPATIBILTIY. +IMCOMPATIBILITY. * Reification and reflection: - Reification is now directly available in HOL-Main in structure diff -r d8ad101cc684 -r d0e4c8f73541 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Aug 30 13:45:57 2013 +0200 +++ b/etc/isar-keywords.el Fri Aug 30 13:46:32 2013 +0200 @@ -69,6 +69,7 @@ "cpodef" "datatype" "datatype_new" + "datatype_new_compat" "declaration" "declare" "def" @@ -167,7 +168,9 @@ "presume" "pretty_setmargin" "prf" + "primcorec" "primrec" + "primrec_new" "print_abbrevs" "print_antiquotations" "print_ast_translation" @@ -345,6 +348,7 @@ "permissive" "pervasive" "rep_compat" + "sequential" "shows" "structure" "type_class" @@ -503,6 +507,7 @@ "context" "datatype" "datatype_new" + "datatype_new_compat" "declaration" "declare" "default_sort" @@ -550,6 +555,7 @@ "parse_translation" "partial_function" "primrec" + "primrec_new" "print_ast_translation" "print_translation" "quickcheck_generator" @@ -601,6 +607,7 @@ "nominal_inductive2" "nominal_primrec" "pcpodef" + "primcorec" "quotient_definition" "quotient_type" "recdef_tc" diff -r d8ad101cc684 -r d0e4c8f73541 src/HOL/BNF/BNF_FP_Base.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/BNF_FP_Base.thy Fri Aug 30 13:46:32 2013 +0200 @@ -0,0 +1,184 @@ +(* Title: HOL/BNF/BNF_FP_Base.thy + Author: Lorenz Panny, TU Muenchen + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013 + +Shared fixed point operations on bounded natural functors, including +*) + +header {* Shared Fixed Point Operations on Bounded Natural Functors *} + +theory BNF_FP_Base +imports BNF_Comp BNF_Ctr_Sugar +keywords + "defaults" +begin + +lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" +by auto + +lemma eq_sym_Unity_conv: "(x = (() = ())) = x" +by blast + +lemma unit_case_Unity: "(case u of () => f) = f" +by (cases u) (hypsubst, rule unit.cases) + +lemma prod_case_Pair_iden: "(case p of (x, y) \ (x, y)) = p" +by simp + +lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x" +by simp + +lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by clarify + +lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by auto + +lemma pointfree_idE: "f \ g = id \ f (g x) = x" +unfolding o_def fun_eq_iff by simp + +lemma o_bij: + assumes gf: "g \ f = id" and fg: "f \ g = id" + shows "bij f" +unfolding bij_def inj_on_def surj_def proof safe + fix a1 a2 assume "f a1 = f a2" + hence "g ( f a1) = g (f a2)" by simp + thus "a1 = a2" using gf unfolding fun_eq_iff by simp +next + fix b + have "b = f (g b)" + using fg unfolding fun_eq_iff by simp + thus "EX a. b = f a" by blast +qed + +lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp + +lemma sum_case_step: +"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" +"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" +by auto + +lemma one_pointE: "\\x. s = x \ P\ \ P" +by simp + +lemma obj_one_pointE: "\x. s = x \ P \ P" +by blast + +lemma obj_sumE_f: +"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" +by (rule allI) (metis sumE) + +lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" +by (cases s) auto + +lemma sum_case_if: +"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" +by simp + +lemma mem_UN_compreh_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" +by blast + +lemma UN_compreh_eq_eq: +"\{y. \x\A. y = {}} = {}" +"\{y. \x\A. y = {x}} = A" +by blast+ + +lemma Inl_Inr_False: "(Inl x = Inr y) = False" +by simp + +lemma prod_set_simps: +"fsts (x, y) = {x}" +"snds (x, y) = {y}" +unfolding fsts_def snds_def by simp+ + +lemma sum_set_simps: +"setl (Inl x) = {x}" +"setl (Inr x) = {}" +"setr (Inl x) = {}" +"setr (Inr x) = {x}" +unfolding sum_set_defs by simp+ + +lemma prod_rel_simp: +"prod_rel P Q (x, y) (x', y') \ P x x' \ Q y y'" +unfolding prod_rel_def by simp + +lemma sum_rel_simps: +"sum_rel P Q (Inl x) (Inl x') \ P x x'" +"sum_rel P Q (Inr y) (Inr y') \ Q y y'" +"sum_rel P Q (Inl x) (Inr y') \ False" +"sum_rel P Q (Inr y) (Inl x') \ False" +unfolding sum_rel_def by simp+ + +lemma spec2: "\x y. P x y \ P x y" +by blast + +lemma rewriteR_comp_comp: "\g o h = r\ \ f o g o h = f o r" + unfolding o_def fun_eq_iff by auto + +lemma rewriteR_comp_comp2: "\g o h = r1 o r2; f o r1 = l\ \ f o g o h = l o r2" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp: "\f o g = l\ \ f o (g o h) = l o h" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp2: "\f o g = l1 o l2; l2 o h = r\ \ f o (g o h) = l1 o r" + unfolding o_def fun_eq_iff by auto + +lemma convol_o: " o h = " + unfolding convol_def by auto + +lemma map_pair_o_convol: "map_pair h1 h2 o =

" + unfolding convol_def by auto + +lemma map_pair_o_convol_id: "(map_pair f id \ ) x = f , g> x" + unfolding map_pair_o_convol id_o o_id .. + +lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x" + unfolding sum_case_o_sum_map id_o o_id .. + +lemma fun_rel_def_butlast: + "(fun_rel R (fun_rel S T)) f g = (\x y. R x y \ (fun_rel S T) (f x) (g y))" + unfolding fun_rel_def .. + +lemma subst_eq_imp: "(\a b. a = b \ P a b) \ (\a. P a a)" + by auto + +lemma eq_subset: "op = \ (\a b. P a b \ a = b)" + by auto + +lemma eq_le_Grp_id_iff: "(op = \ Grp (Collect R) id) = (All R)" + unfolding Grp_def id_apply by blast + +lemma Grp_id_mono_subst: "(\x y. Grp P id x y \ Grp Q id (f x) (f y)) \ + (\x. x \ P \ f x \ Q)" + unfolding Grp_def by rule auto + +lemma if_if_True: + "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = + (if b then x else if b' then x' else f y')" + by simp + +lemma if_if_False: + "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) = + (if b then f y else if b' then x' else f y')" + by simp + +ML_file "Tools/bnf_fp_util.ML" +ML_file "Tools/bnf_fp_def_sugar_tactics.ML" +ML_file "Tools/bnf_fp_def_sugar.ML" +ML_file "Tools/bnf_fp_n2m_tactics.ML" +ML_file "Tools/bnf_fp_n2m.ML" +ML_file "Tools/bnf_fp_n2m_sugar.ML" +ML_file "Tools/bnf_fp_rec_sugar_util.ML" +ML_file "Tools/bnf_fp_rec_sugar_tactics.ML" +ML_file "Tools/bnf_fp_rec_sugar.ML" + +end diff -r d8ad101cc684 -r d0e4c8f73541 src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 13:45:57 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,160 +0,0 @@ -(* Title: HOL/BNF/BNF_FP_Basic.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Basic fixed point operations on bounded natural functors. -*) - -header {* Basic Fixed Point Operations on Bounded Natural Functors *} - -theory BNF_FP_Basic -imports BNF_Comp BNF_Ctr_Sugar -keywords - "defaults" -begin - -lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" -by auto - -lemma eq_sym_Unity_conv: "(x = (() = ())) = x" -by blast - -lemma unit_case_Unity: "(case u of () => f) = f" -by (cases u) (hypsubst, rule unit.cases) - -lemma prod_case_Pair_iden: "(case p of (x, y) \ (x, y)) = p" -by simp - -lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x" -by simp - -lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by clarify - -lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by auto - -lemma pointfree_idE: "f \ g = id \ f (g x) = x" -unfolding o_def fun_eq_iff by simp - -lemma o_bij: - assumes gf: "g \ f = id" and fg: "f \ g = id" - shows "bij f" -unfolding bij_def inj_on_def surj_def proof safe - fix a1 a2 assume "f a1 = f a2" - hence "g ( f a1) = g (f a2)" by simp - thus "a1 = a2" using gf unfolding fun_eq_iff by simp -next - fix b - have "b = f (g b)" - using fg unfolding fun_eq_iff by simp - thus "EX a. b = f a" by blast -qed - -lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp - -lemma sum_case_step: -"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" -"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" -by auto - -lemma one_pointE: "\\x. s = x \ P\ \ P" -by simp - -lemma obj_one_pointE: "\x. s = x \ P \ P" -by blast - -lemma obj_sumE_f: -"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" -by (rule allI) (metis sumE) - -lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" -by (cases s) auto - -lemma sum_case_if: -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" -by simp - -lemma mem_UN_compreh_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" -by blast - -lemma UN_compreh_eq_eq: -"\{y. \x\A. y = {}} = {}" -"\{y. \x\A. y = {x}} = A" -by blast+ - -lemma Inl_Inr_False: "(Inl x = Inr y) = False" -by simp - -lemma prod_set_simps: -"fsts (x, y) = {x}" -"snds (x, y) = {y}" -unfolding fsts_def snds_def by simp+ - -lemma sum_set_simps: -"setl (Inl x) = {x}" -"setl (Inr x) = {}" -"setr (Inl x) = {}" -"setr (Inr x) = {x}" -unfolding sum_set_defs by simp+ - -lemma prod_rel_simp: -"prod_rel P Q (x, y) (x', y') \ P x x' \ Q y y'" -unfolding prod_rel_def by simp - -lemma sum_rel_simps: -"sum_rel P Q (Inl x) (Inl x') \ P x x'" -"sum_rel P Q (Inr y) (Inr y') \ Q y y'" -"sum_rel P Q (Inl x) (Inr y') \ False" -"sum_rel P Q (Inr y) (Inl x') \ False" -unfolding sum_rel_def by simp+ - -lemma spec2: "\x y. P x y \ P x y" -by blast - -lemma rewriteR_comp_comp: "\g o h = r\ \ f o g o h = f o r" - unfolding o_def fun_eq_iff by auto - -lemma rewriteR_comp_comp2: "\g o h = r1 o r2; f o r1 = l\ \ f o g o h = l o r2" - unfolding o_def fun_eq_iff by auto - -lemma rewriteL_comp_comp: "\f o g = l\ \ f o (g o h) = l o h" - unfolding o_def fun_eq_iff by auto - -lemma rewriteL_comp_comp2: "\f o g = l1 o l2; l2 o h = r\ \ f o (g o h) = l1 o r" - unfolding o_def fun_eq_iff by auto - -lemma convol_o: " o h = " - unfolding convol_def by auto - -lemma map_pair_o_convol: "map_pair h1 h2 o =

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