src/Sequents/simpdata.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 56245 84fc7dfa3cd4
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
     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 (Cla.forms_of_seq a, Cla.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 ctxt th = case concl_of th of
    32     Const(@{const_name Pure.eq},_)$_$_ => th
    33   | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
    34         (case (Cla.forms_of_seq a, Cla.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" ^ Display.string_of_thm ctxt th));
    42 
    43 (*Replace premises x=y, X<->Y by X==Y*)
    44 fun mk_meta_prems ctxt =
    45     rule_by_tactic ctxt
    46       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
    47 
    48 (*Congruence rules for = or <-> (instead of ==)*)
    49 fun mk_meta_cong ctxt rl =
    50   Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl))
    51     handle THM _ =>
    52       error("Premises and conclusion of congruence rules must use =-equality or <->");
    53 
    54 
    55 (*** Standard simpsets ***)
    56 
    57 val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
    58   @{thm iff_refl}, reflexive_thm];
    59 
    60 fun unsafe_solver ctxt =
    61   FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac];
    62 
    63 (*No premature instantiation of variables during simplification*)
    64 fun safe_solver ctxt =
    65   FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
    66     eq_assume_tac];
    67 
    68 (*No simprules, but basic infrastructure for simplification*)
    69 val LK_basic_ss =
    70   empty_simpset @{context}
    71   setSSolver (mk_solver "safe" safe_solver)
    72   setSolver (mk_solver "unsafe" unsafe_solver)
    73   |> Simplifier.set_subgoaler asm_simp_tac
    74   |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o gen_all)
    75   |> Simplifier.set_mkcong mk_meta_cong
    76   |> simpset_of;
    77 
    78 val LK_simps =
    79    [@{thm 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   put_simpset LK_basic_ss @{context} addsimps LK_simps
    89   |> Simplifier.add_eqcong @{thm left_cong}
    90   |> Simplifier.add_cong @{thm imp_cong}
    91   |> simpset_of;
    92