adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
--- a/src/HOL/IsaMakefile Thu May 31 10:05:07 2012 +0200
+++ b/src/HOL/IsaMakefile Mon May 28 02:18:46 2012 +0200
@@ -1035,14 +1035,16 @@
ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quicksort.thy ex/ROOT.ML \
ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
- ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
- ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
- ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
+ ex/SAT_Examples.thy ex/Serbian.thy \
+ ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy \
+ ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
+ ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
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/svc_test.thy ../Tools/interpretation_with_defs.ML \
+ ex/set_comprehension_pointfree.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/ex/ROOT.ML Thu May 31 10:05:07 2012 +0200
+++ b/src/HOL/ex/ROOT.ML Mon May 28 02:18:46 2012 +0200
@@ -72,7 +72,8 @@
"Seq",
"Simproc_Tests",
"Executable_Relation",
- "FinFunPred"
+ "FinFunPred",
+ "Set_Comprehension_Pointfree_Tests"
];
use_thy "SVC_Oracle";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Mon May 28 02:18:46 2012 +0200
@@ -0,0 +1,45 @@
+(* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy
+ Author: Lukas Bulwahn
+ Copyright 2012 TU Muenchen
+*)
+
+header {* Tests for the set comprehension to pointfree simproc *}
+
+theory Set_Comprehension_Pointfree_Tests
+imports Main
+uses "~~/src/HOL/ex/set_comprehension_pointfree.ML"
+begin
+
+simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
+
+lemma
+ "finite {f a b| a b. a : A \<and> b : B}"
+apply simp (* works :) *)
+oops
+
+lemma
+ "finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
+(* apply simp -- does not terminate *)
+oops
+
+lemma
+ "finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
+(* apply simp -- does not terminate *)
+oops
+
+lemma
+ "finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
+(* apply simp -- failed *)
+oops
+
+lemma
+ "finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
+(* apply simp -- failed *)
+oops
+
+lemma
+ "finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
+(* apply simp -- failed *)
+oops
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/set_comprehension_pointfree.ML Mon May 28 02:18:46 2012 +0200
@@ -0,0 +1,120 @@
+(* Title: HOL/Tools/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;