1.1 --- a/src/HOL/IsaMakefile	Thu May 31 10:05:07 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon May 28 02:18:46 2012 +0200
     1.3 @@ -1035,14 +1035,16 @@
     1.4    ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
     1.5    ex/Quicksort.thy ex/ROOT.ML						\
     1.6    ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
     1.7 -  ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy			\
     1.8 -  ex/Simproc_Tests.thy ex/SVC_Oracle.thy		\
     1.9 -  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 	\
    1.10 +  ex/SAT_Examples.thy ex/Serbian.thy 					\
    1.11 +  ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy		\
    1.12 +  ex/Simproc_Tests.thy ex/SVC_Oracle.thy				\
    1.13 +  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 				\
    1.14    ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
    1.15    ex/Transfer_Int_Nat.thy						\
    1.16    ex/Tree23.thy	ex/Unification.thy ex/While_Combinator_Example.thy	\
    1.17    ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML		\
    1.18 -  ex/svc_test.thy ../Tools/interpretation_with_defs.ML
    1.19 +  ex/svc_test.thy ../Tools/interpretation_with_defs.ML			\
    1.20 +  ex/set_comprehension_pointfree.ML
    1.21  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.22  
    1.23  

     2.1 --- a/src/HOL/ex/ROOT.ML	Thu May 31 10:05:07 2012 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Mon May 28 02:18:46 2012 +0200
     2.3 @@ -72,7 +72,8 @@
     2.4    "Seq",
     2.5    "Simproc_Tests",
     2.6    "Executable_Relation",
     2.7 -  "FinFunPred"
     2.8 +  "FinFunPred",
     2.9 +  "Set_Comprehension_Pointfree_Tests"
    2.10  ];
    2.11  
    2.12  use_thy "SVC_Oracle";

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Mon May 28 02:18:46 2012 +0200
     3.3 @@ -0,0 +1,45 @@
     3.4 +(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Tests.thy
     3.5 +    Author:     Lukas Bulwahn
     3.6 +    Copyright   2012 TU Muenchen
     3.7 +*)
     3.8 +
     3.9 +header {* Tests for the set comprehension to pointfree simproc *}
    3.10 +
    3.11 +theory Set_Comprehension_Pointfree_Tests
    3.12 +imports Main
    3.13 +uses "~~/src/HOL/ex/set_comprehension_pointfree.ML"
    3.14 +begin
    3.15 +
    3.16 +simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
    3.17 +
    3.18 +lemma
    3.19 +  "finite {f a b| a b. a : A \<and> b : B}"
    3.20 +apply simp (* works :) *)
    3.21 +oops
    3.22 +
    3.23 +lemma
    3.24 +  "finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
    3.25 +(* apply simp -- does not terminate *)
    3.26 +oops
    3.27 +
    3.28 +lemma
    3.29 +  "finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
    3.30 +(* apply simp -- does not terminate *)
    3.31 +oops
    3.32 +
    3.33 +lemma
    3.34 +  "finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
    3.35 +(* apply simp -- failed *) 
    3.36 +oops
    3.37 +
    3.38 +lemma
    3.39 +  "finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
    3.40 +(* apply simp -- failed *)
    3.41 +oops
    3.42 +
    3.43 +lemma
    3.44 +  "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}"
    3.45 +(* apply simp -- failed *)
    3.46 +oops
    3.47 +
    3.48 +end

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/set_comprehension_pointfree.ML	Mon May 28 02:18:46 2012 +0200
     4.3 @@ -0,0 +1,120 @@
     4.4 +(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     4.5 +    Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
     4.6 +
     4.7 +Simproc for rewriting set comprehensions to pointfree expressions.
     4.8 +*)
     4.9 +
    4.10 +signature SET_COMPREHENSION_POINTFREE =
    4.11 +sig
    4.12 +  val simproc : morphism -> simpset -> cterm -> thm option
    4.13 +end
    4.14 +
    4.15 +structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
    4.16 +struct
    4.17 +
    4.18 +(* syntactic operations *)
    4.19 +
    4.20 +fun mk_inf (t1, t2) =
    4.21 +  let
    4.22 +    val T = fastype_of t1
    4.23 +  in
    4.24 +    Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
    4.25 +  end
    4.26 +
    4.27 +fun mk_image t1 t2 =
    4.28 +  let
    4.29 +    val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1
    4.30 +  in
    4.31 +    Const (@{const_name image}, T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2
    4.32 +  end;
    4.33 +
    4.34 +fun mk_sigma (t1, t2) =
    4.35 +  let
    4.36 +    val T1 = fastype_of t1
    4.37 +    val T2 = fastype_of t2
    4.38 +    val setT = HOLogic.dest_setT T1
    4.39 +    val resultT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2))
    4.40 +  in
    4.41 +    Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2
    4.42 +  end;
    4.43 +
    4.44 +fun dest_Bound (Bound x) = x
    4.45 +  | dest_Bound t = raise TERM("dest_Bound", [t]);
    4.46 +
    4.47 +fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
    4.48 +  | dest_Collect t = raise TERM ("dest_Collect", [t])
    4.49 +
    4.50 +(* Copied from predicate_compile_aux.ML *)
    4.51 +fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
    4.52 +  let
    4.53 +    val (xTs, t') = strip_ex t
    4.54 +  in
    4.55 +    ((x, T) :: xTs, t')
    4.56 +  end
    4.57 +  | strip_ex t = ([], t)
    4.58 +
    4.59 +fun list_tupled_abs [] f = f
    4.60 +  | list_tupled_abs [(n, T)] f = (Abs (n, T, f))
    4.61 +  | list_tupled_abs ((n, T)::v::vs) f = HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f))
    4.62 +  
    4.63 +fun mk_pointfree_expr t =
    4.64 +  let
    4.65 +    val (vs, t'') = strip_ex (dest_Collect t)
    4.66 +    val (eq::conjs) = HOLogic.dest_conj t''
    4.67 +    val f = if fst (HOLogic.dest_eq eq) = Bound (length vs)
    4.68 +            then snd (HOLogic.dest_eq eq)
    4.69 +            else raise TERM("mk_pointfree_expr", [t]);
    4.70 +    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs
    4.71 +    val grouped_mems = AList.group (op =) mems
    4.72 +    fun mk_grouped_unions (i, T) =
    4.73 +      case AList.lookup (op =) grouped_mems i of
    4.74 +        SOME ts => foldr1 mk_inf ts
    4.75 +      | NONE => HOLogic.mk_UNIV T
    4.76 +    val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs)
    4.77 +  in
    4.78 +    mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets)
    4.79 +  end;
    4.80 +
    4.81 +(* proof tactic *)
    4.82 +
    4.83 +(* This tactic is terribly incomplete *) 
    4.84 +
    4.85 +val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI}))
    4.86 +
    4.87 +val goal1_tac = etac @{thm CollectE}
    4.88 +  THEN' REPEAT1 o CHANGED o etac @{thm exE}
    4.89 +  THEN' REPEAT1 o CHANGED o etac @{thm conjE}
    4.90 +  THEN' rtac @{thm image_eqI}
    4.91 +  THEN' RANGE [(REPEAT o CHANGED o stac @{thm split}) THEN' goal1_tac_part2, goal1_tac_part2]
    4.92 +
    4.93 +val goal2_tac = etac @{thm imageE}
    4.94 +  THEN' rtac @{thm CollectI}
    4.95 +  THEN' REPEAT o CHANGED o etac @{thm SigmaE}
    4.96 +  THEN' REPEAT o CHANGED o rtac @{thm exI}
    4.97 +  THEN' REPEAT_ALL_NEW (rtac @{thm conjI})
    4.98 +  THEN_ALL_NEW
    4.99 +    (atac ORELSE'
   4.100 +    (asm_full_simp_tac HOL_basic_ss THEN' stac @{thm split} THEN' rtac @{thm refl}))
   4.101 +
   4.102 +val tac =
   4.103 +  rtac @{thm set_eqI} 1
   4.104 +  THEN rtac @{thm iffI} 1
   4.105 +  THEN goal1_tac 1
   4.106 +  THEN goal2_tac 1
   4.107 +
   4.108 +(* simproc *)
   4.109 +
   4.110 +fun simproc _ ss redex =
   4.111 +  let
   4.112 +    val ctxt = Simplifier.the_context ss
   4.113 +    val _ $ set_compr = term_of redex
   4.114 +  in
   4.115 +    case try mk_pointfree_expr set_compr of
   4.116 +      NONE => NONE
   4.117 +    | SOME pointfree_expr =>
   4.118 +        SOME (Goal.prove ctxt [] []
   4.119 +          (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_compr, pointfree_expr))) (K tac)
   4.120 +        RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
   4.121 +  end
   4.122 +
   4.123 +end;