# HG changeset patch # User desharna # Date 1409314884 -7200 # Node ID 6f37a300c82b226297891c57ae0e6486e4722fe3 # Parent 4ae52c60603a0ec01c0b84658a83869ea06b2de2 generate 'case_transfer' for (co)datatypes diff -r 4ae52c60603a -r 6f37a300c82b src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Aug 28 23:57:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Aug 29 14:21:24 2014 +0200 @@ -563,7 +563,7 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel mk const of_bnf dest ctxt simpleTs build_simple = +fun build_map_or_rel is_rel mk const of_bnf dest ctxt simpleTs build_simple = let fun build (TU as (T, U)) = if exists (curry (op =) T) simpleTs then @@ -575,18 +575,19 @@ (Type (s, Ts), Type (s', Us)) => if s = s' then let - val bnf = the (bnf_of ctxt s); - val live = live_of_bnf bnf; - val mapx = mk live Ts Us (of_bnf bnf); - val TUs' = map dest (fst (strip_typeN live (fastype_of mapx))); - in Term.list_comb (mapx, map build TUs') end + val (live, cst0) = + if is_rel andalso s = @{type_name fun} then (2, @{term rel_fun}) + else let val bnf = the (bnf_of ctxt s) in (live_of_bnf bnf, of_bnf bnf) end; + val cst = mk live Ts Us cst0; + val TUs' = map dest (fst (strip_typeN live (fastype_of cst))); + in Term.list_comb (cst, map build TUs') end else build_simple TU | _ => build_simple TU); in build end; -val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT; -val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T; +val build_map = build_map_or_rel false mk_map HOLogic.id_const map_of_bnf dest_funT; +val build_rel = build_map_or_rel true mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T; fun map_flattened_map_args ctxt s map_args fs = let diff -r 4ae52c60603a -r 6f37a300c82b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Aug 28 23:57:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Aug 29 14:21:24 2014 +0200 @@ -98,6 +98,7 @@ val EqN = "Eq_"; +val case_transferN = "case_transfer"; val ctr_transferN = "ctr_transfer"; val corec_codeN = "corec_code"; val map_disc_iffN = "map_disc_iff"; @@ -131,17 +132,10 @@ val name_of_set = name_of_const "set"; - -fun mk_parametricity_goals ctxt Rs fs gs = - let - val prems = - map (foldr1 (uncurry mk_rel_fun) o - uncurry (map2 (build_the_rel ctxt Rs [])) o - pairself (fastype_of #> strip_type #> (fn (Ts, T) => Ts @ [T]))) - (fs ~~ gs); - in - map3 (fn prem => fn f => fn g => HOLogic.mk_Trueprop (prem $ f $ g)) prems fs gs - end +fun mk_parametricity_goal ctxt Rs f g = + let val prem = build_the_rel ctxt Rs [] (fastype_of f) (fastype_of g) in + HOLogic.mk_Trueprop (prem $ f $ g) + end; fun fp_sugar_of ctxt = Symtab.lookup (Data.get (Context.Proof ctxt)) @@ -1105,11 +1099,12 @@ val set_boss = map (map fst o type_args_named_constrained_of_spec) specs; val set_bss = map (map (the_default Binding.empty)) set_boss; - val (((Bs0, Cs), Xs), no_defs_lthy) = + val ((((Bs0, Cs as C1 :: _), Es as E1 :: _), Xs), no_defs_lthy) = no_defs_lthy0 |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As |> mk_TFrees num_As ||>> mk_TFrees nn + ||>> mk_TFrees nn ||>> variant_tfrees fp_b_names; fun add_fake_type spec = @@ -1374,8 +1369,8 @@ sel_default_eqs) lthy end; - fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss, - sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = + 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) = if live = 0 then ((([], [], [], []), ctr_sugar), lthy) else @@ -1475,7 +1470,7 @@ rel_inject_thms ms; val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, - ctr_transfer_thms, (set_cases_thms, set_cases_attrss), + case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) = let val live_AsBs = filter (op <>) (As ~~ Bs); @@ -1498,7 +1493,7 @@ val ctr_transfer_thms = let - val goals = mk_parametricity_goals names_lthy Rs ctrAs ctrBs; + val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs; in Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (K (mk_ctr_transfer_tac rel_intro_thms)) @@ -1695,6 +1690,22 @@ (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) end; + val case_transfer_thms = + let + val (R, names_lthy) = + yield_singleton (mk_Frees "R") (mk_pred2T C1 E1) names_lthy; + + val caseA = mk_case As C1 casex; + val caseB = mk_case Bs E1 casex; + val goal = mk_parametricity_goal names_lthy (R :: Rs) caseA caseB; + in + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_case_transfer_tac ctxt rel_cases_thm case_thms) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + val map_disc_iff_thms = let val discsB = map (mk_disc_or_sel Bs) discs; @@ -1821,7 +1832,7 @@ end; in (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms, - ctr_transfer_thms, (set_cases_thms, set_cases_attrss), + case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) end; @@ -1831,7 +1842,8 @@ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); val notes = - [(ctr_transferN, ctr_transfer_thms, K []), + [(case_transferN, [case_transfer_thms], K []), + (ctr_transferN, ctr_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 4ae52c60603a -r 6f37a300c82b src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Aug 28 23:57:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Aug 29 14:21:24 2014 +0200 @@ -13,6 +13,7 @@ val basic_sumprod_thms_set: thm list val sumprod_thms_rel: thm list + val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic @@ -84,6 +85,18 @@ val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs; +fun mk_case_transfer_tac ctxt rel_cases cases = + let + val n = length (tl (prems_of rel_cases)); + in + REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN + HEADGOAL (etac rel_cases) THEN + ALLGOALS (hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt cases THEN + ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN + ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD})) + 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, @@ -256,7 +269,7 @@ EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs => fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse => (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW - (dtac (rotate_prems (~1) (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] + (dtac (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm arg_cong2} RS iffD1)) THEN' atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN' REPEAT_DETERM o etac conjE))) 1 THEN