src/FOLP/classical.ML
changeset 1459 d12da312eff4
parent 469 b571d997178d
child 4440 9ed4098074bc
     1.1 --- a/src/FOLP/classical.ML	Mon Jan 29 13:56:41 1996 +0100
     1.2 +++ b/src/FOLP/classical.ML	Mon Jan 29 13:58:15 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	FOLP/classical
     1.5 +(*  Title:      FOLP/classical
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  Like Provers/classical but modified because match_tac is unsuitable for
    1.12 @@ -19,10 +19,10 @@
    1.13  
    1.14  signature CLASSICAL_DATA =
    1.15    sig
    1.16 -  val mp: thm    		(* [| P-->Q;  P |] ==> Q *)
    1.17 -  val not_elim: thm		(* [| ~P;  P |] ==> R *)
    1.18 -  val swap: thm			(* ~P ==> (~Q ==> P) ==> Q *)
    1.19 -  val sizef : thm -> int	(* size function for BEST_FIRST *)
    1.20 +  val mp: thm                   (* [| P-->Q;  P |] ==> Q *)
    1.21 +  val not_elim: thm             (* [| ~P;  P |] ==> R *)
    1.22 +  val swap: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    1.23 +  val sizef : thm -> int        (* size function for BEST_FIRST *)
    1.24    val hyp_subst_tacs: (int -> tactic) list
    1.25    end;
    1.26  
    1.27 @@ -71,7 +71,7 @@
    1.28  val imp_elim = make_elim mp;
    1.29  
    1.30  (*Solve goal that assumes both P and ~P. *)
    1.31 -val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
    1.32 +val contr_tac = etac not_elim THEN'  assume_tac;
    1.33  
    1.34  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    1.35  fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
    1.36 @@ -94,13 +94,13 @@
    1.37  
    1.38  datatype claset =
    1.39   CS of {safeIs: thm list,
    1.40 -	safeEs: thm list,
    1.41 -	hazIs: thm list,
    1.42 -	hazEs: thm list,
    1.43 -	(*the following are computed from the above*)
    1.44 -	safe0_brls: (bool*thm)list,
    1.45 -	safep_brls: (bool*thm)list,
    1.46 -	haz_brls: (bool*thm)list};
    1.47 +        safeEs: thm list,
    1.48 +        hazIs: thm list,
    1.49 +        hazEs: thm list,
    1.50 +        (*the following are computed from the above*)
    1.51 +        safe0_brls: (bool*thm)list,
    1.52 +        safep_brls: (bool*thm)list,
    1.53 +        haz_brls: (bool*thm)list};
    1.54    
    1.55  fun rep_claset (CS x) = x;
    1.56  
    1.57 @@ -115,8 +115,8 @@
    1.58            partition (apl(0,op=) o subgoals_of_brl) 
    1.59               (sort lessb (joinrules(safeIs, safeEs)))
    1.60    in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
    1.61 -	safe0_brls=safe0_brls, safep_brls=safep_brls,
    1.62 -	haz_brls = sort lessb (joinrules(hazIs, hazEs))}
    1.63 +        safe0_brls=safe0_brls, safep_brls=safep_brls,
    1.64 +        haz_brls = sort lessb (joinrules(hazIs, hazEs))}
    1.65    end;
    1.66  
    1.67  (*** Manipulation of clasets ***)
    1.68 @@ -151,10 +151,10 @@
    1.69  (*Attack subgoals using safe inferences*)
    1.70  fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
    1.71    FIRST' [uniq_assume_tac,
    1.72 -	  uniq_mp_tac,
    1.73 -	  biresolve_tac safe0_brls,
    1.74 -	  FIRST' hyp_subst_tacs,
    1.75 -	  biresolve_tac safep_brls] ;
    1.76 +          uniq_mp_tac,
    1.77 +          biresolve_tac safe0_brls,
    1.78 +          FIRST' hyp_subst_tacs,
    1.79 +          biresolve_tac safep_brls] ;
    1.80  
    1.81  (*Repeatedly attack subgoals using safe inferences*)
    1.82  fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));