src/HOL/Tools/list_to_set_comprehension.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 46423 51259911b9fa
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
wenzelm@41467
     1
(*  Title:      HOL/Tools/list_to_set_comprehension.ML
wenzelm@41467
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@41463
     3
wenzelm@41467
     4
Simproc for rewriting list comprehensions applied to List.set to set
wenzelm@41467
     5
comprehension.
bulwahn@41463
     6
*)
bulwahn@41463
     7
bulwahn@41463
     8
signature LIST_TO_SET_COMPREHENSION =
bulwahn@41463
     9
sig
bulwahn@41463
    10
  val simproc : simpset -> cterm -> thm option
wenzelm@42168
    11
end
bulwahn@41463
    12
bulwahn@41463
    13
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
bulwahn@41463
    14
struct
bulwahn@41463
    15
bulwahn@41463
    16
(* conversion *)
bulwahn@41463
    17
bulwahn@41463
    18
fun all_exists_conv cv ctxt ct =
wenzelm@42168
    19
  (case Thm.term_of ct of
wenzelm@42168
    20
    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
bulwahn@41463
    21
      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
wenzelm@42168
    22
  | _ => cv ctxt ct)
bulwahn@41463
    23
bulwahn@41463
    24
fun all_but_last_exists_conv cv ctxt ct =
wenzelm@42168
    25
  (case Thm.term_of ct of
bulwahn@41463
    26
    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
bulwahn@41463
    27
      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
wenzelm@42168
    28
  | _ => cv ctxt ct)
bulwahn@41463
    29
bulwahn@41463
    30
fun Collect_conv cv ctxt ct =
bulwahn@41463
    31
  (case Thm.term_of ct of
bulwahn@41463
    32
    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
wenzelm@42168
    33
  | _ => raise CTERM ("Collect_conv", [ct]))
bulwahn@41463
    34
bulwahn@41463
    35
fun Trueprop_conv cv ct =
bulwahn@41463
    36
  (case Thm.term_of ct of
bulwahn@41463
    37
    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
wenzelm@42168
    38
  | _ => raise CTERM ("Trueprop_conv", [ct]))
bulwahn@41463
    39
bulwahn@41463
    40
fun eq_conv cv1 cv2 ct =
bulwahn@41463
    41
  (case Thm.term_of ct of
bulwahn@41463
    42
    Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
wenzelm@42168
    43
  | _ => raise CTERM ("eq_conv", [ct]))
bulwahn@41463
    44
bulwahn@41463
    45
fun conj_conv cv1 cv2 ct =
bulwahn@41463
    46
  (case Thm.term_of ct of
bulwahn@41463
    47
    Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
wenzelm@42168
    48
  | _ => raise CTERM ("conj_conv", [ct]))
bulwahn@41463
    49
bulwahn@41618
    50
fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
wenzelm@42168
    51
wenzelm@42168
    52
fun conjunct_assoc_conv ct =
wenzelm@42168
    53
  Conv.try_conv
wenzelm@42169
    54
    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
wenzelm@42168
    55
wenzelm@42168
    56
