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