# HG changeset patch # User blanchet # Date 1473593727 -7200 # Node ID 813a574da7461db2802c9237daaffe0b23c10a0a # Parent eb6d2aace13af3bfe702a351024ed4406ae08b12 derive relator properties forward diff -r eb6d2aace13a -r 813a574da746 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 13:35:27 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 13:35:27 2016 +0200 @@ -830,7 +830,6 @@ end; val cxIns = map2 (mk_cIn ctor) ks xss; - val cyIns = map2 (mk_cIn (B_ify ctor)) ks yss; fun mk_set0_thm fp_set_thm ctr_def' cxIn = Local_Defs.fold lthy [ctr_def'] @@ -877,42 +876,76 @@ |> Conjunction.elim_balanced (length goals) end; - fun mk_rel_thm postproc ctr_defs' cxIn cyIn = - Local_Defs.fold lthy ctr_defs' - (unfold_thms lthy (pre_rel_def :: abs_inverses @ - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) - (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn]) - fp_rel_thm)) - |> postproc - |> singleton (Proof_Context.export names_lthy lthy); - - fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = - mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; - - fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = - mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] - cxIn cyIn; - - fun mk_rel_intro_thm m thm = - uncurry_thm m (thm RS iffD2) handle THM _ => thm; + val rel_inject_thms = + let + fun mk_goal ctrA ctrB xs ys = + let + val rel = mk_rel live As Bs (rel_of_bnf fp_bnf); + val Rrel = list_comb (rel, Rs); + + val lhs = Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys); + val conjuncts = map2 (build_rel_app lthy Rs []) xs ys; + in + HOLogic.mk_Trueprop + (if null conjuncts then lhs + else HOLogic.mk_eq (lhs, Library.foldr1 HOLogic.mk_conj conjuncts)) + end; + + val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs') + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end; + + val half_rel_distinct_thmss = + let + fun mk_goal ((ctrA, xs), (ctrB, ys)) = + let + val rel = mk_rel live As Bs (rel_of_bnf fp_bnf); + val Rrel = list_comb (rel, Rs); + in + HOLogic.mk_Trueprop (HOLogic.mk_not + (Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys))) + end; + + val rel_infos = (ctrAs ~~ xss, ctrBs ~~ yss); + + val goalss = map (map mk_goal) (mk_half_pairss rel_infos); + val goals = flat goalss; + in + unflat goalss + (if null goals then [] + else + let + val goal = Logic.mk_conjunction_balanced goals; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => + mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs') + |> Thm.close_derivation + |> Conjunction.elim_balanced (length goals) + end) + end; val rel_flip = rel_flip_of_bnf fp_bnf; fun mk_other_half_rel_distinct_thm thm = flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); - - val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); - val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; - - val half_rel_distinct_thmss = map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); val other_half_rel_distinct_thmss = map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; val (rel_distinct_thms, _) = join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; + fun mk_rel_intro_thm m thm = + uncurry_thm m (thm RS iffD2) handle THM _ => thm; + + val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms; + val rel_code_thms = map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms; diff -r eb6d2aace13a -r 813a574da746 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:27 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:27 2016 +0200 @@ -10,7 +10,6 @@ sig val sumprod_thms_set: thm list 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 -> @@ -40,6 +39,7 @@ tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic + val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> @@ -75,11 +75,11 @@ val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)}; val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps}; +val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; val basic_sumprod_thms_set = @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; -val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; fun is_def_looping def = (case Thm.prop_of def of @@ -406,13 +406,20 @@ fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s = TRYALL Goal.conjunction_tac THEN - ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW - REPEAT_DETERM o hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ - @{thms not_True_eq_False not_False_eq_True}) THEN - TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN - unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN - ALLGOALS (rtac ctxt refl); + ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW + REPEAT_DETERM o hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ + @{thms not_True_eq_False not_False_eq_True}) THEN + TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN + unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN + ALLGOALS (rtac ctxt refl); + +fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel ctr_defs' = + TRYALL Goal.conjunction_tac THEN + unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ ctr_defs' @ o_apply :: + sumprod_thms_rel @ @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]] + not_False_eq_True}) THEN + ALLGOALS (resolve_tac ctxt [TrueI, refl]); fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW @@ -483,16 +490,16 @@ fun mk_set_sel_tac ctxt ct exhaust discs sels sets = TRYALL Goal.conjunction_tac THEN - ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW - REPEAT_DETERM o hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ - @{thms not_True_eq_False not_False_eq_True}) THEN - TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN - unfold_thms_tac ctxt (sels @ sets) THEN - ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE' - eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE' - hyp_subst_tac ctxt) THEN' - (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt)); + ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW + REPEAT_DETERM o hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ + @{thms not_True_eq_False not_False_eq_True}) THEN + TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN + unfold_thms_tac ctxt (sels @ sets) THEN + ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE' + eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE' + hyp_subst_tac ctxt) THEN' + (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt)); fun mk_set_cases_tac ctxt ct assms exhaust sets = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)