src/Sequents/simpdata.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21428 f84cf8e9cad8
child 22896 1c2abcabea61
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
paulson@7098
     1
(*  Title:      Sequents/simpdata.ML
paulson@7098
     2
    ID:         $Id$
paulson@7098
     3
    Author:     Lawrence C Paulson
paulson@7098
     4
    Copyright   1999  University of Cambridge
paulson@7098
     5
paulson@7098
     6
Instantiation of the generic simplifier for LK
paulson@7098
     7
paulson@7098
     8
Borrows from the DC simplifier of Soren Heilmann.
paulson@7098
     9
*)
paulson@7098
    10
paulson@7098
    11
(*** Rewrite rules ***)
paulson@7098
    12
wenzelm@21426
    13
local
wenzelm@21426
    14
  val subst = thm "subst"
wenzelm@21426
    15
in
wenzelm@21426
    16
wenzelm@9713
    17
fun prove_fun s =
wenzelm@9713
    18
 (writeln s;
wenzelm@17481
    19
  prove_goal (the_context ()) s
wenzelm@9713
    20
   (fn prems => [ (cut_facts_tac prems 1),
wenzelm@21428
    21
                  (fast_tac (LK_pack add_safes [subst]) 1) ]));
wenzelm@21426
    22
end;
paulson@7098
    23
paulson@7098
    24
val conj_simps = map prove_fun
paulson@7098
    25
 ["|- P & True <-> P",      "|- True & P <-> P",
paulson@7098
    26
  "|- P & False <-> False", "|- False & P <-> False",
paulson@7098
    27
  "|- P & P <-> P", "        |- P & P & Q <-> P & Q",
paulson@7098
    28
  "|- P & ~P <-> False",    "|- ~P & P <-> False",
paulson@7098
    29
  "|- (P & Q) & R <-> P & (Q & R)"];
paulson@7098
    30
paulson@7098
    31
val disj_simps = map prove_fun
paulson@7098
    32
 ["|- P | True <-> True",  "|- True | P <-> True",
paulson@7098
    33
  "|- P | False <-> P",    "|- False | P <-> P",
paulson@7098
    34
  "|- P | P <-> P",        "|- P | P | Q <-> P | Q",
paulson@7098
    35
  "|- (P | Q) | R <-> P | (Q | R)"];
paulson@7098
    36
paulson@7098
    37
val not_simps = map prove_fun
paulson@7098
    38
 ["|- ~ False <-> True",   "|- ~ True <-> False"];
paulson@7098
    39
paulson@7098
    40
val imp_simps = map prove_fun
paulson@7098
    41
 ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
wenzelm@9713
    42
  "|- (False --> P) <-> True",     "|- (True --> P) <-> P",
paulson@7098
    43
  "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
paulson@7098
    44
paulson@7098
    45
val iff_simps = map prove_fun
paulson@7098
    46
 ["|- (True <-> P) <-> P",         "|- (P <-> True) <-> P",
paulson@7098
    47
  "|- (P <-> P) <-> True",
paulson@7098
    48
  "|- (False <-> P) <-> ~P",       "|- (P <-> False) <-> ~P"];
paulson@7098
    49
paulson@7123
    50
paulson@7123
    51
val quant_simps = map prove_fun
wenzelm@9713
    52
 ["|- (ALL x. P) <-> P",
paulson@7123
    53
  "|- (ALL x. x=t --> P(x)) <-> P(t)",
paulson@7123
    54
  "|- (ALL x. t=x --> P(x)) <-> P(t)",
paulson@7123
    55
  "|- (EX x. P) <-> P",
wenzelm@9713
    56
  "|- (EX x. x=t & P(x)) <-> P(t)",
paulson@7123
    57
  "|- (EX x. t=x & P(x)) <-> P(t)"];
paulson@7123
    58
paulson@7123
    59
(*** Miniscoping: pushing quantifiers in
paulson@7123
    60
     We do NOT distribute of ALL over &, or dually that of EX over |
wenzelm@9713
    61
     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
paulson@7123
    62
     show that this step can increase proof length!
paulson@7123
    63
***)
paulson@7123
    64
paulson@7123
    65
(*existential miniscoping*)
wenzelm@9713
    66
