--- a/NEWS Mon Aug 18 15:03:25 2014 +0200
+++ b/NEWS Mon Aug 18 17:19:58 2014 +0200
@@ -17,6 +17,28 @@
*** HOL ***
+* New (co)datatype package:
+ - Renamed theorems:
+ disc_corec ~> corec_disc
+ disc_corec_iff ~> corec_disc_iff
+ disc_exclude ~> distinct_disc
+ disc_exhaust ~> exhaust_disc
+ disc_map_iff ~> map_disc_iff
+ sel_corec ~> corec_sel
+ sel_exhaust ~> exhaust_sel
+ sel_map ~> map_sel
+ sel_set ~> set_sel
+ sel_split ~> split_sel
+ sel_split_asm ~> split_sel_asm
+ strong_coinduct ~> coinduct_strong
+ weak_case_cong ~> case_cong_weak
+ INCOMPATIBILITY.
+
+* Old datatype package:
+ - Renamed theorems:
+ weak_case_cong ~> case_cong_weak
+ INCOMPATIBILITY.
+
* Sledgehammer:
- Minimization is now always enabled by default.
Removed subcommand:
--- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 17:19:58 2014 +0200
@@ -773,8 +773,8 @@
\item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.case_cong[no_vars]}
-\item[@{text "t."}\hthm{weak_case_cong} @{text "[cong]"}\rm:] ~ \\
-@{thm list.weak_case_cong[no_vars]}
+\item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
+@{thm list.case_cong_weak[no_vars]}
\item[@{text "t."}\hthm{split}\rm:] ~ \\
@{thm list.split[no_vars]}
@@ -809,27 +809,27 @@
@{thm list.collapse(1)[no_vars]} \\
@{thm list.collapse(2)[no_vars]}
-\item[@{text "t."}\hthm{disc_exclude} @{text "[dest]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
These properties are missing for @{typ "'a list"} because there is only one
proper discriminator. Had the datatype been introduced with a second
discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
@{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
@{prop "nonnull list \<Longrightarrow> \<not> null list"}
-\item[@{text "t."}\hthm{disc_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
-@{thm list.disc_exhaust[no_vars]}
-
-\item[@{text "t."}\hthm{sel_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
-@{thm list.sel_exhaust[no_vars]}
+\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+@{thm list.exhaust_disc[no_vars]}
+
+\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+@{thm list.exhaust_sel[no_vars]}
\item[@{text "t."}\hthm{expand}\rm:] ~ \\
@{thm list.expand[no_vars]}
-\item[@{text "t."}\hthm{sel_split}\rm:] ~ \\
-@{thm list.sel_split[no_vars]}
-
-\item[@{text "t."}\hthm{sel_split_asm}\rm:] ~ \\
-@{thm list.sel_split_asm[no_vars]}
+\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
+@{thm list.split_sel[no_vars]}
+
+\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
+@{thm list.split_sel_asm[no_vars]}
\item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
@{thm list.case_eq_if[no_vars]}
@@ -868,18 +868,18 @@
@{thm list.set_intros(1)[no_vars]} \\
@{thm list.set_intros(2)[no_vars]}
-\item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
-@{thm list.sel_set[no_vars]}
+\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
+@{thm list.set_sel[no_vars]}
\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}
-\item[@{text "t."}\hthm{disc_map_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm list.disc_map_iff[no_vars]}
-
-\item[@{text "t."}\hthm{sel_map}\rm:] ~ \\
-@{thm list.sel_map[no_vars]}
+\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
+@{thm list.map_disc_iff[no_vars]}
+
+\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
+@{thm list.map_sel[no_vars]}
\item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@@ -1772,10 +1772,10 @@
@{thm llist.coinduct[no_vars]}
\item[\begin{tabular}{@ {}l@ {}}
- @{text "t."}\hthm{strong_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
+ @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
\end{tabular}] ~ \\
-@{thm llist.strong_coinduct[no_vars]}
+@{thm llist.coinduct_strong[no_vars]}
\item[\begin{tabular}{@ {}l@ {}}
@{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
@@ -1786,8 +1786,8 @@
\item[\begin{tabular}{@ {}l@ {}}
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
- @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
- \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
+ @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
+ \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
\phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
\end{tabular}] ~ \\
@@ -1808,17 +1808,17 @@
\item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
@{thm llist.corec_code[no_vars]}
-\item[@{text "t."}\hthm{disc_corec}\rm:] ~ \\
-@{thm llist.disc_corec(1)[no_vars]} \\
-@{thm llist.disc_corec(2)[no_vars]}
-
-\item[@{text "t."}\hthm{disc_corec_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.disc_corec_iff(1)[no_vars]} \\
-@{thm llist.disc_corec_iff(2)[no_vars]}
-
-\item[@{text "t."}\hthm{sel_corec} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.sel_corec(1)[no_vars]} \\
-@{thm llist.sel_corec(2)[no_vars]}
+\item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
+@{thm llist.corec_disc(1)[no_vars]} \\
+@{thm llist.corec_disc(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
+@{thm llist.corec_disc_iff(1)[no_vars]} \\
+@{thm llist.corec_disc_iff(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
+@{thm llist.corec_sel(1)[no_vars]} \\
+@{thm llist.corec_sel(2)[no_vars]}
\end{description}
\end{indentblock}
@@ -1829,7 +1829,7 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec_iff}] @{text t.sel_corec} ~ \\
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\
@{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
\end{description}
@@ -2151,7 +2151,7 @@
@{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
@{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
@{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
-and analogously for @{text strong_coinduct}. These rules and the
+and analogously for @{text coinduct_strong}. These rules and the
underlying corecursors are generated on a per-need basis and are kept in a cache
to speed up subsequent definitions.
*}
--- a/src/Doc/Logics/document/HOL.tex Mon Aug 18 15:03:25 2014 +0200
+++ b/src/Doc/Logics/document/HOL.tex Mon Aug 18 17:19:58 2014 +0200
@@ -1709,7 +1709,7 @@
the arms of the \texttt{case}-construct exposed and simplified. To ensure
full simplification of all parts of a \texttt{case}-construct for datatype
$t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
- example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
+ example by \texttt{delcongs [thm "$t$.case_cong_weak"]}.
\end{warn}
\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Aug 18 17:19:58 2014 +0200
@@ -75,7 +75,7 @@
lemma unfold:
"root (unfold rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
+using dtree.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
apply blast
unfolding cont_def comp_def
by (simp add: case_sum_o_inj map_sum.compositionality image_image)
@@ -83,7 +83,7 @@
lemma corec:
"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
-using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
+using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
unfolding cont_def comp_def id_def
by simp_all
--- a/src/HOL/BNF_Examples/Process.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/BNF_Examples/Process.thy Mon Aug 18 17:19:58 2014 +0200
@@ -29,7 +29,7 @@
(* Constructors versus discriminators *)
theorem isAction_isChoice:
"isAction p \<or> isChoice p"
-by (rule process.disc_exhaust) auto
+by (rule process.exhaust_disc) auto
theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
by (cases rule: process.exhaust[of p]) auto
@@ -54,7 +54,7 @@
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
shows "p = p'"
using assms
- by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3))
+ by (coinduct rule: process.coinduct_strong) (metis process.collapse(1,2) process.disc(3))
subsection {* Coiteration (unfold) *}
--- a/src/HOL/BNF_Examples/Stream.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream.thy Mon Aug 18 17:19:58 2014 +0200
@@ -49,9 +49,9 @@
with Step prems show "P a s" by simp
qed
-lemmas smap_simps[simp] = stream.sel_map
-lemmas shd_sset = stream.sel_set(1)
-lemmas stl_sset = stream.sel_set(2)
+lemmas smap_simps[simp] = stream.map_sel
+lemmas shd_sset = stream.set_sel(1)
+lemmas stl_sset = stream.set_sel(2)
(* only for the non-mutual case: *)
theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]:
--- a/src/HOL/Bali/Basis.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Aug 18 17:19:58 2014 +0200
@@ -13,7 +13,7 @@
declare split_if_asm [split] option.split [split] option.split_asm [split]
setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
-declare if_weak_cong [cong del] option.weak_case_cong [cong del]
+declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
--- a/src/HOL/Bali/Conform.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Bali/Conform.thy Mon Aug 18 17:19:58 2014 +0200
@@ -521,7 +521,7 @@
apply auto
apply (simp only: obj_ty_cong)
apply (force dest: conforms_globsD intro!: lconf_upd
- simp add: oconf_def cong del: sum.weak_case_cong)
+ simp add: oconf_def cong del: sum.case_cong_weak)
done
lemma conforms_set_locals:
--- a/src/HOL/Library/RBT_Impl.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Mon Aug 18 17:19:58 2014 +0200
@@ -1754,7 +1754,7 @@
Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
compare.simps compare.exhaust compare.induct compare.rec compare.simps
- compare.size compare.case_cong compare.weak_case_cong compare.case
+ compare.size compare.case_cong compare.case_cong_weak compare.case
compare.nchotomy compare.split compare.split_asm rec_compare_def
compare.eq.refl compare.eq.simps
compare.EQ_def compare.GT_def compare.LT_def
--- a/src/HOL/Nat.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Nat.thy Mon Aug 18 17:19:58 2014 +0200
@@ -132,9 +132,9 @@
nat.collapse
nat.expand
nat.sel
- nat.sel_exhaust
- nat.sel_split
- nat.sel_split_asm
+ nat.exhaust_sel
+ nat.split_sel
+ nat.split_sel_asm
lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
-- {* for backward compatibility -- names of variables differ *}
--- a/src/HOL/Old_Number_Theory/Factorization.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy Mon Aug 18 17:19:58 2014 +0200
@@ -143,7 +143,7 @@
apply (induct xs)
apply simp
apply (case_tac xs)
- apply (simp_all cong del: list.weak_case_cong)
+ apply (simp_all cong del: list.case_cong_weak)
done
lemma nondec_sort: "nondec (sort xs)"
--- a/src/HOL/Product_Type.thy Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Product_Type.thy Mon Aug 18 17:19:58 2014 +0200
@@ -281,7 +281,7 @@
setup {* Sign.parent_path *}
declare prod.case [nitpick_simp del]
-declare prod.weak_case_cong [cong del]
+declare prod.case_cong_weak [cong del]
subsubsection {* Tuple syntax *}
@@ -486,7 +486,7 @@
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
- by (fact prod.weak_case_cong)
+ by (fact prod.case_cong_weak)
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
by (simp add: split_eta)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Aug 18 17:19:58 2014 +0200
@@ -99,13 +99,13 @@
val EqN = "Eq_";
val corec_codeN = "corec_code";
-val disc_map_iffN = "disc_map_iff";
-val sel_mapN = "sel_map";
-val sel_setN = "sel_set";
+val map_disc_iffN = "map_disc_iff";
+val map_selN = "map_sel";
val set_casesN = "set_cases";
val set_emptyN = "set_empty";
val set_introsN = "set_intros";
val set_inductN = "set_induct";
+val set_selN = "set_sel";
structure Data = Generic_Data
(
@@ -309,14 +309,14 @@
* (thm list list list * Args.src list);
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
- corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs),
- (sel_corecsss, sel_corec_attrs)) =
+ corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
+ (corec_selsss, corec_sel_attrs)) =
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
coinduct_attrs_pair),
map (map (Morphism.thm phi)) corecss,
- map (map (Morphism.thm phi)) disc_corecss,
- (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
- (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
+ map (map (Morphism.thm phi)) corec_discss,
+ (map (map (Morphism.thm phi)) corec_disc_iffss, corec_disc_iff_attrs),
+ (map (map (map (Morphism.thm phi))) corec_selsss, corec_sel_attrs)) : gfp_sugar_thms;
val transfer_gfp_sugar_thms =
morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -961,7 +961,7 @@
val rel_eqs = map rel_eq_of_bnf pre_bnfs;
val rel_monos = map rel_mono_of_bnf pre_bnfs;
val dtor_coinducts =
- [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
+ [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
in
map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
end;
@@ -1010,7 +1010,7 @@
|> map (map (unfold_thms lthy @{thms case_sum_if}))
end;
- val disc_corec_iff_thmss =
+ val corec_disc_iff_thmss =
let
fun mk_goal c cps gcorec n k disc =
mk_Trueprop_eq (disc $ (gcorec $ c),
@@ -1023,7 +1023,7 @@
val case_splitss' = map (map mk_case_split') cpss;
- val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
+ val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
fun prove goal tac =
Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -1037,11 +1037,11 @@
map2 proves goalss tacss
end;
- fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs);
+ fun mk_corec_disc_thms corecs discIs = map (op RS) (corecs ~~ discIs);
- val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
+ val corec_disc_thmss = map2 mk_corec_disc_thms corec_thmss discIss;
- fun mk_sel_corec_thm corec_thm sel sel_thm =
+ fun mk_corec_sel_thm corec_thm sel sel_thm =
let
val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
@@ -1053,17 +1053,17 @@
corec_thm RS arg_cong' RS sel_thm'
end;
- fun mk_sel_corec_thms corec_thmss =
- map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
+ fun mk_corec_sel_thms corec_thmss =
+ map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
- val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
+ val corec_sel_thmsss = mk_corec_sel_thms corec_thmss;
in
((coinduct_thms_pairs,
mk_coinduct_attributes fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss),
corec_thmss,
- disc_corec_thmss,
- (disc_corec_iff_thmss, simp_attrs),
- (sel_corec_thmsss, simp_attrs))
+ corec_disc_thmss,
+ (corec_disc_iff_thmss, simp_attrs),
+ (corec_sel_thmsss, simp_attrs))
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1498,7 +1498,7 @@
map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
rel_inject_thms ms;
- val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+ val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
(set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
let
val live_AsBs = filter (op <>) (As ~~ Bs);
@@ -1702,7 +1702,7 @@
(thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
end;
- val disc_map_iff_thms =
+ val map_disc_iff_thms =
let
val discsB = map (mk_disc_or_sel Bs) discs;
val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs;
@@ -1721,14 +1721,14 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_disc_map_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
map_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
end;
- val sel_map_thms =
+ val map_sel_thms =
let
fun mk_goal (discA, selA) =
let
@@ -1755,14 +1755,14 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_sel_map_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
map_thms (flat sel_thmss))
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
end;
- val sel_set_thms =
+ val set_sel_thms =
let
fun mk_goal discA selA setA ctxt =
let
@@ -1819,14 +1819,14 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
(flat sel_thmss) set0_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
end;
in
- (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+ (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
(set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
end;
@@ -1836,19 +1836,19 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- [(disc_map_iffN, disc_map_iff_thms, K simp_attrs),
- (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ [(mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
+ (map_selN, map_sel_thms, K []),
(rel_casesN, [rel_cases_thm], K rel_cases_attrs),
(rel_distinctN, rel_distinct_thms, K simp_attrs),
(rel_injectN, rel_inject_thms, K simp_attrs),
(rel_introsN, rel_intro_thms, K []),
(rel_selN, rel_sel_thms, K []),
(setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
- (sel_mapN, sel_map_thms, K []),
- (sel_setN, sel_set_thms, K []),
(set_casesN, set_cases_thms, nth set_cases_attrss),
(set_emptyN, set_empty_thms, K []),
- (set_introsN, set_intros_thms, K [])]
+ (set_introsN, set_intros_thms, K []),
+ (set_selN, set_sel_thms, K [])]
|> massage_simple_notes fp_b_name;
val (noted, lthy') =
@@ -1948,10 +1948,10 @@
((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
- val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
+ val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
(coinduct_attrs, common_coinduct_attrs)),
- corec_thmss, disc_corec_thmss,
- (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
+ corec_thmss, corec_disc_thmss,
+ (corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
@@ -1969,7 +1969,7 @@
[thm, eq_ifIN ctxt thms]));
val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
- val sel_corec_thmss = map flat sel_corec_thmsss;
+ val corec_sel_thmss = map flat corec_sel_thmsss;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
@@ -2001,39 +2001,39 @@
val simp_thmss =
map6 mk_simp_thms ctr_sugars
- (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
+ (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
mapss rel_injectss rel_distinctss setss;
val common_notes =
(set_inductN, set_induct_thms, nth set_induct_attrss) ::
(if nn > 1 then
[(coinductN, [coinduct_thm], K common_coinduct_attrs),
- (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs),
- (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)]
+ (coinduct_strongN, [coinduct_strong_thm], K common_coinduct_attrs),
+ (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs)]
else [])
|> massage_simple_notes fp_common_name;
val notes =
[(coinductN, map single coinduct_thms,
fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
+ (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
(corecN, corec_thmss, K []),
(corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
- (disc_corecN, disc_corec_thmss, K []),
- (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
+ (corec_discN, corec_disc_thmss, K []),
+ (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
+ (corec_selN, corec_sel_thmss, K corec_sel_attrs),
(rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
- (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
- (simpsN, simp_thmss, K []),
- (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
+ (simpsN, simp_thmss, K [])]
|> massage_multi_notes;
in
lthy
|> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
- [flat sel_corec_thmss, flat corec_thmss]
+ [flat corec_sel_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes)
|-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
- [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
- corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
+ [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms])
+ corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Aug 18 17:19:58 2014 +0200
@@ -17,15 +17,16 @@
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
thm list list list -> tactic
val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
- val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
- val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
+ val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
@@ -37,13 +38,12 @@
thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list -> tactic
- val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
- val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm list -> tactic
val mk_set_intros_tac: Proof.context -> thm list -> tactic
+ val mk_set_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
end;
structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -126,22 +126,13 @@
HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
end;
-fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
+fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
(map rtac case_splits' @ [K all_tac]) corecs discs);
-fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
- TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt maps THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
- handle THM _ => thm RS eqTrueI) discs) THEN
- ALLGOALS (rtac refl ORELSE' rtac TrueI);
-
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
@@ -221,6 +212,25 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
+fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
+ TRYALL Goal.conjunction_tac THEN
+ ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt maps THEN
+ unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
+ handle THM _ => thm RS eqTrueI) discs) THEN
+ ALLGOALS (rtac refl ORELSE' rtac TrueI);
+
+fun mk_map_sel_tac ctxt ct exhaust discs maps sels =
+ TRYALL Goal.conjunction_tac THEN
+ ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
+ @{thms not_True_eq_False not_False_eq_True}) THEN
+ TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
+ unfold_thms_tac ctxt (maps @ sels) THEN
+ ALLGOALS (rtac refl);
+
fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
@@ -280,17 +290,7 @@
(rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
TRYALL (resolve_tac [TrueI, refl]);
-fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
- TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
- @{thms not_True_eq_False not_False_eq_True}) THEN
- TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
- unfold_thms_tac ctxt (maps @ sels) THEN
- ALLGOALS (rtac refl);
-
-fun mk_sel_set_tac ctxt ct exhaust discs sels sets =
+fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Aug 18 17:19:58 2014 +0200
@@ -257,7 +257,7 @@
fp_bs xtor_co_recs lthy
|>> split_list;
- val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
+ val ((common_co_inducts, co_inductss, co_rec_thmss, corec_disc_thmss, corec_sel_thmsss),
fp_sugar_thms) =
if fp = Least_FP then
derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
@@ -272,30 +272,30 @@
dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
- |> `(fn ((coinduct_thms_pairs, _), corec_thmss, disc_corec_thmss, _,
- (sel_corec_thmsss, _)) =>
+ |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
+ (corec_sel_thmsss, _)) =>
(map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
- disc_corec_thmss, sel_corec_thmsss))
+ corec_disc_thmss, corec_sel_thmsss))
||> (fn info => (NONE, SOME info));
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
- co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
+ co_rec_def maps co_inducts co_rec_thms corec_disc_thms corec_sel_thmss
({rel_injects, rel_distincts, ...} : fp_sugar) =
{T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
- co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
- sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
+ co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = corec_disc_thms,
+ sel_co_recss = corec_sel_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
|> morph_fp_sugar phi;
val target_fp_sugars =
map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
- sel_corec_thmsss fp_sugars0;
+ co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss corec_disc_thmss
+ corec_sel_thmsss fp_sugars0;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Aug 18 17:19:58 2014 +0200
@@ -71,7 +71,10 @@
val caseN: string
val coN: string
val coinductN: string
+ val coinduct_strongN: string
val corecN: string
+ val corec_discN: string
+ val corec_disc_iffN: string
val ctorN: string
val ctor_dtorN: string
val ctor_exhaustN: string
@@ -91,8 +94,6 @@
val ctor_rel_inductN: string
val ctor_set_inclN: string
val ctor_set_set_inclN: string
- val disc_corecN: string
- val disc_corec_iffN: string
val dtorN: string
val dtor_coinductN: string
val dtor_corecN: string
@@ -103,13 +104,13 @@
val dtor_injectN: string
val dtor_mapN: string
val dtor_map_coinductN: string
- val dtor_map_strong_coinductN: string
+ val dtor_map_coinduct_strongN: string
val dtor_map_uniqueN: string
val dtor_relN: string
val dtor_rel_coinductN: string
val dtor_set_inclN: string
val dtor_set_set_inclN: string
- val dtor_strong_coinductN: string
+ val dtor_coinduct_strongN: string
val dtor_unfoldN: string
val dtor_unfold_o_mapN: string
val dtor_unfold_transferN: string
@@ -134,14 +135,13 @@
val rel_distinctN: string
val rel_selN: string
val rvN: string
- val sel_corecN: string
+ val corec_selN: string
val set_inclN: string
val set_set_inclN: string
val setN: string
val simpsN: string
val strTN: string
val str_initN: string
- val strong_coinductN: string
val sum_bdN: string
val sum_bdTN: string
val uniqueN: string
@@ -206,7 +206,7 @@
val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list
- val mk_strong_coinduct_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
+ val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
@@ -393,9 +393,9 @@
val ctor_induct2N = ctor_inductN ^ "2"
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
val dtor_coinductN = dtorN ^ "_" ^ coinductN
-val strong_coinductN = "strong_" ^ coinductN
-val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
-val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
+val coinduct_strongN = coinductN ^ "_strong"
+val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN
+val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN
val colN = "col"
val set_inclN = "set_incl"
val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
@@ -406,9 +406,9 @@
val caseN = "case"
val discN = "disc"
-val disc_corecN = discN ^ "_" ^ corecN
+val corec_discN = corecN ^ "_" ^ discN
val iffN = "_iff"
-val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
+val corec_disc_iffN = corec_discN ^ iffN
val distinctN = "distinct"
val rel_distinctN = relN ^ "_" ^ distinctN
val injectN = "inject"
@@ -421,7 +421,7 @@
val rel_inductN = relN ^ "_" ^ inductN
val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
val selN = "sel"
-val sel_corecN = selN ^ "_" ^ corecN
+val corec_selN = corecN ^ "_" ^ selN
fun co_prefix fp = case_fp fp "" "co";
@@ -634,7 +634,7 @@
split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
end;
-fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
+fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
let
val n = Thm.nprems_of coind;
val m = Thm.nprems_of (hd rel_monos) - n;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Aug 18 17:19:58 2014 +0200
@@ -69,15 +69,15 @@
calls: corec_call list,
discI: thm,
sel_thms: thm list,
- disc_excludess: thm list list,
+ distinct_discss: thm list list,
collapse: thm,
corec_thm: thm,
- disc_corec: thm,
- sel_corecs: thm list};
+ corec_disc: thm,
+ corec_sels: thm list};
type corec_spec =
{corec: term,
- disc_exhausts: thm list,
+ exhaust_discs: thm list,
sel_defs: thm list,
fp_nesting_maps: thm list,
fp_nesting_map_ident0s: thm list,
@@ -159,7 +159,7 @@
(case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
(case dest_case ctxt s Ts t of
- SOME ({sel_splits = _ :: _, ...}, conds', branches) =>
+ SOME ({split_sels = _ :: _, ...}, conds', branches) =>
fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
| _ => f conds t)
| _ => f conds t)
@@ -173,7 +173,7 @@
fun case_of ctxt s =
(case ctr_sugar_of ctxt s of
- SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
+ SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
| _ => NONE);
fun massage_let_if_case ctxt has_call massage_leaf =
@@ -343,8 +343,8 @@
fun case_thms_of_term ctxt t =
let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
- (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars,
- maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
+ (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars,
+ maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars)
end;
fun basic_corec_specs_of ctxt res_T =
@@ -444,32 +444,32 @@
else No_Corec) g_i
| call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
- fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
- corec_thm disc_corec sel_corecs =
+ fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse
+ corec_thm corec_disc corec_sels =
let val nullary = not (can dest_funT (fastype_of ctr)) in
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
- disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
- disc_corec = disc_corec, sel_corecs = sel_corecs}
+ distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
+ corec_disc = corec_disc, corec_sels = corec_sels}
end;
- fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
- : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
+ fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
+ : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
let val p_ios = map SOME p_is @ [NONE] in
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
- disc_excludesss collapses corec_thms disc_corecs sel_corecss
+ distinct_discsss collapses corec_thms corec_discs corec_selss
end;
- fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec,
- co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
- sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
- {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
+ fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
+ co_rec_thms = corec_thms, disc_co_recs = corec_discs,
+ sel_co_recss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
sel_defs = sel_defs,
fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
- ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
- sel_corecss};
+ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
+ corec_selss};
in
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
@@ -993,8 +993,8 @@
|> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
(ctr, map (K []) sels))) basic_ctr_specss);
- val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
- strong_coinduct_thms), lthy') =
+ val ((n2m, corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms,
+ coinduct_strong_thms), lthy') =
corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
val corec_specs = take actual_nn corec_specs';
val ctr_specss = map #ctr_specs corec_specs;
@@ -1061,15 +1061,15 @@
de_facto_exhaustives disc_eqnss
|> list_all_fun_args []
val nchotomy_taut_thmss =
- map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} =>
+ map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
fn {code_rhs_opt, ...} :: _ => fn [] => K []
| [goal] => fn true =>
let
- val (_, _, arg_disc_exhausts, _, _) =
+ val (_, _, arg_exhaust_discs, _, _) =
case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
in
[Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts))
+ mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
|> Thm.close_derivation]
end
| false =>
@@ -1133,7 +1133,7 @@
[]
else
let
- val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
+ val {disc, corec_disc, ...} = nth ctr_specs ctr_no;
val k = 1 + ctr_no;
val m = length prems;
val goal =
@@ -1146,7 +1146,7 @@
if prems = [@{term False}] then
[]
else
- mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
+ mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> pair (#disc (nth ctr_specs ctr_no))
@@ -1163,8 +1163,8 @@
val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
(find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
- val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec)
- |> nth (#sel_corecs ctr_spec);
+ val corec_sel = find_index (curry (op =) sel) (#sels ctr_spec)
+ |> nth (#corec_sels ctr_spec);
val k = 1 + ctr_no;
val m = length prems;
val goal =
@@ -1174,10 +1174,10 @@
|> HOLogic.mk_Trueprop o HOLogic.mk_eq
|> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
|> curry Logic.list_all (map dest_Free fun_args);
- val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
+ val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term;
in
- mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
- fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss
+ mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps
+ fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
@@ -1306,16 +1306,16 @@
val (raw_goal, goal) = (raw_rhs, rhs)
|> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
#> curry Logic.list_all (map dest_Free fun_args));
- val (distincts, discIs, _, sel_splits, sel_split_asms) =
+ val (distincts, discIs, _, split_sels, split_sel_asms) =
case_thms_of_term lthy raw_rhs;
- val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
- sel_split_asms ms ctr_thms
+ val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels
+ split_sel_asms ms ctr_thms
(if exhaustive_code then try the_single nchotomys else NONE)
|> K |> Goal.prove_sorry lthy [] [] raw_goal
|> Thm.close_derivation;
in
- mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
+ mk_primcorec_code_tac lthy distincts split_sels raw_code_thm
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> single
@@ -1337,14 +1337,14 @@
[]
else
let
- val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
+ val {disc, distinct_discss, ...} = nth ctr_specs ctr_no;
val goal =
mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
mk_conjs prems)
|> curry Logic.list_all (map dest_Free fun_args);
in
mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
- (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
+ (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
@@ -1385,7 +1385,7 @@
(exhaustN, nontriv_exhaust_thmss, []),
(selN, sel_thmss, simp_attrs),
(simpsN, simp_thmss, []),
- (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
+ (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, [])]
|> maps (fn (thmN, thmss, attrs) =>
map2 (fn fun_name => fn thms =>
((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
@@ -1394,7 +1394,7 @@
val common_notes =
[(coinductN, if n2m then [coinduct_thm] else [], []),
- (strong_coinductN, if n2m then [strong_coinduct_thm] else [], [])]
+ (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], [])]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Aug 18 17:19:58 2014 +0200
@@ -54,8 +54,8 @@
fun distinct_in_prems_tac distincts =
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
-fun mk_primcorec_nchotomy_tac ctxt disc_exhausts =
- HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt);
+fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
+ HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
let val ks = 1 upto n in
@@ -105,11 +105,11 @@
fun prelude_tac ctxt defs thm =
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
-fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss =
- prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss;
+fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
+ prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
- disc_excludes =
+ distinct_discs =
HEADGOAL (rtac iffI THEN'
rtac fun_exhaust THEN'
K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
@@ -121,7 +121,7 @@
rtac FalseE THEN'
(rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
cut_tac fun_disc') THEN'
- dresolve_tac disc_excludes THEN' etac notE THEN' atac)
+ dresolve_tac distinct_discs THEN' etac notE THEN' atac)
fun_discss) THEN'
(etac FalseE ORELSE'
resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Aug 18 17:19:58 2014 +0200
@@ -103,7 +103,7 @@
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
-val sum_weak_case_cong = @{thm sum.weak_case_cong};
+val sum_case_cong_weak = @{thm sum.case_cong_weak};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
val rev_bspec = Drule.rotate_prems 1 bspec;
@@ -430,7 +430,7 @@
CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
- if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
+ if n = 1 then K all_tac else etac (sum_case_cong_weak RS trans),
rtac (mk_sum_caseN n i RS trans), atac])
ks])
rv_Conss)
@@ -565,7 +565,7 @@
rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
rtac exI, rtac conjI,
if n = 1 then rtac refl
- else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
+ else etac (sum_case_cong_weak RS trans) THEN' rtac (mk_sum_caseN n i),
CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -603,7 +603,7 @@
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
- else (rtac (sum_weak_case_cong RS trans) THEN'
+ else (rtac (sum_case_cong_weak RS trans) THEN'
rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
@@ -628,7 +628,7 @@
CONVERSION (Conv.top_conv
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
- else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
+ else rtac sum_case_cong_weak THEN' rtac (mk_sum_caseN n i' RS trans),
SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl])
ks to_sbd_injs from_to_sbds)];
in
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Aug 18 17:19:58 2014 +0200
@@ -138,12 +138,12 @@
val inducts = map (the_single o #co_inducts) fp_sugars;
fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
- distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
+ distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
(T_name0,
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
- case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+ case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
split_asm = split_asm});
val infos = map_index mk_info (take nn_fp fp_sugars);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Aug 18 17:19:58 2014 +0200
@@ -18,7 +18,7 @@
distincts: thm list,
case_thms: thm list,
case_cong: thm,
- weak_case_cong: thm,
+ case_cong_weak: thm,
split: thm,
split_asm: thm,
disc_defs: thm list,
@@ -26,13 +26,13 @@
discIs: thm list,
sel_defs: thm list,
sel_thmss: thm list list,
- disc_excludesss: thm list list list,
- disc_exhausts: thm list,
- sel_exhausts: thm list,
+ distinct_discsss: thm list list list,
+ exhaust_discs: thm list,
+ exhaust_sels: thm list,
collapses: thm list,
expands: thm list,
- sel_splits: thm list,
- sel_split_asms: thm list,
+ split_sels: thm list,
+ split_sel_asms: thm list,
case_eq_ifs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
@@ -90,7 +90,7 @@
distincts: thm list,
case_thms: thm list,
case_cong: thm,
- weak_case_cong: thm,
+ case_cong_weak: thm,
split: thm,
split_asm: thm,
disc_defs: thm list,
@@ -98,19 +98,19 @@
discIs: thm list,
sel_defs: thm list,
sel_thmss: thm list list,
- disc_excludesss: thm list list list,
- disc_exhausts: thm list,
- sel_exhausts: thm list,
+ distinct_discsss: thm list list list,
+ exhaust_discs: thm list,
+ exhaust_sels: thm list,
collapses: thm list,
expands: thm list,
- sel_splits: thm list,
- sel_split_asms: thm list,
+ split_sels: thm list,
+ split_sel_asms: thm list,
case_eq_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_defs, disc_thmss, discIs, sel_defs,
- sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits,
- sel_split_asms, case_eq_ifs} =
+ case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
+ sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
+ split_sel_asms, case_eq_ifs} =
{ctrs = map (Morphism.term phi) ctrs,
casex = Morphism.term phi casex,
discs = map (Morphism.term phi) discs,
@@ -121,7 +121,7 @@
distincts = map (Morphism.thm phi) distincts,
case_thms = map (Morphism.thm phi) case_thms,
case_cong = Morphism.thm phi case_cong,
- weak_case_cong = Morphism.thm phi weak_case_cong,
+ case_cong_weak = Morphism.thm phi case_cong_weak,
split = Morphism.thm phi split,
split_asm = Morphism.thm phi split_asm,
disc_defs = map (Morphism.thm phi) disc_defs,
@@ -129,13 +129,13 @@
discIs = map (Morphism.thm phi) discIs,
sel_defs = map (Morphism.thm phi) sel_defs,
sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
- disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
- disc_exhausts = map (Morphism.thm phi) disc_exhausts,
- sel_exhausts = map (Morphism.thm phi) sel_exhausts,
+ distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss,
+ exhaust_discs = map (Morphism.thm phi) exhaust_discs,
+ exhaust_sels = map (Morphism.thm phi) exhaust_sels,
collapses = map (Morphism.thm phi) collapses,
expands = map (Morphism.thm phi) expands,
- sel_splits = map (Morphism.thm phi) sel_splits,
- sel_split_asms = map (Morphism.thm phi) sel_split_asms,
+ split_sels = map (Morphism.thm phi) split_sels,
+ split_sel_asms = map (Morphism.thm phi) split_sel_asms,
case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
val transfer_ctr_sugar =
@@ -200,23 +200,23 @@
val case_congN = "case_cong";
val case_eq_ifN = "case_eq_if";
val collapseN = "collapse";
-val disc_excludeN = "disc_exclude";
-val disc_exhaustN = "disc_exhaust";
val discN = "disc";
val discIN = "discI";
val distinctN = "distinct";
+val distinct_discN = "distinct_disc";
val exhaustN = "exhaust";
+val exhaust_discN = "exhaust_disc";
val expandN = "expand";
val injectN = "inject";
val nchotomyN = "nchotomy";
val selN = "sel";
-val sel_exhaustN = "sel_exhaust";
-val sel_splitN = "sel_split";
-val sel_split_asmN = "sel_split_asm";
+val exhaust_selN = "exhaust_sel";
val splitN = "split";
+val split_asmN = "split_asm";
+val split_selN = "split_sel";
+val split_sel_asmN = "split_sel_asm";
val splitsN = "splits";
-val split_asmN = "split_asm";
-val weak_case_cong_thmsN = "weak_case_cong";
+val case_cong_weak_thmsN = "case_cong_weak";
val cong_attrs = @{attributes [cong]};
val dest_attrs = @{attributes [dest]};
@@ -677,7 +677,7 @@
ks goals inject_thmss distinct_thmsss
end;
- val (case_cong_thm, weak_case_cong_thm) =
+ val (case_cong_thm, case_cong_weak_thm) =
let
fun mk_prem xctr xs xf xg =
fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
@@ -733,9 +733,9 @@
end;
val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
- discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
- disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms,
- expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
+ discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+ exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
+ expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) =
if no_discs_sels then
([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
else
@@ -827,7 +827,7 @@
flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
discI_thms);
- val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
+ val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) =
let
fun mk_goal [] = []
| mk_goal [((_, udisc), (_, udisc'))] =
@@ -843,25 +843,25 @@
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 lthy m discD disc_thm) goal])
+ fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal])
half_goalss half_pairss (flat disc_thmss');
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
+ map2 (map2 (prove o mk_other_half_distinct_disc_tac)) half_thmss
other_half_goalss;
in
join_halves n half_thmss other_half_thmss ||> `transpose
|>> has_alternate_disc_def ? K []
end;
- val disc_exhaust_thm =
+ val exhaust_disc_thm =
let
fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
in
Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_disc_exhaust_tac n exhaust_thm discI_thms)
+ mk_exhaust_disc_tac n exhaust_thm discI_thms)
|> Thm.close_derivation
end;
@@ -890,13 +890,13 @@
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 =
+ val exhaust_sel_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)
+ mk_exhaust_sel_tac n exhaust_disc_thm swapped_all_collapse_thms)
|> Thm.close_derivation
end;
@@ -919,14 +919,14 @@
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
in
Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
- (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
- disc_exclude_thmsss')
+ mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm)
+ (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
+ distinct_disc_thmsss')
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
- val (sel_split_thm, sel_split_asm_thm) =
+ val (split_sel_thm, split_sel_asm_thm) =
let
val zss = map (K []) xss;
val goal = mk_split_goal usel_ctrs zss usel_fs;
@@ -949,9 +949,9 @@
end;
in
(sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
- discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
- [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms,
- [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
+ discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
+ [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
+ [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm])
end;
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -966,30 +966,28 @@
(flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
- (* "exhaust" is deliberately put first to avoid apparent circular dependencies in the proof
- objects, which would confuse MaSh. *)
val notes =
- [(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
- (caseN, case_thms, code_nitpicksimp_simp_attrs),
+ [(caseN, case_thms, code_nitpicksimp_simp_attrs),
(case_congN, [case_cong_thm], []),
+ (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
(case_eq_ifN, case_eq_if_thms, []),
(collapseN, safe_collapse_thms, simp_attrs),
(discN, flat nontriv_disc_thmss, simp_attrs),
(discIN, nontriv_discI_thms, []),
- (disc_excludeN, disc_exclude_thms, dest_attrs),
- (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
(distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
+ (distinct_discN, distinct_disc_thms, dest_attrs),
+ (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
+ (exhaust_discN, exhaust_disc_thms, [exhaust_case_names_attr]),
+ (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]),
(expandN, expand_thms, []),
(injectN, inject_thms, iff_attrs @ inductsimp_attrs),
(nchotomyN, [nchotomy_thm], []),
(selN, all_sel_thms, code_nitpicksimp_simp_attrs),
- (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
- (sel_splitN, sel_split_thms, []),
- (sel_split_asmN, sel_split_asm_thms, []),
+ (split_selN, split_sel_thms, []),
+ (split_sel_asmN, split_sel_asm_thms, []),
(splitN, [split_thm], []),
(split_asmN, [split_asm_thm], []),
- (splitsN, [split_thm, split_asm_thm], []),
- (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
+ (splitsN, [split_thm, split_asm_thm], [])]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
((qualify true (Binding.name thmN), attrs), [(thms, [])]));
@@ -1019,12 +1017,12 @@
val ctr_sugar =
{ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
- case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+ case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
- disc_excludesss = disc_exclude_thmsss, 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,
+ distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
+ exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
+ split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
case_eq_ifs = case_eq_if_thms}
|> morph_ctr_sugar (substitute_noted_thm noted);
in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Aug 18 17:19:58 2014 +0200
@@ -22,13 +22,13 @@
val mk_case_eq_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_exhaust_disc_tac: int -> thm -> thm list -> tactic
+ val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic
val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
thm list list list -> thm list list list -> tactic
- val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
+ val mk_half_distinct_disc_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_other_half_distinct_disc_tac: thm -> tactic
val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
thm list list list -> tactic
val mk_split_asm_tac: Proof.context -> thm -> tactic
@@ -67,21 +67,21 @@
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|> k = 1 ? swap |> op @)));
-fun mk_half_disc_exclude_tac ctxt m discD disc' =
+fun mk_half_distinct_disc_tac ctxt m discD disc' =
HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
rtac disc');
-fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
+fun mk_other_half_distinct_disc_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
-fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
+fun mk_exhaust_disc_or_sel_tac n exhaust destIs =
HEADGOAL (rtac exhaust THEN'
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;
+val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
-fun mk_sel_exhaust_tac n disc_exhaust collapses =
- mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
+fun mk_exhaust_sel_tac n exhaust_disc collapses =
+ mk_exhaust_disc_or_sel_tac n exhaust_disc collapses ORELSE
HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
fun mk_collapse_tac ctxt m discD sels =
@@ -92,17 +92,17 @@
REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
-fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
- disc_excludesss' =
+fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
+ distinct_discsss' =
if ms = [0] then
HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
- TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
+ TRY o EVERY' [rtac uexhaust_disc, atac, rtac vexhaust_disc, atac])
else
let val ks = 1 upto n in
- HEADGOAL (rtac udisc_exhaust THEN'
- EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
- EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vdisc_exhaust,
- EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
+ HEADGOAL (rtac uexhaust_disc THEN'
+ EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
+ EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
+ EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
EVERY'
(if k' = k then
[rtac (vuncollapse RS trans), TRY o atac] @
@@ -113,11 +113,11 @@
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
asm_simp_tac (ss_only [] ctxt)])
else
- [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
+ [dtac (the_single (if k = n then distinct_discs else distinct_discs')),
etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
atac, atac]))
- ks disc_excludess disc_excludess' uncollapses)])
- ks ms disc_excludesss disc_excludesss' uncollapses))
+ ks distinct_discss distinct_discss' uncollapses)])
+ ks ms distinct_discsss distinct_discsss' uncollapses))
end;
fun mk_case_same_ctr_tac ctxt injects =
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Aug 18 17:19:58 2014 +0200
@@ -27,7 +27,7 @@
case_name : string,
case_rewrites : thm list,
case_cong : thm,
- weak_case_cong : thm,
+ case_cong_weak : thm,
split : thm,
split_asm: thm}
end
@@ -195,7 +195,7 @@
case_name : string,
case_rewrites : thm list,
case_cong : thm,
- weak_case_cong : thm,
+ case_cong_weak : thm,
split : thm,
split_asm: thm};
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Aug 18 17:19:58 2014 +0200
@@ -95,7 +95,7 @@
head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
- weak_case_cong, split, split_asm, ...} : Datatype_Aux.info) =
+ case_cong_weak, split, split_asm, ...} : Datatype_Aux.info) =
{ctrs = ctrs_of_exhaust exhaust,
casex = case_of_case_rewrite (hd case_rewrites),
discs = [],
@@ -106,7 +106,7 @@
distincts = distinct,
case_thms = case_rewrites,
case_cong = case_cong,
- weak_case_cong = weak_case_cong,
+ case_cong_weak = case_cong_weak,
split = split,
split_asm = split_asm,
disc_defs = [],
@@ -114,13 +114,13 @@
discIs = [],
sel_defs = [],
sel_thmss = [],
- disc_excludesss = [],
- disc_exhausts = [],
- sel_exhausts = [],
+ distinct_discsss = [],
+ exhaust_discs = [],
+ exhaust_sels = [],
collapses = [],
expands = [],
- sel_splits = [],
- sel_split_asms = [],
+ split_sels = [],
+ split_sel_asms = [],
case_eq_ifs = []};
fun register dt_infos =
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Mon Aug 18 17:19:58 2014 +0200
@@ -18,7 +18,7 @@
val make_cases : string list -> descr list -> theory -> term list list
val make_splits : string list -> descr list -> theory -> (term * term) list
val make_case_combs : string list -> descr list -> theory -> string -> term list
- val make_weak_case_congs : string list -> descr list -> theory -> term list
+ val make_case_cong_weaks : string list -> descr list -> theory -> term list
val make_case_congs : string list -> descr list -> theory -> term list
val make_nchotomys : descr list -> term list
end;
@@ -330,7 +330,7 @@
(************************* additional rules for TFL ***************************)
-fun make_weak_case_congs case_names descr thy =
+fun make_case_cong_weaks case_names descr thy =
let
val case_combs = make_case_combs case_names descr thy "f";
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Mon Aug 18 17:19:58 2014 +0200
@@ -395,16 +395,16 @@
|-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
end;
-fun prove_weak_case_congs new_type_names case_names descr thy =
+fun prove_case_cong_weaks new_type_names case_names descr thy =
let
- fun prove_weak_case_cong t =
+ fun prove_case_cong_weak t =
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
- val weak_case_congs =
- map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
+ val case_cong_weaks =
+ map prove_case_cong_weak (Datatype_Prop.make_case_cong_weaks case_names descr thy);
- in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
+ in thy |> Datatype_Aux.store_thms "case_cong_weak" new_type_names case_cong_weaks end;
(* additional theorems for TFL *)
@@ -470,7 +470,7 @@
fun make_dt_info descr induct inducts rec_names rec_rewrites
(index, (((((((((((_, (tname, _, _))), inject), distinct),
- exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
+ exhaust), nchotomy), case_name), case_rewrites), case_cong), case_cong_weak),
(split, split_asm))) =
(tname,
{index = index,
@@ -486,7 +486,7 @@
case_name = case_name,
case_rewrites = case_rewrites,
case_cong = case_cong,
- weak_case_cong = weak_case_cong,
+ case_cong_weak = case_cong_weak,
split = split,
split_asm = split_asm});
@@ -513,8 +513,8 @@
|> prove_case_thms config new_type_names descr rec_names rec_rewrites;
val (case_congs, thy7) = thy6
|> prove_case_congs new_type_names case_names descr nchotomys case_rewrites;
- val (weak_case_congs, thy8) = thy7
- |> prove_weak_case_congs new_type_names case_names descr;
+ val (case_cong_weaks, thy8) = thy7
+ |> prove_case_cong_weaks new_type_names case_names descr;
val (splits, thy9) = thy8
|> prove_split_thms config new_type_names case_names descr
inject distinct exhaust case_rewrites;
@@ -524,7 +524,7 @@
map_index
(make_dt_info flat_descr induct inducts rec_names rec_rewrites)
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
- case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
+ case_names ~~ case_rewrites ~~ case_congs ~~ case_cong_weaks ~~ splits);
val dt_names = map fst dt_infos;
val prfx = Binding.qualify true (space_implode "_" new_type_names);
val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
@@ -553,7 +553,7 @@
((Binding.empty, [iff_add]), [(flat inject, [])]),
((Binding.empty, [Classical.safe_elim NONE]),
[(map (fn th => th RS notE) (flat distinct), [])]),
- ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
+ ((Binding.empty, [Simplifier.cong_add]), [(case_cong_weaks, [])]),
((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
named_rules @ unnamed_rules)
|> snd
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Aug 18 17:19:58 2014 +0200
@@ -190,7 +190,7 @@
(* FIXME: put other record thms here, or declare as "no_atp" *)
fun multi_base_blacklist ctxt ho_atp =
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
- "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nat_of_char_simps", "nibble.simps",
+ "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps",
"nibble.distinct"]
|> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
|> map (prefix Long_Name.separator)
--- a/src/HOL/Tools/TFL/tfl.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Aug 18 17:19:58 2014 +0200
@@ -434,7 +434,7 @@
val case_simpset =
put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
- |> fold (Simplifier.add_cong o #weak_case_cong o snd)
+ |> fold (Simplifier.add_cong o #case_cong_weak o snd)
(Symtab.dest (Datatype.get_all theory))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
val extract = Rules.CONTEXT_REWRITE_RULE
--- a/src/HOL/Tools/record.ML Mon Aug 18 15:03:25 2014 +0200
+++ b/src/HOL/Tools/record.ML Mon Aug 18 17:19:58 2014 +0200
@@ -1785,10 +1785,10 @@
Ctr_Sugar.default_register_ctr_sugar_global T_name
{ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
- case_cong = Drule.dummy_thm, weak_case_cong = Drule.dummy_thm, split = Drule.dummy_thm,
+ case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
- sel_thmss = [sel_thms], disc_excludesss = [], disc_exhausts = [], sel_exhausts = [],
- collapses = [], expands = [], sel_splits = [], sel_split_asms = [], case_eq_ifs = []};
+ sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
+ collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
(* definition *)