# HG changeset patch # User blanchet # Date 1380195734 -7200 # Node ID bf74357f91f86286e18c0d14309e7fe3dde86ba7 # Parent 37c31a619eee590fd1cf6d36b47e9892da76fe88 generate "sel_splits(_asm)" theorems diff -r 37c31a619eee -r bf74357f91f8 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 26 13:42:13 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 26 13:42:14 2013 +0200 @@ -787,6 +787,12 @@ \item[@{text "t."}\hthm{expand}\rm:] ~ \\ @{thm list.expand[no_vars]} +\item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\ +@{thm list.sel_split[no_vars]} + +\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\ +@{thm list.sel_split_asm[no_vars]} + \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ @{thm list.case_conv_if[no_vars]} diff -r 37c31a619eee -r bf74357f91f8 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 13:42:13 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 13:42:14 2013 +0200 @@ -28,6 +28,8 @@ sel_exhausts: thm list, collapses: thm list, expands: thm list, + sel_splits: thm list, + sel_split_asms: thm list, case_conv_ifs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar @@ -82,6 +84,8 @@ sel_exhausts: thm list, collapses: thm list, expands: thm list, + sel_splits: thm list, + sel_split_asms: thm list, case_conv_ifs: thm list}; fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, @@ -90,7 +94,7 @@ fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, - disc_exhausts, sel_exhausts, collapses, expands, case_conv_ifs} = + disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_conv_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -111,6 +115,8 @@ sel_exhausts = map (Morphism.thm phi) sel_exhausts, collapses = map (Morphism.thm phi) collapses, expands = map (Morphism.thm phi) expands, + sel_splits = map (Morphism.thm phi) sel_splits, + sel_split_asms = map (Morphism.thm phi) sel_split_asms, case_conv_ifs = map (Morphism.thm phi) case_conv_ifs}; val transfer_ctr_sugar = @@ -157,6 +163,8 @@ val nchotomyN = "nchotomy"; val selN = "sel"; val sel_exhaustN = "sel_exhaust"; +val sel_splitN = "sel_split"; +val sel_split_asmN = "sel_split_asm"; val splitN = "split"; val splitsN = "splits"; val split_asmN = "split_asm"; @@ -419,10 +427,9 @@ if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1) end); - val (all_sels_distinct, discs, selss, udiscs, uselss, usel_ctrs, vdiscs, vselss, disc_defs, - sel_defs, sel_defss, lthy') = + val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = if no_discs_sels then - (true, [], [], [], [], [], [], [], [], [], [], lthy) + (true, [], [], [], [], [], lthy) else let fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT); @@ -505,16 +512,8 @@ val discs = map (mk_disc_or_sel As) discs0; val selss = map (map (mk_disc_or_sel As)) selss0; - - val udiscs = map (rapp u) discs; - val uselss = map (map (rapp u)) selss; - val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss; - - val vdiscs = map (rapp v) discs; - val vselss = map (map (rapp v)) selss; in - (all_sels_distinct, discs, selss, udiscs, uselss, usel_ctrs, vdiscs, vselss, disc_defs, - sel_defs, sel_defss, lthy') + (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') end; fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); @@ -589,13 +588,76 @@ ks goals inject_thmss distinct_thmsss end; + val (case_cong_thm, weak_case_cong_thm) = + let + fun mk_prem xctr xs xf xg = + fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), + mk_Trueprop_eq (xf, xg))); + + val goal = + Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs, + mk_Trueprop_eq (eta_ufcase, eta_vgcase)); + val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); + in + (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms), + Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1))) + |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) + end; + + val split_lhs = q $ ufcase; + + fun mk_split_conjunct xctr xs f_xs = + list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); + fun mk_split_disjunct xctr xs f_xs = + list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), + HOLogic.mk_not (q $ f_xs))); + + fun mk_split_goal xctrs xss xfs = + mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj + (map3 mk_split_conjunct xctrs xss xfs)); + fun mk_split_asm_goal xctrs xss xfs = + mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj + (map3 mk_split_disjunct xctrs xss xfs))); + + fun prove_split selss goal = + Goal.prove_sorry lthy [] [] goal (fn _ => + mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss) + |> Thm.close_derivation + |> singleton (Proof_Context.export names_lthy lthy); + + fun prove_split_asm asm_goal split_thm = + Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} => + mk_split_asm_tac ctxt split_thm) + |> Thm.close_derivation + |> singleton (Proof_Context.export names_lthy lthy); + + val (split_thm, split_asm_thm) = + let + val goal = mk_split_goal xctrs xss xfs; + val asm_goal = mk_split_asm_goal xctrs xss xfs; + + val thm = prove_split (replicate n []) goal; + val asm_thm = prove_split_asm asm_goal thm; + in + (thm, asm_thm) + end; + val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, - safe_collapse_thms, expand_thms, case_conv_if_thms) = + safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, + case_conv_if_thms) = if no_discs_sels then - ([], [], [], [], [], [], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else let + val udiscs = map (rapp u) discs; + val uselss = map (map (rapp u)) selss; + val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss; + val usel_fs = map2 (curry Term.list_comb) fs uselss; + + val vdiscs = map (rapp v) discs; + val vselss = map (map (rapp v)) selss; + fun make_sel_thm xs' case_thm sel_def = zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs') (Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); @@ -775,10 +837,21 @@ |> Proof_Context.export names_lthy lthy end; + val (sel_split_thm, sel_split_asm_thm) = + let + val zss = map (K []) xss; + val goal = mk_split_goal usel_ctrs zss usel_fs; + val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs; + + val thm = prove_split sel_thmss goal; + val asm_thm = prove_split_asm asm_goal thm; + in + (thm, asm_thm) + end; + val case_conv_if_thms = let - fun mk_body f usels = Term.list_comb (f, usels); - val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss)); + val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); in [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] @@ -788,55 +861,10 @@ in (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm], - all_collapse_thms, safe_collapse_thms, expand_thms, case_conv_if_thms) + all_collapse_thms, safe_collapse_thms, expand_thms, [sel_split_thm], + [sel_split_asm_thm], case_conv_if_thms) end; - val (case_cong_thm, weak_case_cong_thm) = - let - fun mk_prem xctr xs xf xg = - fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), - mk_Trueprop_eq (xf, xg))); - - val goal = - Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs, - mk_Trueprop_eq (eta_ufcase, eta_vgcase)); - val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase)); - in - (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms), - Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1))) - |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy)) - end; - - val (split_thm, split_asm_thm) = - let - fun mk_conjunct xctr xs f_xs = - list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs)); - fun mk_disjunct xctr xs f_xs = - list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), - HOLogic.mk_not (q $ f_xs))); - - val lhs = q $ ufcase; - - val goal = - mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs)); - val asm_goal = - mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj - (map3 mk_disjunct xctrs xss xfs))); - - val split_thm = - Goal.prove_sorry lthy [] [] goal - (fn _ => mk_split_tac lthy uexhaust_thm case_thms inject_thmss distinct_thmsss) - |> Thm.close_derivation - |> singleton (Proof_Context.export names_lthy lthy); - val split_asm_thm = - Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} => - mk_split_asm_tac ctxt split_thm) - |> Thm.close_derivation - |> singleton (Proof_Context.export names_lthy lthy); - in - (split_thm, split_asm_thm) - end; - val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name)); @@ -856,6 +884,8 @@ (nchotomyN, [nchotomy_thm], []), (selN, all_sel_thms, code_nitpick_simp_simp_attrs), (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]), + (sel_splitN, sel_split_thms, []), + (sel_split_asmN, sel_split_asm_thms, []), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []), @@ -875,6 +905,7 @@ split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms, + sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms, case_conv_ifs = case_conv_if_thms}; in (ctr_sugar, diff -r 37c31a619eee -r bf74357f91f8 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 13:42:13 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 13:42:14 2013 +0200 @@ -20,8 +20,8 @@ val mk_nchotomy_tac: int -> thm -> tactic val mk_other_half_disc_exclude_tac: thm -> tactic val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic - val mk_split_tac: Proof.context -> - thm -> thm list -> thm list list -> thm list list list -> tactic + val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list + list list -> tactic val mk_split_asm_tac: Proof.context -> thm -> tactic val mk_unique_disc_def_tac: int -> thm -> tactic end; @@ -141,10 +141,10 @@ HEADGOAL (rtac uexhaust THEN' EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); -fun mk_split_tac ctxt uexhaust cases injectss distinctsss = +fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss = HEADGOAL (rtac uexhaust) THEN ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' - simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ + simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ flat (nth distinctsss (k - 1))) ctxt)) k) THEN ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));