1(*  Title:      Sequents/simpdata.ML
2    Author:     Lawrence C Paulson
3    Copyright   1999  University of Cambridge
4
5Instantiation of the generic simplifier for LK.
6
7Borrows from the DC simplifier of Soren Heilmann.
8*)
9
10
11(** Conversion into rewrite rules **)
12
13(*Make atomic rewrite rules*)
14fun atomize r =
15 case Thm.concl_of r of
16   Const(\<^const_name>\<open>Trueprop\<close>,_) $ 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>\<open>imp\<close>,_)$_$_ => atomize(r RS @{thm mp_R})
21             | Const(\<^const_name>\<open>conj\<close>,_)$_$_   => atomize(r RS @{thm conjunct1}) @
22                   atomize(r RS @{thm conjunct2})
23             | Const(\<^const_name>\<open>All\<close>,_)$_      => atomize(r RS @{thm spec})
24             | Const(\<^const_name>\<open>True\<close>,_)       => []    (*True is DELETED*)
25             | Const(\<^const_name>\<open>False\<close>,_)      => []    (*should False do something?*)
26             | _                     => [r])
27      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
28 | _ => [r];
29
30(*Make meta-equalities.*)
31fun mk_meta_eq ctxt th = case Thm.concl_of th of
32    Const(\<^const_name>\<open>Pure.eq\<close>,_)$_$_ => th
33  | Const(\<^const_name>\<open>Trueprop\<close>,_) $ 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>\<open>equal\<close>,_)$_$_)   => th RS @{thm eq_reflection}
38                    | (Const(\<^const_name>\<open>iff\<close>,_)$_$_) => th RS @{thm iff_reflection}
39                    | (Const(\<^const_name>\<open>Not\<close>,_)$_)      => th RS @{thm iff_reflection_F}
40                    | _                       => th RS @{thm iff_reflection_T})
41           | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
42
43(*Replace premises x=y, X<->Y by X==Y*)
44fun mk_meta_prems ctxt =
45    rule_by_tactic ctxt
46      (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
47
48(*Congruence rules for = or <-> (instead of ==)*)
49fun 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
57val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl},
58  @{thm iff_refl}, reflexive_thm];
59
60fun unsafe_solver ctxt =
61  FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt];
62
63(*No premature instantiation of variables during simplification*)
64fun 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*)
69val 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 Variable.gen_all ctxt)
75  |> Simplifier.set_mkcong mk_meta_cong
76  |> simpset_of;
77
78val 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
87val 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
93