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