# HG changeset patch # User desharna # Date 1406710230 -7200 # Node ID 13b446b628252972785479cb31d14fe49e53b954 # Parent a2c4adb839a998a8c48b275905d2ee552e675ccb document property 'set_induct' diff -r a2c4adb839a9 -r 13b446b62825 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Jul 30 10:50:28 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Jul 30 10:50:30 2014 +0200 @@ -956,14 +956,13 @@ \item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n, induct t]"}\rm:] ~ \\ @{thm list.induct[no_vars]} -\item[@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ -Given $m > 1$ mutually recursive datatypes, this induction rule can be used to -prove $m$ properties simultaneously. - \item[@{text "t."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n, induct pred]"}\rm:] ~ \\ @{thm list.rel_induct[no_vars]} -\item[@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm:] ~ \\ +\item[\begin{tabular}{@ {}l@ {}} + @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm: \\ + @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n]"}\rm: \\ +\end{tabular}] ~ \\ Given $m > 1$ mutually recursive datatypes, this induction rule can be used to prove $m$ properties simultaneously. @@ -1775,6 +1774,13 @@ Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be used to prove $m$ properties simultaneously. +\item[\begin{tabular}{@ {}l@ {}} + @{text "t\<^sub>1_\_t\<^sub>m."}\hthm{set_induct} @{text "[case_names C\<^sub>1 \ C\<^sub>n,"} \\ + \phantom{@{text "t\<^sub>1_\_t\<^sub>m."}\hthm{set_induct} @{text "["}}@{text "induct set: set\<^sub>j_t\<^sub>1, \, induct set: set\<^sub>j_t\<^sub>m]"}\rm: \\ +\end{tabular}] ~ \\ +@{thm llist.set_induct[no_vars]} \\ +If $m = 1$, the attribute @{text "[consumes 1]"} is generated as well. + \item[@{text "t."}\hthm{corec}\rm:] ~ \\ @{thm llist.corec(1)[no_vars]} \\ @{thm llist.corec(2)[no_vars]}