# HG changeset patch # User desharna # Date 1404742006 -7200 # Node ID f9dd8a33f82045ae553ee73fbbae90f7feee64ce # Parent b8448367f9c7bfb9ecd80fe3ab028e2b85f601cf generate 'rel_cases' theorem for (co)datatypes diff -r b8448367f9c7 -r f9dd8a33f820 src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Sat Jul 05 20:51:24 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Mon Jul 07 16:06:46 2014 +0200 @@ -13,6 +13,12 @@ imports BNF_Comp Basic_BNFs begin +lemma False_imp_eq_True: "(False \ Q) \ Trueprop True" + by default simp_all + +lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)" + by default simp_all + lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" by auto diff -r b8448367f9c7 -r f9dd8a33f820 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Jul 05 20:51:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jul 07 16:06:46 2014 +0200 @@ -111,6 +111,9 @@ fun merge data : T = Symtab.merge (K true) data; ); +fun choose_relator Rs AB = find_first + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) Rs; + fun fp_sugar_of ctxt = Symtab.lookup (Data.get (Context.Proof ctxt)) #> Option.map (transfer_fp_sugar ctxt); @@ -472,12 +475,9 @@ ||>> 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_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (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 = @@ -489,8 +489,8 @@ 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 goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq + (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)) IRs)); val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems = prems} => @@ -725,12 +725,9 @@ (mk_discss fpBs Bs, mk_selsss fpBs Bs)) end; - 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_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B); fun build_rel_app selA_t selB_t = (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t @@ -755,8 +752,8 @@ map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss end; - val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)))); + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq + IRs (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)))); val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems = prems} => @@ -1259,7 +1256,7 @@ end; fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss, - sel_thmss, ...} : ctr_sugar, lthy) = + sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) = if live = 0 then ((([], [], [], []), ctr_sugar), lthy) else @@ -1314,14 +1311,93 @@ val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); - val (disc_map_iff_thms, sel_map_thms, sel_set_thms) = + val set_empty_thms = + let + val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o + binder_types o fastype_of) ctrs; + val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets; + val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs; + + fun mk_set_empty_goal disc set T = + Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u), + mk_Trueprop_eq (set $ u, HOLogic.mk_set T [])); + + val goals = + if null discs then + [] + else + map_filter I (flat + (map2 (fn names => fn disc => + map3 (fn name => fn setT => fn set => + if member (op =) names name then NONE + else SOME (mk_set_empty_goal disc set setT)) + setT_names setTs sets) + ctr_argT_namess discs)); + in + if null goals then + [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss)) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + end; + + val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); + + fun mk_rel_thm postproc ctr_defs' cxIn cyIn = + fold_thms lthy ctr_defs' + (unfold_thms lthy (pre_rel_def :: abs_inverse :: + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ + @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) + (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) + |> postproc + |> singleton (Proof_Context.export names_lthy no_defs_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_rel_intro_thm thm = + let + fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm))) + handle THM _ => thm + in + impl (thm RS iffD2) + handle THM _ => thm + end; + + 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_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_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); + val rel_intro_thms = map mk_rel_intro_thm 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; + + val rel_eq_thms = + map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ + map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) + rel_inject_thms ms; + + val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) = let val (((Ds, As), Bs), names_lthy) = lthy |> mk_TFrees (dead_of_bnf fp_bnf) ||>> mk_TFrees (live_of_bnf fp_bnf) ||>> mk_TFrees (live_of_bnf fp_bnf); val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf; - val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; + val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; val fTs = map2 (curry op -->) As Bs; val ((fs, ta), names_lthy) = names_lthy |> mk_Frees "f" fTs @@ -1331,6 +1407,60 @@ val selssA = map (map (mk_disc_or_sel ADs)) selss; val disc_sel_pairs = flat (map2 (map o pair) discsA selssA); + val (rel_cases_thm, rel_cases_attrs) = + let + val rel = mk_rel_of_bnf Ds As Bs fp_bnf; + val (((thesis, Rs), tb), names_lthy) = names_lthy + |> yield_singleton (mk_Frees "thesis") HOLogic.boolT + |>> HOLogic.mk_Trueprop + ||>> mk_Frees "R" (map2 mk_pred2T As Bs) + ||>> yield_singleton (mk_Frees "b") TB; + + val _ = apfst HOLogic.mk_Trueprop; + val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb; + val ctrAs = map (mk_ctr ADs) ctrs; + val ctrBs = map (mk_ctr BDs) ctrs; + + fun mk_assms ctrA ctrB ctxt = + let + val argA_Ts = binder_types (fastype_of ctrA); + val argB_Ts = binder_types (fastype_of ctrB); + val ((argAs, argBs), names_ctxt) = ctxt + |> mk_Frees "x" argA_Ts + ||>> mk_Frees "y" argB_Ts; + val ctrA_args = list_comb (ctrA, argAs); + val ctrB_args = list_comb (ctrB, argBs); + fun build_the_rel A B = + build_rel lthy [] (the o choose_relator Rs) (A, B); + fun build_rel_app a b = + build_the_rel (fastype_of a) (fastype_of b) $ a $ b; + in + (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies + (mk_Trueprop_eq (ta, ctrA_args) :: + mk_Trueprop_eq (tb, ctrB_args) :: + map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs, + thesis)), + names_ctxt) + end; + + val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy; + val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, + thesis); + val thm = Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust + injects rel_inject_thms distincts rel_distinct_thms) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation; + + val ctr_names = quasi_unambiguous_case_names ((map name_of_ctr) ctrAs); + val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); + val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + val cases_pred_attr = Attrib.internal o K o Induct.cases_pred; + in + (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) + end; + val disc_map_iff_thms = let val discsB = map (mk_disc_or_sel BDs) discs; @@ -1453,88 +1583,9 @@ |> Proof_Context.export names_lthy lthy end; in - (disc_map_iff_thms, sel_map_thms, sel_set_thms) - end; - - val set_empty_thms = - let - val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o - binder_types o fastype_of) ctrs; - val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets; - val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs; - - fun mk_set_empty_goal disc set T = - Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u), - mk_Trueprop_eq (set $ u, HOLogic.mk_set T [])); - - val goals = - if null discs then - [] - else - map_filter I (flat - (map2 (fn names => fn disc => - map3 (fn name => fn setT => fn set => - if member (op =) names name then NONE - else SOME (mk_set_empty_goal disc set setT)) - setT_names setTs sets) - ctr_argT_namess discs)); - in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss)) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy + (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) end; - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); - - fun mk_rel_thm postproc ctr_defs' cxIn cyIn = - fold_thms lthy ctr_defs' - (unfold_thms lthy (pre_rel_def :: abs_inverse :: - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @ - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]}) - (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) - |> postproc - |> singleton (Proof_Context.export names_lthy no_defs_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_rel_intro_thm thm = - let - fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm))) - handle THM _ => thm - in - impl (thm RS iffD2) - handle THM _ => thm - end; - - 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_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_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); - val rel_intro_thms = map mk_rel_intro_thm 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; - - val rel_eq_thms = - map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @ - map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) - rel_inject_thms ms; - val anonymous_notes = [([case_cong], fundefcong_attrs), (rel_eq_thms, code_nitpicksimp_attrs)] @@ -1543,6 +1594,7 @@ val notes = [(disc_map_iffN, disc_map_iff_thms, simp_attrs), (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs), + (rel_casesN, [rel_cases_thm], rel_cases_attrs), (rel_distinctN, rel_distinct_thms, simp_attrs), (rel_injectN, rel_inject_thms, simp_attrs), (rel_introsN, rel_intro_thms, []), diff -r b8448367f9c7 -r f9dd8a33f820 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Jul 05 20:51:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jul 07 16:06:46 2014 +0200 @@ -26,6 +26,8 @@ val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic + val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> + thm list -> thm list -> 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 -> thm list -> tactic @@ -211,6 +213,17 @@ (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts = + HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW + rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW + hyp_subst_tac ctxt) THEN + Local_Defs.unfold_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6) + True_implies_equals conj_imp_eq_imp_imp} @ + map (fn thm => iffD2 OF [@{thm eq_False}, thm]) (distincts @ rel_distincts) @ + map (fn thm => thm RS @{thm eqTrueI}) rel_injects) THEN + TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN' + REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt)); + 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 nesting_rel_eqs = rtac dtor_rel_coinduct 1 THEN diff -r b8448367f9c7 -r f9dd8a33f820 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sat Jul 05 20:51:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jul 07 16:06:46 2014 +0200 @@ -124,6 +124,7 @@ val morN: string val nchotomyN: string val recN: string + val rel_casesN: string val rel_coinductN: string val rel_inductN: string val rel_injectN: string @@ -406,6 +407,7 @@ val distinctN = "distinct" val rel_distinctN = relN ^ "_" ^ distinctN val injectN = "inject" +val rel_casesN = relN ^ "_cases" val rel_injectN = relN ^ "_" ^ injectN val rel_introsN = relN ^ "_intros" val rel_coinductN = relN ^ "_" ^ coinductN diff -r b8448367f9c7 -r f9dd8a33f820 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sat Jul 05 20:51:24 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Jul 07 16:06:46 2014 +0200 @@ -54,7 +54,7 @@ fun mk_nchotomy_tac n exhaust = HEADGOAL (rtac allI THEN' rtac exhaust THEN' - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))); + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))); fun mk_unique_disc_def_tac m uexhaust = HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);