# HG changeset patch # User blanchet # Date 1347131066 -7200 # Node ID f493cd25737fa6f96e9ee33b74d96df4fc6d7cb8 # Parent c69c2c18dccba6dcc37878e79d5a386d4e2e1f9b some work towards iterator and recursor properties diff -r c69c2c18dccb -r f493cd25737f 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 @@ -20,12 +20,16 @@ open BNF_FP_Sugar_Tactics val caseN = "case"; +val itersN = "iters"; +val recsN = "recs"; fun retype_free (Free (s, _)) T = Free (s, T); +fun flat_list_comb (f, xss) = fold (fn xs => fn t => Term.list_comb (t, xs)) xss f + fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; -fun mk_doubly_uncurried_fun f xss = +fun mk_uncurried2_fun f xss = mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; @@ -281,12 +285,11 @@ val rec_free = Free (Binding.name_of rec_binder, rec_T); val iter_spec = - mk_Trueprop_eq (fold (fn gs => fn t => Term.list_comb (t, gs)) gss iter_free, + mk_Trueprop_eq (flat_list_comb (iter_free, gss), Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss)); val rec_spec = - mk_Trueprop_eq (fold (fn hs => fn t => Term.list_comb (t, hs)) hss rec_free, - Term.list_comb (fp_rec, - map2 (mk_sum_caseN oo map2 mk_doubly_uncurried_fun) hss zssss)); + mk_Trueprop_eq (flat_list_comb (rec_free, hss), + Term.list_comb (fp_rec, map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) hss zssss)); val (([raw_iter, raw_rec], [raw_iter_def, raw_rec_def]), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => @@ -303,98 +306,51 @@ val iter = Morphism.term phi raw_iter; val recx = Morphism.term phi raw_rec; in - ((iter, recx), lthy) + ([[ctrs], [[iter]], [[recx]], xss, gss, hss], lthy) end; - fun sugar_codatatype no_defs_lthy = - let -(*### - val fp_y_Ts = map range_type (fst (split_last (binder_types (fastype_of fp_iter)))); - val y_prod_Tss = map2 dest_sumTN ns fp_y_Ts; - val y_Tsss = map2 (map2 dest_tupleT) mss y_prod_Tss; - val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css; - val coiter_T = flat g_Tss ---> fpT --> C; - - val fp_z_Ts = map domain_type (fst (split_last (binder_types (fastype_of fp_rec)))); - val z_prod_Tss = map2 dest_sumTN ns fp_z_Ts; - val z_Tsss = map2 (map2 dest_tupleT) mss z_prod_Tss; - val z_Tssss = map (map (map dest_rec_pair)) z_Tsss; - val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css; - val corec_T = flat h_Tss ---> fpT --> C; - - val ((gss, ysss), _) = - no_defs_lthy - |> mk_Freess "f" g_Tss - ||>> mk_Freesss "x" y_Tsss; - - val hss = map2 (map2 retype_free) gss h_Tss; - val (zssss, _) = - no_defs_lthy - |> mk_Freessss "x" z_Tssss; - - val coiter_binder = Binding.suffix_name ("_" ^ coiterN) b; - val corec_binder = Binding.suffix_name ("_" ^ corecN) b; - - val coiter_free = Free (Binding.name_of coiter_binder, coiter_T); - val corec_free = Free (Binding.name_of corec_binder, corec_T); - - val coiter_spec = - mk_Trueprop_eq (fold (fn gs => fn t => Term.list_comb (t, gs)) gss coiter_free, - Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss)); - val corec_spec = - mk_Trueprop_eq (fold (fn hs => fn t => Term.list_comb (t, hs)) hss corec_free, - Term.list_comb (fp_rec, - map2 (mk_sum_caseN oo map2 mk_doubly_uncurried_fun) hss zssss)); - - val (([raw_coiter, raw_corec], [raw_coiter_def, raw_corec_def]), (lthy', lthy)) = - no_defs_lthy - |> apfst split_list o fold_map2 (fn b => fn spec => - Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) - #>> apsnd snd) [coiter_binder, corec_binder] [coiter_spec, corec_spec] - ||> `Local_Theory.restore; - - (*transforms defined frees into consts (and more)*) - val phi = Proof_Context.export_morphism lthy lthy'; - - val coiter_def = Morphism.thm phi raw_coiter_def; - val corec_def = Morphism.thm phi raw_corec_def; - - val coiter = Morphism.term phi raw_coiter; - val corec = Morphism.term phi raw_corec; -*) - val coiter = @{term True}; (*###*) - val corec = @{term True}; (*###*) - in - ((coiter, corec), lthy) - end; + fun sugar_codatatype no_defs_lthy = ([], no_defs_lthy); in wrap_datatype tacss ((ctrs, casex), (disc_binders, sel_binderss)) lthy' |> (if gfp then sugar_codatatype else sugar_datatype) end; -(* ### - val (iter_thms, rec_thms) = - let - fun mk_goal_iter_or_rec fc xctr f xs = - mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, )); + fun pour_more_sugar_on_datatypes ([[ctrss], [[iters]], [[recs]], xsss, gsss, hsss], lthy) = + let + val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; + val giters = map2 (curry flat_list_comb) iters gsss; + val hrecs = map2 (curry flat_list_comb) recs hsss; - val giter = Term.list_comb (iter, gs); - val hrec = Term.list_comb (rec, hs); + val (iter_thmss, rec_thmss) = + let + fun mk_goal_iter_or_rec fc xctr = + mk_Trueprop_eq (fc $ xctr, fc $ xctr); - val goal_iters = map2 (mk_goal_iter_or_rec iter) gss xctrs; - val goal_recs = map2 (mk_goal_iter_or_rec recx) hss xctrs; - val iter_tacs = []; - val rec_tacs = []; - in - (map2 (Skip_Proof.prove lthy [] []) goal_iters iter_tacs, - map2 (Skip_Proof.prove lthy [] []) goal_recs rec_tacs) - end; -*) + val goal_iterss = map2 (fn giter => map (mk_goal_iter_or_rec giter)) giters xctrss; + val goal_recss = []; + val iter_tacss = []; (* ### map (map mk_iter_or_rec_tac); (* needs ctr_def, iter_def, fld_iter *) *) + val rec_tacss = []; + in + (map2 (map2 (Skip_Proof.prove lthy [] [])) goal_iterss iter_tacss, + map2 (map2 (Skip_Proof.prove lthy [] [])) goal_recss rec_tacss) + end; - val ((iters, recs), lthy'') = - fold_map pour_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ fp_recs ~~ + val notes = + [(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; + + val lthy'' = lthy' + |> fold_map pour_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ - disc_binderss ~~ sel_bindersss) lthy' |>> split_list; + disc_binderss ~~ sel_bindersss) + |> (if gfp then snd else pour_more_sugar_on_datatypes o apfst transpose); val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ (if gfp then "co" else "") ^ "datatype"));