val ex_simps = map prove_fun
paulson@7123
    67
                   ["|- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
wenzelm@9713
    68
                    "|- (EX x. P & Q(x)) <-> P & (EX x. Q(x))",
wenzelm@9713
    69
                    "|- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
wenzelm@9713
    70
                    "|- (EX x. P | Q(x)) <-> P | (EX x. Q(x))",
wenzelm@9713
    71
                    "|- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
wenzelm@9713
    72
                    "|- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
paulson@7123
    73
paulson@7123
    74
(*universal miniscoping*)
paulson@7123
    75
val all_simps = map prove_fun
paulson@7123
    76
                    ["|- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
wenzelm@9713
    77
                     "|- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
wenzelm@9713
    78
                     "|- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
wenzelm@9713
    79
                     "|- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))",
wenzelm@9713
    80
                     "|- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
wenzelm@9713
    81
                     "|- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
paulson@7123
    82
paulson@7098
    83
(*These are NOT supplied by default!*)
paulson@7098
    84
val distrib_simps  = map prove_fun
wenzelm@9713
    85
 ["|- P & (Q | R) <-> P&Q | P&R",
paulson@7098
    86
  "|- (Q | R) & P <-> Q&P | R&P",
paulson@7098
    87
  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
paulson@7098
    88
paulson@7098
    89
(** Conversion into rewrite rules **)
paulson@7098
    90
wenzelm@21426
    91
local
wenzelm@21426
    92
  val mp_R = thm "mp_R";
wenzelm@21426
    93
  val conjunct1 = thm "conjunct1";
wenzelm@21426
    94
  val conjunct2 = thm "conjunct2";
wenzelm@21426
    95
  val spec = thm "spec";
wenzelm@21426
    96
in
paulson@7098
    97
(*Make atomic rewrite rules*)
paulson@7098
    98
fun atomize r =
paulson@7098
    99
 case concl_of r of
paulson@7098
   100
   Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
paulson@7098
   101
     (case (forms_of_seq a, forms_of_seq c) of
wenzelm@9713
   102
        ([], [p]) =>
wenzelm@9713
   103
          (case p of
wenzelm@9713
   104
               Const("op -->",_)$_$_ => atomize(r RS mp_R)
wenzelm@9713
   105
             | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
wenzelm@9713
   106
                   atomize(r RS conjunct2)
wenzelm@9713
   107
             | Const("All",_)$_      => atomize(r RS spec)
wenzelm@9713
   108
             | Const("True",_)       => []    (*True is DELETED*)
wenzelm@9713
   109
             | Const("False",_)      => []    (*should False do something?*)
wenzelm@9713
   110
             | _                     => [r])
paulson@7098
   111
      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
paulson@7098
   112
 | _ => [r];
wenzelm@21426
   113
end;
paulson@7098
   114
paulson@9259
   115
Goal "|- ~P ==> |- (P <-> False)";
wenzelm@21426
   116
by (etac (thm "thinR" RS (thm "cut")) 1);
wenzelm@21428
   117
by (fast_tac LK_pack 1);
paulson@9259
   118
qed "P_iff_F";
paulson@9259
   119
wenzelm@21426
   120
bind_thm ("iff_reflection_F", thm "P_iff_F" RS thm "iff_reflection");
paulson@7098
   121
paulson@9259
   122
Goal "|- P ==> |- (P <-> True)";
wenzelm@21426
   123
by (etac (thm "thinR" RS (thm "cut")) 1);
wenzelm@21428
   124
by (fast_tac LK_pack 1);
paulson@9259
   125
qed "P_iff_T";
paulson@9259
   126
wenzelm@21426
   127
bind_thm ("iff_reflection_T", thm "P_iff_T" RS thm "iff_reflection");
paulson@7098
   128
wenzelm@21426
   129
local
wenzelm@21426
   130
  val eq_reflection = thm "eq_reflection"
wenzelm@21426
   131
  val iff_reflection = thm "iff_reflection"
wenzelm@21426
   132
in
paulson@7098
   133
(*Make meta-equalities.*)
paulson@7098
   134
fun mk_meta_eq th = case concl_of th of
paulson@7098
   135
    Const("==",_)$_$_           => th
paulson@7098
   136
  | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
wenzelm@9713
   137
        (case (forms_of_seq a, forms_of_seq c) of
wenzelm@9713
   138
             ([], [p]) =>
wenzelm@9713
   139
                 (case p of
wenzelm@9713
   140
                      (Const("op =",_)$_$_)   => th RS eq_reflection
wenzelm@9713
   141
                    | (Const("op <->",_)$_$_) => th RS iff_reflection
wenzelm@9713
   142
                    | (Const("Not",_)$_)      => th RS iff_reflection_F
wenzelm@9713
   143
                    | _                       => th RS iff_reflection_T)
wenzelm@9713
   144
           | _ => error ("addsimps: unable to use theorem\n" ^
wenzelm@9713
   145
                         string_of_thm th));
wenzelm@21426
   146
end;
paulson@7098
   147
paulson@7123
   148
(*Replace premises x=y, X<->Y by X==Y*)
wenzelm@9713
   149
val mk_meta_prems =
wenzelm@9713
   150
    rule_by_tactic
wenzelm@21426
   151
      (REPEAT_FIRST (resolve_tac [thm "meta_eq_to_obj_eq", thm "def_imp_iff"]));
paulson@7123
   152
wenzelm@9713
   153
(*Congruence rules for = or <-> (instead of ==)*)
paulson@7123
   154
fun mk_meta_cong rl =
paulson@7123
   155
  standard(mk_meta_eq (mk_meta_prems rl))
paulson@7123
   156
  handle THM _ =>
paulson@7123
   157
  error("Premises and conclusion of congruence rules must use =-equality or <->");
paulson@7123
   158
paulson@7123
   159
paulson@7123
   160
(*** Named rewrite rules ***)
paulson@7098
   161
wenzelm@17481
   162
fun prove nm thm  = qed_goal nm (the_context ()) thm
wenzelm@9713
   163
    (fn prems => [ (cut_facts_tac prems 1),
paulson@7098
   164
                   (fast_tac LK_pack 1) ]);
paulson@7098
   165
paulson@7098
   166
prove "conj_commute" "|- P&Q <-> Q&P";
paulson@7098
   167
prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)";
paulson@7098
   168
val conj_comms = [conj_commute, conj_left_commute];
paulson@7098
   169
paulson@7098
   170
prove "disj_commute" "|- P|Q <-> Q|P";
paulson@7098
   171
prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)";
paulson@7098
   172
val disj_comms = [disj_commute, disj_left_commute];
paulson@7098
   173
paulson@7098
   174
prove "conj_disj_distribL" "|- P&(Q|R) <-> (P&Q | P&R)";
paulson@7098
   175
prove "conj_disj_distribR" "|- (P|Q)&R <-> (P&R | Q&R)";
paulson@7098
   176
paulson@7098
   177
prove "disj_conj_distribL" "|- P|(Q&R) <-> (P|Q) & (P|R)";
paulson@7098
   178
prove "disj_conj_distribR" "|- (P&Q)|R <-> (P|R) & (Q|R)";
paulson@7098
   179
paulson@7098
   180
prove "imp_conj_distrib" "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)";
paulson@7098
   181
prove "imp_conj"         "|- ((P&Q)-->R)   <-> (P --> (Q --> R))";
paulson@7098
   182
prove "imp_disj"         "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)";
paulson@7098
   183
paulson@7098
   184
prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)";
paulson@7098
   185
prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)";
paulson@7098
   186
