src/LK/lk.ML
author nipkow
Thu, 26 Nov 1998 12:18:08 +0100
changeset 5974 6acf3ff0f486
parent 0 a5a9c433f639
permissions -rw-r--r--
Added filter_prems_tac
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	LK/lk.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open LK;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*Higher precedence than := facilitates use of references*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
infix 4 add_safes add_unsafes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
signature LK_RESOLVE = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  datatype pack = Pack of thm list * thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val add_safes:   pack * thm list -> pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val add_unsafes: pack * thm list -> pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val allL_thin: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val best_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val could_res: term * term -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val could_resolve_seq: term * term -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val cutL_tac: string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val cutR_tac: string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val conL: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val conR: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val empty_pack: pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val exR_thin: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val fast_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val filseq_resolve_tac: thm list -> int -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val forms_of_seq: term -> term list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val has_prems: int -> thm -> bool   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val iffL: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val iffR: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val less: thm * thm -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val LK_dup_pack: pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val LK_pack: pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val pc_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  val prop_pack: pack
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  val repeat_goal_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val reresolve_tac: thm list -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val safe_goal_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  val step_tac: pack -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val symL: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val TrueR: thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
structure LK_Resolve : LK_RESOLVE = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
(*Cut and thin, replacing the right-side formula*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
fun cutR_tac (sP: string) i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
(*Cut and thin, replacing the left-side formula*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
fun cutL_tac (sP: string) i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
(** If-and-only-if rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
val iffR = prove_goalw LK.thy [iff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val iffL = prove_goalw LK.thy [iff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val TrueR = prove_goalw LK.thy [True_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "$H |- $E, True, $F"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
 (fn _=> [ rtac impR 1, rtac basic 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val allL_thin = prove_goal LK.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
 (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val exR_thin = prove_goal LK.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
    "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
 (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(* Symmetry of equality in hypotheses *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val symL = prove_goal LK.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  [ (rtac cut 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
    (rtac thinL 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    (resolve_tac prems 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
    (resolve_tac [basic RS sym] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
(**** Theorem Packs ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
datatype pack = Pack of thm list * thm list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*A theorem pack has the form  (safe rules, unsafe rules)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  An unsafe rule is incomplete or introduces variables in subgoals,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  and is tried only when the safe rules are not applicable.  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val empty_pack = Pack([],[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
fun (Pack(safes,unsafes)) add_safes ths   = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    Pack(sort less (ths@safes), unsafes);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
fun (Pack(safes,unsafes)) add_unsafes ths = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
    Pack(safes, sort less (ths@unsafes));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
(*The rules of LK*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
val prop_pack = empty_pack add_safes 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
	        [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
		 notL, notR, iffL, iffR];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
val LK_pack = prop_pack add_safes   [allR, exL] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
			add_unsafes [allL_thin, exR_thin];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
val LK_dup_pack = prop_pack add_safes   [allR, exL] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
			    add_unsafes [allL, exR];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
(*Returns the list of all formulas in the sequent*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
fun forms_of_seq (Const("Seqof",_) $ P $ u) = P :: forms_of_seq u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
  | forms_of_seq (H $ u) = forms_of_seq u
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
  | forms_of_seq _ = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
(*Tests whether two sequences (left or right sides) could be resolved.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
  Assumes each formula in seqc is surrounded by sequence variables
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
  -- checks that each concl formula looks like some subgoal formula.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
  It SHOULD check order as well, using recursion rather than forall/exists*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
fun could_res (seqp,seqc) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
                              (forms_of_seq seqp))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
             (forms_of_seq seqc);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
fun could_resolve_seq (prem,conc) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
  case (prem,conc) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
	  could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
    | _ => false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
(*Like filt_resolve_tac, using could_resolve_seq
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
  Much faster than resolve_tac when there are many rules.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
  in  if length rls > maxr  then  no_tac  else resolve_tac rls i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
  end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
(*Predicate: does the rule have n premises? *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
fun has_prems n rule =  (nprems_of rule = n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(*Continuation-style tactical for resolution.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
  The list of rules is partitioned into 0, 1, 2 premises.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
  The resulting tactic, gtac, tries to resolve with rules.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
  If successful, it recursively applies nextac to the new subgoals only.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
  Else fails.  (Treatment of goals due to Ph. de Groote) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
  Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
(*Takes rule lists separated in to 0, 1, 2, >2 premises.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
  The abstraction over state prevents needless divergence in recursion.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
  The 9999 should be a parameter, to delay treatment of flexible goals. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
fun RESOLVE_THEN rules =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
  let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
      fun tac nextac i = STATE (fn state =>  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
	  filseq_resolve_tac rls0 9999 i 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
	  ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
	  ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
					THEN  TRY(nextac i)) )
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
  in  tac  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*repeated resolution applied to the designated goal*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
fun reresolve_tac rules = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
      fun gtac i = restac gtac i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
  in  gtac  end; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
(*tries the safe rules repeatedly before the unsafe rules. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
fun repeat_goal_tac (Pack(safes,unsafes)) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
  let val restac  =    RESOLVE_THEN safes
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
      and lastrestac = RESOLVE_THEN unsafes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
      fun gtac i = restac gtac i  ORELSE  lastrestac gtac i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
  in  gtac  end; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
(*Tries safe rules only*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
fun step_tac (thm_pack as Pack(safes,unsafes)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    safe_goal_tac thm_pack  ORELSE'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
    filseq_resolve_tac unsafes 9999;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
(* Tactic for reducing a goal, using Predicate Calculus rules.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
   A decision procedure for Propositional Calculus, it is incomplete
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
   for Predicate-Calculus because of allL_thin and exR_thin.  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
   Fails if it can do nothing.      *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
(*The following two tactics are analogous to those provided by 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
  Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
fun fast_tac thm_pack =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
fun best_tac thm_pack  = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
	       (step_tac thm_pack 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
(** Contraction.  Useful since some rules are not complete. **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
val conR = prove_goal LK.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
val conL = prove_goal LK.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
open LK_Resolve;