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.

--- 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 \<and> b : B}"
-apply simp (* works :) *)
-oops
+  apply simp
+  oops
 
 lemma
   "finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
-(* apply simp -- does not terminate *)
-oops
+  apply simp
+  oops
 
 lemma
   "finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
-(* apply simp -- does not terminate *)
-oops
+  apply simp
+  oops
 
 lemma
   "finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
-(* apply simp -- failed *) 
-oops
+  apply simp
+  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
+  apply simp
+  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
+  apply simp
+  oops
+
+lemma (* check arbitrary ordering *)
+  "finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
+  apply simp
+  oops
+
+lemma
+  "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
+  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+  by simp
+
+lemma
+  "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
+  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
+  by simp
+
+schematic_lemma (* check interaction with schematics *)
+  "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
+   = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
+  by simp
 
 end

--- 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;
+