# HG changeset patch # User bulwahn # Date 1340274807 -7200 # Node ID 10d628621c4380a6b7e2c33d62b30b3d0ea5add2 # Parent 22994525d0d4a909b7b714807914b64c23b3967e# Parent 0a58f7eefba2025d0147bf7e987d7bc209d10a87 merged diff -r 22994525d0d4 -r 10d628621c43 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sun Jun 17 20:38:12 2012 +0200 +++ b/src/HOL/Finite_Set.thy Thu Jun 21 12:33:27 2012 +0200 @@ -7,6 +7,7 @@ theory Finite_Set imports Option Power +uses ("Tools/set_comprehension_pointfree.ML") begin subsection {* Predicate for finite sets *} @@ -16,6 +17,12 @@ emptyI [simp, intro!]: "finite {}" | insertI [simp, intro!]: "finite A \ finite (insert a A)" +use "Tools/set_comprehension_pointfree.ML" + +simproc_setup finite_Collect ("finite (Collect P)") = + {* Set_Comprehension_Pointfree.simproc *} + + lemma finite_induct [case_names empty insert, induct set: finite]: -- {* Discharging @{text "x \ F"} entails extra work. *} assumes "finite F" diff -r 22994525d0d4 -r 10d628621c43 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jun 17 20:38:12 2012 +0200 +++ b/src/HOL/IsaMakefile Thu Jun 21 12:33:27 2012 +0200 @@ -259,6 +259,7 @@ Tools/rewrite_hol_proof.ML \ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ + Tools/set_comprehension_pointfree.ML \ Tools/split_rule.ML \ Tools/try0.ML \ Tools/typedef.ML \ @@ -1042,8 +1043,7 @@ ex/Transfer_Int_Nat.thy \ ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ - ex/svc_test.thy ../Tools/interpretation_with_defs.ML \ - ex/set_comprehension_pointfree.ML + ex/svc_test.thy ../Tools/interpretation_with_defs.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex diff -r 22994525d0d4 -r 10d628621c43 src/HOL/Tools/set_comprehension_pointfree.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Jun 21 12:33:27 2012 +0200 @@ -0,0 +1,155 @@ +(* 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. +*) + +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 = +struct + +(* syntactic operations *) + +fun mk_inf (t1, t2) = + let + val T = fastype_of t1 + in + Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2 + end + +fun mk_image t1 t2 = + 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 + end; + +fun mk_sigma (t1, t2) = + let + val T1 = fastype_of t1 + val T2 = fastype_of t2 + val setT = HOLogic.dest_setT T1 + val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) + in + Const (@{const_name Sigma}, + T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2 + end; + +fun dest_Bound (Bound x) = x + | dest_Bound t = raise TERM("dest_Bound", [t]); + +fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t + | dest_Collect t = raise TERM ("dest_Collect", [t]) + +(* Copied from predicate_compile_aux.ML *) +fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = + let + val (xTs, t') = strip_ex t + in + ((x, T) :: xTs, t') + end + | strip_ex t = ([], t) + +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)) + +fun mk_pointfree_expr t = + let + val (vs, t'') = strip_ex (dest_Collect t) + val (eq::conjs) = HOLogic.dest_conj t'' + val f = if fst (HOLogic.dest_eq eq) = Bound (length vs) + then snd (HOLogic.dest_eq eq) + else raise TERM("mk_pointfree_expr", [t]); + val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs + val grouped_mems = AList.group (op =) mems + fun mk_grouped_unions (i, T) = + case AList.lookup (op =) grouped_mems i of + SOME ts => foldr1 mk_inf ts + | NONE => HOLogic.mk_UNIV T + val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs) + in + mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets) + end; + +val rewrite_term = try mk_pointfree_expr + +(* proof tactic *) + +(* 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 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 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 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 = + 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 *) + +fun simproc _ ss redex = + let + val ctxt = Simplifier.the_context ss + val _ $ set_compr = term_of redex + in + conv ctxt set_compr + |> Option.map (fn thm => + thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection}) + end; + +end; + diff -r 22994525d0d4 -r 10d628621c43 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Jun 17 20:38:12 2012 +0200 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Thu Jun 21 12:33:27 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 *) @@ -7,39 +7,61 @@ theory Set_Comprehension_Pointfree_Tests imports Main -uses "set_comprehension_pointfree.ML" begin -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 22994525d0d4 -r 10d628621c43 src/HOL/ex/set_comprehension_pointfree.ML --- a/src/HOL/ex/set_comprehension_pointfree.ML Sun Jun 17 20:38:12 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -(* Title: HOL/ex/set_comprehension_pointfree.ML - Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen - -Simproc for rewriting set comprehensions to pointfree expressions. -*) - -signature SET_COMPREHENSION_POINTFREE = -sig - val simproc : morphism -> simpset -> cterm -> thm option -end - -structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE = -struct - -(* syntactic operations *) - -fun mk_inf (t1, t2) = - let - val T = fastype_of t1 - in - Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2 - end - -fun mk_image t1 t2 = - 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 - end; - -fun mk_sigma (t1, t2) = - let - 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)) - in - Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2 - end; - -fun dest_Bound (Bound x) = x - | dest_Bound t = raise TERM("dest_Bound", [t]); - -fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t - | dest_Collect t = raise TERM ("dest_Collect", [t]) - -(* Copied from predicate_compile_aux.ML *) -fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = - let - val (xTs, t') = strip_ex t - in - ((x, T) :: xTs, t') - end - | strip_ex t = ([], t) - -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)) - -fun mk_pointfree_expr t = - let - val (vs, t'') = strip_ex (dest_Collect t) - val (eq::conjs) = HOLogic.dest_conj t'' - val f = if fst (HOLogic.dest_eq eq) = Bound (length vs) - then snd (HOLogic.dest_eq eq) - else raise TERM("mk_pointfree_expr", [t]); - val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs - val grouped_mems = AList.group (op =) mems - fun mk_grouped_unions (i, T) = - case AList.lookup (op =) grouped_mems i of - SOME ts => foldr1 mk_inf ts - | NONE => HOLogic.mk_UNIV T - val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs) - in - mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets) - end; - -(* proof tactic *) - -(* This tactic is terribly incomplete *) - -val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI})) - -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 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 tac = - rtac @{thm set_eqI} 1 - THEN rtac @{thm iffI} 1 - THEN goal1_tac 1 - THEN goal2_tac 1 - -(* simproc *) - -fun simproc _ ss redex = - let - 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 - -end; diff -r 22994525d0d4 -r 10d628621c43 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Sun Jun 17 20:38:12 2012 +0200 +++ b/src/Provers/hypsubst.ML Thu Jun 21 12:33:27 2012 +0200 @@ -2,7 +2,7 @@ Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson Copyright 1995 University of Cambridge -Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst". +Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst". Tactic to substitute using (at least) the assumption x=t in the rest of the subgoal, and to delete (at least) that assumption. Original