# HG changeset patch # User Rafal Kolanski # Date 1340097401 -7200 # Node ID f93433b451b8eb088f05ee7bd4c80f0da6c1f7dd # Parent 6cebeee3863e2f135be104ad3ff1c15886e2f55e Improved tactic for rewriting set comprehensions into pointfree form. Currently the simproc targets a term with an arbitrary number of conjuncts of form "x : S". The tactic should now handle all cases of this form. diff -r 6cebeee3863e -r f93433b451b8 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Jun 19 11:18:09 2012 +0200 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Jun 19 11:16:41 2012 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy - Author: Lukas Bulwahn + Author: Lukas Bulwahn, Rafal Kolanski Copyright 2012 TU Muenchen *) @@ -10,36 +10,62 @@ uses "set_comprehension_pointfree.ML" begin -simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *} +simproc_setup finite_Collect ("finite (Collect P)") = + {* Set_Comprehension_Pointfree.simproc *} + +lemma + "finite {p. EX x. p = (x, x)}" + apply simp + oops lemma "finite {f a b| a b. a : A \ b : B}" -apply simp (* works :) *) -oops + apply simp + oops lemma "finite {f a b| a b. a : A \ a : A' \ b : B}" -(* apply simp -- does not terminate *) -oops + apply simp + oops lemma "finite {f a b| a b. a : A \ b : B \ b : B'}" -(* apply simp -- does not terminate *) -oops + apply simp + oops lemma "finite {f a b c| a b c. a : A \ b : B \ c : C}" -(* apply simp -- failed *) -oops + apply simp + oops lemma "finite {f a b c d| a b c d. a : A \ b : B \ c : C \ d : D}" -(* apply simp -- failed *) -oops + apply simp + oops lemma "finite {f a b c d e | a b c d e. a : A \ b : B \ c : C \ d : D \ e : E}" -(* apply simp -- failed *) -oops + apply simp + oops + +lemma (* check arbitrary ordering *) + "finite {f a d c b e | e b c d a. b : B \ a : A \ e : E' \ c : C \ d : D \ e : E \ b : B'}" + apply simp + oops + +lemma + "\ finite A ; finite B ; finite C ; finite D \ + \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ d : D})" + by simp + +lemma + "finite ((\(a,b,c,d). f a b c d) ` (A \ B \ C \ D)) + \ finite ({f a b c d| a b c d. a : A \ b : B \ c : C \ d : D})" + by simp + +schematic_lemma (* check interaction with schematics *) + "finite {x :: ?'A \ ?'B \ bool. \a b. x = Pair_Rep a b} + = finite ((\(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \ UNIV))" + by simp end diff -r 6cebeee3863e -r f93433b451b8 src/HOL/ex/set_comprehension_pointfree.ML --- a/src/HOL/ex/set_comprehension_pointfree.ML Tue Jun 19 11:18:09 2012 +0200 +++ b/src/HOL/ex/set_comprehension_pointfree.ML Tue Jun 19 11:16:41 2012 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/ex/set_comprehension_pointfree.ML Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen + Rafal Kolanski, NICTA Simproc for rewriting set comprehensions to pointfree expressions. *) @@ -7,6 +8,8 @@ signature SET_COMPREHENSION_POINTFREE = sig val simproc : morphism -> simpset -> cterm -> thm option + val rewrite_term : term -> term option + val conv : Proof.context -> term -> thm option end structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE = @@ -25,7 +28,8 @@ let val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1 in - Const (@{const_name image}, T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2 + Const (@{const_name image}, + T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2 end; fun mk_sigma (t1, t2) = @@ -33,9 +37,10 @@ val T1 = fastype_of t1 val T2 = fastype_of t2 val setT = HOLogic.dest_setT T1 - val resultT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) + val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) in - Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2 + Const (@{const_name Sigma}, + T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2 end; fun dest_Bound (Bound x) = x @@ -55,8 +60,9 @@ fun list_tupled_abs [] f = f | list_tupled_abs [(n, T)] f = (Abs (n, T, f)) - | list_tupled_abs ((n, T)::v::vs) f = HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) - + | list_tupled_abs ((n, T)::v::vs) f = + HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) + fun mk_pointfree_expr t = let val (vs, t'') = strip_ex (dest_Collect t) @@ -75,32 +81,63 @@ mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets) end; +val rewrite_term = try mk_pointfree_expr + (* proof tactic *) -(* This tactic is terribly incomplete *) +(* Tactic works for arbitrary number of m : S conjuncts *) + +val dest_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]} + THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE conjE})) + THEN' hyp_subst_tac; -val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI})) +val intro_image_Sigma_tac = rtac @{thm image_eqI} + THEN' (REPEAT_DETERM1 o + (rtac @{thm refl} + ORELSE' rtac + @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]})); -val goal1_tac = etac @{thm CollectE} - THEN' REPEAT1 o CHANGED o etac @{thm exE} - THEN' REPEAT1 o CHANGED o etac @{thm conjE} - THEN' rtac @{thm image_eqI} - THEN' RANGE [(REPEAT o CHANGED o stac @{thm split}) THEN' goal1_tac_part2, goal1_tac_part2] +val dest_image_Sigma_tac = etac @{thm imageE} + THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm}) + THEN' hyp_subst_tac + THEN' (TRY o REPEAT_DETERM1 o + (etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]})); -val goal2_tac = etac @{thm imageE} - THEN' rtac @{thm CollectI} - THEN' REPEAT o CHANGED o etac @{thm SigmaE} - THEN' REPEAT o CHANGED o rtac @{thm exI} - THEN' REPEAT_ALL_NEW (rtac @{thm conjI}) - THEN_ALL_NEW - (atac ORELSE' - (asm_full_simp_tac HOL_basic_ss THEN' stac @{thm split} THEN' rtac @{thm refl})) +val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]} + THEN' REPEAT_DETERM1 o resolve_tac @{thms exI} + THEN' (TRY o (rtac @{thm conjI})) + THEN' (TRY o hyp_subst_tac) + THEN' rtac @{thm refl}; val tac = - rtac @{thm set_eqI} 1 - THEN rtac @{thm iffI} 1 - THEN goal1_tac 1 - THEN goal2_tac 1 + let + val subset_tac1 = rtac @{thm subsetI} + THEN' dest_Collect_tac + THEN' intro_image_Sigma_tac + THEN' (REPEAT_DETERM1 o + (rtac @{thm SigmaI} + ORELSE' rtac @{thm UNIV_I} + ORELSE' rtac @{thm IntI} + ORELSE' atac)); + + val subset_tac2 = rtac @{thm subsetI} + THEN' dest_image_Sigma_tac + THEN' intro_Collect_tac + THEN' REPEAT_DETERM o + (rtac @{thm conjI} + ORELSE' eresolve_tac @{thms IntD1 IntD2} + ORELSE' atac); + in + rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2 + end; + +fun conv ctxt t = + let + fun mk_thm t' = Goal.prove ctxt [] [] + (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) (K (tac 1)); + in + Option.map mk_thm (rewrite_term t) + end; (* simproc *) @@ -109,12 +146,10 @@ val ctxt = Simplifier.the_context ss val _ $ set_compr = term_of redex in - case try mk_pointfree_expr set_compr of - NONE => NONE - | SOME pointfree_expr => - SOME (Goal.prove ctxt [] [] - (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_compr, pointfree_expr))) (K tac) - RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection}) - end + conv ctxt set_compr + |> Option.map (fn thm => + thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection}) + end; end; +