src/HOL/Tools/simpdata.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63636 6f38b7abb648
child 67329 eabcd2e2bc9b
permissions -rw-r--r--
tuned;
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@59582
    44
fun mk_eq th =
wenzelm@59582
    45
  (case Thm.concl_of th of
haftmann@21163
    46
  (*expects Trueprop if not == *)
wenzelm@59582
    47
    Const (@{const_name Pure.eq},_) $ _ $ _ => th
wenzelm@59582
    48
  | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
wenzelm@59582
    49
  | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
wenzelm@59582
    50
  | _ => th RS @{thm Eq_TrueI})
haftmann@21163
    51
wenzelm@51717
    52
fun mk_eq_True (_: Proof.context) r =
wenzelm@22147
    53
  SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
haftmann@21163
    54
haftmann@21163
    55
(* Produce theorems of the form
haftmann@21163
    56
  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
haftmann@21163
    57
*)
haftmann@22838
    58
wenzelm@60651
    59
fun lift_meta_eq_to_obj_eq ctxt i st =
haftmann@21163
    60
  let
wenzelm@35364
    61
    fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
haftmann@21163
    62
      | count_imp _ = 0;
wenzelm@45622
    63
    val j = count_imp (Logic.strip_assums_concl (Thm.term_of (Thm.cprem_of st i)))
wenzelm@42364
    64
  in
wenzelm@42364
    65
    if j = 0 then @{thm meta_eq_to_obj_eq}
haftmann@21163
    66
    else
haftmann@21163
    67
      let
haftmann@21163
    68
        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
