1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 13 21:09:20 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:32 2012 +0200
     1.3 @@ -7,16 +7,15 @@
     1.4  
     1.5  signature SET_COMPREHENSION_POINTFREE =
     1.6  sig
     1.7 +  val base_simproc : simpset -> cterm -> thm option
     1.8    val code_simproc : simpset -> cterm -> thm option
     1.9    val simproc : simpset -> cterm -> thm option
    1.10 -  val rewrite_term : term -> term option
    1.11 -  (* FIXME: function conv is not a conversion, i.e. of type cterm -> thm, MAYBE rename *)
    1.12 -  val conv : Proof.context -> term -> thm option
    1.13  end
    1.14  
    1.15  structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE =
    1.16  struct
    1.17  
    1.18 +
    1.19  (* syntactic operations *)
    1.20  
    1.21  fun mk_inf (t1, t2) =
    1.22 @@ -59,9 +58,6 @@
    1.23        T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2
    1.24    end;
    1.25  
    1.26 -fun dest_Bound (Bound x) = x
    1.27 -  | dest_Bound t = raise TERM("dest_Bound", [t]);
    1.28 -
    1.29  fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t
    1.30    | dest_Collect t = raise TERM ("dest_Collect", [t])
    1.31  
    1.32 @@ -74,92 +70,213 @@
    1.33    end
    1.34    | strip_ex t = ([], t)
    1.35  
    1.36 -fun list_tupled_abs [] f = f
    1.37 -  | list_tupled_abs [(n, T)] f = (Abs (n, T, f))
    1.38 -  | list_tupled_abs ((n, T)::v::vs) f =
    1.39 -      HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f))
    1.40 +fun mk_prod1 Ts (t1, t2) =
    1.41 +  let
    1.42 +    val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
    1.43 +  in
    1.44 +    HOLogic.pair_const T1 T2 $ t1 $ t2
    1.45 +  end;
    1.46 +
    1.47 +
    1.48 +(* patterns *)
    1.49 +
    1.50 +datatype pattern = TBound of int | TPair of pattern * pattern;
    1.51 +
    1.52 +fun mk_pattern (Bound n) = TBound n
    1.53 +  | mk_pattern (Const (@{const_name "Product_Type.Pair"}, _) $ l $ r) =
    1.54 +      TPair (mk_pattern l, mk_pattern r)
    1.55 +  | mk_pattern t = raise TERM ("mk_pattern: only bound variable tuples currently supported", [t]);
    1.56 +
    1.57 +fun type_of_pattern Ts (TBound n) = nth Ts n
    1.58 +  | type_of_pattern Ts (TPair (l, r)) = HOLogic.mk_prodT (type_of_pattern Ts l, type_of_pattern Ts r)
    1.59 +
    1.60 +fun term_of_pattern _ (TBound n) = Bound n
    1.61 +  | term_of_pattern Ts (TPair (l, r)) =
    1.62 +    let
    1.63 +      val (lt, rt) = pairself (term_of_pattern Ts) (l, r)
    1.64 +      val (lT, rT) = pairself (curry fastype_of1 Ts) (lt, rt) 
    1.65 +    in
    1.66 +      HOLogic.pair_const lT rT $ lt $ rt
    1.67 +    end;
    1.68 +
    1.69 +fun bounds_of_pattern (TBound i) = [i]
    1.70 +  | bounds_of_pattern (TPair (l, r)) = union (op =) (bounds_of_pattern l) (bounds_of_pattern r)
    1.71 +
    1.72 +
    1.73 +(* formulas *)
    1.74 +
    1.75 +datatype formula = Atom of (pattern * term) | Int of formula * formula | Un of formula * formula
    1.76 +
    1.77 +fun mk_atom (Const (@{const_name "Set.member"}, _) $ x $ s) = (mk_pattern x, Atom (mk_pattern x, s))
    1.78 +  | mk_atom (Const (@{const_name "HOL.Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ x $ s)) =
    1.79 +      (mk_pattern x, Atom (mk_pattern x, mk_Compl s))
    1.80 +
    1.81 +fun can_merge (pats1, pats2) =
    1.82 +  let
    1.83 +    fun check pat1 pat2 = (pat1 = pat2)
    1.84 +      orelse (inter (op =) (bounds_of_pattern pat1) (bounds_of_pattern pat2) = [])
    1.85 +  in
    1.86 +    forall (fn pat1 => forall (fn pat2 => check pat1 pat2) pats2) pats1 
    1.87 +  end
    1.88 +
    1.89 +fun merge_patterns (pats1, pats2) =
    1.90 +  if can_merge (pats1, pats2) then
    1.91 +    union (op =) pats1 pats2
    1.92 +  else raise Fail "merge_patterns: variable groups overlap"
    1.93 +
    1.94 +fun merge oper (pats1, sp1) (pats2, sp2) = (merge_patterns (pats1, pats2), oper (sp1, sp2))
    1.95 +
    1.96 +fun mk_formula (@{const HOL.conj} $ t1 $ t2) = merge Int (mk_formula t1) (mk_formula t2)
    1.97 +  | mk_formula (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula t1) (mk_formula t2)
    1.98 +  | mk_formula t = apfst single (mk_atom t)
    1.99 +
   1.100 +
   1.101 +(* term construction *)
   1.102 +
   1.103 +fun reorder_bounds pats t =
   1.104 +  let
   1.105 +    val bounds = maps bounds_of_pattern pats
   1.106 +    val bperm = bounds ~~ ((length bounds - 1) downto 0)
   1.107 +      |> sort (fn (i,j) => int_ord (fst i, fst j)) |> map snd
   1.108 +  in
   1.109 +    subst_bounds (map Bound bperm, t)
   1.110 +  end;
   1.111 +
   1.112 +fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
   1.113 +  | mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t =
   1.114 +      HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
   1.115 +  | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
   1.116  
   1.117  fun mk_pointfree_expr t =
   1.118    let
   1.119      val (vs, t'') = strip_ex (dest_Collect t)
   1.120 +    val Ts = map snd (rev vs)
   1.121 +    fun mk_mem_UNIV n = HOLogic.mk_mem (Bound n, HOLogic.mk_UNIV (nth Ts n))
   1.122 +    fun lookup (pat', t) pat = if pat = pat' then t else HOLogic.mk_UNIV (type_of_pattern Ts pat)
   1.123      val conjs = HOLogic.dest_conj t''
   1.124      val is_the_eq =
   1.125        the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs)))
   1.126      val SOME eq = find_first is_the_eq conjs
   1.127      val f = snd (HOLogic.dest_eq eq)
   1.128      val conjs' = filter_out (fn t => eq = t) conjs
   1.129 -    val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs'
   1.130 -    val grouped_mems = AList.group (op =) mems
   1.131 -    fun mk_grouped_unions (i, T) =
   1.132 -      case AList.lookup (op =) grouped_mems i of
   1.133 -        SOME ts => foldr1 mk_inf ts
   1.134 -      | NONE => HOLogic.mk_UNIV T
   1.135 -    val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs)
   1.136 +    val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
   1.137 +      (0 upto (length vs - 1))
   1.138 +    val (pats, fm) =
   1.139 +      mk_formula (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
   1.140 +    fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
   1.141 +      | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
   1.142 +      | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
   1.143 +    val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
   1.144 +    val t = mk_split_abs (rev vs) pat (reorder_bounds pats f)
   1.145    in
   1.146 -    mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets)
   1.147 +    (fm, mk_image t (mk_set fm))
   1.148    end;
   1.149  
   1.150  val rewrite_term = try mk_pointfree_expr
   1.151  
   1.152 +
   1.153  (* proof tactic *)
   1.154  
   1.155 -(* Tactic works for arbitrary number of m : S conjuncts *)
   1.156 +val prod_case_distrib = @{lemma "(prod_case g x) z = prod_case (% x y. (g x y) z) x" by (simp add: prod_case_beta)}
   1.157  
   1.158 -val dest_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
   1.159 -  THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE conjE}))
   1.160 +(* FIXME: one of many clones *)
   1.161 +fun Trueprop_conv cv ct =
   1.162 +  (case Thm.term_of ct of
   1.163 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
   1.164 +  | _ => raise CTERM ("Trueprop_conv", [ct]))
   1.165 +
   1.166 +(* FIXME: another clone *)
   1.167 +fun eq_conv cv1 cv2 ct =
   1.168 +  (case Thm.term_of ct of
   1.169 +    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
   1.170 +  | _ => raise CTERM ("eq_conv", [ct]))
   1.171 +
   1.172 +val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
   1.173 +  THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
   1.174 +  THEN' TRY o etac @{thm conjE}
   1.175    THEN' hyp_subst_tac;
   1.176  
   1.177 -val intro_image_Sigma_tac = rtac @{thm image_eqI}
   1.178 +fun intro_image_tac ctxt = rtac @{thm image_eqI}
   1.179      THEN' (REPEAT_DETERM1 o
   1.180        (rtac @{thm refl}
   1.181        ORELSE' rtac
   1.182 -        @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}));
   1.183 +        @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
   1.184 +      ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   1.185 +        (Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
   1.186  
   1.187 -val dest_image_Sigma_tac = etac @{thm imageE}
   1.188 +val elim_image_tac = etac @{thm imageE}
   1.189    THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
   1.190    THEN' hyp_subst_tac
   1.191 -  THEN' (TRY o REPEAT_DETERM1 o
   1.192 -    (etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}));
   1.193  
   1.194  val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
   1.195    THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
   1.196 -  THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
   1.197 -  THEN' (K (ALLGOALS (TRY o ((TRY o hyp_subst_tac) THEN' rtac @{thm refl}))))
   1.198 +  THEN' (TRY o (rtac @{thm conjI}))
   1.199 +  THEN' (TRY o hyp_subst_tac)
   1.200 +  THEN' rtac @{thm refl};
   1.201  
   1.202 -val tac =
   1.203 +fun tac1_of_formula (Int (fm1, fm2)) =
   1.204 +    TRY o etac @{thm conjE}
   1.205 +    THEN' rtac @{thm IntI}
   1.206 +    THEN' (fn i => tac1_of_formula fm2 (i + 1))
   1.207 +    THEN' tac1_of_formula fm1
   1.208 +  | tac1_of_formula (Un (fm1, fm2)) =
   1.209 +    etac @{thm disjE} THEN' rtac @{thm UnI1}
   1.210 +    THEN' tac1_of_formula fm1
   1.211 +    THEN' rtac @{thm UnI2}
   1.212 +    THEN' tac1_of_formula fm2
   1.213 +  | tac1_of_formula (Atom _) =
   1.214 +    (REPEAT_DETERM1 o (rtac @{thm SigmaI}
   1.215 +      ORELSE' rtac @{thm UNIV_I}
   1.216 +      ORELSE' rtac @{thm iffD2[OF Compl_iff]}
   1.217 +      ORELSE' atac))
   1.218 +
   1.219 +fun tac2_of_formula (Int (fm1, fm2)) =
   1.220 +    TRY o etac @{thm IntE}
   1.221 +    THEN' TRY o rtac @{thm conjI}
   1.222 +    THEN' (fn i => tac2_of_formula fm2 (i + 1))
   1.223 +    THEN' tac2_of_formula fm1
   1.224 +  | tac2_of_formula (Un (fm1, fm2)) =
   1.225 +    etac @{thm UnE} THEN' rtac @{thm disjI1}
   1.226 +    THEN' tac2_of_formula fm1
   1.227 +    THEN' rtac @{thm disjI2}
   1.228 +    THEN' tac2_of_formula fm2
   1.229 +  | tac2_of_formula (Atom _) =
   1.230 +    TRY o REPEAT_DETERM1 o
   1.231 +      (dtac @{thm iffD1[OF mem_Sigma_iff]}
   1.232 +       ORELSE' etac @{thm conjE}
   1.233 +       ORELSE' etac @{thm ComplE}
   1.234 +       ORELSE' atac)
   1.235 +
   1.236 +fun tac ctxt fm =
   1.237    let
   1.238      val subset_tac1 = rtac @{thm subsetI}
   1.239 -      THEN' dest_Collect_tac
   1.240 -      THEN' intro_image_Sigma_tac
   1.241 -      THEN' (REPEAT_DETERM1 o
   1.242 -        (rtac @{thm SigmaI}
   1.243 -        ORELSE' rtac @{thm UNIV_I}
   1.244 -        ORELSE' rtac @{thm IntI}
   1.245 -        ORELSE' atac));
   1.246 -
   1.247 +      THEN' elim_Collect_tac
   1.248 +      THEN' (intro_image_tac ctxt)
   1.249 +      THEN' (tac1_of_formula fm)
   1.250      val subset_tac2 = rtac @{thm subsetI}
   1.251 -      THEN' dest_image_Sigma_tac
   1.252 +      THEN' elim_image_tac
   1.253        THEN' intro_Collect_tac
   1.254 -      THEN' REPEAT_DETERM o (eresolve_tac @{thms IntD1 IntD2} ORELSE' atac);
   1.255 +      THEN' tac2_of_formula fm
   1.256    in
   1.257      rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
   1.258    end;
   1.259  
   1.260 +
   1.261 +(* main simprocs *)
   1.262 +
   1.263  fun conv ctxt t =
   1.264    let
   1.265      val ct = cterm_of (Proof_Context.theory_of ctxt) t
   1.266      val Bex_def = mk_meta_eq @{thm Bex_def}
   1.267      val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
   1.268 -    val t' = term_of (Thm.rhs_of unfold_eq) 
   1.269 -    fun mk_thm t'' = Goal.prove ctxt [] []
   1.270 -      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (K (tac 1))
   1.271 +    val t' = term_of (Thm.rhs_of unfold_eq)
   1.272 +    fun mk_thm (fm, t'') = Goal.prove ctxt [] []
   1.273 +      (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
   1.274      fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
   1.275    in
   1.276      Option.map (unfold o mk_thm) (rewrite_term t')
   1.277    end;
   1.278  
   1.279 -(* simproc *)
   1.280 -
   1.281  fun base_simproc ss redex =
   1.282    let
   1.283      val ctxt = Simplifier.the_context ss