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