# HG changeset patch # User desharna # Date 1407839502 -7200 # Node ID 7bc128647d6e11445cdf2d287f5a93ff9eaff471 # Parent 3d61d6a61cfcb7ccb36ec8dfc6581fefa066f4ca generate 'set_cases' theorem for (co)datatypes diff -r 3d61d6a61cfc -r 7bc128647d6e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 12 12:01:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 12 12:31:42 2014 +0200 @@ -102,6 +102,7 @@ val disc_map_iffN = "disc_map_iff"; val sel_mapN = "sel_map"; val sel_setN = "sel_set"; +val set_casesN = "set_cases"; val set_emptyN = "set_empty"; val set_introsN = "set_intros"; val set_inductN = "set_induct"; @@ -114,6 +115,12 @@ fun merge data : T = Symtab.merge (K true) data; ); +fun zipping_map f = + let + fun zmap _ [] = [] + | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys + in zmap [] end; + fun choose_binary_fun fs AB = find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; fun build_binary_fun_app fs a b = @@ -503,7 +510,7 @@ (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal - (fn {context = ctxt, prems = prems} => + (fn {context = ctxt, prems} => mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) |> singleton (Proof_Context.export names_lthy lthy) @@ -754,7 +761,7 @@ IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts))); val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal - (fn {context = ctxt, prems = prems} => + (fn {context = ctxt, prems} => 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 @@ -804,7 +811,7 @@ fun mk_prems_for_ctr A Ps ctr ctxt = let - val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt; + val (args, ctxt') = mk_Frees "z" (binder_types (fastype_of ctr)) ctxt; in fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt' |>> map (fold_rev Logic.all args) o flat @@ -837,7 +844,7 @@ |>> apsnd flat; val thm = Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion) - (fn {context = ctxt, prems = prems} => + (fn {context = ctxt, prems} => mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) |> singleton (Proof_Context.export ctxt'' ctxt) @@ -1491,7 +1498,7 @@ rel_inject_thms ms; val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms, - (rel_cases_thm, rel_cases_attrs)) = + (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) = let val (((Ds, As), Bs), names_lthy) = lthy |> mk_TFrees (dead_of_bnf fp_bnf) @@ -1501,11 +1508,13 @@ val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; val fTs = map2 (curry op -->) As Bs; val rel = mk_rel_of_bnf Ds As Bs fp_bnf; - val ((((fs, Rs), ta), tb), names_lthy) = names_lthy + val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy |> mk_Frees "f" fTs ||>> mk_Frees "R" (map2 mk_pred2T As Bs) ||>> yield_singleton (mk_Frees "a") TA - ||>> yield_singleton (mk_Frees "b") TB; + ||>> yield_singleton (mk_Frees "b") TB + ||>> apfst HOLogic.mk_Trueprop o + yield_singleton (mk_Frees "thesis") HOLogic.boolT; val map_term = mk_map_of_bnf Ds As Bs fp_bnf; val ctrAs = map (mk_ctr ADs) ctrs; val setAs = map (mk_set ADs) (sets_of_bnf fp_bnf); @@ -1513,6 +1522,68 @@ val selAss = map (map (mk_disc_or_sel ADs)) selss; val discAs_selAss = flat (map2 (map o pair) discAs selAss); + val (set_cases_thms, set_cases_attrss) = + let + fun mk_prems assms elem t ctxt = + (case fastype_of t of + Type (type_name, xs) => + (case bnf_of ctxt type_name of + NONE => ([], ctxt) + | SOME bnf => + apfst flat (fold_map (fn set => fn ctxt => + let + val X = HOLogic.dest_setT (range_type (fastype_of set)); + val new_var = not (X = fastype_of elem); + val (x, ctxt') = + if new_var then yield_singleton (mk_Frees "x") X ctxt + else (elem, ctxt); + in + mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt' + |>> map (if new_var then Logic.all x else I) + end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt)) + | T => rpair ctxt + (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis] + else [])); + in + split_list (map (fn set => + let + val A = HOLogic.dest_setT (range_type (fastype_of set)); + val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy; + val premss = + map (fn ctr => + let + val (args, names_lthy) = + mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy; + in + flat (zipping_map (fn (prev_args, arg, next_args) => + let + val (args_with_elem, args_without_elem) = + if fastype_of arg = A then + (prev_args @ [elem] @ next_args, prev_args @ next_args) + else + `I (prev_args @ [arg] @ next_args); + in + mk_prems + [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))] + elem arg names_lthy + |> fst + |> map (fold_rev Logic.all args_without_elem) + end) args) + end) ctrAs; + val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis); + val thm = + Goal.prove_sorry lthy [] (flat premss) goal + (fn {context = ctxt, prems} => + mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + |> rotate_prems ~1; + in + (thm, [](* TODO: [@{attributes [elim?]}, + Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *)) + end) setAs) + end; + val set_intros_thms = let fun mk_goals A setA ctr_args t ctxt = @@ -1593,9 +1664,6 @@ val (rel_cases_thm, rel_cases_attrs) = let - val (thesis, names_lthy) = apfst HOLogic.mk_Trueprop - (yield_singleton (mk_Frees "thesis") HOLogic.boolT names_lthy); - val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb; val ctrBs = map (mk_ctr BDs) ctrs; @@ -1761,7 +1829,7 @@ end; in (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms, - (rel_cases_thm, rel_cases_attrs)) + (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) end; val anonymous_notes = @@ -1780,6 +1848,7 @@ (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)), (sel_mapN, sel_map_thms, K []), (sel_setN, sel_set_thms, K []), + (set_casesN, set_cases_thms, nth set_cases_attrss), (set_emptyN, set_empty_thms, K []), (set_introsN, set_intros_thms, K [])] |> massage_simple_notes fp_b_name; diff -r 3d61d6a61cfc -r 7bc128647d6e src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Aug 12 12:01:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Aug 12 12:31:42 2014 +0200 @@ -39,6 +39,7 @@ 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_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic @@ -302,6 +303,14 @@ hyp_subst_tac ctxt) THEN' (rtac @{thm singletonI} ORELSE' atac)); +fun mk_set_cases_tac ctxt ct assms exhaust sets = + HEADGOAL (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN + unfold_thms_tac ctxt sets THEN + REPEAT_DETERM (HEADGOAL + (eresolve_tac @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE' + hyp_subst_tac ctxt ORELSE' + SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac))))); + fun mk_set_empty_tac ctxt ct exhaust sets discs = TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW @@ -314,8 +323,8 @@ TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN TRYALL (REPEAT o - (resolve_tac @{thms UnI1 UnI2} ORELSE' eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' - (rtac @{thm singletonI} ORELSE' atac)); + (resolve_tac @{thms UnI1 UnI2} ORELSE' + eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac)); fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses =