(* Copyright (C) 2004 Konstantine Arkoudas <konstantine@alum.mit.edu>     *)
(* Licensed under the terms of the GNU GPL.                               *)

structure ProofSimplification =

(* This structure contains an implementation of first-order NDL proofs,   *)
(* an interpreter that evaluates such proofs, and all the simplification  *)
(* algorithms defined in the paper "Simplifying proofs in Fitch-style     *)
(* natural deduction systems." Experiments can be run by constructing NDL *)
(* proofs in the SML-NJ environment and then applying "simplify" to them. *)

struct

type Var = string;
type FunSymbol = string;
type PredSymbol = string;
type Name = string;

val counter = ref(0);
val makeFreshName = fn () => (counter := !counter + 1;"fv"^Int.toString(!counter));

(* Note: for simplicity, we stipulate that fresh variables are of the form "fv0", "fv1", etc. *)
(* and require that the input proof to be simplified does not contain any variables of this form. *)
(* A more proper implementation would maintain a hash table of all variables that have been *)
(* used in a given session and generate a truly fresh one. *)

datatype Term = conTerm of Name | varTerm of Var | appTerm of FunSymbol * Term list

fun printTerm(conTerm(a)) = a
  | printTerm(varTerm(x)) = x
  | printTerm(appTerm(f,terms)) = "("^f^" "^(printTerms terms)^")"
and
    printTerms([]) = ""
  | printTerms([t]) = printTerm(t)
  | printTerms(t1::t2::rest) = printTerm(t1)^" "^(printTerms (t2::rest));

fun listEq([],[],_) = true
  | listEq(x::more1,y::more2,eq) = if eq(x,y) then listEq(more1,more2,eq) else false
  | listEq(_,_,_) = false;

fun termVars(conTerm(_)) = [] 
  | termVars(varTerm(x)) = [x]
  | termVars(appTerm(f,args)) = termVarsLst(args)
and
    termVarsLst([]) = []
  | termVarsLst(t::rest) = termVars(t)@termVarsLst(rest);

fun termEq(conTerm(s1),conTerm(s2)) = (s1 = s2)
  | termEq(varTerm(s1),varTerm(s2)) = (s1 = s2)
  | termEq(appTerm(f1,terms1),appTerm(f2,terms2)) = (f1 = f2) andalso listEq(terms1,terms2,termEq)
  | termEq(_) = false;

val empty_sub = fn x:Var => varTerm(x);

fun addToSub((x,t),sub) = fn v => if x = v then t else (sub v);

fun makeSub(x,t) = addToSub((x,t),empty_sub);

fun appSubToTerm(sub,t as conTerm(_)) = t
  | appSubToTerm(sub,varTerm(x)) = sub x  
  | appSubToTerm(sub,appTerm(f,args)) = appTerm(f,map (fn a => appSubToTerm(sub,a)) args)

datatype Prop =  atom of PredSymbol * Term list
               | trueProp
               | falseProp
               | neg of Prop
               | conj of Prop * Prop 
               | disj of Prop * Prop 
               | cond of Prop * Prop 
               | biCond of Prop * Prop
               | ugen of Var * Prop 
	       | egen of Var * Prop 

fun printProp(atom(R,[])) = R
  | printProp(atom(R,terms as _::_)) = "("^R^" "^(printTerms terms)^")"
  | printProp(trueProp) = "true"
  | printProp(falseProp) = "false"
  | printProp(neg(P)) = "(not "^(printProp P)^")"
  | printProp(conj(P1,P2)) = "(and "^(printProp P1)^" "^(printProp P2)^")"
  | printProp(disj(P1,P2)) = "(or "^(printProp P1)^" "^(printProp P2)^")"
  | printProp(cond(P1,P2)) = "(if "^(printProp P1)^" "^(printProp P2)^")"
  | printProp(biCond(P1,P2)) = "(iff "^(printProp P1)^" "^(printProp P2)^")"
  | printProp(ugen(x,P)) = "(forall "^x^" "^(printProp P)^")"
  | printProp(egen(x,P)) = "(exists "^x^" "^(printProp P)^")";


fun appSubToProp(sub,atom(R,args)) = atom(R,map (fn a => appSubToTerm(sub,a)) args)
  | appSubToProp(sub,trueProp) = trueProp
  | appSubToProp(sub,falseProp) = falseProp
  | appSubToProp(sub,neg(P)) = neg(appSubToProp(sub,P))
  | appSubToProp(sub,conj(P1,P2)) = conj(appSubToProp(sub,P1),appSubToProp(sub,P2))
  | appSubToProp(sub,disj(P1,P2)) = disj(appSubToProp(sub,P1),appSubToProp(sub,P2))
  | appSubToProp(sub,cond(P1,P2)) = cond(appSubToProp(sub,P1),appSubToProp(sub,P2))
  | appSubToProp(sub,biCond(P1,P2)) = biCond(appSubToProp(sub,P1),appSubToProp(sub,P2))
  | appSubToProp(sub,ugen(x,P)) = ugen(x,appSubToProp(addToSub((x,varTerm(x)),sub),P))
  | appSubToProp(sub,egen(x,P)) = egen(x,appSubToProp(addToSub((x,varTerm(x)),sub),P));

fun renameProp(neg(P)) = neg(renameProp(P))
  | renameProp(conj(P1,P2)) = conj(renameProp(P1),renameProp(P2))
  | renameProp(disj(P1,P2)) = disj(renameProp(P1),renameProp(P2))
  | renameProp(cond(P1,P2)) = cond(renameProp(P1),renameProp(P2))
  | renameProp(biCond(P1,P2)) = biCond(renameProp(P1),renameProp(P2))
  | renameProp(ugen(x,P)) = let val z = makeFreshName()
			    in 
			      ugen(z,renameProp(appSubToProp(makeSub(x,varTerm(z)),P)))
		            end
  | renameProp(egen(x,P)) = let val z = makeFreshName()
			    in 
			      egen(z,renameProp(appSubToProp(makeSub(x,varTerm(z)),P)))
		            end
  | renameProp(P) = P

fun safeAppSubToProp(sub,P) = appSubToProp(sub,renameProp(P));

(* Alphabetic equality on propositions: *)

fun alEq(atom(R1,args1),atom(R2,args2)) = (R1 = R2) andalso listEq(args1,args2,termEq)
  | alEq(trueProp,trueProp) = true
  | alEq(falseProp,falseProp) = true
  | alEq(neg(P1),neg(P2)) = alEq(P1,P2)
  | alEq(conj(P1,P2),conj(Q1,Q2)) = alEq(P1,Q1) andalso alEq(P2,Q2)
  | alEq(disj(P1,P2),disj(Q1,Q2)) = alEq(P1,Q1) andalso alEq(P2,Q2)
  | alEq(cond(P1,P2),cond(Q1,Q2)) = alEq(P1,Q1) andalso alEq(P2,Q2)
  | alEq(biCond(P1,P2),biCond(Q1,Q2)) = alEq(P1,Q1) andalso alEq(P2,Q2)
  | alEq(ugen(x,P),ugen(y,Q)) = let val z = varTerm(makeFreshName())
 				in
				   alEq(safeAppSubToProp(makeSub(x,z),P),
					safeAppSubToProp(makeSub(y,z),Q))
				end
  | alEq(egen(x,P),egen(y,Q)) = let val z = varTerm(makeFreshName())
 				in
				   alEq(safeAppSubToProp(makeSub(x,z),P),
					safeAppSubToProp(makeSub(y,z),Q))
				end
  | alEq(_) = false;


fun remove(x,L,eq) = List.filter (fn y => not(eq(x,y))) L;

fun removeDuplicates([],_) = []
  | removeDuplicates (x::rest,eq) = x::removeDuplicates(remove(x,rest,eq),eq);

fun freeVars(P:Prop) = 
  let fun f(atom(_,args)) = termVarsLst(args)
         | f(neg(P)) = f(P)
         | f(conj(P1,P2)) = f(P1)@f(P2)
         | f(disj(P1,P2)) = f(P1)@f(P2)
         | f(cond(P1,P2)) = f(P1)@f(P2)
         | f(biCond(P1,P2)) = f(P1)@f(P2)
         | f(ugen(x,P)) = remove(x,f(P),op=)
         | f(egen(x,P)) = remove(x,f(P),op=)
         | f(_) = []
   in
      removeDuplicates(f(P),op=)
   end;

datatype prim_rule = claim | dn | mp | both | leftAnd | rightAnd | cases 
                     | leftEither | rightEither | equiv | leftIff | rightIff 
                     | absurd | trueIntro | condRule | negRule;

datatype proof = ruleApp of prim_rule * Prop list 
               | assumeProof of Prop * proof * bool
               | supAbProof of Prop * proof * bool
               | compProof of proof * proof
	       | pickAnyProof of Var * proof * bool
               | pickWitnessProof of Var * Prop * proof * bool
               | specializeProof of Prop * Term
               | exGenProof of Prop * Term
	       | gen of Var * Prop;

fun ruleName(claim) = "claim"
  | ruleName(dn) = "double-negation"
  | ruleName(mp) = "modus-ponens"
  | ruleName(both) = "both"
  | ruleName(leftAnd) = "left-and"
  | ruleName(rightAnd) = "right-and"
  | ruleName(cases) = "cases"
  | ruleName(leftEither) = "left-either"
  | ruleName(rightEither) = "right-either"
  | ruleName(equiv) = "equiv"
  | ruleName(leftIff) = "left-iff"
  | ruleName(rightIff) = "right-iff"
  | ruleName(absurd) = "absurd"
  | ruleName(trueIntro) = "true-intro"
  | ruleName(condRule) = "cond"
  | ruleName(negRule) = "neg";

fun printProps([],_) = ""
  | printProps([P],f) = f(P)
  | printProps(P1::P2::rest,f) = f(P1)^", "^(printProps(P2::rest,f));

fun printRuleApp(r,args,printProp) = ruleName(r)^" "^(printProps(args,printProp))

fun printProof(D,printProp) = 
  let fun f(D as ruleApp(r,args)) = printRuleApp(r,args,printProp)
        | f(assumeProof(P,D,_)) = "(assume "^(printProp P)^" in "^(f D)^")"
        | f(supAbProof(P,D,_)) = "(suppose-absurd "^(printProp P)^" in "^(f D)^")"
  	| f(compProof(D1,D2)) = "begin "^(f D1)^"; "^f(D2)^" end"
        | f(pickAnyProof(x,D,_)) = "pick-any "^x^" in "^(f D)
        | f(pickWitnessProof(x,P,D,_)) = "pick-witness "^x^" for "^(printProp P)^" in "^(f D)
	| f(specializeProof(P,t)) = "specialize "^(printProp P)^" with "^(printTerm t)
	| f(exGenProof(P,t)) = "ex-generalize "^(printProp P)^" from "^(printTerm t)
  in
    (f D)
  end;

fun desugar(gen(x,P)) = pickAnyProof(x,ruleApp(claim,[P]),false)
  | desugar(D) = D;

exception IllFormedProof;
exception EvalError;

fun illFormed() = raise IllFormedProof;

fun evError(str) = (print("\n"^str^"\n");raise EvalError);

fun size(assumeProof(_,D,_)) = 1 + size(D)
  | size(supAbProof(_,D,_)) = 1 + size(D)
  | size(compProof(D1,D2)) = size(D1) + size(D2)
  | size(pickAnyProof(_,D,_)) = 1 + size(D)
  | size(pickWitnessProof(_,_,D,_)) = 1 + size(D)
  | size(_) = 1

fun appSubToProof(sub,ruleApp(rule,args)) = ruleApp(rule,map (fn P => safeAppSubToProp(sub,P)) args)
  | appSubToProof(sub,assumeProof(H,D,b)) = assumeProof(safeAppSubToProp(sub,H),appSubToProof(sub,D),b)
  | appSubToProof(sub,supAbProof(H,D,b)) =  supAbProof(safeAppSubToProp(sub,H),appSubToProof(sub,D),b)
  | appSubToProof(sub,compProof(D1,D2)) = compProof(appSubToProof(sub,D1),appSubToProof(sub,D2))
  | appSubToProof(sub,specializeProof(P,t)) = specializeProof(appSubToProp(sub,P),appSubToTerm(sub,t))
  | appSubToProof(sub,exGenProof(P,t)) = exGenProof(appSubToProp(sub,P),appSubToTerm(sub,t))
  | appSubToProof(sub,pickAnyProof(x,D,b)) = pickAnyProof(x,appSubToProof(addToSub((x,varTerm(x)),sub),D),b)
  | appSubToProof(sub,pickWitnessProof(x,P,D,b)) = 
      pickWitnessProof(x,safeAppSubToProp(sub,P),appSubToProof(addToSub((x,varTerm(x)),sub),D),b)
  | appSubToProof(sub,D as gen(_)) = appSubToProof(sub,desugar(D));

fun renameProof(assumeProof(H,D,b)) = assumeProof(H,renameProof(D),b)
  | renameProof(supAbProof(H,D,b)) = supAbProof(H,renameProof(D),b)
  | renameProof(compProof(D1,D2)) = compProof(renameProof(D1),renameProof(D2))
  | renameProof(ugproof as pickAnyProof(x,D,b)) = 
	let val z =  makeFreshName()
	    val sub_res = appSubToProof(makeSub(x,varTerm(z)),D)
	in
          pickAnyProof(z,renameProof sub_res,b)
	end
  | renameProof(pickWitnessProof(x,P,D,b)) = 
	let val z =  makeFreshName()
	in
            pickWitnessProof(z,P,renameProof(appSubToProof(makeSub(x,varTerm(z)),D)),b)
        end
  | renameProof(D as gen(_)) = renameProof(desugar(D))
  | renameProof(D) = D;

fun safeAppSubToProof(sub,D) = appSubToProof(sub,renameProof(D));

fun eigenVariant(assumeProof(H1,D1,_),assumeProof(H2,D2,_)) = alEq(H1,H2) andalso eigenVariant(D1,D2)
  | eigenVariant(supAbProof(H1,D1,_),supAbProof(H2,D2,_)) = alEq(H1,H2) andalso eigenVariant(D1,D2)
  | eigenVariant(compProof(D1,D2),compProof(D1',D2')) = eigenVariant(D1,D1') andalso eigenVariant(D2,D2')
  | eigenVariant(pickAnyProof(x,D1,_),pickAnyProof(y,D2,_)) = 
       let val z = varTerm(makeFreshName())
       in
	   eigenVariant(appSubToProof(makeSub(x,z),D1),appSubToProof(makeSub(y,z),D2))
       end
  | eigenVariant(pickWitnessProof(x,P1,D1,_),pickWitnessProof(y,P2,D2,_)) = 
       let val z = varTerm(makeFreshName())
       in
	  alEq(P1,P2) andalso eigenVariant(appSubToProof(makeSub(x,z),D1),appSubToProof(makeSub(y,z),D2))
       end
  | eigenVariant(specializeProof(P1,t1),specializeProof(P2,t2)) = 
	 alEq(P1,P2) andalso termEq(t1,t2)
  | eigenVariant(exGenProof(P1,t1),specializeProof(P2,t2)) = 
	 alEq(P1,P2) andalso termEq(t1,t2)
  | eigenVariant(ruleApp(R1,args1),ruleApp(R2,args2)) = (R1 = R2) andalso listEq(args1,args2,alEq)
  | eigenVariant(D1 as gen(_),D2 as gen(_)) = eigenVariant(desugar(D1),desugar(D2))
  | eigenVariant(_) = false;

fun fp f = fn D => let val D' = f D
                    in
                       if eigenVariant(D,D') then D else fp f D'
                    end;

fun weave f [] = f
  | weave f (g::rest) = f o g o (weave f rest);

fun member(x,L,eq) = List.exists (fn a => eq(a,x)) L;

fun members(L1,L2,eq) = List.all (fn x => member(x,L2,eq)) L1;

fun emptyIntersection(L1,L2,eq) = not (List.exists (fn x => member(x,L2,eq)) L1);

fun freeVarsLst(L) = 
  let fun loop([],res) = res
        | loop(P::more,res) = loop(more,op@(freeVars(P),res))
  in
    removeDuplicates(loop(L,[]),op=)
   end

fun getThreadElements(compProof(D1,D2)) = D1::getThreadElements(D2)
  | getThreadElements(D) = [D];

fun makeThread([D]) = D
  | makeThread(D::rest) = compProof(D,makeThread(rest))
 
fun isClaim(ruleApp(claim,_)) = true
  | isClaim(_) = false

fun ruleConcl(claim,[P]) = P
  | ruleConcl(dn,[neg(neg(P))]) = P
  | ruleConcl(condRule,[P,Q]) = cond(P,Q)
  | ruleConcl(negRule,[P]) = neg(P)
  | ruleConcl(mp,[cond(P1,P2),P3]) = if alEq(P1,P3) then P2 else illFormed()
  | ruleConcl(both,[P1,P2]) = conj(P1,P2)
  | ruleConcl(leftAnd,[conj(P1,P2)]) = P1
  | ruleConcl(rightAnd,[conj(P1,P2)]) = P2
  | ruleConcl(equiv,[cond(P1,P2),cond(P3,P4)]) = 
      if alEq(P1,P4) andalso alEq(P2,P3) then biCond(P1,P2) else illFormed()
  | ruleConcl(leftIff,[biCond(P,Q)]) = cond(P,Q)
  | ruleConcl(rightIff,[biCond(P,Q)]) = cond(Q,P)
  | ruleConcl(leftEither,[P,Q]) = disj(P,Q)
  | ruleConcl(rightEither,[P,Q]) = disj(P,Q)
  | ruleConcl(cases,[disj(P1,P2),cond(P3,Q),cond(P4,Q')]) = 
     if alEq(P1,P3) andalso alEq(P2,P4) andalso Q = Q' then Q else illFormed()
  | ruleConcl(absurd,[P1,neg(P2)]) = if alEq(P1,P2) then falseProp else illFormed()
  | ruleConcl(trueIntro,[]) = trueProp
  | ruleConcl(_) = illFormed();

fun concl(ruleApp(M,args)) = ruleConcl(M,args)
  | concl(assumeProof(P,D,_)) = cond(P,concl(D))
  | concl(supAbProof(P,D,_)) = neg(P)
  | concl(compProof(_,D2)) = concl(D2)
  | concl(pickAnyProof(x,D,_)) = ugen(x,concl(D))
  | concl(pickWitnessProof(w,P,D,_)) = concl(D)
  | concl(specializeProof(ugen(x,P),t)) = safeAppSubToProp(makeSub(x,t),P)
  | concl(exGenProof(Q as egen(x,P),_)) = Q
  | concl(D as gen(_)) = concl(desugar(D));
                                          
exception OAException of string;

fun OAError(str) = raise OAException(str);
  
fun oa D = 
 let fun h(ruleApp(leftEither,[P1,_])) = [P1]
       | h(ruleApp(rightEither,[_,P2])) = [P2]
       | h(ruleApp(condRule,[_,P])) = [P]
       | h(ruleApp(M,args)) = args 
       | h(assumeProof(P,D,_)) = remove(P,h D,alEq)
       | h(supAbProof(P,D,_)) = remove(P,h D,alEq)
       | h(compProof(D1,D2)) = h(D1)@(remove(concl D1,h D2,alEq))
       | h(specializeProof(P,_)) = [P]
       | h(exGenProof(egen(x,P),t)) = [safeAppSubToProp(makeSub(x,t),P)]
       | h(pickAnyProof(x,D,_)) = let val O = oa D 
				  in
				    if member(x,freeVarsLst O,op=) then 
				       OAError("\nFree variable error in pick-any.\n")
				    else O
 				  end
       | h(pickWitnessProof(x,W as egen(y,P),D,_)) = 
			let val O = oa D
			    val O' = remove(safeAppSubToProp(makeSub(y,varTerm(x)),P),O,alEq)
		        in		
		            if member(x,freeVarsLst O',op=) then 
		  	       OAError("\nFree variable error in pick-witness.\n")
			    else
			       W::O'
			end
 in            
   removeDuplicates(h D,alEq)
 end;

fun ov(D) = removeDuplicates(freeVarsLst(oa(D))@freeVars(concl(D)),op=);

fun evalRuleApp(r,args,oa,ab) = 
   if not(members(oa,ab,alEq)) then evError("Invalid rule application.")  else ruleConcl(r,args);

fun eval(D as ruleApp(r,args)) = (fn ab => evalRuleApp(r,args,oa D,ab))
  | eval(assumeProof(P,D',_))  = (fn ab => cond(P,eval D' (P::ab)))
  | eval(supAbProof(P,D',_))   = (fn ab => (case (eval D' (P::ab)) of
					       falseProp => neg(P)
					     | _ => evError("Invalid proof by contradiction.")))
  | eval(compProof(D1,D2))     = (fn ab => eval D2 ((eval D1 ab)::ab))
  | eval(specializeProof(U as ugen(x,P),t)) = 
	(fn ab => if member(U,ab,alEq) then safeAppSubToProp(makeSub(x,t),P) 
		  else evError("Invalid universal specialization."))
  | eval(exGenProof(E as egen(x,P),t)) = 
        (fn ab => if member(safeAppSubToProp(makeSub(x,t),P),ab,alEq) then E 
		  else evError("Invalid existential generalization."))
  | eval(pickAnyProof(x,D,_)) = 
	(fn ab => let val z = makeFreshName()
 		  in
		    ugen(z,eval (safeAppSubToProof(makeSub(x,varTerm(z)),D)) ab)
		  end)
  | eval(pickWitnessProof(w,E as egen(x,P),D,_)) =
	(fn ab => if member(E,ab,alEq) then
	  	     let val z = makeFreshName()
		         val G = eval (safeAppSubToProof(makeSub(w,varTerm z),D)) 
			 	      ((safeAppSubToProp(makeSub(x,varTerm z),P))::ab)
 		     in
		        if member(z,freeVars G,op=) then 
			   evError("Invalid existential instantiation; witness variable free in conclusion.")
		        else G
 		    end
		    else evError("Invalid existential instantiation; witness premise not in a.b."))
  | eval(D as gen(_)) = eval(desugar(D))
		    

fun makeStrict(assumeProof(P,D,mark)) = assumeProof(P,makeStrict(D),mark)
  | makeStrict(supAbProof(P,D,mark)) = supAbProof(P,makeStrict(D),mark)
  | makeStrict(compProof(D1,D2)) = 
     let val D1' = makeStrict(D1)
         val D2' = makeStrict(D2)
     in 
        if member(concl D1',oa D2',alEq) then compProof(D1',D2') else D2'
     end
  | makeStrict(pickAnyProof(x,D,mark)) = pickAnyProof(x,makeStrict(D),mark)
  | makeStrict(pickWitnessProof(w,E as egen(x,P),D,mark)) = 
        let val D' = makeStrict(D)
	in
	   if member(safeAppSubToProp(makeSub(x,varTerm(w)),P),oa D',alEq) then
	      pickWitnessProof(w,E,D',mark) 
	   else D'
        end
  | makeStrict(D) = D;

 fun removeRepetitions(D) = 
 let fun RR(D,L) = 
        let val P = concl(D)
        in
           if member(P,L,alEq) then ruleApp(claim,[P])
           else
              case D of
                 assumeProof(hyp,D_b,mark) => assumeProof(hyp,RR(D_b,hyp::L),mark)
               | supAbProof(hyp,D_b,mark) => supAbProof(hyp,RR(D_b,hyp::L),mark)
               | compProof(D1,D2) => let val D1' = RR(D1,L)
                                          in
                                             compProof(D1',RR(D2,concl(D1')::L))
                                          end
	       | pickAnyProof(x,D',mark) => pickAnyProof(x,RR(D',L),mark)
	       | pickWitnessProof(w,E as egen(x,P),D',mark) =>
		   pickWitnessProof(w,E,RR(D',(safeAppSubToProp(makeSub(x,varTerm(w)),P))::L),mark)
               | _ => D
        end 
 in
    RR(D,[])
 end;

fun elimClaims(assumeProof(P,D_b,mark)) = assumeProof(P,elimClaims(D_b),mark)
  | elimClaims(supAbProof(P,D_b,mark)) = supAbProof(P,elimClaims(D_b),mark)
  | elimClaims(compProof(D1,D2)) = 
      let val (D1',D2') = (elimClaims(D1),elimClaims(D2))
          val comp = compProof(D1',D2')
      in
         (case D1' of
             ruleApp(claim,_) => D2'
           | _ => (case D2' of 
                     ruleApp(claim,_) => 
                       if alEq(concl(D1'),concl(D2')) then D1' else comp
                   | _ => comp))
      end
  | elimClaims(pickAnyProof(x,D,mark)) = pickAnyProof(x,elimClaims(D),mark)
  | elimClaims(pickWitnessProof(x,P,D,mark)) = pickWitnessProof(x,P,elimClaims(D),mark)
  | elimClaims(D) = D;

val contract = fp (elimClaims o removeRepetitions o makeStrict);

fun H(compProof(D1,D2),L,V) = 
             let val (D1',L1,Delta1) = H(D1,L,V)
                 val (D2',L2,Delta2) = H(D2,L1,V)
             in
                (compProof(D1',D2'),L2,Delta1 @ Delta2)
             end
  | H(D,L,V) = let val C = concl(D)
               in  
                 if emptyIntersection(oa(D),L,alEq) andalso emptyIntersection(ov(D),V,op=) then
                    (ruleApp(claim,[C]),L,[D])
                 else
                    (D,C::L,[])
               end;

val maximizeScope = 
 let val rightLinearize = 
           let fun rl(assumeProof(P,D,b)) = assumeProof(P,rl(D),b)
                 | rl(supAbProof(P,D,b)) = supAbProof(P,rl(D),b)
                 | rl(compProof(D_l,D_r)) = 
                      (case D_l of
                          compProof(D1,D2) => rl(compProof(D1,compProof(D2,D_r)))
                        | _ => compProof(rl(D_l),rl(D_r)))
		 | rl(pickAnyProof(x,D,b)) = pickAnyProof(x,rl(D),b)
		 | rl(pickWitnessProof(w,P,D,b)) = pickWitnessProof(w,P,rl(D),b)
                 | rl(D) = D
           in
             rl
           end
     fun allMarked(assumeProof(_,D,mark)) = mark andalso allMarked(D)
       | allMarked(supAbProof(_,D,mark)) =  mark andalso allMarked(D)
       | allMarked(pickAnyProof(_,D,mark)) = mark andalso allMarked(D)
       | allMarked(pickWitnessProof(_,_,D,mark)) = mark andalso allMarked(D)
       | allMarked(compProof(D1,D2)) = allMarked(D1) andalso allMarked(D2)
       | allMarked(_) = true
     fun hoist(assumeProof(P,D_b,mark as false)) =
           if allMarked(D_b) then
              let val (D_b',_,Delta) = H(D_b,[P],[])
              in
                if not(null(Delta)) andalso alEq(concl(makeThread(Delta)),concl(D_b'))
                then makeThread(Delta@[ruleApp(condRule,[P,concl(D_b')])])
                else
                   makeThread(Delta@[assumeProof(P,D_b',true)])
              end
           else
              assumeProof(P,hoist(D_b),mark)
       | hoist(supAbProof(P,D_b,mark as false)) =     
           if allMarked(D_b) then
              let val (D_b',_,Delta) = H(D_b,[P],[])
              in
                if not(null(Delta)) andalso alEq(concl(makeThread(Delta)),concl(D_b'))
                then makeThread(Delta@[ruleApp(negRule,[P])])
                else
                   makeThread(Delta@[supAbProof(P,D_b',true)])
              end
           else
              supAbProof(P,hoist(D_b),mark)
       | hoist(pickAnyProof(x,D_b,mark as false)) = 
          if allMarked(D_b) then
	     let val (D_b',_,Delta) = H(D_b,[],[x])
	     in
		makeThread(Delta@[pickAnyProof(x,D_b',true)])
	     end
	  else
	     pickAnyProof(x,hoist(D_b),mark)
       | hoist(pickWitnessProof(w,P,D_b,mark as false)) = 
          if allMarked(D_b) then
	     let val (D_b',_,Delta) = H(D_b,[],[w])
	     in
		makeThread(Delta@[pickWitnessProof(w,P,D_b',true)])
	     end
	  else
	     pickWitnessProof(w,P,hoist(D_b),mark)
       | hoist(compProof(D1,D2)) = compProof(hoist(D1),hoist(D2))
       | hoist(D) = D
 in
    (fp (rightLinearize o hoist)) o rightLinearize 
 end;

fun A(D) = 
  let fun T(assumeProof(P,D_b,mark),L) = 
            if member(P,L,alEq) then 
               let val D_b' = T(D_b,L)
               in
                  compProof(D_b',ruleApp(condRule,[P,concl D_b']))
               end
            else
               assumeProof(P,T(D_b,P::L),mark)
        | T(supAbProof(P,D_b,mark),L) = 
            if member(P,L,alEq) then 
               let val D_b' = T(D_b,L)
               in
                 compProof(D_b',ruleApp(negRule,[P]))
               end
            else
               supAbProof(P,T(D_b,P::L),mark)
        | T(compProof(D1,D2),L) = 
              let val D1' = T(D1,L)
              in
                compProof(D1',T(D2,(concl D1')::L))
              end
	| T(pickAnyProof(x,D,mark),L) = pickAnyProof(x,T(D,L),mark)
	| T(pickWitnessProof(w,E as egen(x,P),D,mark),L) = 
	      pickWitnessProof(w,E,T(D,(safeAppSubToProp(makeSub(x,varTerm(w)),P))::L),mark)
        | T(D,_) = D
  in
     T(D,oa(D))
  end;

fun A3(assumeProof(P,D,mark)) = assumeProof(P,A3(D),mark)
  | A3(supAbProof(P,D,mark)) = supAbProof(P,A3(D),mark)
  | A3(compProof(assumeProof(P,D_b,mark),D)) = 
        let val (D_b',D') = (A3(D_b),A3(D))
            val (D'',_,Delta) = H(D',[cond(P,concl D_b')],[])
        in
          if member(P,map concl (getThreadElements D),alEq)
          then 
             (if not(null(Delta)) andalso alEq(concl(makeThread(Delta)),concl(D''))
              then makeThread(Delta)
              else 
                 makeThread(Delta@[assumeProof(P,D_b',mark),D'']))
          else 
              compProof(assumeProof(P,D_b',mark),D')
        end
  | A3(compProof(supAbProof(P,D_b,mark),D)) = 
        let val (D_b',D') = (A3(D_b),A3(D))
            val (D'',_,Delta) = H(D',[neg(P)],[])
        in
           if member(P,map concl (getThreadElements D),alEq)
           then 
               (if not(null(Delta)) andalso alEq(concl(makeThread(Delta)),concl(D''))
                then makeThread(Delta)
                else
                   makeThread(Delta@[supAbProof(P,D_b',mark),D'']))
           else
               compProof(supAbProof(P,D_b',mark),D')
        end
  | A3(compProof(D1,D2)) = compProof(A3(D1),A3(D2))
  | A3(pickAnyProof(x,D,mark)) = pickAnyProof(x,A3(D),mark)
  | A3(pickWitnessProof(w,P,D,mark)) = pickWitnessProof(w,P,A3(D),mark)
  | A3(D) = D;

val restructure =  weave maximizeScope [A,A3];

val simplify = contract o restructure;

end; (* of structure Simplify *)