# HG changeset patch # User paulson # Date 1430409643 -3600 # Node ID 670cddd9756327c8418566e24ada0c6100ce16dc # Parent 1d218c3e84e2d894972cc57fa47d8221d36c8e2c# Parent 52aa014308cb1d3176d3b4961677976d65657282 Merge diff -r 1d218c3e84e2 -r 670cddd97563 src/HOL/List.thy --- a/src/HOL/List.thy Thu Apr 30 15:33:59 2015 +0100 +++ b/src/HOL/List.thy Thu Apr 30 17:00:43 2015 +0100 @@ -486,35 +486,38 @@ ML_val {* let - val read = Syntax.read_term @{context}; - fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1); + val read = Syntax.read_term @{context} o Syntax.implode_input; + fun check s1 s2 = + read s1 aconv read s2 orelse + error ("Check failed: " ^ + quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]); in - check "[(x,y,z). b]" "if b then [(x, y, z)] else []"; - check "[(x,y,z). x\xs]" "map (\x. (x, y, z)) xs"; - check "[e x y. x\xs, y\ys]" "concat (map (\x. map (\y. e x y) ys) xs)"; - check "[(x,y,z). xb]" "if x < a then if b < x then [(x, y, z)] else [] else []"; - check "[(x,y,z). x\xs, x>b]" "concat (map (\x. if b < x then [(x, y, z)] else []) xs)"; - check "[(x,y,z). xxs]" "if x < a then map (\x. (x, y, z)) xs else []"; - check "[(x,y). Cons True x \ xs]" - "concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)"; - check "[(x,y,z). Cons x [] \ xs]" - "concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)"; - check "[(x,y,z). xb, x=d]" - "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []"; - check "[(x,y,z). xb, y\ys]" - "if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []"; - check "[(x,y,z). xxs,y>b]" - "if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []"; - check "[(x,y,z). xxs, y\ys]" - "if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []"; - check "[(x,y,z). x\xs, x>b, yx. if b < x then if y < a then [(x, y, z)] else [] else []) xs)"; - check "[(x,y,z). x\xs, x>b, y\ys]" - "concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)"; - check "[(x,y,z). x\xs, y\ys,y>x]" - "concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)"; - check "[(x,y,z). x\xs, y\ys,z\zs]" - "concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)" + check \[(x,y,z). b]\ \if b then [(x, y, z)] else []\; + check \[(x,y,z). x\xs]\ \map (\x. (x, y, z)) xs\; + check \[e x y. x\xs, y\ys]\ \concat (map (\x. map (\y. e x y) ys) xs)\; + check \[(x,y,z). xb]\ \if x < a then if b < x then [(x, y, z)] else [] else []\; + check \[(x,y,z). x\xs, x>b]\ \concat (map (\x. if b < x then [(x, y, z)] else []) xs)\; + check \[(x,y,z). xxs]\ \if x < a then map (\x. (x, y, z)) xs else []\; + check \[(x,y). Cons True x \ xs]\ + \concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)\; + check \[(x,y,z). Cons x [] \ xs]\ + \concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)\; + check \[(x,y,z). xb, x=d]\ + \if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\; + check \[(x,y,z). xb, y\ys]\ + \if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []\; + check \[(x,y,z). xxs,y>b]\ + \if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []\; + check \[(x,y,z). xxs, y\ys]\ + \if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []\; + check \[(x,y,z). x\xs, x>b, y + \concat (map (\x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)\; + check \[(x,y,z). x\xs, x>b, y\ys]\ + \concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)\; + check \[(x,y,z). x\xs, y\ys,y>x]\ + \concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)\; + check \[(x,y,z). x\xs, y\ys,z\zs]\ + \concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)\ end; *} @@ -569,116 +572,128 @@ datatype termlets = If | Case of typ * int -fun simproc ctxt redex = +local + +val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])} +val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} +val inst_Collect_mem_eq = @{lemma "set A = {x. x \ set A}" by simp} +val del_refl_eq = @{lemma "(t = t \ P) \ P" by simp} + +fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T) +fun dest_set (Const (@{const_name set}, _) $ xs) = xs + +fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t + | dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) + +(*We check that one case returns a singleton list and all other cases + return [], and return the index of the one singleton list case.*) +fun possible_index_of_singleton_case cases = let - val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])} - val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} - val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} - val del_refl_eq = @{lemma "(t = t \ P) \ P" by simp} - fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T) - fun dest_set (Const (@{const_name set}, _) $ xs) = xs - fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t - | dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) - (* We check that one case returns a singleton list and all other cases - return [], and return the index of the one singleton list case *) - fun possible_index_of_singleton_case cases = - let - fun check (i, case_t) s = - (case strip_abs_body case_t of - (Const (@{const_name Nil}, _)) => s - | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE)) - in - fold_index check cases (SOME NONE) |> the_default NONE - end - (* returns (case_expr type index chosen_case constr_name) option *) - fun dest_case case_term = - let - val (case_const, args) = strip_comb case_term - in - (case try dest_Const case_const of - SOME (c, T) => - (case Ctr_Sugar.ctr_sugar_of_case ctxt c of - SOME {ctrs, ...} => - (case possible_index_of_singleton_case (fst (split_last args)) of - SOME i => - let - val constr_names = map (fst o dest_Const) ctrs - val (Ts, _) = strip_type T - val T' = List.last Ts - in SOME (List.last args, T', i, nth args i, nth constr_names i) end - | NONE => NONE) + fun check (i, case_t) s = + (case strip_abs_body case_t of + (Const (@{const_name Nil}, _)) => s + | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE)) + in + fold_index check cases (SOME NONE) |> the_default NONE + end + +(*returns condition continuing term option*) +fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = + SOME (cond, then_t) + | dest_if _ = NONE + +(*returns (case_expr type index chosen_case constr_name) option*) +fun dest_case ctxt case_term = + let + val (case_const, args) = strip_comb case_term + in + (case try dest_Const case_const of + SOME (c, T) => + (case Ctr_Sugar.ctr_sugar_of_case ctxt c of + SOME {ctrs, ...} => + (case possible_index_of_singleton_case (fst (split_last args)) of + SOME i => + let + val constr_names = map (fst o dest_Const) ctrs + val (Ts, _) = strip_type T + val T' = List.last Ts + in SOME (List.last args, T', i, nth args i, nth constr_names i) end | NONE => NONE) | NONE => NONE) - end - (* returns condition continuing term option *) - fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = - SOME (cond, then_t) - | dest_if _ = NONE - fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 - | tac ctxt (If :: cont) = - Splitter.split_tac ctxt [@{thm split_if}] 1 - THEN rtac @{thm conjI} 1 - THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv - then_conv - rewr_conv' @{lemma "(True \ P) = P" by simp})) context) 1) ctxt 1 - THEN tac ctxt cont + | NONE => NONE) + end + +fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 + | tac ctxt (If :: cont) = + Splitter.split_tac ctxt @{thms split_if} 1 + THEN rtac @{thm conjI} 1 + THEN rtac @{thm impI} 1 + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv + then_conv + rewr_conv' @{lemma "(True \ P) = P" by simp})) ctxt') 1) ctxt 1 + THEN tac ctxt cont + THEN rtac @{thm impI} 1 + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv + then_conv rewr_conv' @{lemma "(False \ P) = False" by simp})) ctxt') 1) ctxt 1 + THEN rtac set_Nil_I 1 + | tac ctxt (Case (T, i) :: cont) = + let + val SOME {injects, distincts, case_thms, split, ...} = + Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T)) + in + (* do case distinction *) + Splitter.split_tac ctxt [split] 1 + THEN EVERY (map_index (fn (i', _) => + (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac) + THEN REPEAT_DETERM (rtac @{thm allI} 1) THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv - then_conv rewr_conv' @{lemma "(False \ P) = False" by simp})) context) 1) ctxt 1 - THEN rtac set_Nil_I 1 - | tac ctxt (Case (T, i) :: cont) = - let - val SOME {injects, distincts, case_thms, split, ...} = - Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T)) - in - (* do case distinction *) - Splitter.split_tac ctxt [split] 1 - THEN EVERY (map_index (fn (i', _) => - (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac) - THEN REPEAT_DETERM (rtac @{thm allI} 1) - THEN rtac @{thm impI} 1 - THEN (if i' = i then - (* continue recursively *) - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K - ((HOLogic.conj_conv - (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv - (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) - Conv.all_conv) - then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) - then_conv conjunct_assoc_conv)) context - then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => + THEN (if i' = i then + (* continue recursively *) + Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K + ((HOLogic.conj_conv + (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv + (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) + Conv.all_conv) + then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) + then_conv conjunct_assoc_conv)) ctxt' + then_conv + (HOLogic.Trueprop_conv + (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt'') => Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' - @{lemma "(\x. x = t \ P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 - THEN tac ctxt cont - else - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION - (right_hand_set_comprehension_conv (K - (HOLogic.conj_conv - ((HOLogic.eq_conv Conv.all_conv - (rewr_conv' (List.last prems))) then_conv - (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) - Conv.all_conv then_conv - (rewr_conv' @{lemma "(False \ P) = False" by simp}))) context then_conv - HOLogic.Trueprop_conv - (HOLogic.eq_conv Conv.all_conv - (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv - (Conv.bottom_conv - (K (rewr_conv' - @{lemma "(\x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 - THEN rtac set_Nil_I 1)) case_thms) - end + @{lemma "(\x. x = t \ P x) = P t" by simp})) ctxt'')) ctxt')))) 1) ctxt 1 + THEN tac ctxt cont + else + Subgoal.FOCUS (fn {prems, context = ctxt', ...} => + CONVERSION + (right_hand_set_comprehension_conv (K + (HOLogic.conj_conv + ((HOLogic.eq_conv Conv.all_conv + (rewr_conv' (List.last prems))) then_conv + (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) + Conv.all_conv then_conv + (rewr_conv' @{lemma "(False \ P) = False" by simp}))) ctxt' then_conv + HOLogic.Trueprop_conv + (HOLogic.eq_conv Conv.all_conv + (Collect_conv (fn (_, ctxt'') => + Conv.repeat_conv + (Conv.bottom_conv + (K (rewr_conv' @{lemma "(\x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1 + THEN rtac set_Nil_I 1)) case_thms) + end + +in + +fun simproc ctxt redex = + let fun make_inner_eqs bound_vs Tis eqs t = - (case dest_case t of + (case dest_case ctxt t of SOME (x, T, i, cont, constr_name) => let val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont) @@ -695,7 +710,7 @@ (case dest_if t of SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont | NONE => - if eqs = [] then NONE (* no rewriting, nothing to be done *) + if null eqs then NONE (*no rewriting, nothing to be done*) else let val Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t) @@ -720,19 +735,21 @@ in SOME ((Goal.prove ctxt [] [] rewrite_rule_t - (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) + (fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection}) end)) in make_inner_eqs [] [] [] (dest_set (Thm.term_of redex)) end end + +end *} -simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} +simproc_setup list_to_set_comprehension ("set xs") = + {* K List_to_Set_Comprehension.simproc *} code_datatype set coset - hide_const (open) coset