fun right_hand_set_comprehension_conv conv ctxt =
wenzelm@42168
    57
  Trueprop_conv (eq_conv Conv.all_conv
wenzelm@42168
    58
    (Collect_conv (all_exists_conv conv o #2) ctxt))
wenzelm@42168
    59
bulwahn@41463
    60
bulwahn@41463
    61
(* term abstraction of list comprehension patterns *)
wenzelm@42168
    62
bulwahn@41463
    63
datatype termlets = If | Case of (typ * int)
bulwahn@41463
    64
bulwahn@41463
    65
fun simproc ss redex =
bulwahn@41463
    66
  let
bulwahn@41463
    67
    val ctxt = Simplifier.the_context ss
wenzelm@42361
    68
    val thy = Proof_Context.theory_of ctxt
bulwahn@41463
    69
    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]
bulwahn@41463
    70
    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
bulwahn@41463
    71
    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
wenzelm@42168
    72
    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
bulwahn@41463
    73
    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
bulwahn@41463
    74
    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
bulwahn@41463
    75
    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
wenzelm@42168
    76
          $ t $ (Const (@{const_name List.Nil}, _))) = t
bulwahn@41463
    77
      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
bulwahn@41463
    78
    (* We check that one case returns a singleton list and all other cases
wenzelm@42168
    79
       return [], and return the index of the one singleton list case *)
bulwahn@41463
    80
    fun possible_index_of_singleton_case cases =
wenzelm@42168
    81
      let
bulwahn@41463
    82
        fun check (i, case_t) s =
bulwahn@41463
    83
          (case strip_abs_body case_t of
bulwahn@41463
    84
            (Const (@{const_name List.Nil}, _)) => s
bulwahn@46423
    85
          | _ => (case s of NONE => SOME i | SOME _ => NONE))
bulwahn@41463
    86
      in
bulwahn@41463
    87
        fold_index check cases NONE
bulwahn@41463
    88
      end
bulwahn@41463
    89
    (* returns (case_expr type index chosen_case) option  *)
bulwahn@41463
    90
    fun dest_case case_term =
bulwahn@41463
    91
      let
bulwahn@41463
    92
        val (case_const, args) = strip_comb case_term
bulwahn@41463
    93
      in
wenzelm@42168
    94
        (case try dest_Const case_const of
wenzelm@42168
    95
          SOME (c, T) =>
wenzelm@45906
    96
            (case Datatype.info_of_case thy c of
wenzelm@42168
    97
              SOME _ =>
wenzelm@42168
    98
                (case possible_index_of_singleton_case (fst (split_last args)) of
wenzelm@42168
    99
                  SOME i =>
wenzelm@42168
   100
                    let
wenzelm@42168
   101
                      val (Ts, _) = strip_type T
wenzelm@42168
   102
                      val T' = List.last Ts
wenzelm@42168
   103
                    in SOME (List.last args, T', i, nth args i) end
wenzelm@42168
   104
                | NONE => NONE)
bulwahn@41463
   105
            | NONE => NONE)
wenzelm@42168
   106
        | NONE => NONE)
bulwahn@41463
   107
      end
bulwahn@41463
   108
    (* returns condition continuing term option *)
bulwahn@41463
   109
    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
wenzelm@42169
   110
          SOME (cond, then_t)
bulwahn@41463
   111
      | dest_if _ = NONE
wenzelm@42168
   112
    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
wenzelm@42168
   113
      | tac ctxt (If :: cont) =
wenzelm@42168
   114
          Splitter.split_tac [@{thm split_if}] 1
wenzelm@42168
   115
          THEN rtac @{thm conjI} 1
wenzelm@42168
   116
          THEN rtac @{thm impI} 1
wenzelm@42168
   117
          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
wenzelm@42168
   118
            CONVERSION (right_hand_set_comprehension_conv (K
wenzelm@42168
   119
              (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
wenzelm@42169
   120
               then_conv
wenzelm@42169
   121
               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
wenzelm@42168
   122
          THEN tac ctxt cont
bulwahn@41463
   123
          THEN rtac @{thm impI} 1
wenzelm@42168
   124
          THEN Subgoal.FOCUS (fn {prems, context, ...} =>
wenzelm@42168
   125
              CONVERSION (right_hand_set_comprehension_conv (K
wenzelm@42168
   126
                (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
wenzelm@42169
   127
                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
wenzelm@42168
   128
          THEN rtac set_Nil_I 1
wenzelm@42168
   129
      | tac ctxt (Case (T, i) :: cont) =
wenzelm@42168
   130
          let
wenzelm@42168
   131
            val info = Datatype.the_info thy (fst (dest_Type T))
wenzelm@42168
   132
          in
wenzelm@42168
   133
            (* do case distinction *)
wenzelm@42168
   134
            Splitter.split_tac [#split info] 1
bulwahn@46423
   135
            THEN EVERY (map_index (fn (i', _) =>
wenzelm@42168
   136
              (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)
wenzelm@42168
   137
              THEN REPEAT_DETERM (rtac @{thm allI} 1)
wenzelm@42168
   138
              THEN rtac @{thm impI} 1
wenzelm@42168
   139
              THEN (if i' = i then
wenzelm@42168
   140
                (* continue recursively *)
wenzelm@42168
   141
                Subgoal.FOCUS (fn {prems, context, ...} =>
wenzelm@42168
   142
                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
wenzelm@42168
   143
                      ((conj_conv
wenzelm@42168
   144
                        (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
wenzelm@42168
   145
                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
wenzelm@42168
   146
                        Conv.all_conv)
wenzelm@42168
   147
                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
wenzelm@42168
   148
                        then_conv conjunct_assoc_conv)) context
wenzelm@42168
   149
                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
wenzelm@42168
   150
                      Conv.repeat_conv
wenzelm@42168
   151
                        (all_but_last_exists_conv
wenzelm@42169
   152
                          (K (rewr_conv'
wenzelm@42169
   153
                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
wenzelm@42168
   154
                THEN tac ctxt cont
wenzelm@42168
   155
              else
wenzelm@42168
   156
                Subgoal.FOCUS (fn {prems, context, ...} =>
wenzelm@42169
   157
                  CONVERSION
wenzelm@42169
   158
                    (right_hand_set_comprehension_conv (K
wenzelm@42169
   159
                      (conj_conv
wenzelm@42169
   160
                        ((eq_conv Conv.all_conv
wenzelm@42169
   161
                          (rewr_conv' (List.last prems))) then_conv
wenzelm@42169
   162
                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
wenzelm@42169
   163
                        Conv.all_conv then_conv
wenzelm@42169
   164
                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
wenzelm@42169
   165
                      Trueprop_conv
wenzelm@42169
   166
                        (eq_conv Conv.all_conv
wenzelm@42169
   167
                          (Collect_conv (fn (_, ctxt) =>
wenzelm@42169
   168
                            Conv.repeat_conv
wenzelm@42169
   169
                              (Conv.bottom_conv
wenzelm@42169
   170
                                (K (rewr_conv'
wenzelm@42169
   171
                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
wenzelm@42168
   172
                THEN rtac set_Nil_I 1)) (#case_rewrites info))
wenzelm@42168
   173
          end
bulwahn@41463
   174
    fun make_inner_eqs bound_vs Tis eqs t =
wenzelm@42168
   175
      (case dest_case t of
bulwahn@41463
   176
        SOME (x, T, i, cont) =>
bulwahn@41463
   177
          let
bulwahn@41463
   178
            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
bulwahn@41463
   179
            val x' = incr_boundvars (length vs) x
bulwahn@41463
   180
            val eqs' = map (incr_boundvars (length vs)) eqs
wenzelm@45906
   181
            val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
wenzelm@42168
   182
            val constr_t =
wenzelm@42168
   183
              list_comb
wenzelm@42168
   184
                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))
bulwahn@41463
   185
            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'
bulwahn@41463
   186
          in
bulwahn@41463
   187
            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body
bulwahn@41463
   188
          end
bulwahn@41463
   189
      | NONE =>
wenzelm@42168
   190
          (case dest_if t of
wenzelm@42168
   191
            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
wenzelm@42168
   192
          | NONE =>
wenzelm@42168
   193
            if eqs = [] then NONE (* no rewriting, nothing to be done *)
wenzelm@42168
   194
            else
wenzelm@42168
   195
              let
wenzelm@42168
   196
                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
wenzelm@42168
   197
                val pat_eq =
wenzelm@42168
   198
                  (case try dest_singleton_list t of
wenzelm@42168
   199
                    SOME t' =>
wenzelm@42168
   200
                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
wenzelm@42168
   201
                        Bound (length bound_vs) $ t'
wenzelm@42168
   202
                  | NONE =>
wenzelm@42168
   203
                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $
wenzelm@42168
   204
                        Bound (length bound_vs) $ (mk_set rT $ t))
wenzelm@42168
   205
                val reverse_bounds = curry subst_bounds
wenzelm@42168
   206
                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])
wenzelm@42168
   207
                val eqs' = map reverse_bounds eqs
wenzelm@42168
   208
                val pat_eq' = reverse_bounds pat_eq
wenzelm@42168
   209
                val inner_t =
bulwahn@46423
   210
                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)
wenzelm@42168
   211
                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')
wenzelm@42168
   212
                val lhs = term_of redex
wenzelm@42168
   213
                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
wenzelm@42168
   214
                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
wenzelm@42168
   215
              in
wenzelm@42168
   216
                SOME
wenzelm@42168
   217
                  ((Goal.prove ctxt [] [] rewrite_rule_t
wenzelm@42168
   218
                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})
wenzelm@42168
   219
              end))
bulwahn@41463
   220
  in
bulwahn@41463
   221
    make_inner_eqs [] [] [] (dest_set (term_of redex))
bulwahn@41463
   222
  end
bulwahn@41463
   223
bulwahn@41463
   224
end