# HG changeset patch # User blanchet # Date 1384342346 -3600 # Node ID 4ca60c4301472b72be1757f9eff3f341f3408ae0 # Parent 632be352a5a3152c76d0d912bed77a087d8a6037 shortened generated property name diff -r 632be352a5a3 -r 4ca60c430147 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Nov 13 10:53:36 2013 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Nov 13 12:32:26 2013 +0100 @@ -810,8 +810,8 @@ \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]} +\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\ +@{thm list.case_if[no_vars]} \end{description} \end{indentblock} diff -r 632be352a5a3 -r 4ca60c430147 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 13 10:53:36 2013 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 13 12:32:26 2013 +0100 @@ -118,7 +118,7 @@ expands = [], sel_splits = [], sel_split_asms = [], - case_conv_ifs = []}; + case_ifs = []}; fun register dt_infos = Data.map (fn {types, constrs, cases} => diff -r 632be352a5a3 -r 4ca60c430147 src/HOL/Tools/ctr_sugar.ML --- a/src/HOL/Tools/ctr_sugar.ML Wed Nov 13 10:53:36 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar.ML Wed Nov 13 12:32:26 2013 +0100 @@ -30,7 +30,7 @@ expands: thm list, sel_splits: thm list, sel_split_asms: thm list, - case_conv_ifs: thm list}; + case_ifs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar @@ -90,7 +90,7 @@ expands: thm list, sel_splits: thm list, sel_split_asms: thm list, - case_conv_ifs: thm list}; + case_ifs: thm list}; fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) = @@ -98,7 +98,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, sel_splits, sel_split_asms, case_conv_ifs} = + disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -121,7 +121,7 @@ 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}; + case_ifs = map (Morphism.thm phi) case_ifs}; val transfer_ctr_sugar = morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of; @@ -160,7 +160,7 @@ val caseN = "case"; val case_congN = "case_cong"; -val case_conv_ifN = "case_conv_if"; +val case_ifN = "case_if"; val collapseN = "collapse"; val disc_excludeN = "disc_exclude"; val disc_exhaustN = "disc_exhaust"; @@ -657,8 +657,7 @@ 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, sel_split_thms, sel_split_asm_thms, - case_conv_if_thms) = + safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) = if no_discs_sels then ([], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else @@ -862,12 +861,12 @@ (thm, asm_thm) end; - val case_conv_if_thm = + val case_if_thm = let 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) + mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -875,7 +874,7 @@ (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_thm], [sel_split_thm], - [sel_split_asm_thm], [case_conv_if_thm]) + [sel_split_asm_thm], [case_if_thm]) end; val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); @@ -891,7 +890,7 @@ val notes = [(caseN, case_thms, code_nitpicksimp_simp_attrs), (case_congN, [case_cong_thm], []), - (case_conv_ifN, case_conv_if_thms, []), + (case_ifN, case_if_thms, []), (collapseN, safe_collapse_thms, simp_attrs), (discN, nontriv_disc_thms, simp_attrs), (discIN, nontriv_discI_thms, []), @@ -922,7 +921,7 @@ 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}; + case_ifs = case_if_thms}; in (ctr_sugar, lthy diff -r 632be352a5a3 -r 4ca60c430147 src/HOL/Tools/ctr_sugar_tactics.ML --- a/src/HOL/Tools/ctr_sugar_tactics.ML Wed Nov 13 10:53:36 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_tactics.ML Wed Nov 13 12:32:26 2013 +0100 @@ -18,8 +18,8 @@ val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic - val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> - thm list list -> tactic + val mk_case_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> + tactic val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> @@ -143,7 +143,7 @@ else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) end; -fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss = +fun mk_case_if_tac ctxt n uexhaust cases discss' selss = HEADGOAL (rtac uexhaust THEN' EVERY' (map3 (fn casex => fn if_discs => fn sels => EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),