merged

--- a/src/HOL/Product_Type.thy	Wed Oct 17 22:11:12 2012 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 17 22:45:40 2012 +0200
@@ -306,6 +306,12 @@
 
 subsubsection {* Fundamental operations and properties *}
 
+lemma Pair_inject:
+  assumes "(a, b) = (a', b')"
+    and "a = a' ==> b = b' ==> R"
+  shows R
+  using assms by simp
+
 lemma surj_pair [simp]: "EX x y. p = (x, y)"
   by (cases p) simp
 
@@ -1140,12 +1146,6 @@
   obtains x y where "p = (x, y)"
   by (fact prod.exhaust)
 
-lemma Pair_inject:
-  assumes "(a, b) = (a', b')"
-    and "a = a' ==> b = b' ==> R"
-  shows R
-  using assms by simp
-
 lemmas Pair_eq = prod.inject
 
 lemmas split = split_conv  -- {* for backwards compatibility *}

--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 22:11:12 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 22:45:40 2012 +0200
@@ -89,6 +89,17 @@
       HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
   | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
 
+(* a variant of HOLogic.strip_psplits *)
+val strip_psplits =
+  let
+    fun strip [] qs vs t = (t, rev vs, qs)
+      | strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) =
+          strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
+      | strip (p :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
+      | strip (p :: ps) qs vs t = strip ps qs
+          ((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs)
+          (incr_boundvars 1 t $ Bound 0)
+  in strip [[]] [] [] end;
 
 (* patterns *)
 
@@ -119,26 +130,32 @@
 
 datatype formula = Atom of (pattern * term) | Int of formula * formula | Un of formula * formula
 
+fun map_atom f (Atom a) = Atom (f a)
+  | map_atom _ x = x
+
 fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) =
-    (case try mk_pattern x of
+    if not (null (loose_bnos s)) then
+      raise TERM ("mk_atom: bound variables in the set expression", [s])
+    else
+      (case try mk_pattern x of
       SOME pat => (pat, Atom (pat, s))
     | NONE =>
-      let
-        val bs = loose_bnos x
-        val vs' = map (nth (rev vs)) bs
-        val x' = subst_atomic (map_index (fn (i, j) => (Bound j, Bound i)) (rev bs)) x
-        val tuple = foldr1 TPair (map TBound bs)
-        val rT = HOLogic.dest_setT (fastype_of s)
-        fun mk_split [(x, T)] t = (T, Abs (x, T, t))
-          | mk_split ((x, T) :: vs) t =
-              let
-                val (T', t') = mk_split vs t
-                val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
-              in (domain_type (fastype_of t''), t'') end
-        val (_, f) = mk_split vs' x'
-      in (tuple, Atom (tuple, mk_vimage f s)) end)
-  | mk_atom _ (Const (@{const_name "HOL.Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ x $ s)) =
-      (mk_pattern x, Atom (mk_pattern x, mk_Compl s))
+        let
+          val bs = loose_bnos x
+          val vs' = map (nth (rev vs)) bs
+          val x' = subst_atomic (map_index (fn (i, j) => (Bound j, Bound i)) (rev bs)) x
+          val tuple = foldr1 TPair (map TBound bs)
+          val rT = HOLogic.dest_setT (fastype_of s)
+          fun mk_split [(x, T)] t = (T, Abs (x, T, t))
+            | mk_split ((x, T) :: vs) t =
+                let
+                  val (T', t') = mk_split vs t
+                  val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
+                in (domain_type (fastype_of t''), t'') end
+          val (_, f) = mk_split vs' x'
+        in (tuple, Atom (tuple, mk_vimage f s)) end)
+  | mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) =
+      apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
 
 fun can_merge (pats1, pats2) =
   let
@@ -292,6 +309,47 @@
   end;
 
 
+(* preprocessing conversion:
+  rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *)
+
+fun comprehension_conv ctxt ct =
+let
+  fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t)
+    | dest_Collect t = raise TERM ("dest_Collect", [t])
+  fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t
+  fun mk_term t =
+    let
+      val (T, t') = dest_Collect t
+      val (t'', vs, fp) = case strip_psplits t' of
+          (_, [_], _) => raise TERM("mk_term", [t'])
+        | (t'', vs, fp) => (t'', vs, fp)
+      val Ts = map snd vs
+      val eq = HOLogic.eq_const T $ Bound (length Ts) $
+        (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts)))
+    in
+      HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
+    end;
+  val tac = 
+    rtac @{thm set_eqI}
+    THEN' Simplifier.simp_tac
+      (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm mem_Collect_eq}, @{thm prod.cases}])
+    THEN' rtac @{thm iffI}
+    THEN' REPEAT_DETERM o rtac @{thm exI}
+    THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
+    THEN' REPEAT_DETERM o etac @{thm exE}
+    THEN' etac @{thm conjE}
+    THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+    THEN' hyp_subst_tac
+    THEN' (atac ORELSE' rtac @{thm refl})
+in
+  case try mk_term (term_of ct) of
+    NONE => Thm.reflexive ct
+  | SOME t' =>
+     Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) (K (tac 1))
+       RS @{thm eq_reflection}
+end
+
+
 (* main simprocs *)
 
 val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
@@ -304,7 +362,7 @@
 fun conv ctxt t =
   let
     val ct = cterm_of (Proof_Context.theory_of ctxt) t
-    val prep_eq = Raw_Simplifier.rewrite true prep_thms ct 
+    val prep_eq = (comprehension_conv ctxt then_conv Raw_Simplifier.rewrite true prep_thms) ct
     val t' = term_of (Thm.rhs_of prep_eq)
     fun mk_thm (fm, t'') = Goal.prove ctxt [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)

--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 17 22:11:12 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 17 22:45:40 2012 +0200
@@ -39,7 +39,7 @@
     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}"
   by simp
 
-lemma (* check arbitrary ordering *)
+lemma
   "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
     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'}"
   by simp
@@ -104,21 +104,16 @@
     ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
   by (auto intro: finite_vimageI)
 
+lemma
+  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
+  (* injectivity to be automated with further rules and automation *)
 
 schematic_lemma (* check interaction with schematics *)
   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   by simp
 
-lemma
-  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
-proof -
-  have eq: "{(a,b,c,d). ([a, b], [c, d]) : S} = ((%(a, b, c, d). ([a, b], [c, d])) -` S)"
-   unfolding vimage_def by (auto split: prod.split)  (* to be proved with the simproc *)
-  from `finite S` show ?thesis
-    unfolding eq by (auto intro!: finite_vimageI simp add: inj_on_def)
-    (* to be automated with further rules and automation *)
-qed
 
 section {* Testing simproc in code generation *}
 
@@ -132,6 +127,4 @@
 
 export_code union common_subsets in Haskell file -
 
-
-
 end