src/HOL/Tools/Presburger/cooper_proof.ML

   val qe_disjI : thm
   val qe_impI : thm
   val qe_eqI : thm
   val qe_exI : thm
   val qe_get_terms : thm -> term * term
-  val cooper_prv : Sign.sg -> term -> term -> string list -> thm
+  val cooper_prv : Sign.sg -> term -> term -> thm
   val proof_of_evalc : Sign.sg -> term -> thm
   val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
   val proof_of_linform : Sign.sg -> string list -> term -> thm
+  val prove_elementar : Sign.sg -> string -> term -> thm
+  val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
 end;
 
 structure CooperProof : COOPER_PROOF =
 struct
-
 open CooperDec;
 
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*---         Protocoling part                                  ---*)
-(*---                                                           ---*)
-(*---           includes the protocolling datastructure         ---*)
-(*---                                                           ---*)
-(*---          and the protocolling fuctions                    ---*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
+(*
 val presburger_ss = simpset_of (theory "Presburger")
-  addsimps [diff_int_def] delsimps [thm"diff_int_def_symmetric"];
+  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
+*)
+
+val presburger_ss = simpset_of (theory "Presburger")
+  addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
 
 (*Theorems that will be used later for the proofgeneration*)
 
 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
 val unity_coeff_ex = thm "unity_coeff_ex";
 
-(* Theorems for proving the adjustment of the coefficients*)
+(* Thorems for proving the adjustment of the coeffitients*)
 
 val ac_lt_eq =  thm "ac_lt_eq";
 val ac_eq_eq = thm "ac_eq_eq";
 val ac_dvd_eq = thm "ac_dvd_eq";
 val ac_pi_eq = thm "ac_pi_eq";

 val qe_impI = thm "qe_impI";
 val qe_eqI = thm "qe_eqI";
 val qe_exI = thm "qe_exI";
 val qe_ALLI = thm "qe_ALLI";
 
-(*Modulo D property for Pminusinf and Plusinf *)
+(*Modulo D property for Pminusinf an Plusinf *)
 val fm_modd_minf = thm "fm_modd_minf";
 val not_dvd_modd_minf = thm "not_dvd_modd_minf";
 val dvd_modd_minf = thm "dvd_modd_minf";
 
 val fm_modd_pinf = thm "fm_modd_pinf";
 val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
 val dvd_modd_pinf = thm "dvd_modd_pinf";
 
-(* the minusinfinity property*)
+(* the minusinfinity proprty*)
 
 val fm_eq_minf = thm "fm_eq_minf";
 val neq_eq_minf = thm "neq_eq_minf";
 val eq_eq_minf = thm "eq_eq_minf";
 val le_eq_minf = thm "le_eq_minf";
 val len_eq_minf = thm "len_eq_minf";
 val not_dvd_eq_minf = thm "not_dvd_eq_minf";
 val dvd_eq_minf = thm "dvd_eq_minf";
 
-(* the Plusinfinity property*)
+(* the Plusinfinity proprty*)
 
 val fm_eq_pinf = thm "fm_eq_pinf";
 val neq_eq_pinf = thm "neq_eq_pinf";
 val eq_eq_pinf = thm "eq_eq_pinf";
 val le_eq_pinf = thm "le_eq_pinf";

 
 val eq_pinf_conjI = thm "eq_pinf_conjI";
 val eq_pinf_disjI = thm "eq_pinf_disjI";
 val modd_pinf_disjI = thm "modd_pinf_disjI";
 val modd_pinf_conjI = thm "modd_pinf_conjI";
-
 
 (*Cooper Backwards...*)
 (*Bset*)
 val not_bst_p_fm = thm "not_bst_p_fm";
 val not_bst_p_ne = thm "not_bst_p_ne";

 val lf_lt = thm "lf_lt";
 val lf_eq = thm "lf_eq";
 val lf_dvd = thm "lf_dvd";
 
 
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the cooperprocedure.*)
-(* ------------------------------------------------------------------------- *)
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the adjustcoeff step.*)
-(* ------------------------------------------------------------------------- *)
-datatype CpLog = No
-                |Simp of term*CpLog
-		|Blast of CpLog*CpLog
-		|Aset of (term*term*(term list)*term)
-		|Bset of (term*term*(term list)*term)
-		|Minusinf of CpLog*CpLog
-		|Cooper of term*CpLog*CpLog*CpLog
-		|Eq_minf of term*term
-		|Modd_minf of term*term
-		|Eq_minf_conjI of CpLog*CpLog
-		|Modd_minf_conjI of CpLog*CpLog	
-		|Modd_minf_disjI of CpLog*CpLog
-		|Eq_minf_disjI of CpLog*CpLog	
-		|Not_bst_p of term*term*term*term*CpLog
-		|Not_bst_p_atomic of term
-		|Not_bst_p_conjI of CpLog*CpLog
-		|Not_bst_p_disjI of CpLog*CpLog
-		|Not_ast_p of term*term*term*term*CpLog
-		|Not_ast_p_atomic of term
-		|Not_ast_p_conjI of CpLog*CpLog
-		|Not_ast_p_disjI of CpLog*CpLog
-		|CpLogError;
-
-
-
-datatype ACLog = ACAt of int*term
-                |ACPI of int*term
-                |ACfm of term
-                |ACNeg of ACLog
-		|ACConst of string*ACLog*ACLog;
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the CNNF step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype NNFLog = NNFAt of term
-                |NNFSimp of NNFLog
-                |NNFNN of NNFLog
-		|NNFConst of string*NNFLog*NNFLog;
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the linform  step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype LfLog = LfAt of term
-                |LfAtdvd of term
-                |Lffm of term
-                |LfConst of string*LfLog*LfLog
-		|LfNot of LfLog
-		|LfQ of string*string*typ*LfLog;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the evaluation- evalc-  step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype EvalLog = EvalAt of term
-                |Evalfm of term
-		|EvalConst of string*EvalLog*EvalLog;
-
 (* ------------------------------------------------------------------------- *)
 (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
 (*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
 (*this is necessary because the theorems use this representation.*)
 (* This function should be elminated in next versions...*)

          else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   |_ => fm;
 
-
-(* ------------------------------------------------------------------------- *)
-(* Intended to tell that here we changed the structure of the formula with respect to the posineq theorem : ~(0 < t) = 0 < 1-t*)
-(* ------------------------------------------------------------------------- *)
-fun adjustcoeffeq_wp  x l fm = 
-    case fm of  
-  (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
-  if (x = y) 
-  then let  
-       val m = l div (dest_numeral c) 
-       val n = abs (m)
-       val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
-       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
-       in (ACPI(n,fm),rs)
-       end
-  else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )) 
-        in (ACPI(1,fm),rs)
-        end
-
-  |(Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
-      c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
-        let val m = l div (dest_numeral c) 
-           val n = (if p = "op <" then abs(m) else m)  
-           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
-           val rs = (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
-	   in (ACAt(n,fm),rs)
-	   end
-        else (ACfm(fm),fm) 
-  |( Const ("Not", _) $ p) => let val (rsp,rsr) = adjustcoeffeq_wp x l p 
-                              in (ACNeg(rsp),HOLogic.Not $ rsr) 
-                              end
-  |( Const ("op &",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
-                                     val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
-                                  in (ACConst ("CJ",rspp,rsqp), HOLogic.mk_conj (rspr,rsqr)) 
-                                  end 
-  |( Const ("op |",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
-                                     val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
-                                  in (ACConst ("DJ",rspp,rsqp), HOLogic.mk_disj (rspr,rsqr)) 
-                                  end
-
-  |_ => (ACfm(fm),fm);
-
-
-(*_________________________________________*)
-(*-----------------------------------------*)
-(* Protocol generation for the liform step *)
-(*_________________________________________*)
-(*-----------------------------------------*)
-
-
-fun linform_wp fm = 
-  let fun at_linform_wp at =
-    case at of
-      (Const("op <=",_)$s$t) => LfAt(at)
-      |(Const("op <",_)$s$t) => LfAt(at)
-      |(Const("op =",_)$s$t) => LfAt(at)
-      |(Const("Divides.op dvd",_)$s$t) => LfAtdvd(at)
-  in
-  if is_arith_rel fm 
-  then at_linform_wp fm 
-  else case fm of
-    (Const("Not",_) $ A) => LfNot(linform_wp A)
-   |(Const("op &",_)$ A $ B) => LfConst("CJ",linform_wp A, linform_wp B)
-   |(Const("op |",_)$ A $ B) => LfConst("DJ",linform_wp A, linform_wp B)
-   |(Const("op -->",_)$ A $ B) => LfConst("IM",linform_wp A, linform_wp B)
-   |(Const("op =",Type ("fun",[Type ("bool", []),_]))$ A $ B) => LfConst("EQ",linform_wp A, linform_wp B)
-   |Const("Ex",_)$Abs(x,T,p) => 
-     let val (xn,p1) = variant_abs(x,T,p)
-     in LfQ("Ex",xn,T,linform_wp p1)
-     end 
-   |Const("All",_)$Abs(x,T,p) => 
-     let val (xn,p1) = variant_abs(x,T,p)
-     in LfQ("All",xn,T,linform_wp p1)
-     end 
-end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*For simlified formulas we just notice the original formula, for whitch we habe been
-intendes to make the proof.*)
-(* ------------------------------------------------------------------------- *)
-fun simpl_wp (fm,pr) = let val fm2 = simpl fm
-				in (fm2,Simp(fm,pr))
-				end;
-
-	
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{minus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wph x fm = let fun mk_atomar_minusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-  
-	      fun combine_minusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
-		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
-		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
-	in 
- 
- case fm of 
- (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
-     if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_minusinf_proof x fm))
-        else (fm ,(mk_atomar_minusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
-  	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
-	 then (HOLogic.false_const ,(mk_atomar_minusinf_proof x fm))
-	 				 else (fm,(mk_atomar_minusinf_proof x fm)) 
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
-       if (y=x) andalso (c1 = zero) then 
-        if c2 = one then (HOLogic.false_const,(mk_atomar_minusinf_proof x fm)) else
-	(HOLogic.true_const,(mk_atomar_minusinf_proof x fm))
-	else (fm,(mk_atomar_minusinf_proof x fm))
-  
-  |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_minusinf_proof x fm)
-  
-  |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_minusinf_proof x fm)
-  
-  |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
-  				    val (qfm,qpr) = minusinf_wph x q
-				    val pr = (combine_minusinf_proofs "CJ" ppr qpr)
-				     in 
-				     (HOLogic.conj $ pfm $qfm , pr)
-				     end 
-  |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
-  				     val (qfm,qpr) = minusinf_wph x q
-				     val pr = (combine_minusinf_proofs "DJ" ppr qpr)
-				     in 
-				     (HOLogic.disj $ pfm $qfm , pr)
-				     end 
-
-  |_ => (fm,(mk_atomar_minusinf_proof x fm))
-  
-  end;					 
-(* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wp x fm  = let val (fm2,pr) = (minusinf_wph x fm)
-                       in (fm2,Minusinf(pr))
-                        end;
-
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{plus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-
-fun plusinf_wph x fm = let fun mk_atomar_plusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-  
-	      fun combine_plusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
-		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
-		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
-	in 
- 
- case fm of 
- (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
-     if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_plusinf_proof x fm))
-        else (fm ,(mk_atomar_plusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
-  	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
-	 then (HOLogic.false_const ,(mk_atomar_plusinf_proof x fm))
-	 				 else (fm,(mk_atomar_plusinf_proof x fm)) 
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
-       if (y=x) andalso (c1 = zero) then 
-        if c2 = one then (HOLogic.true_const,(mk_atomar_plusinf_proof x fm)) else
-	(HOLogic.false_const,(mk_atomar_plusinf_proof x fm))
-	else (fm,(mk_atomar_plusinf_proof x fm))
-  
-  |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_plusinf_proof x fm)
-  
-  |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_plusinf_proof x fm)
-  
-  |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
-  				    val (qfm,qpr) = plusinf_wph x q
-				    val pr = (combine_plusinf_proofs "CJ" ppr qpr)
-				     in 
-				     (HOLogic.conj $ pfm $qfm , pr)
-				     end 
-  |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
-  				     val (qfm,qpr) = plusinf_wph x q
-				     val pr = (combine_plusinf_proofs "DJ" ppr qpr)
-				     in 
-				     (HOLogic.disj $ pfm $qfm , pr)
-				     end 
-
-  |_ => (fm,(mk_atomar_plusinf_proof x fm))
-  
-  end;					 
-(* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun plusinf_wp x fm  = let val (fm2,pr) = (plusinf_wph x fm)
-                       in (fm2,Minusinf(pr))
-                        end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Bset.*)
-(* ------------------------------------------------------------------------- *)
-fun bset_wp x fm = let val bs = bset x fm in
-				(bs,Bset(x,fm,bs,mk_numeral (divlcm x fm)))
-				end;
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Aset.*)
-(* ------------------------------------------------------------------------- *)
-fun aset_wp x fm = let val ast = aset x fm in
-				(ast,Aset(x,fm,ast,mk_numeral (divlcm x fm)))
-				end;
- 
-
-
 (* ------------------------------------------------------------------------- *)
 (*function list to Set, constructs a set containing all elements of a given list.*)
 (* ------------------------------------------------------------------------- *)
 fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in 
 	case l of 
 		[] => Const ("{}",T)
 		|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
 		end;
 		
-
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wph fm = case fm of
-	Const("Not",_) $ R => if (is_arith_rel R) then (Not_bst_p_atomic (fm)) else CpLogError
-	|Const("op &",_) $ ls $ rs => Not_bst_p_conjI((not_bst_p_wph ls),(not_bst_p_wph rs))
-	|Const("op |",_) $ ls $ rs => Not_bst_p_disjI((not_bst_p_wph ls),(not_bst_p_wph rs))
-	|_ => Not_bst_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)	
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wp x fm = let val prt = not_bst_p_wph fm
-			    val D = mk_numeral (divlcm x fm)
-			    val B = map norm_zero_one (bset x fm)
-			in (Not_bst_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
-			end;
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wph fm = case fm of
-	Const("Not",_) $ R => if (is_arith_rel R) then (Not_ast_p_atomic (fm)) else CpLogError
-	|Const("op &",_) $ ls $ rs => Not_ast_p_conjI((not_ast_p_wph ls),(not_ast_p_wph rs))
-	|Const("op |",_) $ ls $ rs => Not_ast_p_disjI((not_ast_p_wph ls),(not_ast_p_wph rs))
-	|_ => Not_ast_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)	
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wp x fm = let val prt = not_ast_p_wph fm
-			    val D = mk_numeral (divlcm x fm)
-			    val B = map norm_zero_one (aset x fm)
-			in (Not_ast_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
-			end;
-
-(*======================================================*)
-(* Protokolgeneration for the formula evaluation process*)
-(*======================================================*)
-
-fun evalc_wp fm = 
-  let fun evalc_atom_wp at =case at of  
-    (Const (p,_) $ s $ t) =>(  
-    case assoc (operations,p) of 
-        Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)) else EvalAt(HOLogic.mk_eq(at, HOLogic.false_const)))  
-		   handle _ => Evalfm(at)) 
-        | _ =>  Evalfm(at)) 
-     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-       case assoc (operations,p) of 
-         Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
-	  EvalAt(HOLogic.mk_eq(at, HOLogic.false_const))  else EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)))  
-		      handle _ => Evalfm(at)) 
-         | _ => Evalfm(at)) 
-     | _ => Evalfm(at)  
- 
-  in
-   case fm of
-    (Const("op &",_)$A$B) => EvalConst("CJ",evalc_wp A,evalc_wp B)
-   |(Const("op |",_)$A$B) => EvalConst("DJ",evalc_wp A,evalc_wp B) 
-   |(Const("op -->",_)$A$B) => EvalConst("IM",evalc_wp A,evalc_wp B) 
-   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => EvalConst("EQ",evalc_wp A,evalc_wp B) 
-   |_ => evalc_atom_wp fm
-  end;
-
-
-
-(*======================================================*)
-(* Protokolgeneration for the NNF Transformation        *)
-(*======================================================*)
-
-fun cnnf_wp f = 
-  let fun hcnnf_wp fm =
-    case fm of
-    (Const ("op &",_) $ p $ q) => NNFConst("CJ",hcnnf_wp p,hcnnf_wp q) 
-    | (Const ("op |",_) $ p $ q) =>  NNFConst("DJ",hcnnf_wp p,hcnnf_wp q)
-    | (Const ("op -->",_) $ p $q) => NNFConst("IM",hcnnf_wp (HOLogic.Not $ p),hcnnf_wp q)
-    | (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q) => NNFConst("EQ",hcnnf_wp (HOLogic.mk_conj(p,q)),hcnnf_wp (HOLogic.mk_conj((HOLogic.Not $ p), (HOLogic.Not $ q)))) 
-
-    | (Const ("Not",_) $ (Const("Not",_) $ p)) => NNFNN(hcnnf_wp p) 
-    | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => NNFConst ("NCJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
-    | (Const ("Not",_) $(Const ("op |",_) $ (A as (Const ("op &",_) $ p $ q)) $  
-    			(B as (Const ("op &",_) $ p1 $ r)))) => if p1 = negate p then 
-		         NNFConst("SDJ",  
-			   NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q)),
-			   NNFConst("CJ",hcnnf_wp p1,hcnnf_wp(HOLogic.Not $ r)))
-			 else  NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ A)),(hcnnf_wp(HOLogic.Not $ B))) 
-
-    | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
-    | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) =>  NNFConst ("NIM",(hcnnf_wp(p)),(hcnnf_wp(HOLogic.Not $ q))) 
-    | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_]))  $ p $ q)) =>NNFConst ("NEQ",(NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q))),(NNFConst("CJ",hcnnf_wp(HOLogic.Not $ p),hcnnf_wp q))) 
-    | _ => NNFAt(fm)  
-  in NNFSimp(hcnnf_wp f)
-end; 
-   
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Cooper decision Procedure with proof protocoling*)
-(* ------------------------------------------------------------------------- *)
-
-fun coopermi_wp vars fm =
-  case fm of
-   Const ("Ex",_) $ Abs(xo,T,po) => let 
-    val (xn,np) = variant_abs(xo,T,po) 
-    val x = (Free(xn , T))
-    val p = np     (* Is this a legal proof for the P=NP Problem??*)
-    val (p_inf,miprt) = simpl_wp (minusinf_wp x p)
-    val (bset,bsprt) = bset_wp x p
-    val nbst_p_prt = not_bst_p_wp x p
-    val dlcm = divlcm x p 
-    val js = 1 upto dlcm 
-    fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p 
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset) 
-   in (list_disj (map stage js),Cooper(mk_numeral dlcm,miprt,bsprt,nbst_p_prt))
-   end
-   
-  | _ => (error "cooper: not an existential formula",No);
-				
-fun cooperpi_wp vars fm =
-  case fm of
-   Const ("Ex",_) $ Abs(xo,T,po) => let 
-    val (xn,np) = variant_abs(xo,T,po) 
-    val x = (Free(xn , T))
-    val p = np     (* Is this a legal proof for the P=NP Problem??*)
-    val (p_inf,piprt) = simpl_wp (plusinf_wp x p)
-    val (aset,asprt) = aset_wp x p
-    val nast_p_prt = not_ast_p_wp x p
-    val dlcm = divlcm x p 
-    val js = 1 upto dlcm 
-    fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p 
-    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset) 
-   in (list_disj (map stage js),Cooper(mk_numeral dlcm,piprt,asprt,nast_p_prt))
-   end
-  | _ => (error "cooper: not an existential formula",No);
-				
-
-
-
-
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*---      Interpretation and Proofgeneration Part              ---*)
-(*---                                                           ---*)
-(*---      Protocole interpretation functions                   ---*)
-(*---                                                           ---*)
-(*---      and proofgeneration functions                        ---*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*---                                                           ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
 (* ------------------------------------------------------------------------- *)
 (* Returns both sides of an equvalence in the theorem*)
 (* ------------------------------------------------------------------------- *)
 fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
-
-
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
 
 (* ------------------------------------------------------------------------- *)
 (* Modified version of the simple version with minimal amount of checking and postprocessing*)
 (* ------------------------------------------------------------------------- *)
 

           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   in check (Seq.pull (EVERY tacs (trivial G))) end;
 
 (*-------------------------------------------------------------*)
 (*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
 
 fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
 
 (* ------------------------------------------------------------------------- *)
 (*This function proove elementar will be used to generate proofs at runtime*)

 (* ------------------------------------------------------------------------- *)
 fun prove_elementar sg s fm2 = case s of 
   (*"ss" like simplification with simpset*)
   "ss" =>
     let
-      val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
+      val ss = presburger_ss addsimps
+        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
       val ct =  cert_Trueprop sg fm2
     in 
       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     end
 

       val ss = presburger_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2
     in 
       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     end
+  (* like Existance Conjunction *)
+  | "ec" =>
+    let
+      val ss = presburger_ss addsimps zadd_ac
+      val ct = cert_Trueprop sg fm2
+    in 
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
+    end
 
   | "ac" =>
     let
       val ss = HOL_basic_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2

       val ct = cert_Trueprop sg fm2
     in 
       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     end;
 
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of the adjustcoffeq result.*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* ------------------------------------------------------------------------- *)
-fun proof_of_adjustcoeffeq sg (prt,rs) = case prt of
-   ACfm fm => instantiate' [Some cboolT]
-    [Some (cterm_of sg fm)] refl
- | ACAt (k,at as (Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
-      c $ x ) $t ))) => 
-   let
-     val ck = cterm_of sg (mk_numeral k)
-     val cc = cterm_of sg c
-     val ct = cterm_of sg t
-     val cx = cterm_of sg x
-     val ca = cterm_of sg a
-   in case p of
-     "op <" => let val pre = prove_elementar sg "lf" 
-	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
-	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
-		      in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
-                   end
-    |"op =" =>let val pre = prove_elementar sg "lf" 
+(*=============================================================*)
+(*-------------------------------------------------------------*)
+(*              The new compact model                          *)
+(*-------------------------------------------------------------*)
+(*=============================================================*)
+
+fun thm_of sg decomp t = 
+    let val (ts,recomb) = decomp t 
+    in recomb (map (thm_of sg decomp) ts) 
+    end;
+
+(*==================================================*)
+(*     Compact Version for adjustcoeffeq            *)
+(*==================================================*)
+
+fun decomp_adjustcoeffeq sg x l fm = case fm of
+    (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
+     let  
+        val m = l div (dest_numeral c) 
+        val n = if (x = y) then abs (m) else 1
+        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
+        val rs = if (x = y) 
+                 then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
+                 else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
+        val ck = cterm_of sg (mk_numeral n)
+        val cc = cterm_of sg c
+        val ct = cterm_of sg z
+        val cx = cterm_of sg y
+        val pre = prove_elementar sg "lf" 
+            (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
+        val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
+        in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+        end
+
+  |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
+      c $ y ) $t )) => 
+   if (is_arith_rel fm) andalso (x = y) 
+   then  
+        let val m = l div (dest_numeral c) 
+           val k = (if p = "op <" then abs(m) else m)  
+           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
+           val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
+
+           val ck = cterm_of sg (mk_numeral k)
+           val cc = cterm_of sg c
+           val ct = cterm_of sg t
+           val cx = cterm_of sg x
+           val ca = cterm_of sg a
+
+	   in 
+	case p of
+	  "op <" => 
+	let val pre = prove_elementar sg "lf" 
+	    (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
+            val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
+	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+         end
+
+           |"op =" =>
+	     let val pre = prove_elementar sg "lf" 
 	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
-	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
-	             in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
-                      end
-                  end
-    |"Divides.op dvd" =>let val pre = prove_elementar sg "lf" 
+	         val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
+	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+             end
+
+             |"Divides.op dvd" =>
+	       let val pre = prove_elementar sg "lf" 
 	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
-	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
-                         in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
+                   val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
+               in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
                         
-                          end
-  end
- |ACPI(k,at as (Const("Not",_)$(Const("op <",_) $a $( Const ("op +", _)$(Const ("op *",_) $ c $ x ) $t )))) => 
-   let
-     val ck = cterm_of sg (mk_numeral k)
-     val cc = cterm_of sg c
-     val ct = cterm_of sg t
-     val cx = cterm_of sg x
-     val pre = prove_elementar sg "lf" 
-       (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
-       val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
-
-         in [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
-   end
- |ACNeg(pr) => let val (Const("Not",_)$nrs) = rs
-               in (proof_of_adjustcoeffeq sg (pr,nrs)) RS (qe_Not) 
                end
- |ACConst(s,pr1,pr2) =>
-   let val (Const(_,_)$rs1$rs2) = rs
-       val th1 = proof_of_adjustcoeffeq sg (pr1,rs1)
-       val th2 = proof_of_adjustcoeffeq sg (pr2,rs2)
-       in case s of 
-	 "CJ" => [th1,th2] MRS (qe_conjI)
-         |"DJ" => [th1,th2] MRS (qe_disjI)
-         |"IM" => [th1,th2] MRS (qe_impI)
-         |"EQ" => [th1,th2] MRS (qe_eqI)
-   end;
-
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_minf_proof_of sg dlcm (Modd_minf (x,fm1)) =
-  let
+              end
+  else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
+
+ |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
+  |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+  |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+
+  |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
+
+(*==================================================*)
+(*   Finding rho for modd_minusinfinity             *)
+(*==================================================*)
+fun rho_for_modd_minf x dlcm sg fm1 =
+let
     (*Some certified Terms*)
     
    val ctrue = cterm_of sg HOLogic.true_const
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1

 		      end
 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
 		
     
    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
-   end	
-
- |atomar_minf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
-       (*Some certified types*)
+   end;	 
+(*=========================================================================*)
+(*=========================================================================*)
+fun rho_for_eq_minf x dlcm  sg fm1 =  
+   let
    val fm = norm_zero_one fm1
     in  case fm1 of 
       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))

 
       		
     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
  end;
 
-
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{-infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_minf_proof s pr1 pr2 = case s of
-    "ECJ" => [pr1 , pr2] MRS (eq_minf_conjI)
-
-   |"EDJ" => [pr1 , pr2] MRS (eq_minf_disjI)
-   
-   |"MCJ" => [pr1 , pr2] MRS (modd_minf_conjI)
-
-   |"MDJ" => [pr1 , pr2] MRS (modd_minf_disjI);
-
-(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
-(* ------------------------------------------------------------------------- *)
-fun minf_proof_ofh sg dlcm prl = case prl of 
-
-    Eq_minf (_) => atomar_minf_proof_of sg dlcm prl
-    
-   |Modd_minf (_) => atomar_minf_proof_of sg dlcm prl
-   
-   |Eq_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
-   				    val pr2 = minf_proof_ofh sg dlcm prl2
-				 in (combine_minf_proof "ECJ" pr1 pr2)
-				 end
-				 
-   |Eq_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
-   				    val pr2 = minf_proof_ofh sg dlcm prl2
-				 in (combine_minf_proof "EDJ" pr1 pr2)
-				 end
-				 
-   |Modd_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
-   				    val pr2 = minf_proof_ofh sg dlcm prl2
-				 in (combine_minf_proof "MCJ" pr1 pr2)
-				 end
-				 
-   |Modd_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
-   				    val pr2 = minf_proof_ofh sg dlcm prl2
-				 in (combine_minf_proof "MDJ" pr1 pr2)
-				 end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
-(* ------------------------------------------------------------------------- *)
-fun  minf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
-  let val pr1 = minf_proof_ofh sg dlcm prl1
-      val pr2 = minf_proof_ofh sg dlcm prl2
-  in (pr1, pr2)
-end;
-				 
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_pinf_proof_of sg dlcm (Modd_minf (x,fm1)) =
- let
+(*=====================================================*)
+(*=====================================================*)
+(*=========== minf proofs with the compact version==========*)
+fun decomp_minf_eq x dlcm sg t =  case t of
+   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
+   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
+   |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
+
+fun decomp_minf_modd x dlcm sg t = case t of
+   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
+   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
+   |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
+
+(* -------------------------------------------------------------*)
+(*                    Finding rho for pinf_modd                 *)
+(* -------------------------------------------------------------*)
+fun rho_for_modd_pinf x dlcm sg fm1 = 
+let
     (*Some certified Terms*)
     
   val ctrue = cterm_of sg HOLogic.true_const
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1

 		      end
 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
 		
     
    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
-   end	
-
- |atomar_pinf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
+   end;	
+(* -------------------------------------------------------------*)
+(*                    Finding rho for pinf_eq                 *)
+(* -------------------------------------------------------------*)
+fun rho_for_eq_pinf x dlcm sg fm1 = 
+  let
 					val fm = norm_zero_one fm1
     in  case fm1 of 
       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
          if  (x=y) andalso (c1=zero) andalso (c2=one) 
 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))

       		
     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  end;
 
 
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{+infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_pinf_proof s pr1 pr2 = case s of
-    "ECJ" => [pr1 , pr2] MRS (eq_pinf_conjI)
-
-   |"EDJ" => [pr1 , pr2] MRS (eq_pinf_disjI)
-   
-   |"MCJ" => [pr1 , pr2] MRS (modd_pinf_conjI)
-
-   |"MDJ" => [pr1 , pr2] MRS (modd_pinf_disjI);
-
-(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
-(* ------------------------------------------------------------------------- *)
-fun pinf_proof_ofh sg dlcm prl = case prl of 
-
-    Eq_minf (_) => atomar_pinf_proof_of sg dlcm prl
-    
-   |Modd_minf (_) => atomar_pinf_proof_of sg dlcm prl
-   
-   |Eq_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
-   				    val pr2 = pinf_proof_ofh sg dlcm prl2
-				 in (combine_pinf_proof "ECJ" pr1 pr2)
-				 end
-				 
-   |Eq_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
-   				    val pr2 = pinf_proof_ofh sg dlcm prl2
-				 in (combine_pinf_proof "EDJ" pr1 pr2)
-				 end
-				 
-   |Modd_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
-   				    val pr2 = pinf_proof_ofh sg dlcm prl2
-				 in (combine_pinf_proof "MCJ" pr1 pr2)
-				 end
-				 
-   |Modd_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
-   				    val pr2 = pinf_proof_ofh sg dlcm prl2
-				 in (combine_pinf_proof "MDJ" pr1 pr2)
-				 end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
-(* ------------------------------------------------------------------------- *)
-fun pinf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
-  let val pr1 = pinf_proof_ofh sg dlcm prl1
-      val pr2 = pinf_proof_ofh sg dlcm prl2
-  in (pr1, pr2)
+
+fun  minf_proof_of_c sg x dlcm t =
+  let val minf_eqth   = thm_of sg (decomp_minf_eq x dlcm sg) t
+      val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
+  in (minf_eqth, minf_moddth)
 end;
-				 
-
-
-(* ------------------------------------------------------------------------- *)    
-(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
+
+(*=========== pinf proofs with the compact version==========*)
+fun decomp_pinf_eq x dlcm sg t = case t of
+   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
+   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
+   |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
+
+fun decomp_pinf_modd x dlcm sg t =  case t of
+   Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
+   |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
+   |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
+
+fun  pinf_proof_of_c sg x dlcm t =
+  let val pinf_eqth   = thm_of sg (decomp_pinf_eq x dlcm sg) t
+      val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
+  in (pinf_eqth,pinf_moddth)
+end;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Here we generate the theorem for the Bset Property in the simple direction*)
+(* It is just an instantiation*)
+(* ------------------------------------------------------------------------- *)
+(*
+fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm   = 
+  let
+    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+    val cdlcm = cterm_of sg dlcm
+    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
+  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
+end;
+
+fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = 
+  let
+    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+    val cdlcm = cterm_of sg dlcm
+    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
+  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
+end;
+*)
 
 (* For the generation of atomic Theorems*)
 (* Prove the premisses on runtime and then make RS*)
 (* ------------------------------------------------------------------------- *)
+
+(*========= this is rho ============*)
 fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = 
   let
     val cdlcm = cterm_of sg dlcm
     val cB = cterm_of sg B
     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))

       		
    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
       		
     end;
     
+
 (* ------------------------------------------------------------------------- *)    
 (* Main interpretation function for this backwards dirction*)
 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
 (*Help Function*)
 (* ------------------------------------------------------------------------- *)
-fun not_bst_p_proof_of_h sg x fm dlcm B prt = case prt of 
-	(Not_bst_p_atomic(fm2)) => (generate_atomic_not_bst_p sg x fm dlcm B fm2)
-	
-	|(Not_bst_p_conjI(pr1,pr2)) => 
-			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
-			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
-			    in ([th1,th2] MRS (not_bst_p_conjI))
-			    end
-
-	|(Not_bst_p_disjI(pr1,pr2)) => 
-			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
-			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
-			    in ([th1,th2] MRS not_bst_p_disjI)
-			    end;
-(* Main function*)
-fun not_bst_p_proof_of sg (Not_bst_p(x as Free(xn,xT),fm,dlcm,B,prl)) =
-  let val th =  not_bst_p_proof_of_h sg x fm dlcm B prl
+
+(*==================== Proof with the compact version   *)
+
+fun decomp_nbstp sg x dlcm B fm t = case t of 
+   Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
+  |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
+  |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
+
+fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
+  let 
+       val th =  thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
       val fma = absfree (xn,xT, norm_zero_one fm)
   in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
      in [th,th1] MRS (not_bst_p_Q_elim)
      end
   end;

 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
 
 (* For the generation of atomic Theorems*)
 (* Prove the premisses on runtime and then make RS*)
 (* ------------------------------------------------------------------------- *)
+(*========= this is rho ============*)
 fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = 
   let
     val cdlcm = cterm_of sg dlcm
     val cA = cterm_of sg A
     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))

       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
       		
    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
       		
     end;
