# HG changeset patch # User blanchet # Date 1380195733 -7200 # Node ID 37c31a619eee590fd1cf6d36b47e9892da76fe88 # Parent 0e2c4dff5d130132c783ead1e65e8ca60a78c24e generate "sel_exhaust" theorem diff -r 0e2c4dff5d13 -r 37c31a619eee src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 26 13:34:42 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 26 13:42:13 2013 +0200 @@ -781,6 +781,9 @@ \item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ @{thm list.disc_exhaust[no_vars]} +\item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ +@{thm list.sel_exhaust[no_vars]} + \item[@{text "t."}\hthm{expand}\rm:] ~ \\ @{thm list.expand[no_vars]} diff -r 0e2c4dff5d13 -r 37c31a619eee src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 13:34:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 13:42:13 2013 +0200 @@ -25,6 +25,7 @@ discIs: thm list, sel_thmss: thm list list, disc_exhausts: thm list, + sel_exhausts: thm list, collapses: thm list, expands: thm list, case_conv_ifs: thm list}; @@ -78,6 +79,7 @@ discIs: thm list, sel_thmss: thm list list, disc_exhausts: thm list, + sel_exhausts: thm list, collapses: thm list, expands: thm list, case_conv_ifs: thm list}; @@ -88,7 +90,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, collapses, expands, case_conv_ifs} = + disc_exhausts, sel_exhausts, collapses, expands, case_conv_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -106,6 +108,7 @@ discIs = map (Morphism.thm phi) discIs, sel_thmss = map (map (Morphism.thm phi)) sel_thmss, disc_exhausts = map (Morphism.thm phi) disc_exhausts, + sel_exhausts = map (Morphism.thm phi) sel_exhausts, collapses = map (Morphism.thm phi) collapses, expands = map (Morphism.thm phi) expands, case_conv_ifs = map (Morphism.thm phi) case_conv_ifs}; @@ -153,6 +156,7 @@ val injectN = "inject"; val nchotomyN = "nchotomy"; val selN = "sel"; +val sel_exhaustN = "sel_exhaust"; val splitN = "split"; val splitsN = "splits"; val split_asmN = "split_asm"; @@ -415,10 +419,10 @@ 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, vdiscs, vselss, disc_defs, sel_defs, - sel_defss, lthy') = + val (all_sels_distinct, discs, selss, udiscs, uselss, usel_ctrs, vdiscs, vselss, 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); @@ -504,12 +508,13 @@ 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, vdiscs, vselss, disc_defs, sel_defs, - sel_defss, lthy') + (all_sels_distinct, discs, selss, udiscs, uselss, usel_ctrs, vdiscs, vselss, disc_defs, + sel_defs, sel_defss, lthy') end; fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); @@ -585,10 +590,10 @@ end; val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, - disc_exclude_thms, disc_exhaust_thms, all_collapse_thms, safe_collapse_thms, - expand_thms, case_conv_if_thms) = + disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, + safe_collapse_thms, expand_thms, case_conv_if_thms) = if no_discs_sels then - ([], [], [], [], [], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], [], [], [], [], []) else let fun make_sel_thm xs' case_thm sel_def = @@ -711,15 +716,14 @@ val (safe_collapse_thms, all_collapse_thms) = let - fun mk_goal ctr udisc usels = + fun mk_goal m ctr udisc usel_ctr = let val prem = HOLogic.mk_Trueprop udisc; - val concl = - mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u)); + val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap); in (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl))) end; - val (trivs, goals) = map3 mk_goal ctrs udiscs uselss |> split_list; + val (trivs, goals) = map4 mk_goal ms ctrs udiscs usel_ctrs |> split_list; val thms = map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => @@ -732,6 +736,19 @@ thms) end; + val swapped_all_collapse_thms = + map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms; + + val sel_exhaust_thm = + let + fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)]; + val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs)); + in + Goal.prove_sorry lthy [] [] goal (fn _ => + mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms) + |> Thm.close_derivation + end; + val expand_thms = let fun mk_prems k udisc usels vdisc vsels = @@ -770,8 +787,8 @@ end; in (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, - nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], all_collapse_thms, - safe_collapse_thms, expand_thms, case_conv_if_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) end; val (case_cong_thm, weak_case_cong_thm) = @@ -838,6 +855,7 @@ (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), (selN, all_sel_thms, code_nitpick_simp_simp_attrs), + (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []), @@ -856,7 +874,8 @@ case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm, split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss, discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms, - collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms}; + sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms, + case_conv_ifs = case_conv_if_thms}; in (ctr_sugar, lthy diff -r 0e2c4dff5d13 -r 37c31a619eee src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 13:34:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 13:42:13 2013 +0200 @@ -19,6 +19,7 @@ val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic 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_asm_tac: Proof.context -> thm -> tactic @@ -56,10 +57,16 @@ fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half); -fun mk_disc_exhaust_tac n exhaust discIs = +fun mk_disc_or_sel_exhaust_tac n exhaust destIs = HEADGOAL (rtac exhaust THEN' - EVERY' (map2 (fn k => fn discI => - dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)); + EVERY' (map2 (fn k => fn destI => dtac destI THEN' + select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs)); + +val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac; + +fun mk_sel_exhaust_tac n disc_exhaust collapses = + if n = 1 then HEADGOAL (etac meta_mp THEN' resolve_tac collapses) + else mk_disc_or_sel_exhaust_tac n disc_exhaust collapses; fun mk_collapse_tac ctxt m discD sels = HEADGOAL (dtac discD THEN'