# HG changeset patch
# User noschinl
# Date 1436449931 -7200
# Node ID 5e03e1bd1be02ae5c54f8a81c15513bbe78521d3
# Parent  61352c31b273672ab1ee3d50cf0368d06828747a
case_of_simps: do not split for types with a single constructor

diff -r 61352c31b273 -r 5e03e1bd1be0 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Thu Jul 09 15:45:00 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Thu Jul 09 15:52:11 2015 +0200
@@ -22,10 +22,12 @@
   | collect_Tcons (TFree _) = []
   | collect_Tcons (TVar _) = []
 
-fun get_split_ths ctxt = collect_Tcons
+fun get_type_infos ctxt =
+    maps collect_Tcons
     #> distinct (op =)
     #> map_filter (Ctr_Sugar.ctr_sugar_of ctxt)
-    #> map #split
+
+fun get_split_ths ctxt = get_type_infos ctxt #> map #split
 
 val strip_eq = Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq
 
@@ -36,16 +38,18 @@
     | transpose ([] :: xss) = transpose xss
     | transpose xss = map hd xss :: transpose (map tl xss);
 
-  fun same_fun (ts as _ $ _ :: _) =
+  fun same_fun single_ctrs (ts as _ $ _ :: _) =
       let
         val (fs, argss) = map strip_comb ts |> split_list
         val f = hd fs
-      in if forall (fn x => f = x) fs then SOME (f, argss) else NONE end
-    | same_fun _ = NONE
+        fun is_single_ctr (Const (name, _)) = member (op =) single_ctrs name
+          | is_single_ctr _ = false
+      in if not (is_single_ctr f) andalso forall (fn x => f = x) fs then SOME (f, argss) else NONE end
+    | same_fun _ _ = NONE
 
   (* pats must be non-empty *)
-  fun split_pat pats ctxt =
-      case same_fun pats of
+  fun split_pat single_ctrs pats ctxt =
+      case same_fun single_ctrs pats of
         NONE =>
           let
             val (name, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
@@ -54,13 +58,13 @@
       | SOME (f, argss) =>
           let
             val (((def_pats, def_frees), case_patss), ctxt') =
-              split_pats argss ctxt
+              split_pats single_ctrs argss ctxt
             val def_pat = list_comb (f, def_pats)
           in (((def_pat, flat def_frees), case_patss), ctxt') end
   and
-      split_pats patss ctxt =
+      split_pats single_ctrs patss ctxt =
         let
-          val (splitted, ctxt') = fold_map split_pat (transpose patss) ctxt
+          val (splitted, ctxt') = fold_map (split_pat single_ctrs) (transpose patss) ctxt
           val r = splitted |> split_list |> apfst split_list |> apsnd (transpose #> map flat)
         in (r, ctxt') end
 
@@ -74,13 +78,16 @@
 *)
 fun build_case_t fun_t lhss rhss ctxt =
   let
+    val single_ctrs =
+      get_type_infos ctxt (map fastype_of (flat lhss))
+      |> map_filter (fn ti => case #ctrs ti of [Const (name, _)] => SOME name | _ => NONE)
     val (((def_pats, def_frees), case_patss), ctxt') =
-      split_pats lhss ctxt
+      split_pats single_ctrs lhss ctxt
     val pattern = map HOLogic.mk_tuple case_patss
     val case_arg = HOLogic.mk_tuple (flat def_frees)
     val cases = Case_Translation.make_case ctxt' Case_Translation.Warning Name.context
       case_arg (pattern ~~ rhss)
-    val split_thms = get_split_ths ctxt' (fastype_of case_arg)
+    val split_thms = get_split_ths ctxt' [fastype_of case_arg]
     val t = (list_comb (fun_t, def_pats), cases)
       |> HOLogic.mk_eq
       |> HOLogic.mk_Trueprop
@@ -196,7 +203,7 @@
 fun to_simps ctxt thm =
   let
     val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of
-    val splitthms = get_split_ths ctxt T
+    val splitthms = get_split_ths ctxt [T]
   in gen_to_simps ctxt splitthms thm end
 
 
diff -r 61352c31b273 -r 5e03e1bd1be0 src/HOL/ex/Simps_Case_Conv_Examples.thy
--- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Thu Jul 09 15:45:00 2015 +0200
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Thu Jul 09 15:52:11 2015 +0200
@@ -75,6 +75,11 @@
   "test (Some x) y = x"
   by (fact test_simps1)+
 
+text {* Single-constructor patterns*}
+case_of_simps fst_conv_simps: fst_conv
+lemma "fst x = (case x of (a,b) \<Rightarrow> a)"
+  by (fact fst_conv_simps)
+
 text {* Partial split of case *}
 simps_of_case nosplit_simps2: nosplit_def (splits: list.split)
 lemma