-    
-(* ------------------------------------------------------------------------- *)    
+
+(* ------------------------------------------------------------------------ *)
 (* Main interpretation function for this backwards dirction*)
 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
 (*Help Function*)
 (* ------------------------------------------------------------------------- *)
-fun not_ast_p_proof_of_h sg x fm dlcm A prt = case prt of 
-	(Not_ast_p_atomic(fm2)) => (generate_atomic_not_ast_p sg x fm dlcm A fm2)
-	
-	|(Not_ast_p_conjI(pr1,pr2)) => 
-			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
-			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
-			    in ([th1,th2] MRS (not_ast_p_conjI))
-			    end
-
-	|(Not_ast_p_disjI(pr1,pr2)) => 
-			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
-			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
-			    in ([th1,th2] MRS (not_ast_p_disjI))
-			    end;
-(* Main function*)
-fun not_ast_p_proof_of sg (Not_ast_p(x as Free(xn,xT),fm,dlcm,A,prl)) =
-  let val th =  not_ast_p_proof_of_h sg x fm dlcm A prl
+
+fun decomp_nastp sg x dlcm A fm t = case t of 
+   Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
+  |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
+  |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
+
+fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
+  let 
+       val th =  thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
       val fma = absfree (xn,xT, norm_zero_one fm)
