# HG changeset patch # User desharna # Date 1409315811 -7200 # Node ID b280d40284432c9f6c973826543a3aa6a1b5d43e # Parent 117c5d2c26428aa9b9b57421034247828a1d39a5 generate 'disc_transfer' for (co)datatypes diff -r 117c5d2c2642 -r b280d4028443 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Aug 29 14:21:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Aug 29 14:36:51 2014 +0200 @@ -100,6 +100,7 @@ val case_transferN = "case_transfer"; val ctr_transferN = "ctr_transfer"; +val disc_transferN = "disc_transfer"; val corec_codeN = "corec_code"; val map_disc_iffN = "map_disc_iff"; val map_selN = "map_sel"; @@ -1370,7 +1371,8 @@ end; fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs, - exhaust, disc_thmss, sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = + exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, + ...} : ctr_sugar, lthy) = if live = 0 then ((([], [], [], []), ctr_sugar), lthy) else @@ -1470,8 +1472,8 @@ rel_inject_thms ms; val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, - case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), - (rel_cases_thm, rel_cases_attrs)) = + case_transfer_thms, ctr_transfer_thms, disc_transfer_thms, + (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) = let val live_AsBs = filter (op <>) (As ~~ Bs); val fTs = map (op -->) live_AsBs; @@ -1488,6 +1490,7 @@ val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf); val setAs = map (mk_set As) (sets_of_bnf fp_bnf); val discAs = map (mk_disc_or_sel As) discs; + val discBs = map (mk_disc_or_sel Bs) discs; val selAss = map (map (mk_disc_or_sel As)) selss; val discAs_selAss = flat (map2 (map o pair) discAs selAss); @@ -1614,7 +1617,6 @@ val rel_sel_thms = let - val discBs = map (mk_disc_or_sel Bs) discs; val selBss = map (map (mk_disc_or_sel Bs)) selss; val n = length discAs; @@ -1706,6 +1708,21 @@ |> Thm.close_derivation end; + val disc_transfer_thms = + let + val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs; + in + if null goals then [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_disc_transfer_tac ctxt (the_single rel_sel_thms) + (the_single exhaust_discs) (flat (flat distinct_discsss))) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; + val map_disc_iff_thms = let val discsB = map (mk_disc_or_sel Bs) discs; @@ -1832,8 +1849,8 @@ end; in (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, - case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), - (rel_cases_thm, rel_cases_attrs)) + case_transfer_thms, ctr_transfer_thms, disc_transfer_thms, + (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) end; val anonymous_notes = @@ -1844,6 +1861,7 @@ val notes = [(case_transferN, [case_transfer_thms], K []), (ctr_transferN, ctr_transfer_thms, K []), + (disc_transferN, disc_transfer_thms, K []), (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)), (map_disc_iffN, map_disc_iff_thms, K simp_attrs), (map_selN, map_sel_thms, K []), diff -r 117c5d2c2642 -r b280d4028443 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Aug 29 14:21:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Aug 29 14:36:51 2014 +0200 @@ -22,6 +22,7 @@ val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic val mk_ctr_transfer_tac: thm list -> tactic + val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> @@ -97,6 +98,24 @@ ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD})) end; +fun mk_ctr_transfer_tac rel_intros = + HEADGOAL Goal.conjunction_tac THEN + ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN' + REPEAT_DETERM o atac)); + +fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc= + let + fun last_disc_tac iffD = + HEADGOAL (rtac (rotate_prems ~1 exhaust_disc) THEN' atac THEN' + REPEAT_DETERM o (rotate_tac ~1 THEN' dtac (rotate_prems 1 iffD) THEN' atac THEN' + rotate_tac ~1 THEN' etac (rotate_prems 1 notE) THEN' eresolve_tac distinct_disc)); + in + HEADGOAL Goal.conjunction_tac THEN + REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI} THEN' dtac (rel_sel RS iffD1) THEN' + REPEAT_DETERM o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN + TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1) + end; + fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' = unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, @@ -109,11 +128,6 @@ SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN' atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])); -fun mk_ctr_transfer_tac rel_intros = - HEADGOAL Goal.conjunction_tac THEN - ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN' - REPEAT_DETERM o atac)); - fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs = unfold_thms_tac ctxt (ctor_inject :: abs_inject :: @{thms sum.inject} @ ctr_defs) THEN HEADGOAL (rtac @{thm sum.distinct(1)});