# HG changeset patch # User blanchet # Date 1408375198 -7200 # Node ID 6edc3529bb4e9d95e91ae201120429ba20383da0 # Parent d2bc61d7837048a02fbecb056464d7e2dab9a56c reordered some (co)datatype property names for more consistency diff -r d2bc61d78370 -r 6edc3529bb4e NEWS --- 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: diff -r d2bc61d78370 -r 6edc3529bb4e src/Doc/Datatypes/Datatypes.thy --- 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 \ \ nonnull list"} \\ @{prop "nonnull list \ \ null list"} -\item[@{text "t."}\hthm{disc_exhaust} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ -@{thm list.disc_exhaust[no_vars]} - -\item[@{text "t."}\hthm{sel_exhaust} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ -@{thm list.sel_exhaust[no_vars]} +\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ +@{thm list.exhaust_disc[no_vars]} + +\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \ 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 \ t\<^sub>m,"} \\ - \phantom{@{text "t."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: + @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \ 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 \ t\<^sub>m,"} \\ @@ -1786,8 +1786,8 @@ \item[\begin{tabular}{@ {}l@ {}} @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m, case_conclusion D\<^sub>1 \ D\<^sub>n]"} \\ - @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{strong_coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ - \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: \\ + @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ + \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \ D\<^sub>n]"}\rm: \\ @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \ t\<^sub>m,"} \\ \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \ 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. *} diff -r d2bc61d78370 -r 6edc3529bb4e src/Doc/Logics/document/HOL.tex --- 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} diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/BNF_Examples/Derivation_Trees/DTree.thy --- 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) \ cont (unfold rt ct b) = image (id \ 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) \ cont (corec rt ct b) = image (id \ ([[id, corec rt ct]])) (ct b)" -using dtree.sel_corec[of rt "the_inv fset \ ct" b] unfolding corec_def +using dtree.corec_sel[of rt "the_inv fset \ ct" b] unfolding corec_def unfolding cont_def comp_def id_def by simp_all diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/BNF_Examples/Process.thy --- 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 \ isChoice p" -by (rule process.disc_exhaust) auto +by (rule process.exhaust_disc) auto theorem not_isAction_isChoice: "\ (isAction p \ isChoice p)" by (cases rule: process.exhaust[of p]) auto @@ -54,7 +54,7 @@ Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ (\ p p' \ p = p') \ (\ q q' \ 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) *} diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/BNF_Examples/Stream.thy --- 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"]: diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Bali/Basis.thy --- 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)}" diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Bali/Conform.thy --- 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: diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Library/RBT_Impl.thy --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Nat.thy --- 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 *} diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Old_Number_Theory/Factorization.thy --- 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)" diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Product_Type.thy --- 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 \ 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) diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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' diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_fp_util.ML --- 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; diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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, [])])); diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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)); diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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); diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- 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 = diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Datatype/datatype_aux.ML --- 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}; diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Datatype/datatype_data.ML --- 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 = diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Datatype/datatype_prop.ML --- 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"; diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Datatype/rep_datatype.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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) diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/TFL/tfl.ML --- 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 diff -r d2bc61d78370 -r 6edc3529bb4e src/HOL/Tools/record.ML --- 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 *)