# HG changeset patch # User blanchet # Date 1380057016 -7200 # Node ID c9aefa1fc451d7c3ff4fa25f507a18073dd401d8 # Parent 54c8dee1295add83161267d0c96a10621ef45c3b renamed generated property diff -r 54c8dee1295a -r c9aefa1fc451 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 22:21:51 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 23:10:16 2013 +0200 @@ -784,8 +784,8 @@ \item[@{text "t."}\hthm{expand}\rm:] ~ \\ @{thm list.expand[no_vars]} -\item[@{text "t."}\hthm{case\_conv}\rm:] ~ \\ -@{thm list.case_conv[no_vars]} +\item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ +@{thm list.case_conv_if[no_vars]} \end{description} \end{indentblock} diff -r 54c8dee1295a -r c9aefa1fc451 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Sep 24 22:21:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Sep 24 23:10:16 2013 +0200 @@ -27,7 +27,7 @@ disc_exhausts: thm list, collapses: thm list, expands: thm list, - case_convs: thm list}; + case_conv_ifs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar @@ -76,11 +76,11 @@ disc_exhausts: thm list, collapses: thm list, expands: thm list, - case_convs: thm list}; + case_conv_ifs: thm list}; 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_convs} = + disc_exhausts, collapses, expands, case_conv_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -100,7 +100,7 @@ disc_exhausts = map (Morphism.thm phi) disc_exhausts, collapses = map (Morphism.thm phi) collapses, expands = map (Morphism.thm phi) expands, - case_convs = map (Morphism.thm phi) case_convs}; + case_conv_ifs = map (Morphism.thm phi) case_conv_ifs}; val rep_compat_prefix = "new"; @@ -111,7 +111,7 @@ val caseN = "case"; val case_congN = "case_cong"; -val case_convN = "case_conv"; +val case_conv_ifN = "case_conv_if"; val collapseN = "collapse"; val disc_excludeN = "disc_exclude"; val disc_exhaustN = "disc_exhaust"; @@ -523,7 +523,7 @@ 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_thms) = + expand_thms, case_conv_if_thms) = if no_discs_sels then ([], [], [], [], [], [], [], [], [], [], [], []) else @@ -695,20 +695,20 @@ |> Proof_Context.export names_lthy lthy end; - val case_conv_thms = + 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)); in [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] + mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)] |> map Thm.close_derivation |> Proof_Context.export names_lthy lthy 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_thms) + safe_collapse_thms, expand_thms, case_conv_if_thms) end; val (case_cong_thm, weak_case_cong_thm) = @@ -763,7 +763,7 @@ val notes = [(caseN, case_thms, code_nitpick_simp_simp_attrs), (case_congN, [case_cong_thm], []), - (case_convN, case_conv_thms, []), + (case_conv_ifN, case_conv_if_thms, []), (collapseN, safe_collapse_thms, simp_attrs), (discN, nontriv_disc_thms, simp_attrs), (discIN, nontriv_discI_thms, []), @@ -792,7 +792,7 @@ 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_convs = case_conv_thms}, + collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms}, lthy |> not rep_compat ? (Local_Theory.declaration {syntax = false, pervasive = true} diff -r 54c8dee1295a -r c9aefa1fc451 src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Sep 24 22:21:51 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Sep 24 23:10:16 2013 +0200 @@ -10,8 +10,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_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> - tactic + val mk_case_conv_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 -> @@ -123,7 +123,7 @@ else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) end; -fun mk_case_conv_tac ctxt n uexhaust cases discss' selss = +fun mk_case_conv_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)),