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