src/HOL/Tools/list_to_set_comprehension.ML
changeset 50422 ee729dbd1b7f
parent 50416 2e1b47e22fc6
child 50423 027d405951c8
     1.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Dec 07 14:30:00 2012 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,224 +0,0 @@
     1.4 -(*  Title:      HOL/Tools/list_to_set_comprehension.ML
     1.5 -    Author:     Lukas Bulwahn, TU Muenchen
     1.6 -
     1.7 -Simproc for rewriting list comprehensions applied to List.set to set
     1.8 -comprehension.
     1.9 -*)
    1.10 -
    1.11 -signature LIST_TO_SET_COMPREHENSION =
    1.12 -sig
    1.13 -  val simproc : simpset -> cterm -> thm option
    1.14 -end
    1.15 -
    1.16 -structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
    1.17 -struct
    1.18 -
    1.19 -(* conversion *)
    1.20 -
    1.21 -fun all_exists_conv cv ctxt ct =
    1.22 -  (case Thm.term_of ct of
    1.23 -    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
    1.24 -      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
    1.25 -  | _ => cv ctxt ct)
    1.26 -
    1.27 -fun all_but_last_exists_conv cv ctxt ct =
    1.28 -  (case Thm.term_of ct of
    1.29 -    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
    1.30 -      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
    1.31 -  | _ => cv ctxt ct)
    1.32 -
    1.33 -fun Collect_conv cv ctxt ct =
    1.34 -  (case Thm.term_of ct of
    1.35 -    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
    1.36 -  | _ => raise CTERM ("Collect_conv", [ct]))
    1.37 -
    1.38 -fun Trueprop_conv cv ct =
    1.39 -  (case Thm.term_of ct of
    1.40 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    1.41 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    1.42 -
    1.43 -fun eq_conv cv1 cv2 ct =
    1.44 -  (case Thm.term_of ct of
    1.45 -    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    1.46 -  | _ => raise CTERM ("eq_conv", [ct]))
    1.47 -
    1.48 -fun conj_conv cv1 cv2 ct =
    1.49 -  (case Thm.term_of ct of
    1.50 -    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    1.51 -  | _ => raise CTERM ("conj_conv", [ct]))
    1.52 -
    1.53 -fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
    1.54 -
    1.55 -fun conjunct_assoc_conv ct =
    1.56 -  Conv.try_conv
    1.57 -    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    1.58 -
    1.59 -fun right_hand_set_comprehension_conv conv ctxt =
    1.60 -  Trueprop_conv (eq_conv Conv.all_conv
    1.61 -    (Collect_conv (all_exists_conv conv o #2) ctxt))
    1.62 -
    1.63 -
    1.64 -(* term abstraction of list comprehension patterns *)
    1.65 -
    1.66 -datatype termlets = If | Case of (typ * int)
    1.67 -
    1.68 -fun simproc ss redex =
    1.69 -  let
    1.70 -    val ctxt = Simplifier.the_context ss
    1.71 -    val thy = Proof_Context.theory_of ctxt
    1.72 -    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
    1.73 -    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
    1.74 -    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
    1.75 -    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
    1.76 -    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
    1.77 -    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
    1.78 -    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
    1.79 -          $ t $ (Const (@{const_name List.Nil}, _))) = t
    1.80 -      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
    1.81 -    (* We check that one case returns a singleton list and all other cases
    1.82 -       return [], and return the index of the one singleton list case *)
    1.83 -    fun possible_index_of_singleton_case cases =
    1.84 -      let
    1.85 -        fun check (i, case_t) s =
    1.86 -          (case strip_abs_body case_t of
    1.87 -            (Const (@{const_name List.Nil}, _)) => s
    1.88 -          | _ => (case s of NONE => SOME i | SOME _ => NONE))
    1.89 -      in
    1.90 -        fold_index check cases NONE
    1.91 -      end
    1.92 -    (* returns (case_expr type index chosen_case) option  *)
    1.93 -    fun dest_case case_term =
    1.94 -      let
    1.95 -        val (case_const, args) = strip_comb case_term
    1.96 -      in
    1.97 -        (case try dest_Const case_const of
    1.98 -          SOME (c, T) =>
    1.99 -            (case Datatype.info_of_case thy c of
   1.100 -              SOME _ =>
   1.101 -                (case possible_index_of_singleton_case (fst (split_last args)) of
   1.102 -                  SOME i =>
   1.103 -                    let
   1.104 -                      val (Ts, _) = strip_type T
   1.105 -                      val T' = List.last Ts
   1.106 -                    in SOME (List.last args, T', i, nth args i) end
   1.107 -                | NONE => NONE)
   1.108 -            | NONE => NONE)
   1.109 -        | NONE => NONE)
   1.110 -      end
   1.111 -    (* returns condition continuing term option *)
   1.112 -    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
   1.113 -          SOME (cond, then_t)
   1.114 -      | dest_if _ = NONE
   1.115 -    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
   1.116 -      | tac ctxt (If :: cont) =
   1.117 -          Splitter.split_tac [@{thm split_if}] 1
   1.118 -          THEN rtac @{thm conjI} 1
   1.119 -          THEN rtac @{thm impI} 1
   1.120 -          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   1.121 -            CONVERSION (right_hand_set_comprehension_conv (K
   1.122 -              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
   1.123 -               then_conv
   1.124 -               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
   1.125 -          THEN tac ctxt cont
   1.126 -          THEN rtac @{thm impI} 1
   1.127 -          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
   1.128 -              CONVERSION (right_hand_set_comprehension_conv (K
   1.129 -                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
   1.130 -                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
   1.131 -          THEN rtac set_Nil_I 1
   1.132 -      | tac ctxt (Case (T, i) :: cont) =
   1.133 -          let
   1.134 -            val info = Datatype.the_info thy (fst (dest_Type T))
   1.135 -          in
   1.136 -            (* do case distinction *)
   1.137 -            Splitter.split_tac [#split info] 1
   1.138 -            THEN EVERY (map_index (fn (i', _) =>
   1.139 -              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
   1.140 -              THEN REPEAT_DETERM (rtac @{thm allI} 1)
   1.141 -              THEN rtac @{thm impI} 1
   1.142 -              THEN (if i' = i then
   1.143 -                (* continue recursively *)
   1.144 -                Subgoal.FOCUS (fn {prems, context, ...} =>
   1.145 -                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
   1.146 -                      ((conj_conv
   1.147 -                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
   1.148 -                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
   1.149 -                        Conv.all_conv)
   1.150 -                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
   1.151 -                        then_conv conjunct_assoc_conv)) context
   1.152 -                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
   1.153 -                      Conv.repeat_conv
   1.154 -                        (all_but_last_exists_conv
   1.155 -                          (K (rewr_conv'
   1.156 -                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
   1.157 -                THEN tac ctxt cont
   1.158 -              else
   1.159 -                Subgoal.FOCUS (fn {prems, context, ...} =>
   1.160 -                  CONVERSION
   1.161 -                    (right_hand_set_comprehension_conv (K
   1.162 -                      (conj_conv
   1.163 -                        ((eq_conv Conv.all_conv
   1.164 -                          (rewr_conv' (List.last prems))) then_conv
   1.165 -                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
   1.166 -                        Conv.all_conv then_conv
   1.167 -                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
   1.168 -                      Trueprop_conv
   1.169 -                        (eq_conv Conv.all_conv
   1.170 -                          (Collect_conv (fn (_, ctxt) =>
   1.171 -                            Conv.repeat_conv
   1.172 -                              (Conv.bottom_conv
   1.173 -                                (K (rewr_conv'
   1.174 -                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
   1.175 -                THEN rtac set_Nil_I 1)) (#case_rewrites info))
   1.176 -          end
   1.177 -    fun make_inner_eqs bound_vs Tis eqs t =
   1.178 -      (case dest_case t of
   1.179 -        SOME (x, T, i, cont) =>
   1.180 -          let
   1.181 -            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
   1.182 -            val x' = incr_boundvars (length vs) x
   1.183 -            val eqs' = map (incr_boundvars (length vs)) eqs
   1.184 -            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
   1.185 -            val constr_t =
   1.186 -              list_comb
   1.187 -                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
   1.188 -            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
   1.189 -          in
   1.190 -            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
   1.191 -          end
   1.192 -      | NONE =>
   1.193 -          (case dest_if t of
   1.194 -            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
   1.195 -          | NONE =>
   1.196 -            if eqs = [] then NONE (* no rewriting, nothing to be done *)
   1.197 -            else
   1.198 -              let
   1.199 -                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
   1.200 -                val pat_eq =
   1.201 -                  (case try dest_singleton_list t of
   1.202 -                    SOME t' =>
   1.203 -                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
   1.204 -                        Bound (length bound_vs) $ t'
   1.205 -                  | NONE =>
   1.206 -                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
   1.207 -                        Bound (length bound_vs) $ (mk_set rT $ t))
   1.208 -                val reverse_bounds = curry subst_bounds
   1.209 -                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
   1.210 -                val eqs' = map reverse_bounds eqs
   1.211 -                val pat_eq' = reverse_bounds pat_eq
   1.212 -                val inner_t =
   1.213 -                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
   1.214 -                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
   1.215 -                val lhs = term_of redex
   1.216 -                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
   1.217 -                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   1.218 -              in
   1.219 -                SOME
   1.220 -                  ((Goal.prove ctxt [] [] rewrite_rule_t
   1.221 -                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
   1.222 -              end))
   1.223 -  in
   1.224 -    make_inner_eqs [] [] [] (dest_set (term_of redex))
   1.225 -  end
   1.226 -
   1.227 -end