-      val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
-  in [th,th1] MRS (not_ast_p_Q_elim)
+  in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
+     in [th,th1] MRS (not_ast_p_Q_elim)
+     end
+  end;
+
+
+(* -------------------------------*)
+(* Finding rho and beta for evalc *)
+(* -------------------------------*)
+
+fun rho_for_evalc sg at = case at of  
+    (Const (p,_) $ s $ t) =>(  
+    case assoc (operations,p) of 
+        Some f => 
+           ((if (f ((dest_numeral s),(dest_numeral t))) 
+             then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
+             else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
+		   handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl
+        | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )) 
+     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
+       case assoc (operations,p) of 
+         Some f => 
+           ((if (f ((dest_numeral s),(dest_numeral t))) 
+             then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
+             else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
+		      handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl) 
+         | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ) 
+     | _ =>   instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
+
+
+(*=========================================================*)
+fun decomp_evalc sg t = case t of
+   (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+   |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+   |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+   |_ => ([], fn [] => rho_for_evalc sg t);
+
+
+fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
+
+(*==================================================*)
+(*     Proof of linform with the compact model      *)
+(*==================================================*)
+
+
+fun decomp_linform sg vars t = case t of
+   (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+   |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+   |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+   |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
+   |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
+   |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
+
+fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
+
+(* ------------------------------------------------------------------------- *)
+(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
+(* ------------------------------------------------------------------------- *)
+fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
+  (* Get the Bset thm*)
+  let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm 
+      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
+      val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
+  in (dpos,minf_eqth,nbstpthm,minf_moddth)
 end;
 
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
-(* ------------------------------------------------------------------------- *)
-
-
-fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
-  (* Get the Bset thm*)
-  let val (mit1,mit2) = minf_proof_of sg dlcm miprt
-      val fm1 = norm_zero_one (simpl fm) 
+(* ------------------------------------------------------------------------- *)
+(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
+(* ------------------------------------------------------------------------- *)
+fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
+  let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
-      val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
-    (* Return the four theorems needed to proove the whole Cooper Theorem*)
-  in (dpos,mit2,nbstpthm,mit1)
+      val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
+  in (dpos,pinf_eqth,nastpthm,pinf_moddth)
 end;
 
-
-(* ------------------------------------------------------------------------- *)
-(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
-(* ------------------------------------------------------------------------- *)
-
-
-fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
-  let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
-      val fm1 = norm_zero_one (simpl fm) 
-      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
-      val nastpthm = not_ast_p_proof_of sg nast_p_prt
-  in (dpos,mit2,nastpthm,mit1)
-end;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Interpretaion of Protocols of the cooper procedure : full version*)
 (* ------------------------------------------------------------------------- *)
-
-
-
-fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
-  "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	      val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
-		   in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
+fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
+  "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm 
+	      in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
            end
-  |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
-	       val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
-		   in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
+  |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
+	       in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
                 end
  |_ => error "parameter error";
 
 (* ------------------------------------------------------------------------- *)
 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
 (* ------------------------------------------------------------------------- *)
 
-fun cooper_prv sg (x as Free(xn,xT)) efm vars = let 
-   val l = formlcm x efm
-   val ac_thm = proof_of_adjustcoeffeq sg (adjustcoeffeq_wp  x l efm)
+fun cooper_prv sg (x as Free(xn,xT)) efm = let 
+   val lfm_thm = proof_of_linform sg [xn] efm
+   val efm2 = snd(qe_get_terms lfm_thm)
+   val l = formlcm x efm2
+   val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
    val fm = snd (qe_get_terms ac_thm)
    val  cfm = unitycoeff x fm
    val afm = adjustcoeff x l fm
    val P = absfree(xn,xT,afm)
    val ss = presburger_ss addsimps
      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
-   val cms = if ((length (aset x cfm)) < (length (bset x cfm))) then "pi" else "mi"
-   val cp_thm = cooper_thm sg cms x vars cfm
+   val A = aset x cfm
+   val B = bset x cfm
+   val dlcm = mk_numeral (divlcm x cfm)
+   val cms = if ((length A) < (length B )) then "pi" else "mi"
+   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    val (lsuth,rsuth) = qe_get_terms (uth)
    val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    val (lscth,rscth) = qe_get_terms (exp_cp_thm)
    val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
  in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
    end
-|cooper_prv _ _ _ _ = error "Parameters format";
-
-
-(*====================================================*)
-(*Interpretation function for the evaluation protokol *)
-(*====================================================*)
-
-fun proof_of_evalc sg fm =
-let
-fun proof_of_evalch prt = case prt of
-  EvalAt(at) => prove_elementar sg "ss" at
- |Evalfm(fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
- |EvalConst(s,pr1,pr2) => 
-   let val th1 = proof_of_evalch pr1
-       val th2 = proof_of_evalch pr2
-   in case s of
-     "CJ" =>[th1,th2] MRS (qe_conjI)
-    |"DJ" =>[th1,th2] MRS (qe_disjI)
-    |"IM" =>[th1,th2] MRS (qe_impI)
-    |"EQ" =>[th1,th2] MRS (qe_eqI)
-    end
-in proof_of_evalch (evalc_wp fm)
+|cooper_prv _ _ _ =  error "Parameters format";
+
+
+
+fun decomp_cnnf sg lfnp P = case P of 
+     Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
+   |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS  qe_disjI)
+   |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
+   |Const("Not",_) $ (Const(opn,T) $ p $ q) => 
+     if opn = "op |" 
+      then case (p,q) of 
+         (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+          if r1 = negate r 
+          then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],fn [th1_1,th1_2,th2_1,th2_2] => [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
+
+          else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+        |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+      else (
+         case (opn,T) of 
+           ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
+           |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
+           |("op =",Type ("fun",[Type ("bool", []),_])) => 
+           ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
+            |(_,_) => ([], fn [] => lfnp P)
+)
+
+   |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
+
+   |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
+     ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
+   |_ => ([], fn [] => lfnp P);
+
+
+
+
+fun proof_of_cnnf sg p lfnp = 
+ let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
+     val rs = snd(qe_get_terms th1)
+     val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
+  in [th1,th2] MRS trans
+  end;
+
 end;
-
-(*============================================================*)
-(*Interpretation function for the NNF-Transformation protokol *)
-(*============================================================*)
-
-fun proof_of_cnnf sg fm pf = 
-let fun proof_of_cnnfh prt pat = case prt of
-  NNFAt(at) => pat at
- |NNFSimp (pr) => let val th1 = proof_of_cnnfh pr pat
-                  in let val fm2 = snd (qe_get_terms th1) 
-		     in [th1,prove_elementar sg "ss" (HOLogic.mk_eq(fm2 ,simpl fm2))] MRS trans
-                     end
-                  end
- |NNFNN (pr) => (proof_of_cnnfh pr pat) RS (nnf_nn)
- |NNFConst (s,pr1,pr2) =>
-   let val th1 = proof_of_cnnfh pr1 pat
-       val th2 = proof_of_cnnfh pr2 pat
-   in case s of
-     "CJ" => [th1,th2] MRS (qe_conjI)
-    |"DJ" => [th1,th2] MRS (qe_disjI)
-    |"IM" => [th1,th2] MRS (nnf_im)
-    |"EQ" => [th1,th2] MRS (nnf_eq)
-    |"SDJ" => let val (Const("op &",_)$A$_) = fst (qe_get_terms th1)
-	          val (Const("op &",_)$C$_) = fst (qe_get_terms th2)
-	      in [th1,th2,prove_elementar sg "ss" (HOLogic.mk_eq (A,HOLogic.Not $ C))] MRS (nnf_sdj)
-	      end
-    |"NCJ" => [th1,th2] MRS (nnf_ncj)
-    |"NIM" => [th1,th2] MRS (nnf_nim)
-    |"NEQ" => [th1,th2] MRS (nnf_neq)
-    |"NDJ" => [th1,th2] MRS (nnf_ndj)
-   end
-in proof_of_cnnfh (cnnf_wp fm) pf
-end;
-
-
-
-
-(*====================================================*)
-(* Interpretation function for the linform protokol   *)
-(*====================================================*)
-
-
-fun proof_of_linform sg vars f = 
-  let fun proof_of_linformh prt = 
-  case prt of
-    (LfAt (at)) =>  prove_elementar sg "lf" (HOLogic.mk_eq (at, linform vars at))
-   |(LfAtdvd (Const("Divides.op dvd",_)$d$t)) => (prove_elementar sg "lf" (HOLogic.mk_eq (t, lint vars t))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd))
-   |(Lffm (fm)) => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
-   |(LfConst (s,pr1,pr2)) =>
-     let val th1 = proof_of_linformh pr1
-	 val th2 = proof_of_linformh pr2
-     in case s of
-       "CJ" => [th1,th2] MRS (qe_conjI)
-      |"DJ" =>[th1,th2] MRS (qe_disjI)
-      |"IM" =>[th1,th2] MRS (qe_impI)
-      |"EQ" =>[th1,th2] MRS (qe_eqI)
-     end
-   |(LfNot(pr)) => 
-     let val th = proof_of_linformh pr
-     in (th RS (qe_Not))
-     end
-   |(LfQ(s,xn,xT,pr)) => 
-     let val th = forall_intr (cterm_of sg (Free(xn,xT)))(proof_of_linformh pr)
-     in if s = "Ex" 
-        then (th COMP(qe_exI) )
-        else (th COMP(qe_ALLI) )
-     end
-in
- proof_of_linformh (linform_wp f)
-end;
-
-end;