paulson@7098
   187
prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)";
paulson@7098
   188
prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)";
paulson@7098
   189
paulson@7098
   190
prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
paulson@7098
   191
paulson@7098
   192
wenzelm@9713
   193
val [p1,p2] = Goal
paulson@7098
   194
    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
paulson@7098
   195
by (lemma_tac p1 1);
wenzelm@21428
   196
by (safe_tac LK_pack 1);
wenzelm@21426
   197
by (REPEAT (rtac (thm "cut") 1
wenzelm@9713
   198
            THEN
wenzelm@21426
   199
            DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
wenzelm@9713
   200
            THEN
wenzelm@21428
   201
            safe_tac LK_pack 1));
paulson@7098
   202
qed "imp_cong";
paulson@7098
   203
wenzelm@9713
   204
val [p1,p2] = Goal
paulson@7098
   205
    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
paulson@7098
   206
by (lemma_tac p1 1);
wenzelm@21428
   207
by (safe_tac LK_pack 1);
wenzelm@21426
   208
by (REPEAT (rtac (thm "cut") 1
wenzelm@9713
   209
            THEN
wenzelm@21426
   210
            DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
wenzelm@9713
   211
            THEN
wenzelm@21428
   212
            safe_tac LK_pack 1));
paulson@7098
   213
qed "conj_cong";
paulson@7098
   214