wenzelm@45622
    69
        val mk_simp_implies = fold_rev (fn R => fn S =>
wenzelm@45622
    70
          Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps;
wenzelm@42364
    71
      in
wenzelm@60651
    72
        Goal.prove_global (Proof_Context.theory_of ctxt) []
wenzelm@45622
    73
          [mk_simp_implies @{prop "(x::'a) == y"}]
wenzelm@45622
    74
          (mk_simp_implies @{prop "(x::'a) = y"})
wenzelm@54742
    75
          (fn {context = ctxt, prems} => EVERY
wenzelm@54742
    76
           [rewrite_goals_tac ctxt @{thms simp_implies_def},
wenzelm@59499
    77
            REPEAT (assume_tac ctxt 1 ORELSE
wenzelm@59499
    78
              resolve_tac ctxt
wenzelm@59499
    79
                (@{thm meta_eq_to_obj_eq} ::
wenzelm@59499
    80
                  map (rewrite_rule ctxt @{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@59498
    85
fun mk_meta_cong ctxt rl =
wenzelm@59498
    86
  let
wenzelm@59498
    87
    val rl' = Seq.hd (TRYALL (fn i => fn st =>
wenzelm@60651
    88
      resolve_tac ctxt [lift_meta_eq_to_obj_eq ctxt i st] i st) rl)
wenzelm@59498
    89
  in
wenzelm@59498
    90
    mk_meta_eq rl' handle THM _ =>
wenzelm@59582
    91
      if can Logic.dest_equals (Thm.concl_of rl') then rl'
wenzelm@59498
    92
      else error "Conclusion of congruence rules must be =-equality"
wenzelm@59498
    93
  end |> zero_var_indexes;
haftmann@21163
    94
wenzelm@59169
    95
fun mk_atomize ctxt pairs =
haftmann@21163
    96
  let
wenzelm@21313
    97
    fun atoms thm =
wenzelm@21313
    98
      let
wenzelm@21313
    99
        fun res th = map (fn rl => th RS rl);   (*exception THM*)
wenzelm@59169
   100
        val thm_ctxt = Variable.declare_thm thm ctxt;
wenzelm@21313
   101
        fun res_fixed rls =
wenzelm@21313
   102
          if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
wenzelm@59169
   103
          else Variable.trade (K (fn [thm'] => res thm' rls)) thm_ctxt [thm];
wenzelm@21313
   104
      in
wenzelm@59582
   105
        case Thm.concl_of thm
wenzelm@35364
   106
          of Const (@{const_name Trueprop}, _) $ p => (case head_of p
wenzelm@21313
   107
            of Const (a, _) => (case AList.lookup (op =) pairs a
wenzelm@21313
   108
              of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
wenzelm@21313
   109
              | NONE => [thm])
wenzelm@21313
   110
            | _ => [thm])
wenzelm@21313
   111
          | _ => [thm]
wenzelm@21313
   112
      end;
haftmann@21163
   113
  in atoms end;
haftmann@21163
   114
wenzelm@60822
   115
fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt;
haftmann@21163
   116
wenzelm@51717
   117
fun unsafe_solver_tac ctxt =
nipkow@56073
   118
  let
nipkow@56073
   119
    val sol_thms =
nipkow@56073
   120
      reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
nipkow@56073
   121
    fun sol_tac i =
wenzelm@59498
   122
      FIRST
wenzelm@59498
   123
       [resolve_tac ctxt sol_thms i,
wenzelm@59498
   124
        assume_tac ctxt i,
wenzelm@59498
   125
        eresolve_tac ctxt @{thms FalseE} i] ORELSE
nipkow@60171
   126
          (match_tac ctxt [@{thm conjI}]
nipkow@60171
   127
      THEN_ALL_NEW sol_tac) i
nipkow@56073
   128
  in
wenzelm@58957
   129
    (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
nipkow@56073
   130
  end;
wenzelm@22147
   131
haftmann@21163
   132
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
haftmann@21163
   133
haftmann@22838
   134
haftmann@21163
   135
(*No premature instantiation of variables during simplification*)
wenzelm@51717
   136
fun safe_solver_tac ctxt =
wenzelm@58957
   137
  (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN'
wenzelm@58957
   138
  FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
wenzelm@58957
   139
    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
wenzelm@22147
   140
haftmann@21163
   141
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
haftmann@21163
   142
wenzelm@32177
   143
structure Splitter = Splitter
wenzelm@32177
   144
(
wenzelm@59970
   145
  val context = @{context}
wenzelm@32177
   146
  val mk_eq = mk_eq
wenzelm@32177
   147
  val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
wenzelm@32177
   148
  val iffD = @{thm iffD2}
wenzelm@32177
   149
  val disjE = @{thm disjE}
wenzelm@32177
   150
  val conjE = @{thm conjE}
wenzelm@32177
   151
  val exE = @{thm exE}
wenzelm@32177
   152
  val contrapos = @{thm contrapos_nn}
wenzelm@32177
   153
  val contrapos2 = @{thm contrapos_pp}
wenzelm@32177
   154
  val notnotD = @{thm notnotD}
nipkow@63636
   155
  val safe_tac = Classical.safe_tac
wenzelm@32177
   156
);
haftmann@21163
   157
wenzelm@32177
   158
val split_tac = Splitter.split_tac;
wenzelm@21674
   159
val split_inside_tac = Splitter.split_inside_tac;
wenzelm@21674
   160
wenzelm@21674
   161
haftmann@21163
   162
(* integration of simplifier with classical reasoner *)
haftmann@21163
   163
wenzelm@42478
   164
structure Clasimp = Clasimp
wenzelm@42478
   165
(
wenzelm@42478
   166
  structure Simplifier = Simplifier
wenzelm@42478
   167
    and Splitter = Splitter
wenzelm@42478
   168
    and Classical  = Classical
wenzelm@42478
   169
    and Blast = Blast
wenzelm@42478
   170
  val iffD1 = @{thm iffD1}
wenzelm@42478
   171
  val iffD2 = @{thm iffD2}
wenzelm@42478
   172
  val notE = @{thm notE}
wenzelm@42478
   173
);
wenzelm@21674
   174
open Clasimp;
haftmann@21163
   175
haftmann@21163
   176
val mksimps_pairs =
haftmann@38786
   177
 [(@{const_name HOL.implies}, [@{thm mp}]),
haftmann@38795
   178
  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
wenzelm@35364
   179
  (@{const_name All}, [@{thm spec}]),
wenzelm@35364
   180
  (@{const_name True}, []),
wenzelm@35364
   181
  (@{const_name False}, []),
wenzelm@35364
   182
  (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
haftmann@21163
   183
wenzelm@21674
   184
val HOL_basic_ss =
wenzelm@51717
   185
  empty_simpset @{context}
wenzelm@45625
   186
  setSSolver safe_solver
wenzelm@45625
   187
  setSolver unsafe_solver
wenzelm@45625
   188
  |> Simplifier.set_subgoaler asm_simp_tac
wenzelm@45625
   189
  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
wenzelm@45625
   190
  |> Simplifier.set_mkeqTrue mk_eq_True
wenzelm@51717
   191
  |> Simplifier.set_mkcong mk_meta_cong
wenzelm@51717
   192
  |> simpset_of;
haftmann@21163
   193
wenzelm@51717
   194
fun hol_simplify ctxt rews =
wenzelm@51717
   195
  Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
wenzelm@51717
   196
wenzelm@54998
   197
fun unfold_tac ctxt ths =
wenzelm@51717
   198
  ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
haftmann@21163
   199
wenzelm@21313
   200
end;
haftmann@21551
   201
haftmann@21551
   202
structure Splitter = Simpdata.Splitter;
haftmann@21551
   203
structure Clasimp = Simpdata.Clasimp;