src/HOL/Tools/simpdata.ML
author wenzelm
Wed Jun 29 21:34:16 2011 +0200 (2011-06-29)
changeset 43597 b4a093e755db
parent 43596 78211f66cf8d
child 45620 f2a587696afb
permissions -rw-r--r--
tuned signature;
haftmann@37744
     1
(*  Title:      HOL/Tools/simpdata.ML
haftmann@21163
     2
    Author:     Tobias Nipkow
haftmann@21163
     3
    Copyright   1991  University of Cambridge
haftmann@21163
     4
haftmann@21163
     5
Instantiation of the generic simplifier for HOL.
haftmann@21163
     6
*)
haftmann@21163
     7
haftmann@21163
     8
(** tools setup **)
haftmann@21163
     9
wenzelm@42458
    10
structure Quantifier1 = Quantifier1
wenzelm@42458
    11
(
haftmann@21163
    12
  (*abstract syntax*)
wenzelm@42460
    13
  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
haftmann@21163
    14
    | dest_eq _ = NONE;
wenzelm@42460
    15
  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
haftmann@21163
    16
    | dest_conj _ = NONE;
wenzelm@42460
    17
  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
haftmann@21163
    18
    | dest_imp _ = NONE;
haftmann@21163
    19
  val conj = HOLogic.conj
haftmann@21163
    20
  val imp  = HOLogic.imp
haftmann@21163
    21
  (*rules*)
wenzelm@22147
    22
  val iff_reflection = @{thm eq_reflection}
wenzelm@22147
    23
  val iffI = @{thm iffI}
wenzelm@22147
    24
  val iff_trans = @{thm trans}
wenzelm@22147
    25
  val conjI= @{thm conjI}
wenzelm@22147
    26
  val conjE= @{thm conjE}
wenzelm@22147
    27
  val impI = @{thm impI}
wenzelm@22147
    28
  val mp   = @{thm mp}
wenzelm@22147
    29
  val uncurry = @{thm uncurry}
wenzelm@22147
    30
  val exI  = @{thm exI}
wenzelm@22147
    31
  val exE  = @{thm exE}
wenzelm@22147
    32
  val iff_allI = @{thm iff_allI}
wenzelm@22147
    33
  val iff_exI = @{thm iff_exI}
wenzelm@22147
    34
  val all_comm = @{thm all_comm}
wenzelm@22147
    35
  val ex_comm = @{thm ex_comm}
wenzelm@42458
    36
);
haftmann@21163
    37
haftmann@21551
    38
structure Simpdata =
haftmann@21163
    39
struct
haftmann@21163
    40
wenzelm@22147
    41
fun mk_meta_eq r = r RS @{thm eq_reflection};
haftmann@21163
    42
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
haftmann@21163
    43
wenzelm@22147
    44
fun mk_eq th = case concl_of th
haftmann@21163
    45
  (*expects Trueprop if not == *)
wenzelm@35364
    46
  of Const (@{const_name "=="},_) $ _ $ _ => th
haftmann@38864
    47
   | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
haftmann@38558
    48
   | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
wenzelm@22147
    49
   | _ => th RS @{thm Eq_TrueI}
haftmann@21163
    50
wenzelm@36543
    51
fun mk_eq_True (_: simpset) r =
wenzelm@22147
    52
  SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
haftmann@21163
    53
haftmann@21163
    54
(* Produce theorems of the form
haftmann@21163
    55
  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
haftmann@21163
    56
*)
haftmann@22838
    57
wenzelm@22147
    58
fun lift_meta_eq_to_obj_eq i st =
haftmann@21163
    59
  let
wenzelm@35364
    60
    fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
haftmann@21163
    61
      | count_imp _ = 0;
wenzelm@42364
    62
    val j = count_imp (Logic.strip_assums_concl (nth (prems_of st) (i - 1)))
wenzelm@42364
    63
  in
wenzelm@42364
    64
    if j = 0 then @{thm meta_eq_to_obj_eq}
haftmann@21163
    65
    else
haftmann@21163
    66
      let
haftmann@21163
    67
        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
