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