src/Doc/Datatypes/Datatypes.thy
changeset 57983 6edc3529bb4e
parent 57982 d2bc61d78370
child 57984 cbe9a16f8e11
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -773,8 +773,8 @@
     1.4  \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
     1.5  @{thm list.case_cong[no_vars]}
     1.6  
     1.7 -\item[@{text "t."}\hthm{weak_case_cong} @{text "[cong]"}\rm:] ~ \\
     1.8 -@{thm list.weak_case_cong[no_vars]}
     1.9 +\item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
    1.10 +@{thm list.case_cong_weak[no_vars]}
    1.11  
    1.12  \item[@{text "t."}\hthm{split}\rm:] ~ \\
    1.13  @{thm list.split[no_vars]}
    1.14 @@ -809,27 +809,27 @@
    1.15  @{thm list.collapse(1)[no_vars]} \\
    1.16  @{thm list.collapse(2)[no_vars]}
    1.17  
    1.18 -\item[@{text "t."}\hthm{disc_exclude} @{text "[dest]"}\rm:] ~ \\
    1.19 +\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
    1.20  These properties are missing for @{typ "'a list"} because there is only one
    1.21  proper discriminator. Had the datatype been introduced with a second
    1.22  discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
    1.23  @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
    1.24  @{prop "nonnull list \<Longrightarrow> \<not> null list"}
    1.25  
    1.26 -\item[@{text "t."}\hthm{disc_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    1.27 -@{thm list.disc_exhaust[no_vars]}
    1.28 -
    1.29 -\item[@{text "t."}\hthm{sel_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    1.30 -@{thm list.sel_exhaust[no_vars]}
    1.31 +\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    1.32 +@{thm list.exhaust_disc[no_vars]}
    1.33 +
    1.34 +\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    1.35 +@{thm list.exhaust_sel[no_vars]}
    1.36  
    1.37  \item[@{text "t."}\hthm{expand}\rm:] ~ \\
    1.38  @{thm list.expand[no_vars]}
    1.39  
    1.40 -\item[@{text "t."}\hthm{sel_split}\rm:] ~ \\
    1.41 -@{thm list.sel_split[no_vars]}
    1.42 -
    1.43 -\item[@{text "t."}\hthm{sel_split_asm}\rm:] ~ \\
    1.44 -@{thm list.sel_split_asm[no_vars]}
    1.45 +\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
    1.46 +@{thm list.split_sel[no_vars]}
    1.47 +
    1.48 +\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
    1.49 +@{thm list.split_sel_asm[no_vars]}
    1.50  
    1.51  \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
    1.52  @{thm list.case_eq_if[no_vars]}
    1.53 @@ -868,18 +868,18 @@
    1.54  @{thm list.set_intros(1)[no_vars]} \\
    1.55  @{thm list.set_intros(2)[no_vars]}
    1.56  
    1.57 -\item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
    1.58 -@{thm list.sel_set[no_vars]}
    1.59 +\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
    1.60 +@{thm list.set_sel[no_vars]}
    1.61  
    1.62  \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
    1.63  @{thm list.map(1)[no_vars]} \\
    1.64  @{thm list.map(2)[no_vars]}
    1.65  
    1.66 -\item[@{text "t."}\hthm{disc_map_iff} @{text "[simp]"}\rm:] ~ \\
    1.67 -@{thm list.disc_map_iff[no_vars]}
    1.68 -
    1.69 -\item[@{text "t."}\hthm{sel_map}\rm:] ~ \\
    1.70 -@{thm list.sel_map[no_vars]}
    1.71 +\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
    1.72 +@{thm list.map_disc_iff[no_vars]}
    1.73 +
    1.74 +\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
    1.75 +@{thm list.map_sel[no_vars]}
    1.76  
    1.77  \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
    1.78  @{thm list.rel_inject(1)[no_vars]} \\
    1.79 @@ -1772,10 +1772,10 @@
    1.80  @{thm llist.coinduct[no_vars]}
    1.81  
    1.82  \item[\begin{tabular}{@ {}l@ {}}
    1.83 -  @{text "t."}\hthm{strong_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    1.84 -  \phantom{@{text "t."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
    1.85 +  @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    1.86 +  \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
    1.87  \end{tabular}] ~ \\
    1.88 -@{thm llist.strong_coinduct[no_vars]}
    1.89 +@{thm llist.coinduct_strong[no_vars]}
    1.90  
    1.91  \item[\begin{tabular}{@ {}l@ {}}
    1.92    @{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    1.93 @@ -1786,8 +1786,8 @@
    1.94  
    1.95  \item[\begin{tabular}{@ {}l@ {}}
    1.96    @{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]"} \\
    1.97 -  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    1.98 -  \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
    1.99 +  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
   1.100 +  \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
   1.101    @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
   1.102    \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
   1.103  \end{tabular}] ~ \\
   1.104 @@ -1808,17 +1808,17 @@
   1.105  \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
   1.106  @{thm llist.corec_code[no_vars]}
   1.107  
   1.108 -\item[@{text "t."}\hthm{disc_corec}\rm:] ~ \\
   1.109 -@{thm llist.disc_corec(1)[no_vars]} \\
   1.110 -@{thm llist.disc_corec(2)[no_vars]}
   1.111 -
   1.112 -\item[@{text "t."}\hthm{disc_corec_iff} @{text "[simp]"}\rm:] ~ \\
   1.113 -@{thm llist.disc_corec_iff(1)[no_vars]} \\
   1.114 -@{thm llist.disc_corec_iff(2)[no_vars]}
   1.115 -
   1.116 -\item[@{text "t."}\hthm{sel_corec} @{text "[simp]"}\rm:] ~ \\
   1.117 -@{thm llist.sel_corec(1)[no_vars]} \\
   1.118 -@{thm llist.sel_corec(2)[no_vars]}
   1.119 +\item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
   1.120 +@{thm llist.corec_disc(1)[no_vars]} \\
   1.121 +@{thm llist.corec_disc(2)[no_vars]}
   1.122 +
   1.123 +\item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
   1.124 +@{thm llist.corec_disc_iff(1)[no_vars]} \\
   1.125 +@{thm llist.corec_disc_iff(2)[no_vars]}
   1.126 +
   1.127 +\item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
   1.128 +@{thm llist.corec_sel(1)[no_vars]} \\
   1.129 +@{thm llist.corec_sel(2)[no_vars]}
   1.130  
   1.131  \end{description}
   1.132  \end{indentblock}
   1.133 @@ -1829,7 +1829,7 @@
   1.134  \begin{indentblock}
   1.135  \begin{description}
   1.136  
   1.137 -\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec_iff}] @{text t.sel_corec} ~ \\
   1.138 +\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\
   1.139  @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
   1.140  
   1.141  \end{description}
   1.142 @@ -2151,7 +2151,7 @@
   1.143  @{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
   1.144  @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
   1.145  @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
   1.146 -and analogously for @{text strong_coinduct}. These rules and the
   1.147 +and analogously for @{text coinduct_strong}. These rules and the
   1.148  underlying corecursors are generated on a per-need basis and are kept in a cache
   1.149  to speed up subsequent definitions.
   1.150  *}