src/Sequents/simpdata.ML
author paulson
Tue, 27 Jul 1999 19:02:43 +0200
changeset 7098 86583034aacf
child 7123 4ab38de3fd20
permissions -rw-r--r--
installation of simplifier and classical reasoner, better rules etc
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
MAJOR LIMITATION: left-side sequent formulae are not added to the simpset.
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    11
  However, congruence rules for --> and & are available.
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    12
  The rule backwards_impR can be used to convert assumptions into right-side
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    13
  implications.
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    14
*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    15
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    16
(*** Rewrite rules ***)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    17
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    18
fun prove_fun s = 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    19
 (writeln s;  
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    20
  prove_goal LK.thy s
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    21
   (fn prems => [ (cut_facts_tac prems 1), 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    22
                  (fast_tac LK_pack 1) ]));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    23
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    24
val conj_simps = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    25
 ["|- P & True <-> P",      "|- True & P <-> P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    26
  "|- P & False <-> False", "|- False & P <-> False",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    27
  "|- P & P <-> P", "        |- P & P & Q <-> P & Q",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    28
  "|- P & ~P <-> False",    "|- ~P & P <-> False",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    29
  "|- (P & Q) & R <-> P & (Q & R)"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    30
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    31
val disj_simps = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    32
 ["|- P | True <-> True",  "|- True | P <-> True",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    33
  "|- P | False <-> P",    "|- False | P <-> P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    34
  "|- P | P <-> P",        "|- P | P | Q <-> P | Q",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    35
  "|- (P | Q) | R <-> P | (Q | R)"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    36
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    37
val not_simps = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    38
 ["|- ~ False <-> True",   "|- ~ True <-> False"];
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 imp_simps = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    41
 ["|- (P --> False) <-> ~P",       "|- (P --> True) <-> True",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    42
  "|- (False --> P) <-> True",     "|- (True --> P) <-> P", 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    43
  "|- (P --> P) <-> True",         "|- (P --> ~P) <-> ~P"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    44
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    45
val iff_simps = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    46
 ["|- (True <-> P) <-> P",         "|- (P <-> True) <-> P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    47
  "|- (P <-> P) <-> True",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    48
  "|- (False <-> P) <-> ~P",       "|- (P <-> False) <-> ~P"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    49
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    50
(*These are NOT supplied by default!*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    51
val distrib_simps  = map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    52
 ["|- P & (Q | R) <-> P&Q | P&R", 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    53
  "|- (Q | R) & P <-> Q&P | R&P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    54
  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    55
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    56
(** Conversion into rewrite rules **)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    57
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    58
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    59
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    60
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    61
(*Make atomic rewrite rules*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    62
fun atomize r =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    63
 case concl_of r of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    64
   Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    65
     (case (forms_of_seq a, forms_of_seq c) of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    66
	([], [p]) =>
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    67
	  (case p of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    68
	       Const("op -->",_)$_$_ => atomize(r RS mp_R)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    69
	     | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    70
		   atomize(r RS conjunct2)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    71
	     | Const("All",_)$_      => atomize(r RS spec)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    72
	     | Const("True",_)       => []    (*True is DELETED*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    73
	     | Const("False",_)      => []    (*should False do something?*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    74
	     | _                     => [r])
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    75
      | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    76
 | _ => [r];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    77
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    78
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    79
qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)"
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    80
    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    81
val iff_reflection_F = P_iff_F RS iff_reflection;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    82
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    83
qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)"
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    84
    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    85
val iff_reflection_T = P_iff_T RS iff_reflection;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    86
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    87
(*Make meta-equalities.*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    88
fun mk_meta_eq th = case concl_of th of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    89
    Const("==",_)$_$_           => th
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    90
  | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    91
	(case (forms_of_seq a, forms_of_seq c) of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    92
	     ([], [p]) => 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    93
		 (case p of
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    94
		      (Const("op =",_)$_$_)   => th RS eq_reflection
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    95
		    | (Const("op <->",_)$_$_) => th RS iff_reflection
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    96
		    | (Const("Not",_)$_)      => th RS iff_reflection_F
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    97
		    | _                       => th RS iff_reflection_T)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    98
	   | _ => error ("addsimps: unable to use theorem\n" ^
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
    99
			 string_of_thm th));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   100
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   101
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   102
(*** Named rewrite rules proved for PL ***)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   103
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   104
fun prove nm thm  = qed_goal nm LK.thy thm
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   105
    (fn prems => [ (cut_facts_tac prems 1), 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   106
                   (fast_tac LK_pack 1) ]);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   107
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   108
prove "conj_commute" "|- P&Q <-> Q&P";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   109
prove "conj_left_commute" "|- P&(Q&R) <-> Q&(P&R)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   110
val conj_comms = [conj_commute, conj_left_commute];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   111
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   112
prove "disj_commute" "|- P|Q <-> Q|P";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   113
prove "disj_left_commute" "|- P|(Q|R) <-> Q|(P|R)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   114
val disj_comms = [disj_commute, disj_left_commute];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   115
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   116
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
   117
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
   118
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   119
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
   120
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
   121
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   122
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
   123
prove "imp_conj"         "|- ((P&Q)-->R)   <-> (P --> (Q --> R))";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   124
prove "imp_disj"         "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   125
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   126
prove "imp_disj1" "|- (P-->Q) | R <-> (P-->Q | R)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   127
prove "imp_disj2" "|- Q | (P-->R) <-> (P-->Q | R)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   128
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   129
prove "de_Morgan_disj" "|- (~(P | Q)) <-> (~P & ~Q)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   130
prove "de_Morgan_conj" "|- (~(P & Q)) <-> (~P | ~Q)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   131
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   132
prove "not_iff" "|- ~(P <-> Q) <-> (P <-> ~Q)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   133
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   134
prove "iff_refl" "|- (P <-> P)";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   135
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   136
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   137
val [p1,p2] = Goal 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   138
    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   139
by (lemma_tac p1 1);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   140
by (Safe_tac 1);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   141
by (REPEAT (rtac cut 1 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   142
	    THEN
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   143
	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   144
	    THEN
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   145
	    Safe_tac 1));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   146
qed "imp_cong";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   147
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   148
val [p1,p2] = Goal 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   149
    "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   150
by (lemma_tac p1 1);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   151
by (Safe_tac 1);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   152
by (REPEAT (rtac cut 1 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   153
	    THEN
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   154
	    DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   155
	    THEN
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   156
	    Safe_tac 1));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   157
qed "conj_cong";
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   158
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
open Simplifier;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   161
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   162
(*** Standard simpsets ***)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   163
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   164
(*Add congruence rules for = or <-> (instead of ==) *)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   165
infix 4 addcongs delcongs;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   166
fun ss addcongs congs =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   167
        ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   168
fun ss delcongs congs =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   169
        ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   170
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   171
fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   172
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   173
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   174
val triv_rls = [FalseL, TrueR, basic, refl, iff_refl];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   175
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   176
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   177
				 assume_tac];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   178
(*No premature instantiation of variables during simplification*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   179
fun   safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i),
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   180
				 eq_assume_tac];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   181
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   182
(*No simprules, but basic infrastructure for simplification*)
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   183
val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   184
			   setSSolver   safe_solver
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   185
			   setSolver    unsafe_solver
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   186
			   setmksimps   (map mk_meta_eq o atomize o gen_all);
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   187
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   188
val LK_simps =
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   189
   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   190
    imp_simps @ iff_simps @
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   191
    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   192
    map prove_fun
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   193
     ["|- P | ~P",             "|- ~P | P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   194
      "|- ~ ~ P <-> P",        "|- (~P --> P) <-> P",
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   195
      "|- (~P <-> ~Q) <-> (P<->Q)"];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   196
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   197
val LK_ss = LK_basic_ss addsimps LK_simps addcongs [imp_cong];
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   198
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   199
simpset_ref() := LK_ss;
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   200
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   201
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   202
(* Subst rule *)
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
qed_goal "subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   205
  (fn prems =>
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   206
   [cut_facts_tac prems 1,
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents:
diff changeset
   207
    asm_simp_tac LK_basic_ss 1]);
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