1.1 --- a/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 22:21:51 2013 +0200
1.2 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Sep 24 23:10:16 2013 +0200
1.3 @@ -784,8 +784,8 @@
1.4 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
1.5 @{thm list.expand[no_vars]}
1.6
1.7 -\item[@{text "t."}\hthm{case\_conv}\rm:] ~ \\
1.8 -@{thm list.case_conv[no_vars]}
1.9 +\item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
1.10 +@{thm list.case_conv_if[no_vars]}
1.11
1.12 \end{description}
1.13 \end{indentblock}
2.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Sep 24 22:21:51 2013 +0200
2.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Sep 24 23:10:16 2013 +0200
2.3 @@ -27,7 +27,7 @@
2.4 disc_exhausts: thm list,
2.5 collapses: thm list,
2.6 expands: thm list,
2.7 - case_convs: thm list};
2.8 + case_conv_ifs: thm list};
2.9
2.10 val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
2.11
2.12 @@ -76,11 +76,11 @@
2.13 disc_exhausts: thm list,
2.14 collapses: thm list,
2.15 expands: thm list,
2.16 - case_convs: thm list};
2.17 + case_conv_ifs: thm list};
2.18
2.19 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
2.20 case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
2.21 - disc_exhausts, collapses, expands, case_convs} =
2.22 + disc_exhausts, collapses, expands, case_conv_ifs} =
2.23 {ctrs = map (Morphism.term phi) ctrs,
2.24 casex = Morphism.term phi casex,
2.25 discs = map (Morphism.term phi) discs,
2.26 @@ -100,7 +100,7 @@
2.27 disc_exhausts = map (Morphism.thm phi) disc_exhausts,
2.28 collapses = map (Morphism.thm phi) collapses,
2.29 expands = map (Morphism.thm phi) expands,
2.30 - case_convs = map (Morphism.thm phi) case_convs};
2.31 + case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
2.32
2.33 val rep_compat_prefix = "new";
2.34
2.35 @@ -111,7 +111,7 @@
2.36
2.37 val caseN = "case";
2.38 val case_congN = "case_cong";
2.39 -val case_convN = "case_conv";
2.40 +val case_conv_ifN = "case_conv_if";
2.41 val collapseN = "collapse";
2.42 val disc_excludeN = "disc_exclude";
2.43 val disc_exhaustN = "disc_exhaust";
2.44 @@ -523,7 +523,7 @@
2.45
2.46 val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
2.47 disc_exclude_thms, disc_exhaust_thms, all_collapse_thms, safe_collapse_thms,
2.48 - expand_thms, case_conv_thms) =
2.49 + expand_thms, case_conv_if_thms) =
2.50 if no_discs_sels then
2.51 ([], [], [], [], [], [], [], [], [], [], [], [])
2.52 else
2.53 @@ -695,20 +695,20 @@
2.54 |> Proof_Context.export names_lthy lthy
2.55 end;
2.56
2.57 - val case_conv_thms =
2.58 + val case_conv_if_thms =
2.59 let
2.60 fun mk_body f usels = Term.list_comb (f, usels);
2.61 val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
2.62 in
2.63 [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
2.64 - mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
2.65 + mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
2.66 |> map Thm.close_derivation
2.67 |> Proof_Context.export names_lthy lthy
2.68 end;
2.69 in
2.70 (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
2.71 nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], all_collapse_thms,
2.72 - safe_collapse_thms, expand_thms, case_conv_thms)
2.73 + safe_collapse_thms, expand_thms, case_conv_if_thms)
2.74 end;
2.75
2.76 val (case_cong_thm, weak_case_cong_thm) =
2.77 @@ -763,7 +763,7 @@
2.78 val notes =
2.79 [(caseN, case_thms, code_nitpick_simp_simp_attrs),
2.80 (case_congN, [case_cong_thm], []),
2.81 - (case_convN, case_conv_thms, []),
2.82 + (case_conv_ifN, case_conv_if_thms, []),
2.83 (collapseN, safe_collapse_thms, simp_attrs),
2.84 (discN, nontriv_disc_thms, simp_attrs),
2.85 (discIN, nontriv_discI_thms, []),
2.86 @@ -792,7 +792,7 @@
2.87 case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
2.88 split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
2.89 discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
2.90 - collapses = all_collapse_thms, expands = expand_thms, case_convs = case_conv_thms},
2.91 + collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms},
2.92 lthy
2.93 |> not rep_compat ?
2.94 (Local_Theory.declaration {syntax = false, pervasive = true}
3.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Sep 24 22:21:51 2013 +0200
3.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Tue Sep 24 23:10:16 2013 +0200
3.3 @@ -10,8 +10,8 @@
3.4 val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
3.5 val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
3.6 val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
3.7 - val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
3.8 - tactic
3.9 + val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
3.10 + thm list list -> tactic
3.11 val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
3.12 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
3.13 val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
3.14 @@ -123,7 +123,7 @@
3.15 else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
3.16 end;
3.17
3.18 -fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
3.19 +fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
3.20 HEADGOAL (rtac uexhaust THEN'
3.21 EVERY' (map3 (fn casex => fn if_discs => fn sels =>
3.22 EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),