# HG changeset patch # User desharna # Date 1404226888 -7200 # Node ID 11cd462e31eced4c34ef2edb7f367ab9cd6d47a2 # Parent d3eac6fd0bd61a8e72ca52979ee8776d1375cbd4 generate 'rel_induct' theorem for datatypes diff -r d3eac6fd0bd6 -r 11cd462e31ec src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Tue Jul 01 16:26:14 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Tue Jul 01 17:01:28 2014 +0200 @@ -89,6 +89,9 @@ lemma Inl_Inr_False: "(Inl x = Inr y) = False" by simp +lemma Inr_Inl_False: "(Inr x = Inl y) = False" + by simp + lemma spec2: "\x y. P x y \ P x y" by blast diff -r d3eac6fd0bd6 -r 11cd462e31ec src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Tue Jul 01 16:26:14 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Tue Jul 01 17:01:28 2014 +0200 @@ -1,3 +1,4 @@ + (* Title: HOL/BNF_LFP.thy Author: Dmitriy Traytel, TU Muenchen Author: Lorenz Panny, TU Muenchen @@ -194,4 +195,5 @@ hide_fact (open) id_transfer + end diff -r d3eac6fd0bd6 -r 11cd462e31ec src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 16:26:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 17:01:28 2014 +0200 @@ -243,10 +243,6 @@ fun merge_type_args fp (As, As') = if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp; -fun reassoc_conjs thm = - reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]}) - handle THM _ => thm; - fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs; fun type_binding_of_spec (((((_, b), _), _), _), _) = b; fun mixfix_of_spec ((((_, mx), _), _), _) = mx; @@ -444,6 +440,69 @@ map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) end; +fun postproc_co_induct lthy nn prop prop_conj = + Drule.zero_var_indexes + #> `(conj_dests nn) + #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop)) + ##> (fn thm => Thm.permute_prems 0 (~nn) + (if nn = 1 then thm RS prop + else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm)); + +fun mk_induct_attrs ctrss = + let + val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); + val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); + in + [induct_case_names_attr] + end; + +fun derive_rel_induct_thm_for_types lthy fpA_Ts ns As Bs mss ctrAss ctrAs_Tsss ctr_sugars + ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = + let + val B_ify = typ_subst_nonatomic (As ~~ Bs) + val fpB_Ts = map B_ify fpA_Ts; + val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss; + val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss; + + val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy + |> mk_Frees "R" (map2 mk_pred2T As Bs) + ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) + ||>> mk_Freesss "a" ctrAs_Tsss + ||>> mk_Freesss "b" ctrBs_Tsss; + + fun choose_relator AB = the (find_first + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs)); + + val premises = + let + fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B); + fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) $ a $ b; + + fun mk_prem ctrA ctrB argAs argBs = + fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies) + (map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs) + (HOLogic.mk_Trueprop + (build_rel_app (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs))))); + in + flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss) + end; + + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj + (map2 mk_leq (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)) IRs)); + + val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal + (fn {context = ctxt, prems = prems} => + mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) + (map #exhaust ctr_sugars) ctor_defss ctor_injects pre_rel_defs abs_inverses + live_nesting_rel_eqs) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation; + in + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} + rel_induct0_thm, + mk_induct_attrs ctrAss) + end; + fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy = @@ -552,9 +611,6 @@ `(conj_dests nn) thm end; - val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); - val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); - val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms = @@ -594,11 +650,11 @@ val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms; in - ((induct_thms, induct_thm, [induct_case_names_attr]), + ((induct_thms, induct_thm, mk_induct_attrs ctrss), (rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) end; -fun coinduct_attrs fpTs ctr_sugars mss = +fun mk_coinduct_attrs fpTs ctr_sugars mss = let val nn = length fpTs; val fp_b_names = map base_name_of_typ fpTs; @@ -635,16 +691,8 @@ (coinduct_attrs, common_coinduct_attrs) end; -fun postproc_coinduct nn prop prop_conj = - Drule.zero_var_indexes - #> `(conj_dests nn) - #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop)) - ##> (fn thm => Thm.permute_prems 0 nn - (if nn = 1 then thm RS prop - else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm)); - -fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects - ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct = +fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects + ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs = let val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts; @@ -713,12 +761,13 @@ mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects - rel_pre_defs abs_inverses) + rel_pre_defs abs_inverses live_nesting_rel_eqs) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; in - (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, - coinduct_attrs fpA_Ts ctr_sugars mss) + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} + rel_coinduct0_thm, + mk_coinduct_attrs fpA_Ts ctr_sugars mss) end; fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _)) @@ -817,7 +866,7 @@ val dtor_coinducts = [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] in - map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals + map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals end; fun mk_maybe_not pos = not pos ? HOLogic.mk_not; @@ -912,7 +961,7 @@ val sel_corec_thmsss = mk_sel_corec_thms corec_thmss; in - ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss), + ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss), (corec_thmss, code_nitpicksimp_attrs), (disc_corec_thmss, []), (disc_corec_iff_thmss, simp_attrs), @@ -1531,17 +1580,37 @@ abs_inverses ctrss ctr_defss recs rec_defs lthy; val induct_type_attr = Attrib.internal o K o Induct.induct_type; + val induct_pred_attr = Attrib.internal o K o Induct.induct_pred; + + val ((rel_induct_thmss, common_rel_induct_thms), + (rel_induct_attrs, common_rel_induct_attrs)) = + if live = 0 then + ((replicate nn [], []), ([], [])) + else + let + val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) = + derive_rel_induct_thm_for_types lthy fpTs ns As Bs mss ctrss ctr_Tsss ctr_sugars + rel_xtor_co_induct_thm ctr_defss ctor_injects pre_rel_defs abs_inverses + (map rel_eq_of_bnf live_nesting_bnfs); + in + ((map single rel_induct_thms, single common_rel_induct_thm), + (rel_induct_attrs, rel_induct_attrs)) + end; val simp_thmss = map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss; val common_notes = - (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) + (if nn > 1 then + [(inductN, [induct_thm], induct_attrs), + (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)] + else []) |> massage_simple_notes fp_common_name; val notes = [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), (recN, rec_thmss, K rec_attrs), + (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])), (simpsN, simp_thmss, K [])] |> massage_multi_notes; in @@ -1567,11 +1636,6 @@ ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs (Proof_Context.export lthy' no_defs_lthy) lthy; - val ((rel_coinduct_thms, rel_coinduct_thm), - (rel_coinduct_attrs, common_rel_coinduct_attrs)) = - derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses - abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm; - val sel_corec_thmss = map flat sel_corec_thmsss; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1579,6 +1643,22 @@ val flat_corec_thms = append oo append; + val ((rel_coinduct_thmss, common_rel_coinduct_thms), + (rel_coinduct_attrs, common_rel_coinduct_attrs)) = + if live = 0 then + ((replicate nn [], []), ([], [])) + else + let + val ((rel_coinduct_thms, common_rel_coinduct_thm), + (rel_coinduct_attrs, common_rel_coinduct_attrs)) = + derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses + abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm + (map rel_eq_of_bnf live_nesting_bnfs) + in + ((map single rel_coinduct_thms, single common_rel_coinduct_thm), + (rel_coinduct_attrs, common_rel_coinduct_attrs)) + end; + val simp_thmss = map6 mk_simp_thms ctr_sugars (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) @@ -1586,21 +1666,19 @@ val common_notes = (if nn > 1 then - [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs), - (coinductN, [coinduct_thm], common_coinduct_attrs), + [(coinductN, [coinduct_thm], common_coinduct_attrs), + (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs), (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)] - else - []) + else []) |> massage_simple_notes fp_common_name; val notes = [(coinductN, map single coinduct_thms, fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]), - (rel_coinductN, map single rel_coinduct_thms, - K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), (corecN, corec_thmss, K corec_attrs), (disc_corecN, disc_corec_thmss, K disc_corec_attrs), (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs), + (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), (sel_corecN, sel_corec_thmss, K sel_corec_attrs), (simpsN, simp_thmss, K []), (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)] diff -r d3eac6fd0bd6 -r 11cd462e31ec src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 16:26:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 17:01:28 2014 +0200 @@ -28,7 +28,9 @@ tactic val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> - thm list -> thm list -> tactic + thm list -> thm list -> thm list -> tactic + val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list -> + thm list list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic @@ -210,7 +212,7 @@ selsss)); fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss - dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses = + dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs = rtac dtor_rel_coinduct 1 THEN 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 => @@ -222,14 +224,29 @@ Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels @ simp_thms') THEN Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject :: - abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps - rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject - prod.inject}) THEN + abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def + rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] + sum.inject prod.inject}) THEN REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN' (rtac refl ORELSE' atac)))) cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses); +fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects + rel_pre_list_defs Abs_inverses nesting_rel_eqs = + rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs => + fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse => + HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW + (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2) + THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN + unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ + @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN + TRYALL (hyp_subst_tac ctxt) THEN + unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False + Inr_Inl_False sum.inject prod.inject}) THEN + TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac)) + cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses); + fun mk_sel_map_tac ctxt ct exhaust discs maps sels = TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW