src/HOL/Tools/simpdata.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45625 750c5a47400b
child 51717 9e7d1c139569
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
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@45622
    62
    val j = count_imp (Logic.strip_assums_concl (Thm.term_of (Thm.cprem_of st i)))
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@45622
    68
        val mk_simp_implies = fold_rev (fn R => fn S =>
wenzelm@45622
    69
          Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps;
wenzelm@42364
    70
      in
wenzelm@42364
    71
        Goal.prove_global (Thm.theory_of_thm st) []
wenzelm@45622
    72
          [mk_simp_implies @{prop "(x::'a) == y"}]
wenzelm@45622
    73
          (mk_simp_implies @{prop "(x::'a) = y"})
wenzelm@42364
    74
          (fn {prems, ...} => EVERY
wenzelm@42364
    75
           [rewrite_goals_tac @{thms simp_implies_def},
wenzelm@42364
    76
            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
wenzelm@42364
    77
              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
haftmann@21163
    78
      end
haftmann@21163
    79
  end;
haftmann@21163
    80
haftmann@21163
    81
(*Congruence rules for = (instead of ==)*)
wenzelm@36543
    82
fun mk_meta_cong (_: simpset) rl = zero_var_indexes
haftmann@21163
    83
  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
haftmann@21163
    84
     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
haftmann@21163
    85
   in mk_meta_eq rl' handle THM _ =>
haftmann@21163
    86
     if can Logic.dest_equals (concl_of rl') then rl'
haftmann@21163
    87
     else error "Conclusion of congruence rules must be =-equality"
haftmann@21163
    88
   end);
haftmann@21163
    89
haftmann@21163
    90
fun mk_atomize pairs =
haftmann@21163
    91
  let
wenzelm@21313
    92
    fun atoms thm =
wenzelm@21313
    93
      let
wenzelm@21313
    94
        fun res th = map (fn rl => th RS rl);   (*exception THM*)
wenzelm@21313
    95
        fun res_fixed rls =
wenzelm@21313
    96
          if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
wenzelm@36603
    97
          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
wenzelm@21313
    98
      in
wenzelm@21313
    99
        case concl_of thm
wenzelm@35364
   100
          of Const (@{const_name Trueprop}, _) $ p => (case head_of p
wenzelm@21313
   101
            of Const (a, _) => (case AList.lookup (op =) pairs a
wenzelm@21313
   102
              of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
wenzelm@21313
   103
              | NONE => [thm])
wenzelm@21313
   104
            | _ => [thm])
wenzelm@21313
   105
          | _ => [thm]
wenzelm@21313
   106
      end;
haftmann@21163
   107
  in atoms end;
haftmann@21163
   108
wenzelm@36543
   109
fun mksimps pairs (_: simpset) =
wenzelm@21313
   110
  map_filter (try mk_eq) o mk_atomize pairs o gen_all;
haftmann@21163
   111
wenzelm@43596
   112
fun unsafe_solver_tac ss =
wenzelm@22147
   113
  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
wenzelm@43597
   114
  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
wenzelm@43597
   115
    atac, etac @{thm FalseE}];
wenzelm@22147
   116
haftmann@21163
   117
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
haftmann@21163
   118
haftmann@22838
   119
haftmann@21163
   120
(*No premature instantiation of variables during simplification*)
wenzelm@43596
   121
fun safe_solver_tac ss =
wenzelm@22147
   122
  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
wenzelm@43597
   123
  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ss),
wenzelm@43597
   124
    eq_assume_tac, ematch_tac @{thms FalseE}];
wenzelm@22147
   125
haftmann@21163
   126
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
haftmann@21163
   127
wenzelm@32177
   128
structure Splitter = Splitter
wenzelm@32177
   129
(
wenzelm@32177
   130
  val thy = @{theory}
wenzelm@32177
   131
  val mk_eq = mk_eq
wenzelm@32177
   132
  val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
wenzelm@32177
   133
  val iffD = @{thm iffD2}
wenzelm@32177
   134
  val disjE = @{thm disjE}
wenzelm@32177
   135
  val conjE = @{thm conjE}
wenzelm@32177
   136
  val exE = @{thm exE}
wenzelm@32177
   137
  val contrapos = @{thm contrapos_nn}
wenzelm@32177
   138
  val contrapos2 = @{thm contrapos_pp}
wenzelm@32177
   139
  val notnotD = @{thm notnotD}
wenzelm@32177
   140
);
haftmann@21163
   141
wenzelm@32177
   142
val split_tac = Splitter.split_tac;
wenzelm@21674
   143
val split_inside_tac = Splitter.split_inside_tac;
wenzelm@21674
   144
wenzelm@21674
   145
haftmann@21163
   146
(* integration of simplifier with classical reasoner *)
haftmann@21163
   147
wenzelm@42478
   148
structure Clasimp = Clasimp
wenzelm@42478
   149
(
wenzelm@42478
   150
  structure Simplifier = Simplifier
wenzelm@42478
   151
    and Splitter = Splitter
wenzelm@42478
   152
    and Classical  = Classical
wenzelm@42478
   153
    and Blast = Blast
wenzelm@42478
   154
  val iffD1 = @{thm iffD1}
wenzelm@42478
   155
  val iffD2 = @{thm iffD2}
wenzelm@42478
   156
  val notE = @{thm notE}
wenzelm@42478
   157
);
wenzelm@21674
   158
open Clasimp;
haftmann@21163
   159
haftmann@21163
   160
val mksimps_pairs =
haftmann@38786
   161
 [(@{const_name HOL.implies}, [@{thm mp}]),
haftmann@38795
   162
  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
wenzelm@35364
   163
  (@{const_name All}, [@{thm spec}]),
wenzelm@35364
   164
  (@{const_name True}, []),
wenzelm@35364
   165
  (@{const_name False}, []),
wenzelm@35364
   166
  (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
haftmann@21163
   167
wenzelm@21674
   168
val HOL_basic_ss =
wenzelm@35232
   169
  Simplifier.global_context @{theory} empty_ss
wenzelm@45625
   170
  setSSolver safe_solver
wenzelm@45625
   171
  setSolver unsafe_solver
wenzelm@45625
   172
  |> Simplifier.set_subgoaler asm_simp_tac
wenzelm@45625
   173
  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
wenzelm@45625
   174
  |> Simplifier.set_mkeqTrue mk_eq_True
wenzelm@45625
   175
  |> Simplifier.set_mkcong mk_meta_cong;
haftmann@21163
   176
wenzelm@21674
   177
fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
haftmann@21163
   178
haftmann@21163
   179
fun unfold_tac ths =
wenzelm@21674
   180
  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
haftmann@21163
   181
  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
haftmann@21163
   182
wenzelm@21313
   183
end;
haftmann@21551
   184
haftmann@21551
   185
structure Splitter = Simpdata.Splitter;
haftmann@21551
   186
structure Clasimp = Simpdata.Clasimp;