src/FOLP/classical.ML
changeset 0 a5a9c433f639
child 469 b571d997178d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOLP/classical.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,191 @@
     1.4 +(*  Title: 	FOLP/classical
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Like Provers/classical but modified because match_tac is unsuitable for
    1.10 +proof objects.
    1.11 +
    1.12 +Theorem prover for classical reasoning, including predicate calculus, set
    1.13 +theory, etc.
    1.14 +
    1.15 +Rules must be classified as intr, elim, safe, hazardous.
    1.16 +
    1.17 +A rule is unsafe unless it can be applied blindly without harmful results.
    1.18 +For a rule to be safe, its premises and conclusion should be logically
    1.19 +equivalent.  There should be no variables in the premises that are not in
    1.20 +the conclusion.
    1.21 +*)
    1.22 +
    1.23 +signature CLASSICAL_DATA =
    1.24 +  sig
    1.25 +  val mp: thm    		(* [| P-->Q;  P |] ==> Q *)
    1.26 +  val not_elim: thm		(* [| ~P;  P |] ==> R *)
    1.27 +  val swap: thm			(* ~P ==> (~Q ==> P) ==> Q *)
    1.28 +  val sizef : thm -> int	(* size function for BEST_FIRST *)
    1.29 +  val hyp_subst_tacs: (int -> tactic) list
    1.30 +  end;
    1.31 +
    1.32 +(*Higher precedence than := facilitates use of references*)
    1.33 +infix 4 addSIs addSEs addSDs addIs addEs addDs;
    1.34 +
    1.35 +
    1.36 +signature CLASSICAL =
    1.37 +  sig
    1.38 +  type claset
    1.39 +  val empty_cs: claset
    1.40 +  val addDs : claset * thm list -> claset
    1.41 +  val addEs : claset * thm list -> claset
    1.42 +  val addIs : claset * thm list -> claset
    1.43 +  val addSDs: claset * thm list -> claset
    1.44 +  val addSEs: claset * thm list -> claset
    1.45 +  val addSIs: claset * thm list -> claset
    1.46 +  val print_cs: claset -> unit
    1.47 +  val rep_claset: claset -> 
    1.48 +      {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
    1.49 +       safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
    1.50 +       haz_brls: (bool*thm)list}
    1.51 +  val best_tac : claset -> int -> tactic
    1.52 +  val chain_tac : int -> tactic
    1.53 +  val contr_tac : int -> tactic
    1.54 +  val fast_tac : claset -> int -> tactic
    1.55 +  val inst_step_tac : int -> tactic
    1.56 +  val joinrules : thm list * thm list -> (bool * thm) list
    1.57 +  val mp_tac: int -> tactic
    1.58 +  val safe_tac : claset -> tactic
    1.59 +  val safe_step_tac : claset -> int -> tactic
    1.60 +  val slow_step_tac : claset -> int -> tactic
    1.61 +  val step_tac : claset -> int -> tactic
    1.62 +  val swapify : thm list -> thm list
    1.63 +  val swap_res_tac : thm list -> int -> tactic
    1.64 +  val uniq_mp_tac: int -> tactic
    1.65 +  end;
    1.66 +
    1.67 +
    1.68 +functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
    1.69 +struct
    1.70 +
    1.71 +local open Data in
    1.72 +
    1.73 +(** Useful tactics for classical reasoning **)
    1.74 +
    1.75 +val imp_elim = make_elim mp;
    1.76 +
    1.77 +(*Solve goal that assumes both P and ~P. *)
    1.78 +val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
    1.79 +
    1.80 +(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    1.81 +fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
    1.82 +
    1.83 +(*Like mp_tac but instantiates no variables*)
    1.84 +fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    1.85 +
    1.86 +(*Creates rules to eliminate ~A, from rules to introduce A*)
    1.87 +fun swapify intrs = intrs RLN (2, [swap]);
    1.88 +
    1.89 +(*Uses introduction rules in the normal way, or on negated assumptions,
    1.90 +  trying rules in order. *)
    1.91 +fun swap_res_tac rls = 
    1.92 +    let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
    1.93 +    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
    1.94 +    end;
    1.95 +
    1.96 +(*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)
    1.97 +fun chain_tac i =
    1.98 +    eresolve_tac [imp_elim] i  THEN
    1.99 +    (assume_tac (i+1)  ORELSE  contr_tac (i+1));
   1.100 +
   1.101 +(*** Classical rule sets ***)
   1.102 +
   1.103 +datatype claset =
   1.104 + CS of {safeIs: thm list,
   1.105 +	safeEs: thm list,
   1.106 +	hazIs: thm list,
   1.107 +	hazEs: thm list,
   1.108 +	(*the following are computed from the above*)
   1.109 +	safe0_brls: (bool*thm)list,
   1.110 +	safep_brls: (bool*thm)list,
   1.111 +	haz_brls: (bool*thm)list};
   1.112 +  
   1.113 +fun rep_claset (CS x) = x;
   1.114 +
   1.115 +(*For use with biresolve_tac.  Combines intrs with swap to catch negated
   1.116 +  assumptions.  Also pairs elims with true. *)
   1.117 +fun joinrules (intrs,elims) =  
   1.118 +  map (pair true) (elims @ swapify intrs)  @  map (pair false) intrs;
   1.119 +
   1.120 +(*Note that allE precedes exI in haz_brls*)
   1.121 +fun make_cs {safeIs,safeEs,hazIs,hazEs} =
   1.122 +  let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
   1.123 +          partition (apl(0,op=) o subgoals_of_brl) 
   1.124 +             (sort lessb (joinrules(safeIs, safeEs)))
   1.125 +  in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
   1.126 +	safe0_brls=safe0_brls, safep_brls=safep_brls,
   1.127 +	haz_brls = sort lessb (joinrules(hazIs, hazEs))}
   1.128 +  end;
   1.129 +
   1.130 +(*** Manipulation of clasets ***)
   1.131 +
   1.132 +val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
   1.133 +
   1.134 +fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   1.135 + (writeln"Introduction rules";  prths hazIs;
   1.136 +  writeln"Safe introduction rules";  prths safeIs;
   1.137 +  writeln"Elimination rules";  prths hazEs;
   1.138 +  writeln"Safe elimination rules";  prths safeEs;
   1.139 +  ());
   1.140 +
   1.141 +fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
   1.142 +  make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
   1.143 +
   1.144 +fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths =
   1.145 +  make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs};
   1.146 +
   1.147 +fun cs addSDs ths = cs addSEs (map make_elim ths);
   1.148 +
   1.149 +fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths =
   1.150 +  make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs};
   1.151 +
   1.152 +fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths =
   1.153 +  make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs};
   1.154 +
   1.155 +fun cs addDs ths = cs addEs (map make_elim ths);
   1.156 +
   1.157 +(*** Simple tactics for theorem proving ***)
   1.158 +
   1.159 +(*Attack subgoals using safe inferences*)
   1.160 +fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
   1.161 +  FIRST' [uniq_assume_tac,
   1.162 +	  uniq_mp_tac,
   1.163 +	  biresolve_tac safe0_brls,
   1.164 +	  FIRST' hyp_subst_tacs,
   1.165 +	  biresolve_tac safep_brls] ;
   1.166 +
   1.167 +(*Repeatedly attack subgoals using safe inferences*)
   1.168 +fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
   1.169 +
   1.170 +(*These steps could instantiate variables and are therefore unsafe.*)
   1.171 +val inst_step_tac = assume_tac APPEND' contr_tac;
   1.172 +
   1.173 +(*Single step for the prover.  FAILS unless it makes progress. *)
   1.174 +fun step_tac (cs as (CS{haz_brls,...})) i = 
   1.175 +  FIRST [safe_tac cs,
   1.176 +         inst_step_tac i,
   1.177 +         biresolve_tac haz_brls i];
   1.178 +
   1.179 +(*** The following tactics all fail unless they solve one goal ***)
   1.180 +
   1.181 +(*Dumb but fast*)
   1.182 +fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   1.183 +
   1.184 +(*Slower but smarter than fast_tac*)
   1.185 +fun best_tac cs = 
   1.186 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   1.187 +
   1.188 +(*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   1.189 +  allows backtracking from "safe" rules to "unsafe" rules here.*)
   1.190 +fun slow_step_tac (cs as (CS{haz_brls,...})) i = 
   1.191 +    safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
   1.192 +
   1.193 +end; 
   1.194 +end;