paulson@7123
   215
Goal "|- (x=y) <-> (y=x)";
wenzelm@21428
   216
by (fast_tac (LK_pack add_safes [thm "subst"]) 1);
paulson@7123
   217
qed "eq_sym_conv";
paulson@7123
   218
paulson@7123
   219
paulson@7098
   220
paulson@7098
   221
(*** Standard simpsets ***)
paulson@7098
   222
wenzelm@21426
   223
val triv_rls = [thm "FalseL", thm "TrueR", thm "basic", thm "refl",
wenzelm@21426
   224
  thm "iff_refl", reflexive_thm];
paulson@7098
   225
paulson@7098
   226
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
wenzelm@9713
   227
                                 assume_tac];
paulson@7098
   228
(*No premature instantiation of variables during simplification*)
paulson@7098
   229
fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
wenzelm@9713
   230
                                 eq_assume_tac];
paulson@7098
   231
paulson@7098
   232
(*No simprules, but basic infrastructure for simplification*)
wenzelm@9713
   233
val LK_basic_ss =
wenzelm@17892
   234
  Simplifier.theory_context (the_context ()) empty_ss
wenzelm@17892
   235
    setsubgoaler asm_simp_tac
wenzelm@9713
   236
    setSSolver (mk_solver "safe" safe_solver)
wenzelm@9713
   237
    setSolver (mk_solver "unsafe" unsafe_solver)
wenzelm@12725
   238
    setmksimps (map mk_meta_eq o atomize o gen_all)
wenzelm@9713
   239
    setmkcong mk_meta_cong;
paulson@7098
   240
paulson@7098
   241
val LK_simps =
paulson@7123
   242
   [triv_forall_equality, (* prunes params *)
wenzelm@21426
   243
    thm "refl" RS P_iff_T] @
wenzelm@9713
   244
    conj_simps @ disj_simps @ not_simps @
paulson@7123
   245
    imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
paulson@7098
   246
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
paulson@7098
   247
    map prove_fun
paulson@7098
   248
     ["|- P | ~P",             "|- ~P | P",
paulson@7098
   249
      "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
paulson@7098
   250
      "|- (~P <-> ~Q) <-> (P<->Q)"];
paulson@7098
   251
wenzelm@9713
   252
val LK_ss =
wenzelm@9713
   253
  LK_basic_ss addsimps LK_simps
wenzelm@21428
   254
  addeqcongs [thm "left_cong"]
wenzelm@9713
   255
  addcongs [imp_cong];
paulson@7098
   256
wenzelm@17876
   257
change_simpset (fn _ => LK_ss);
paulson@7098
   258
paulson@7098
   259
paulson@7123
   260
(* To create substition rules *)
paulson@7098
   261
wenzelm@17481
   262
qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
paulson@7098
   263
  (fn prems =>
paulson@7098
   264
   [cut_facts_tac prems 1,
paulson@7098
   265
    asm_simp_tac LK_basic_ss 1]);
paulson@7098
   266
paulson@7123
   267
Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
wenzelm@21426
   268
by (res_inst_tac [ ("P","Q") ] (thm "cut") 1);
wenzelm@21426
   269
by (simp_tac (simpset() addsimps [thm "if_P"]) 2);
wenzelm@21426
   270
by (res_inst_tac [ ("P","~Q") ] (thm "cut") 1);
wenzelm@21426
   271
by (simp_tac (simpset() addsimps [thm "if_not_P"]) 2);
wenzelm@21428
   272
by (fast_tac LK_pack 1);
paulson@7123
   273
qed "split_if";
paulson@7098
   274
paulson@7123
   275
Goal "|- (if P then x else x) = x";
paulson@7123
   276
by (lemma_tac split_if 1);
wenzelm@21428
   277
by (fast_tac LK_pack 1);
paulson@7123
   278
qed "if_cancel";
paulson@7123
   279
paulson@7123
   280
Goal "|- (if x=y then y else x) = x";
paulson@7123
   281
by (lemma_tac split_if 1);
wenzelm@21428
   282
by (safe_tac LK_pack 1);
wenzelm@21426
   283
by (rtac (thm "symL") 1);
wenzelm@21426
   284
by (rtac (thm "basic") 1);
paulson@7123
   285
qed "if_eq_cancel";
paulson@7123
   286
paulson@7123
   287
(*Putting in automatic case splits seems to require a lot of work.*)