# HG changeset patch # User blanchet # Date 1347131066 -7200 # Node ID d01a5c918298acab5c709cc366112931963e1a36 # Parent 0c9546fc789fb9e725b72a5673b5b51c2fc3922a renamed xxxBNF to pre_xxx diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200 @@ -485,19 +485,24 @@ val rec_tacss = map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss; in + ([], []) +(* NOTYET (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) goal_iterss iter_tacss, map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) goal_recss rec_tacss) +*) end; - val notes = + val notes = []; +(* NOTYET [(itersN, iter_thmss), (recsN, rec_thmss)] |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss); +*) in lthy |> Local_Theory.notes notes |> snd end; diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Sat Sep 08 21:04:26 2012 +0200 @@ -53,10 +53,9 @@ val iter_like_thms = @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv}; -fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt = - Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN - Local_Defs.unfold_tac ctxt iter_like_thms THEN - rtac refl 1; +fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt = + Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN + Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1; val coiter_like_ss = ss_only @{thms if_True if_False}; val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases}; diff -r 0c9546fc789f -r d01a5c918298 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200 @@ -134,6 +134,9 @@ ((name, Typedef.transform_info phi info), lthy) end; +val pre_N = "pre_" +val raw_N = "raw_" + val coN = "co" val algN = "alg" val IITN = "IITN" @@ -299,7 +302,7 @@ val Dss = map3 (append oo map o nth) livess kill_poss deadss; val ((bnfs'', deadss), lthy'') = - fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy' + fold_map3 (seal_bnf unfold') (map (Binding.prefix_name pre_N) bs) Dss bnfs' lthy' |>> split_list; val pre_map_defs = map map_def_of_bnf bnfs''; @@ -319,7 +322,7 @@ val (lhss, rhss) = split_list eqs; val sort = fp_sort lhss (SOME resBs); val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) - (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss + (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort) bs rhss (empty_unfold, lthy)); in mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy' @@ -332,7 +335,7 @@ val sort = fp_sort lhss NONE; val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) (fold_map2 (fn b => fn rawT => - (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT))) + (bnf_of_typ Smart_Inline (Binding.prefix_name raw_N b) I sort (Syntax.read_typ lthy rawT))) bs raw_bnfs (empty_unfold, lthy)); in snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')