take out 'x = C' of the simplifier for unit types
authorblanchet
Wed Sep 03 00:06:23 2014 +0200 (2014-09-03)
changeset 58151414deb2ef328
parent 58150 2bf3ed0f62cf
child 58152 6fe60a9a5bad
take out 'x = C' of the simplifier for unit types
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 03 00:06:22 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 03 00:06:23 2014 +0200
     1.3 @@ -807,7 +807,10 @@
     1.4  
     1.5  \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
     1.6  @{thm list.collapse(1)[no_vars]} \\
     1.7 -@{thm list.collapse(2)[no_vars]}
     1.8 +@{thm list.collapse(2)[no_vars]} \\
     1.9 +(The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped
    1.10 +with a single nullary constructor, because a property of the form
    1.11 +@{prop "x = C"} is not suitable as a simplification rule.)
    1.12  
    1.13  \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
    1.14  These properties are missing for @{typ "'a list"} because there is only one
    1.15 @@ -840,8 +843,8 @@
    1.16  \end{indentblock}
    1.17  
    1.18  \noindent
    1.19 -In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
    1.20 -attribute.
    1.21 +In addition, equational versions of @{text t.disc} are registered with the
    1.22 +@{text "[code]"} attribute.
    1.23  *}
    1.24  
    1.25  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 00:06:22 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 00:06:23 2014 +0200
     2.3 @@ -983,7 +983,7 @@
     2.4             (case_congN, [case_cong_thm], []),
     2.5             (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
     2.6             (case_eq_ifN, case_eq_if_thms, []),
     2.7 -           (collapseN, safe_collapse_thms, simp_attrs),
     2.8 +           (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs),
     2.9             (discN, flat nontriv_disc_thmss, simp_attrs),
    2.10             (discIN, nontriv_discI_thms, []),
    2.11             (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),