# HG changeset patch # User blanchet # Date 1348155349 -7200 # Node ID 0194a18f80cf725eda3994d951d9504c1cf45a84 # Parent 470e612db99ab48fd990c53efe248ee1892eedb5 finished "disc_coiter_iff" etc. generation diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 17:35:49 2012 +0200 @@ -77,7 +77,6 @@ val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list val wits_of_bnf: BNF -> nonemptiness_witness list - val no_reflexive: thm list -> thm list val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline @@ -513,13 +512,6 @@ val smart_max_inline_size = 25; (*FUDGE*) -fun is_refl thm = - op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm))) - handle TERM _ => false; - -val no_refl = filter_out is_refl; -val no_reflexive = filter_out Thm.is_reflexive; - (* Define new BNFs *) diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 17:35:49 2012 +0200 @@ -20,11 +20,11 @@ val coinductN: string val coiterN: string val coitersN: string - val coiter_iffN: string val corecN: string val corecsN: string - val corec_iffN: string + val disc_coiter_iffN: string val disc_coitersN: string + val disc_corec_iffN: string val disc_corecsN: string val exhaustN: string val fldN: string @@ -240,8 +240,8 @@ val disc_coitersN = discN ^ "_" ^ coitersN val disc_corecsN = discN ^ "_" ^ corecsN val iffN = "_iff" -val coiter_iffN = coiterN ^ iffN -val corec_iffN = corecN ^ iffN +val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN +val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN val selN = "sel" val sel_coitersN = selN ^ "_" ^ coitersN val sel_corecsN = selN ^ "_" ^ corecsN diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 17:35:49 2012 +0200 @@ -227,8 +227,9 @@ val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1))); val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1))); - val ((iter_only as (gss, _, _), rec_only as (hss, _, _)), - (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) = + val (((iter_only as (gss, _, _), rec_only as (hss, _, _)), + (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))), + names_lthy) = if lfp then let val y_Tsss = @@ -236,7 +237,7 @@ ns mss fp_iter_fun_Ts; val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css; - val ((gss, ysss), _) = + val ((gss, ysss), lthy) = lthy |> mk_Freess "f" g_Tss ||>> mk_Freesss "x" y_Tsss; @@ -253,13 +254,13 @@ val hss = map2 (map2 retype_free) h_Tss gss; val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss; - val (zssss_tl, _) = + val (zssss_tl, lthy) = lthy |> mk_Freessss "y" (map (map (map tl)) z_Tssss); val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; in - (((gss, g_Tss, yssss), (hss, h_Tss, zssss)), - ([], [], [], (([], []), ([], [])), (([], []), ([], [])))) + ((((gss, g_Tss, yssss), (hss, h_Tss, zssss)), + ([], [], [], (([], []), ([], [])), (([], []), ([], [])))), lthy) end else let @@ -288,7 +289,7 @@ val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts; - val ((((Free (z, _), cs), pss), gssss), _) = + val ((((Free (z, _), cs), pss), gssss), lthy) = lthy |> yield_singleton (mk_Frees "z") dummyT ||>> mk_Frees "a" Cs @@ -303,7 +304,7 @@ val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts; val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss; - val ((sssss, hssss_tl), _) = + val ((sssss, hssss_tl), lthy) = lthy |> mk_Freessss "q" s_Tssss ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); @@ -323,9 +324,9 @@ val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss; in (pfss, cqfsss) end; in - ((([], [], []), ([], [], [])), - ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)), - (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) + (((([], [], []), ([], [], [])), + ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)), + (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy) end; fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec), @@ -518,7 +519,7 @@ in Term.list_comb (mapx, args) end; val mk_simp_thmss = - map3 (fn (_, injects, distincts, cases, _, _) => fn rec_likes => fn iter_likes => + map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes => injects @ distincts @ cases @ rec_likes @ iter_likes); fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss, @@ -594,8 +595,7 @@ val goal = Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, - HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 (curry (op $)) phis vs))); + HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs))); val kksss = map (map (map (fst o snd) o #2)) raw_premss; @@ -619,7 +619,7 @@ val giters = map (lists_bmoc gss) iters; val hrecs = map (lists_bmoc hss) recs; - fun mk_iter_like_goal fss fiter_like xctr f xs fxs = + fun mk_goal fss fiter_like xctr f xs fxs = fold_rev (fold_rev Logic.all) (xs :: fss) (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs))); @@ -645,8 +645,8 @@ val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss; val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss; - val iterss_goal = map5 (map4 o mk_iter_like_goal gss) giters xctrss gss xsss gxsss; - val recss_goal = map5 (map4 o mk_iter_like_goal hss) hrecs xctrss hss xsss hxsss; + val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss; + val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss; val iter_tacss = map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms @@ -654,11 +654,11 @@ val rec_tacss = map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms ctr_defss; + + fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context); in - (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) - iterss_goal iter_tacss, - map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context))) - recss_goal rec_tacss) + (map2 (map2 prove) iter_goalss iter_tacss, + map2 (map2 prove) rec_goalss rec_tacss) end; val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss; @@ -690,9 +690,11 @@ fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _, ctr_defss, coiter_defs, corec_defs), lthy) = let - val selsss = map #1 wrap_ress; - val discIss = map #5 wrap_ress; - val sel_thmsss = map #6 wrap_ress; + val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress; + val selsss = map #2 wrap_ress; + val disc_thmsss = map #6 wrap_ress; + val discIss = map #7 wrap_ress; + val sel_thmsss = map #8 wrap_ress; val (vs', _) = lthy @@ -707,17 +709,17 @@ `(conj_dests nn) coinduct_thm end; + fun mk_maybe_not pos = not pos ? HOLogic.mk_not; + + val z = the_single zs; + val gcoiters = map (lists_bmoc pgss) coiters; + val hcorecs = map (lists_bmoc phss) corecs; + val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) = let - val z = the_single zs; - val gcoiters = map (lists_bmoc pgss) coiters; - val hcorecs = map (lists_bmoc phss) corecs; - - fun mk_cond_goal pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); - - fun mk_coiter_like_goal pfss c cps fcoiter_like n k ctr m cfs' = + fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) - (Logic.list_implies (seq_conds mk_cond_goal n k cps, + (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs')))); fun build_call fiter_likes maybe_tack (T, U) = @@ -742,10 +744,10 @@ val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss; val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss; - val coiterss_goal = - map8 (map4 oooo mk_coiter_like_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; - val corecss_goal = - map8 (map4 oooo mk_coiter_like_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; + val coiter_goalss = + map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss'; + val corec_goalss = + map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; val coiter_tacss = map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs @@ -754,15 +756,13 @@ map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs ctr_defss; - val coiter_thmss = - map2 (map2 (fn goal => fn tac => - Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation)) - coiterss_goal coiter_tacss; + fun prove goal tac = + Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation; + + val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss; val corec_thmss = - map2 (map2 (fn goal => fn tac => - Skip_Proof.prove lthy [] [] goal (tac o #context) - |> unfold_defs lthy @{thms sum_case_if} |> Thm.close_derivation)) - corecss_goal corec_tacss; + map2 (map2 prove) corec_goalss corec_tacss + |> map (map (unfold_defs lthy @{thms sum_case_if})); val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss; val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss; @@ -777,14 +777,36 @@ (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) end; - val (coiter_iff_thmss, corec_iff_thmss) = + val (disc_coiter_iff_thmss, disc_corec_iff_thmss) = let - (* TODO: smoothly handle the n = 1 case *) + fun mk_goal c cps fcoiter_like n k disc = + mk_Trueprop_eq (disc $ (fcoiter_like $ c), + if n = 1 then @{const True} + else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); + + val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss; + val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss; + + fun mk_case_split' cp = + Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split}; + + val case_splitss' = map (map mk_case_split') cpss; - val coiter_iff_thmss = []; - val corec_iff_thmss = []; + val coiter_tacss = + map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss; + val corec_tacss = + map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss; + + fun prove goal tac = + Skip_Proof.prove lthy [] [] goal (tac o #context) + |> Thm.close_derivation + |> singleton (Proof_Context.export names_lthy no_defs_lthy); + + fun proves [_] [_] = [] + | proves goals tacs = map2 prove goals tacs; in - (coiter_iff_thmss, corec_iff_thmss) + (map2 proves coiter_goalss coiter_tacss, + map2 proves corec_goalss corec_tacss) end; fun mk_disc_coiter_like_thms coiter_likes discIs = @@ -831,10 +853,10 @@ val notes = [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *) (coitersN, coiter_thmss, []), - (coiter_iffN, coiter_iff_thmss, simp_attrs), (corecsN, corec_thmss, []), - (corec_iffN, corec_iff_thmss, simp_attrs), + (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs), (disc_coitersN, disc_coiter_thmss, simp_attrs), + (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs), (disc_corecsN, disc_corec_thmss, simp_attrs), (sel_coitersN, sel_coiter_thmss, simp_attrs), (sel_corecsN, sel_corec_thmss, simp_attrs), diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 17:35:49 2012 +0200 @@ -9,8 +9,7 @@ sig val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic - val mk_coiter_like_iff_tac: Proof.context -> int -> int -> thm list -> thm list -> - thm list list -> tactic + val mk_disc_coiter_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic @@ -71,13 +70,13 @@ unfold_defs_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1; -val iter_like_thms = +val iter_like_unfold_thms = @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps split_conv}; fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt = unfold_defs_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @ - iter_like_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1; + iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1; val coiter_like_ss = ss_only @{thms if_True if_False}; val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases}; @@ -89,13 +88,12 @@ unfold_defs_tac ctxt @{thms id_def} THEN TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1); -fun mk_coiter_like_iff_tac ctxt n k case_splits' coiter_like_thms distinctss = - EVERY (map4 (fn k' => fn case_split_tac => fn coiter_like_thm => fn distincts => - case_split_tac 1 THEN - unfold_defs_tac ctxt [coiter_like_thm] THEN +fun mk_disc_coiter_like_iff_tac case_splits' coiter_likes discs ctxt = + EVERY (map3 (fn case_split_tac => fn coiter_like_thm => fn disc => + case_split_tac 1 THEN unfold_defs_tac ctxt [coiter_like_thm] THEN asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN - (if k' = k then all_tac else rtac (the_single distincts) 1)) - (1 upto n) (map rtac case_splits' @ [K all_tac]) coiter_like_thms distinctss); + (if is_refl disc then all_tac else rtac disc 1)) + (map rtac case_splits' @ [K all_tac]) coiter_likes discs); val solve_prem_prem_tac = REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE' @@ -109,8 +107,7 @@ fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs = EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp, - SELECT_GOAL (unfold_defs_tac ctxt - (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), + SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)), solve_prem_prem_tac]) (rev kks)) 1; fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks = diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 17:35:49 2012 +0200 @@ -125,6 +125,10 @@ val mk_trans: thm -> thm -> thm val mk_unabs_def: int -> thm -> thm + val is_refl: thm -> bool + val no_refl: thm list -> thm list + val no_reflexive: thm list -> thm list + val fold_defs: Proof.context -> thm list -> thm -> thm val unfold_defs: Proof.context -> thm list -> thm -> thm @@ -592,6 +596,13 @@ fun mk_unabs_def 0 thm = thm | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]}; +fun is_refl thm = + op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm))) + handle TERM _ => false; + +val no_refl = filter_out is_refl; +val no_reflexive = filter_out Thm.is_reflexive; + fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms); fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 17:35:49 2012 +0200 @@ -9,11 +9,13 @@ sig val mk_half_pairss: 'a list -> ('a * 'a) list list val mk_ctr: typ list -> term -> term + val mk_disc_or_sel: typ list -> term -> term val base_name_of_ctr: term -> string val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list -> ((bool * term list) * term) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> - (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory + (term list * term list list * thm list * thm list * thm list * thm list list * thm list * + thm list list) * local_theory val parse_wrap_options: bool parser val parse_bound_term: (binding * string) parser end; @@ -70,6 +72,9 @@ Term.subst_atomic_types (Ts0 ~~ Ts) ctr end; +fun mk_disc_or_sel Ts t = + Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; + fun base_name_of_ctr c = Long_Name.base_name (case head_of c of Const (s, _) => s @@ -279,9 +284,6 @@ val discs0 = map (Morphism.term phi) raw_discs; val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); - fun mk_disc_or_sel Ts c = - Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c; - val discs = map (mk_disc_or_sel As) discs0; val selss = map (map (mk_disc_or_sel As)) selss0; in @@ -295,7 +297,7 @@ fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss)) end; - val injectss_goal = + val inject_goalss = let fun mk_goal _ _ [] [] = [] | mk_goal xctr yctr xs ys = @@ -305,7 +307,7 @@ map4 mk_goal xctrs yctrs xss yss end; - val half_distinctss_goal = + val half_distinct_goalss = let fun mk_goal ((xs, xc), (xs', xc')) = fold_rev Logic.all (xs @ xs') @@ -318,7 +320,7 @@ map3 (fn xs => fn xctr => fn xf => fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; - val goalss = [exhaust_goal] :: injectss_goal @ half_distinctss_goal @ [cases_goal]; + val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; fun after_qed thmss lthy = let @@ -352,10 +354,10 @@ Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) end; - val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, - collapse_thms, case_eq_thms) = + val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, + disc_exhaust_thms, collapse_thms, case_eq_thms) = if no_dests then - ([], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], []) else let fun make_sel_thm xs' case_thm sel_def = @@ -444,16 +446,16 @@ val infos = ms ~~ discD_thms ~~ discs ~~ no_discs; val half_pairss = mk_half_pairss infos; - val halvess_goal = map mk_goal half_pairss; + val half_goalss = map mk_goal half_pairss; val half_thmss = map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) - halvess_goal half_pairss (flat disc_thmss'); + half_goalss half_pairss (flat disc_thmss'); - val other_halvess_goal = map (mk_goal o map swap) half_pairss; + val other_half_goalss = map (mk_goal o map swap) half_pairss; val other_half_thmss = map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss - other_halvess_goal; + other_half_goalss; in interleave (flat half_thmss) (flat other_half_thmss) end; @@ -508,8 +510,8 @@ |> Proof_Context.export names_lthy lthy end; in - (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, - collapse_thms, case_eq_thms) + (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, + disc_exhaust_thms, collapse_thms, case_eq_thms) end; val (case_cong_thm, weak_case_cong_thm) = @@ -586,7 +588,7 @@ [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); in - ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss), + ((discs, selss, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd) end; in diff -r 470e612db99a -r 0194a18f80cf src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 17:25:07 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 17:35:49 2012 +0200 @@ -43,47 +43,40 @@ (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1; -fun mk_half_disc_exclude_tac m discD disc'_thm = - (dtac discD THEN' - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - rtac disc'_thm) 1; +fun mk_half_disc_exclude_tac m discD disc' = + (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1; -fun mk_other_half_disc_exclude_tac half_thm = - (etac @{thm contrapos_pn} THEN' etac half_thm) 1; +fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1; fun mk_disc_exhaust_tac n exhaust discIs = (rtac exhaust THEN' EVERY' (map2 (fn k => fn discI => dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; -fun mk_collapse_tac ctxt m discD sel_thms = +fun mk_collapse_tac ctxt m discD sels = (dtac discD THEN' (if m = 0 then atac else - REPEAT_DETERM_N m o etac exE THEN' - hyp_subst_tac THEN' - SELECT_GOAL (unfold_defs_tac ctxt sel_thms) THEN' - rtac refl)) 1; + REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' + SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1; -fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss = +fun mk_case_eq_tac ctxt n exhaust' cases discss' selss = (rtac exhaust' THEN' - EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => - EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_disc_thms @ sel_thms)), - rtac case_thm]) - case_thms (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) disc_thmss') sel_thmss)) 1; + EVERY' (map3 (fn casex => fn if_discs => fn sels => + EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex]) + cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; -fun mk_case_cong_tac exhaust' case_thms = +fun mk_case_cong_tac exhaust' cases = (rtac exhaust' THEN' - EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; + EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; val naked_ctxt = Proof_Context.init_global @{theory HOL}; -fun mk_split_tac exhaust' case_thms injectss distinctsss = +fun mk_split_tac exhaust' cases injectss distinctsss = rtac exhaust' 1 THEN ALLGOALS (fn k => (hyp_subst_tac THEN' - simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ + simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ flat (nth distinctsss (k - 1))))) k) THEN ALLGOALS (blast_tac naked_ctxt);