# HG changeset patch # User blanchet # Date 1379512575 -7200 # Node ID 7b453b619b5f2fe8d7f24a5b6ad5dae2af1cd642 # Parent 71b020d161c5ae5096932ae6b7a7d5fe641bf2af use singular to avoid confusion diff -r 71b020d161c5 -r 7b453b619b5f src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:33:32 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:56:15 2013 +0200 @@ -750,13 +750,13 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{discs} @{text "[simp]"}\rm:] ~ \\ -@{thm list.discs(1)[no_vars]} \\ -@{thm list.discs(2)[no_vars]} - -\item[@{text "t."}\hthm{sels} @{text "[simp]"}\rm:] ~ \\ -@{thm list.sels(1)[no_vars]} \\ -@{thm list.sels(2)[no_vars]} +\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\ +@{thm list.disc(1)[no_vars]} \\ +@{thm list.disc(2)[no_vars]} + +\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\ +@{thm list.sel(1)[no_vars]} \\ +@{thm list.sel(2)[no_vars]} \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\ @{thm list.collapse(1)[no_vars]} \\ @@ -792,9 +792,9 @@ \begin{indentblock} \begin{description} -\item[@{text "t."}\hthm{sets} @{text "[code]"}\rm:] ~ \\ -@{thm list.sets(1)[no_vars]} \\ -@{thm list.sets(2)[no_vars]} +\item[@{text "t."}\hthm{set} @{text "[code]"}\rm:] ~ \\ +@{thm list.set(1)[no_vars]} \\ +@{thm list.set(2)[no_vars]} \item[@{text "t."}\hthm{map} @{text "[code]"}\rm:] ~ \\ @{thm list.map(1)[no_vars]} \\ @@ -847,7 +847,7 @@ \begin{description} \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\ -@{text t.rel_distinct} @{text t.sets} +@{text t.rel_distinct} @{text t.set} \end{description} \end{indentblock} @@ -1547,7 +1547,7 @@ \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec}$^*$ @{text t.disc_corec}] ~ \\ @{text t.disc_corec_iff} @{text t.sel_corec} @{text t.unfold}$^*$ @{text t.disc_unfold} @{text t.disc_unfold_iff} ~ \\ -@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.sets} +@{text t.sel_unfold} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set} \end{description} \end{indentblock} diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Examples/Process.thy --- a/src/HOL/BNF/Examples/Process.thy Wed Sep 18 15:33:32 2013 +0200 +++ b/src/HOL/BNF/Examples/Process.thy Wed Sep 18 15:56:15 2013 +0200 @@ -44,7 +44,7 @@ Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ \ p p' \ \ q q'" shows "p = p'" using assms - by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.discs(3)) + by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.disc(3)) (* Stronger coinduction, up to equality: *) theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]: @@ -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.discs(3)) + by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3)) subsection {* Coiteration (unfold) *} diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 15:33:32 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Wed Sep 18 15:56:15 2013 +0200 @@ -33,7 +33,7 @@ *} code_datatype Stream -lemmas [code] = stream.sels stream.sets stream.case +lemmas [code] = stream.sel stream.set stream.case lemma stream_case_cert: assumes "CASE \ stream_case c" @@ -495,7 +495,7 @@ lemma sinterleave_code[code]: "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1" - by (metis sinterleave_simps stream.exhaust stream.sels) + by (metis sinterleave_simps stream.exhaust stream.sel) lemma sinterleave_snth[simp]: "even n \ sinterleave s1 s2 !! n = s1 !! (n div 2)" diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 15:33:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 15:56:15 2013 +0200 @@ -115,13 +115,13 @@ val collapseN = "collapse"; val disc_excludeN = "disc_exclude"; val disc_exhaustN = "disc_exhaust"; -val discsN = "discs"; +val discN = "disc"; val distinctN = "distinct"; val exhaustN = "exhaust"; val expandN = "expand"; val injectN = "inject"; val nchotomyN = "nchotomy"; -val selsN = "sels"; +val selN = "sel"; val splitN = "split"; val splitsN = "splits"; val split_asmN = "split_asm"; @@ -750,7 +750,7 @@ (case_congN, [case_cong_thm], []), (case_convN, case_conv_thms, []), (collapseN, collapse_thms, simp_attrs), - (discsN, disc_thms, simp_attrs), + (discN, disc_thms, simp_attrs), (disc_excludeN, disc_exclude_thms, []), (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), @@ -758,7 +758,7 @@ (expandN, expand_thms, []), (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), - (selsN, all_sel_thms, simp_attrs), + (selN, all_sel_thms, simp_attrs), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []), diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 15:33:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Sep 18 15:56:15 2013 +0200 @@ -1395,7 +1395,7 @@ [(mapN, map_thms, code_simp_attrs), (rel_distinctN, rel_distinct_thms, code_simp_attrs), (rel_injectN, rel_inject_thms, code_simp_attrs), - (setsN, flat set_thmss, code_simp_attrs)] + (setN, flat set_thmss, code_simp_attrs)] |> massage_simple_notes fp_b_name; in (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), diff -r 71b020d161c5 -r 7b453b619b5f src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 15:33:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Sep 18 15:56:15 2013 +0200 @@ -111,7 +111,7 @@ val set_inclN: string val set_set_inclN: string val sel_unfoldN: string - val setsN: string + val setN: string val simpsN: string val strTN: string val str_initN: string @@ -287,7 +287,7 @@ val LevN = "Lev" val rvN = "recover" val behN = "beh" -val setsN = "sets" +val setN = "set" val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN fun mk_set_inductN i = mk_setN i ^ "_induct"