--- a/src/HOL/Library/simps_case_conv.ML Thu Jul 09 16:49:08 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Thu Jul 09 17:36:04 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
--- a/src/HOL/ex/Simps_Case_Conv_Examples.thy Thu Jul 09 16:49:08 2015 +0200
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy Thu Jul 09 17:36:04 2015 +0200
@@ -28,10 +28,25 @@
text {* Function with complete, non-overlapping patterns *}
case_of_simps foo_cases1: foo.simps
+lemma
+ fixes xs :: "'a list" and ys :: "'b list"
+ shows "foo xs ys = (case (xs, ys) of
+ ( [], []) \<Rightarrow> 3
+ | ([], y # ys) \<Rightarrow> 1
+ | (x # xs, []) \<Rightarrow> 0
+ | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+ by (fact foo_cases1)
text {* Redundant equations are ignored *}
case_of_simps foo_cases2: foo.simps foo.simps
-print_theorems
+lemma
+ fixes xs :: "'a list" and ys :: "'b list"
+ shows "foo xs ys = (case (xs, ys) of
+ ( [], []) \<Rightarrow> 3
+ | ([], y # ys) \<Rightarrow> 1
+ | (x # xs, []) \<Rightarrow> 0
+ | (x # xs, y # ys) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+ by (fact foo_cases2)
text {* Variable patterns *}
case_of_simps bar_cases: bar.simps
@@ -39,33 +54,66 @@
text {* Case expression not at top level *}
simps_of_case split_rule_test_simps: split_rule_test_def
-print_theorems
+lemma
+ "split_rule_test (Inl x) f = f (x 1)"
+ "split_rule_test (Inr (x, None)) f = f (inv f 0)"
+ "split_rule_test (Inr (x, Some y)) f = f (y x)"
+ by (fact split_rule_test_simps)+
text {* Argument occurs both as case parameter and seperately*}
simps_of_case nosplit_simps1: nosplit_def
-print_theorems
+lemma
+ "nosplit [] = [] @ [1]"
+ "nosplit (x # xs) = (x # xs) @ x # xs"
+ by (fact nosplit_simps1)+
text {* Nested case expressions *}
simps_of_case test_simps1: test_def
-print_theorems
+lemma
+ "test None [] = 1"
+ "test None (x # xs) = 2"
+ "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)
-print_theorems
+lemma
+ "nosplit [] = [] @ [1]"
+ "nosplit (x # xs) = (x # xs) @ x # xs"
+ by (fact nosplit_simps1)+
+
simps_of_case test_simps2: test_def (splits: option.split)
-print_theorems
+lemma
+ "test None y = (case y of [] \<Rightarrow> 1 | x # xs \<Rightarrow> 2)"
+ "test (Some x) y = x"
+ by (fact test_simps2)+
text {* Reversal *}
case_of_simps test_def1: test_simps1
-print_theorems
+lemma
+ "test x y = (case (x,y) of
+ (None, []) \<Rightarrow> 1
+ | (None, _#_) \<Rightarrow> 2
+ | (Some x, _) \<Rightarrow> x)"
+ by (fact test_def1)
text {* Case expressions on RHS *}
case_of_simps test_def2: test_simps2
-print_theorems
+lemma "test xs y = (case (xs, y) of (None, []) \<Rightarrow> 1 | (None, x # xa) \<Rightarrow> 2 | (Some x, y) \<Rightarrow> x)"
+ by (fact test_def2)
text {* Partial split of simps *}
case_of_simps foo_cons_def: foo.simps(1,2)
-print_theorems
-
+lemma
+ fixes xs :: "'a list" and ys :: "'b list"
+ shows "foo (x # xs) ys = (case (x,xs,ys) of
+ (_,_,[]) \<Rightarrow> 0
+ | (_,_,_ # _) \<Rightarrow> foo ([] :: 'a list) ([] :: 'b list))"
+ by (fact foo_cons_def)
end