wenzelm@33339
    68
        fun mk_simp_implies Q = fold_rev (fn R => fn S =>
wenzelm@35364
    69
          Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps Q
haftmann@21163
    70
        val aT = TFree ("'a", HOLogic.typeS);
haftmann@21163
    71
        val x = Free ("x", aT);
haftmann@21163
    72
        val y = Free ("y", aT)
wenzelm@42364
    73
      in
wenzelm@42364
    74
        Goal.prove_global (Thm.theory_of_thm st) []
wenzelm@42364
    75
          [mk_simp_implies (Logic.mk_equals (x, y))]
wenzelm@42364
    76
          (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
wenzelm@42364
    77
          (fn {prems, ...} => EVERY
wenzelm@42364
    78
           [rewrite_goals_tac @{thms simp_implies_def},
wenzelm@42364
    79
            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
wenzelm@42364
    80
              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
haftmann@21163
    81
      end
haftmann@21163
    82
  end;
haftmann@21163
    83
haftmann@21163
    84
(*Congruence rules for = (instead of ==)*)
wenzelm@36543
    85
fun mk_meta_cong (_: simpset) rl = zero_var_indexes
haftmann@21163
    86
  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
haftmann@21163
    87
     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
haftmann@21163
    88
   in mk_meta_eq rl' handle THM _ =>
haftmann@21163
    89
     if can Logic.dest_equals (concl_of rl') then rl'
haftmann@21163
    90
     else error "Conclusion of congruence rules must be =-equality"
haftmann@21163
    91
   end);
haftmann@21163
    92
haftmann@21163
    93
fun mk_atomize pairs =
haftmann@21163
    94
  let
wenzelm@21313
    95
    fun atoms thm =
wenzelm@21313
    96
      let
wenzelm@21313
    97
        fun res th = map (fn rl => th RS rl);   (*exception THM*)
wenzelm@21313
    98
        fun res_fixed rls =
wenzelm@21313
    99
          if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
wenzelm@36603
   100
          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
wenzelm@21313
   101
      in
wenzelm@21313
   102
        case concl_of thm
wenzelm@35364
   103
          of Const (@{const_name Trueprop}, _) $ p => (case head_of p
wenzelm@21313
   104
            of Const (a, _) => (case AList.lookup (op =) pairs a
wenzelm@21313
   105
              of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
wenzelm@21313
   106
              | NONE => [thm])
wenzelm@21313
   107
            | _ => [thm])
wenzelm@21313
   108
          | _ => [thm]
wenzelm@21313
   109
      end;
haftmann@21163
   110
  in atoms end;
haftmann@21163
   111
wenzelm@36543
   112
fun mksimps pairs (_: simpset) =
wenzelm@21313
   113
  map_filter (try mk_eq) o mk_atomize pairs o gen_all;
haftmann@21163
   114
wenzelm@43596
   115
fun unsafe_solver_tac ss =
wenzelm@22147
   116
  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
wenzelm@43597
   117
  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
wenzelm@43597
   118
    atac, etac @{thm FalseE}];
wenzelm@22147
   119
haftmann@21163
   120
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
haftmann@21163
   121
haftmann@22838
   122
haftmann@21163
   123
(*No premature instantiation of variables during simplification*)
wenzelm@43596
   124
fun safe_solver_tac ss =
wenzelm@22147
   125
  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
wenzelm@43597
   126
  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
wenzelm@43597
   127
    eq_assume_tac, ematch_tac @{thms FalseE}];
wenzelm@22147
   128
haftmann@21163
   129
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
haftmann@21163
   130
wenzelm@32177
   131
structure Splitter = Splitter
wenzelm@32177
   132
(
wenzelm@32177
   133
  val thy = @{theory}
wenzelm@32177
   134
  val mk_eq = mk_eq
wenzelm@32177
   135
  val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
wenzelm@32177
   136
  val iffD = @{thm iffD2}
wenzelm@32177
   137
  val disjE = @{thm disjE}
wenzelm@32177
   138
  val conjE = @{thm conjE}
wenzelm@32177
   139
  val exE = @{thm exE}
wenzelm@32177
   140
  val contrapos = @{thm contrapos_nn}
wenzelm@32177
   141
  val contrapos2 = @{thm contrapos_pp}
wenzelm@32177
   142
  val notnotD = @{thm notnotD}
wenzelm@32177
   143
);
haftmann@21163
   144
wenzelm@32177
   145
val split_tac = Splitter.split_tac;
wenzelm@21674
   146
val split_inside_tac = Splitter.split_inside_tac;
wenzelm@21674
   147
wenzelm@32177
   148
val op addsplits = Splitter.addsplits;
wenzelm@32177
   149
val op delsplits = Splitter.delsplits;
wenzelm@21674
   150
wenzelm@21674
   151
haftmann@21163
   152
(* integration of simplifier with classical reasoner *)
haftmann@21163
   153
wenzelm@42478
   154
structure Clasimp = Clasimp
wenzelm@42478
   155
(
wenzelm@42478
   156
  structure Simplifier = Simplifier
wenzelm@42478
   157
    and Splitter = Splitter
wenzelm@42478
   158
    and Classical  = Classical
wenzelm@42478
   159
    and Blast = Blast
wenzelm@42478
   160
  val iffD1 = @{thm iffD1}
wenzelm@42478
   161
  val iffD2 = @{thm iffD2}
wenzelm@42478
   162
  val notE = @{thm notE}
wenzelm@42478
   163
);
wenzelm@21674
   164
open Clasimp;
haftmann@21163
   165
haftmann@21163
   166
val mksimps_pairs =
haftmann@38786
   167
 [(@{const_name HOL.implies}, [@{thm mp}]),
haftmann@38795
   168
  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
wenzelm@35364
   169
  (@{const_name All}, [@{thm spec}]),
wenzelm@35364
   170
  (@{const_name True}, []),
wenzelm@35364
   171
  (@{const_name False}, []),
wenzelm@35364
   172
  (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
haftmann@21163
   173
wenzelm@21674
   174
val HOL_basic_ss =
wenzelm@35232
   175
  Simplifier.global_context @{theory} empty_ss
haftmann@21163
   176
    setsubgoaler asm_simp_tac
haftmann@21163
   177
    setSSolver safe_solver
haftmann@21163
   178
    setSolver unsafe_solver
haftmann@21163
   179
    setmksimps (mksimps mksimps_pairs)
haftmann@21163
   180
    setmkeqTrue mk_eq_True
haftmann@21163
   181
    setmkcong mk_meta_cong;
haftmann@21163
   182
wenzelm@21674
   183
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
haftmann@21163
   184
haftmann@21163
   185
fun unfold_tac ths =
wenzelm@21674
   186
  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
haftmann@21163
   187
  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
haftmann@21163
   188
wenzelm@21313
   189
end;
haftmann@21551
   190
haftmann@21551
   191
structure Splitter = Simpdata.Splitter;
haftmann@21551
   192
structure Clasimp = Simpdata.Clasimp;