src/Sequents/simpdata.ML
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 61268 abe08fb15a12
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
paulson@7098
     1
(*  Title:      Sequents/simpdata.ML
paulson@7098
     2
    Author:     Lawrence C Paulson
paulson@7098
     3
    Copyright   1999  University of Cambridge
paulson@7098
     4
wenzelm@27149
     5
Instantiation of the generic simplifier for LK.
paulson@7098
     6
paulson@7098
     7
Borrows from the DC simplifier of Soren Heilmann.
paulson@7098
     8
*)
paulson@7098
     9
paulson@7098
    10
paulson@7098
    11
(** Conversion into rewrite rules **)
paulson@7098
    12
paulson@7098
    13
(*Make atomic rewrite rules*)
paulson@7098
    14
fun atomize r =
wenzelm@59582
    15
 case Thm.concl_of r of
haftmann@38500
    16
   Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
wenzelm@55228
    17
     (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
wenzelm@9713
    18
        ([], [p]) =>
wenzelm@9713
    19
          (case p of
haftmann@38500
    20
               Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R})
haftmann@38500
    21
             | Const(@{const_name conj},_)$_$_   => atomize(r RS @{thm conjunct1}) @
wenzelm@22896
    22
                   atomize(r RS @{thm conjunct2})
haftmann@38500
    23
             | Const(@{const_name All},_)$_      => atomize(r RS @{thm spec})
haftmann@38500
    24
             | Const(@{const_name True},_)       => []    (*True is DELETED*)
haftmann@38500
    25
             | Const(@{const_name False},_)      => []    (*should False do something?*)
wenzelm@9713
    26
             | _                     => [r])
paulson@7098
    27
      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
paulson@7098
    28
 | _ => [r];
paulson@7098
    29
paulson@7098
    30
(*Make meta-equalities.*)
wenzelm@59582
    31
fun mk_meta_eq ctxt th = case Thm.concl_of th of
wenzelm@56245
    32
    Const(@{const_name Pure.eq},_)$_$_ => th
haftmann@38500
    33
  | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
wenzelm@55228
    34
        (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
wenzelm@9713
    35
             ([], [p]) =>
wenzelm@9713
    36
                 (case p of
haftmann@38500
    37
                      (Const(@{const_name equal},_)$_$_)   => th RS @{thm eq_reflection}
haftmann@38500
    38
                    | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
haftmann@38500
    39
                    | (Const(@{const_name Not},_)$_)      => th RS @{thm iff_reflection_F}
wenzelm@27149
    40
                    | _                       => th RS @{thm iff_reflection_T})
wenzelm@61268
    41
           | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
paulson@7098
    42
paulson@7123
    43
(*Replace premises x=y, X<->Y by X==Y*)
wenzelm@36546
    44
fun mk_meta_prems ctxt =
wenzelm@36546
    45
    rule_by_tactic ctxt
wenzelm@59498
    46
      (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
paulson@7123
    47
wenzelm@9713
    48
(*Congruence rules for = or <-> (instead of ==)*)
wenzelm@51717
    49
fun mk_meta_cong ctxt rl =
wenzelm@55228
    50
  Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl))
wenzelm@35021
    51
    handle THM _ =>
wenzelm@35021
    52
      error("Premises and conclusion of congruence rules must use =-equality or <->");
paulson@7123
    53
paulson@7123
    54
paulson@7098
    55
(*** Standard simpsets ***)
paulson@7098
    56
wenzelm@27149
    57
val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
wenzelm@27149
    58
  @{thm iff_refl}, reflexive_thm];
paulson@7098
    59
wenzelm@51717
    60
fun unsafe_solver ctxt =
wenzelm@59498
    61
  FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt];
wenzelm@27149
    62
paulson@7098
    63
(*No premature instantiation of variables during simplification*)
wenzelm@51717
    64
fun safe_solver ctxt =
wenzelm@58957
    65
  FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
wenzelm@58957
    66
    eq_assume_tac];
paulson@7098
    67
paulson@7098
    68
(*No simprules, but basic infrastructure for simplification*)
wenzelm@9713
    69
val LK_basic_ss =
wenzelm@51717
    70
  empty_simpset @{context}
wenzelm@45625
    71
  setSSolver (mk_solver "safe" safe_solver)
wenzelm@45625
    72
  setSolver (mk_solver "unsafe" unsafe_solver)
wenzelm@45625
    73
  |> Simplifier.set_subgoaler asm_simp_tac
wenzelm@60822
    74
  |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
wenzelm@51717
    75
  |> Simplifier.set_mkcong mk_meta_cong
wenzelm@51717
    76
  |> simpset_of;
paulson@7098
    77
paulson@7098
    78
val LK_simps =
wenzelm@46186
    79
   [@{thm triv_forall_equality}, (* prunes params *)
wenzelm@27149
    80
    @{thm refl} RS @{thm P_iff_T}] @
wenzelm@27149
    81
    @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @
wenzelm@27149
    82
    @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @
wenzelm@27149
    83
    @{thms all_simps} @ @{thms ex_simps} @
wenzelm@27149
    84
    [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @
wenzelm@27149
    85
    @{thms LK_extra_simps};
paulson@7098
    86
wenzelm@9713
    87
val LK_ss =
wenzelm@51717
    88
  put_simpset LK_basic_ss @{context} addsimps LK_simps
wenzelm@45620
    89
  |> Simplifier.add_eqcong @{thm left_cong}
wenzelm@51717
    90
  |> Simplifier.add_cong @{thm imp_cong}
wenzelm@51717
    91
  |> simpset_of;
paulson@7098
    92