# HG changeset patch # User noschinl # Date 1436456164 -7200 # Node ID 8963331cc0de3beca9c031bcf9d53d5766e90406 # Parent 5e03e1bd1be02ae5c54f8a81c15513bbe78521d3# Parent 7536369a5546b867d3f6864a3537c5b8edb691e4 merged diff -r 7536369a5546 -r 8963331cc0de src/HOL/Library/simps_case_conv.ML --- 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 diff -r 7536369a5546 -r 8963331cc0de src/HOL/ex/Simps_Case_Conv_Examples.thy --- 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 + ( [], []) \ 3 + | ([], y # ys) \ 1 + | (x # xs, []) \ 0 + | (x # xs, y # ys) \ 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 + ( [], []) \ 3 + | ([], y # ys) \ 1 + | (x # xs, []) \ 0 + | (x # xs, y # ys) \ 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) \ 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 [] \ 1 | x # xs \ 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, []) \ 1 + | (None, _#_) \ 2 + | (Some x, _) \ 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, []) \ 1 | (None, x # xa) \ 2 | (Some x, y) \ 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 + (_,_,[]) \ 0 + | (_,_,_ # _) \ foo ([] :: 'a list) ([] :: 'b list))" + by (fact foo_cons_def) end