src/HOL/Integ/cooper_proof.ML
changeset 13876 68f4ed8311ac
child 13905 3e496c70f2f3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Mar 25 09:47:05 2003 +0100
     1.3 @@ -0,0 +1,1488 @@
     1.4 +(*  Title:      HOL/Integ/cooper_proof.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +File containing the implementation of the proof
    1.10 +generation for Cooper Algorithm
    1.11 +*)
    1.12 +
    1.13 +signature COOPER_PROOF =
    1.14 +sig
    1.15 +  val qe_Not : thm
    1.16 +  val qe_conjI : thm
    1.17 +  val qe_disjI : thm
    1.18 +  val qe_impI : thm
    1.19 +  val qe_eqI : thm
    1.20 +  val qe_exI : thm
    1.21 +  val qe_get_terms : thm -> term * term
    1.22 +  val cooper_prv : Sign.sg -> term -> term -> string list -> thm
    1.23 +  val proof_of_evalc : Sign.sg -> term -> thm
    1.24 +  val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    1.25 +  val proof_of_linform : Sign.sg -> string list -> term -> thm
    1.26 +end;
    1.27 +
    1.28 +structure CooperProof : COOPER_PROOF =
    1.29 +struct
    1.30 +
    1.31 +open CooperDec;
    1.32 +
    1.33 +(*-----------------------------------------------------------------*)
    1.34 +(*-----------------------------------------------------------------*)
    1.35 +(*-----------------------------------------------------------------*)
    1.36 +(*---                                                           ---*)
    1.37 +(*---                                                           ---*)
    1.38 +(*---         Protocoling part                                  ---*)
    1.39 +(*---                                                           ---*)
    1.40 +(*---           includes the protocolling datastructure         ---*)
    1.41 +(*---                                                           ---*)
    1.42 +(*---          and the protocolling fuctions                    ---*)
    1.43 +(*---                                                           ---*)
    1.44 +(*---                                                           ---*)
    1.45 +(*-----------------------------------------------------------------*)
    1.46 +(*-----------------------------------------------------------------*)
    1.47 +(*-----------------------------------------------------------------*)
    1.48 +
    1.49 +val presburger_ss = simpset_of (theory "Presburger")
    1.50 +  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
    1.51 +val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    1.52 +
    1.53 +(*Theorems that will be used later for the proofgeneration*)
    1.54 +
    1.55 +val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
    1.56 +val unity_coeff_ex = thm "unity_coeff_ex";
    1.57 +
    1.58 +(* Thorems for proving the adjustment of the coeffitients*)
    1.59 +
    1.60 +val ac_lt_eq =  thm "ac_lt_eq";
    1.61 +val ac_eq_eq = thm "ac_eq_eq";
    1.62 +val ac_dvd_eq = thm "ac_dvd_eq";
    1.63 +val ac_pi_eq = thm "ac_pi_eq";
    1.64 +
    1.65 +(* The logical compination of the sythetised properties*)
    1.66 +val qe_Not = thm "qe_Not";
    1.67 +val qe_conjI = thm "qe_conjI";
    1.68 +val qe_disjI = thm "qe_disjI";
    1.69 +val qe_impI = thm "qe_impI";
    1.70 +val qe_eqI = thm "qe_eqI";
    1.71 +val qe_exI = thm "qe_exI";
    1.72 +val qe_ALLI = thm "qe_ALLI";
    1.73 +
    1.74 +(*Modulo D property for Pminusinf an Plusinf *)
    1.75 +val fm_modd_minf = thm "fm_modd_minf";
    1.76 +val not_dvd_modd_minf = thm "not_dvd_modd_minf";
    1.77 +val dvd_modd_minf = thm "dvd_modd_minf";
    1.78 +
    1.79 +val fm_modd_pinf = thm "fm_modd_pinf";
    1.80 +val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
    1.81 +val dvd_modd_pinf = thm "dvd_modd_pinf";
    1.82 +
    1.83 +(* the minusinfinity proprty*)
    1.84 +
    1.85 +val fm_eq_minf = thm "fm_eq_minf";
    1.86 +val neq_eq_minf = thm "neq_eq_minf";
    1.87 +val eq_eq_minf = thm "eq_eq_minf";
    1.88 +val le_eq_minf = thm "le_eq_minf";
    1.89 +val len_eq_minf = thm "len_eq_minf";
    1.90 +val not_dvd_eq_minf = thm "not_dvd_eq_minf";
    1.91 +val dvd_eq_minf = thm "dvd_eq_minf";
    1.92 +
    1.93 +(* the Plusinfinity proprty*)
    1.94 +
    1.95 +val fm_eq_pinf = thm "fm_eq_pinf";
    1.96 +val neq_eq_pinf = thm "neq_eq_pinf";
    1.97 +val eq_eq_pinf = thm "eq_eq_pinf";
    1.98 +val le_eq_pinf = thm "le_eq_pinf";
    1.99 +val len_eq_pinf = thm "len_eq_pinf";
   1.100 +val not_dvd_eq_pinf = thm "not_dvd_eq_pinf";
   1.101 +val dvd_eq_pinf = thm "dvd_eq_pinf";
   1.102 +
   1.103 +(*Logical construction of the Property*)
   1.104 +val eq_minf_conjI = thm "eq_minf_conjI";
   1.105 +val eq_minf_disjI = thm "eq_minf_disjI";
   1.106 +val modd_minf_disjI = thm "modd_minf_disjI";
   1.107 +val modd_minf_conjI = thm "modd_minf_conjI";
   1.108 +
   1.109 +val eq_pinf_conjI = thm "eq_pinf_conjI";
   1.110 +val eq_pinf_disjI = thm "eq_pinf_disjI";
   1.111 +val modd_pinf_disjI = thm "modd_pinf_disjI";
   1.112 +val modd_pinf_conjI = thm "modd_pinf_conjI";
   1.113 +
   1.114 +(*A/B - set Theorem *)
   1.115 +
   1.116 +val bst_thm = thm "bst_thm";
   1.117 +val ast_thm = thm "ast_thm";
   1.118 +
   1.119 +(*Cooper Backwards...*)
   1.120 +(*Bset*)
   1.121 +val not_bst_p_fm = thm "not_bst_p_fm";
   1.122 +val not_bst_p_ne = thm "not_bst_p_ne";
   1.123 +val not_bst_p_eq = thm "not_bst_p_eq";
   1.124 +val not_bst_p_gt = thm "not_bst_p_gt";
   1.125 +val not_bst_p_lt = thm "not_bst_p_lt";
   1.126 +val not_bst_p_ndvd = thm "not_bst_p_ndvd";
   1.127 +val not_bst_p_dvd = thm "not_bst_p_dvd";
   1.128 +
   1.129 +(*Aset*)
   1.130 +val not_ast_p_fm = thm "not_ast_p_fm";
   1.131 +val not_ast_p_ne = thm "not_ast_p_ne";
   1.132 +val not_ast_p_eq = thm "not_ast_p_eq";
   1.133 +val not_ast_p_gt = thm "not_ast_p_gt";
   1.134 +val not_ast_p_lt = thm "not_ast_p_lt";
   1.135 +val not_ast_p_ndvd = thm "not_ast_p_ndvd";
   1.136 +val not_ast_p_dvd = thm "not_ast_p_dvd";
   1.137 +
   1.138 +(*Logical construction of the prop*)
   1.139 +(*Bset*)
   1.140 +val not_bst_p_conjI = thm "not_bst_p_conjI";
   1.141 +val not_bst_p_disjI = thm "not_bst_p_disjI";
   1.142 +val not_bst_p_Q_elim = thm "not_bst_p_Q_elim";
   1.143 +
   1.144 +(*Aset*)
   1.145 +val not_ast_p_conjI = thm "not_ast_p_conjI";
   1.146 +val not_ast_p_disjI = thm "not_ast_p_disjI";
   1.147 +val not_ast_p_Q_elim = thm "not_ast_p_Q_elim";
   1.148 +
   1.149 +(*Cooper*)
   1.150 +val cppi_eq = thm "cppi_eq";
   1.151 +val cpmi_eq = thm "cpmi_eq";
   1.152 +
   1.153 +(*Others*)
   1.154 +val simp_from_to = thm "simp_from_to";
   1.155 +val P_eqtrue = thm "P_eqtrue";
   1.156 +val P_eqfalse = thm "P_eqfalse";
   1.157 +
   1.158 +(*For Proving NNF*)
   1.159 +
   1.160 +val nnf_nn = thm "nnf_nn";
   1.161 +val nnf_im = thm "nnf_im";
   1.162 +val nnf_eq = thm "nnf_eq";
   1.163 +val nnf_sdj = thm "nnf_sdj";
   1.164 +val nnf_ncj = thm "nnf_ncj";
   1.165 +val nnf_nim = thm "nnf_nim";
   1.166 +val nnf_neq = thm "nnf_neq";
   1.167 +val nnf_ndj = thm "nnf_ndj";
   1.168 +
   1.169 +(*For Proving term linearizition*)
   1.170 +val linearize_dvd = thm "linearize_dvd";
   1.171 +val lf_lt = thm "lf_lt";
   1.172 +val lf_eq = thm "lf_eq";
   1.173 +val lf_dvd = thm "lf_dvd";
   1.174 +
   1.175 +
   1.176 +
   1.177 +(* ------------------------------------------------------------------------- *)
   1.178 +(*Datatatype declarations for Proofprotocol for the cooperprocedure.*)
   1.179 +(* ------------------------------------------------------------------------- *)
   1.180 +
   1.181 +
   1.182 +
   1.183 +(* ------------------------------------------------------------------------- *)
   1.184 +(*Datatatype declarations for Proofprotocol for the adjustcoeff step.*)
   1.185 +(* ------------------------------------------------------------------------- *)
   1.186 +datatype CpLog = No
   1.187 +                |Simp of term*CpLog
   1.188 +		|Blast of CpLog*CpLog
   1.189 +		|Aset of (term*term*(term list)*term)
   1.190 +		|Bset of (term*term*(term list)*term)
   1.191 +		|Minusinf of CpLog*CpLog
   1.192 +		|Cooper of term*CpLog*CpLog*CpLog
   1.193 +		|Eq_minf of term*term
   1.194 +		|Modd_minf of term*term
   1.195 +		|Eq_minf_conjI of CpLog*CpLog
   1.196 +		|Modd_minf_conjI of CpLog*CpLog	
   1.197 +		|Modd_minf_disjI of CpLog*CpLog
   1.198 +		|Eq_minf_disjI of CpLog*CpLog	
   1.199 +		|Not_bst_p of term*term*term*term*CpLog
   1.200 +		|Not_bst_p_atomic of term
   1.201 +		|Not_bst_p_conjI of CpLog*CpLog
   1.202 +		|Not_bst_p_disjI of CpLog*CpLog
   1.203 +		|Not_ast_p of term*term*term*term*CpLog
   1.204 +		|Not_ast_p_atomic of term
   1.205 +		|Not_ast_p_conjI of CpLog*CpLog
   1.206 +		|Not_ast_p_disjI of CpLog*CpLog
   1.207 +		|CpLogError;
   1.208 +
   1.209 +
   1.210 +
   1.211 +datatype ACLog = ACAt of int*term
   1.212 +                |ACPI of int*term
   1.213 +                |ACfm of term
   1.214 +                |ACNeg of ACLog
   1.215 +		|ACConst of string*ACLog*ACLog;
   1.216 +
   1.217 +
   1.218 +
   1.219 +(* ------------------------------------------------------------------------- *)
   1.220 +(*Datatatype declarations for Proofprotocol for the CNNF step.*)
   1.221 +(* ------------------------------------------------------------------------- *)
   1.222 +
   1.223 +
   1.224 +datatype NNFLog = NNFAt of term
   1.225 +                |NNFSimp of NNFLog
   1.226 +                |NNFNN of NNFLog
   1.227 +		|NNFConst of string*NNFLog*NNFLog;
   1.228 +
   1.229 +(* ------------------------------------------------------------------------- *)
   1.230 +(*Datatatype declarations for Proofprotocol for the linform  step.*)
   1.231 +(* ------------------------------------------------------------------------- *)
   1.232 +
   1.233 +
   1.234 +datatype LfLog = LfAt of term
   1.235 +                |LfAtdvd of term
   1.236 +                |Lffm of term
   1.237 +                |LfConst of string*LfLog*LfLog
   1.238 +		|LfNot of LfLog
   1.239 +		|LfQ of string*string*typ*LfLog;
   1.240 +
   1.241 +
   1.242 +(* ------------------------------------------------------------------------- *)
   1.243 +(*Datatatype declarations for Proofprotocol for the evaluation- evalc-  step.*)
   1.244 +(* ------------------------------------------------------------------------- *)
   1.245 +
   1.246 +
   1.247 +datatype EvalLog = EvalAt of term
   1.248 +                |Evalfm of term
   1.249 +		|EvalConst of string*EvalLog*EvalLog;
   1.250 +
   1.251 +(* ------------------------------------------------------------------------- *)
   1.252 +(*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
   1.253 +(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
   1.254 +(*this is necessary because the theorems use this representation.*)
   1.255 +(* This function should be elminated in next versions...*)
   1.256 +(* ------------------------------------------------------------------------- *)
   1.257 +
   1.258 +fun norm_zero_one fm = case fm of
   1.259 +  (Const ("op *",_) $ c $ t) => 
   1.260 +    if c = one then (norm_zero_one t)
   1.261 +    else if (dest_numeral c = ~1) 
   1.262 +         then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   1.263 +         else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   1.264 +  |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   1.265 +  |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   1.266 +  |_ => fm;
   1.267 +
   1.268 +
   1.269 +(* ------------------------------------------------------------------------- *)
   1.270 +(* Intended to tell that here we changed the structure of the formula with respect to the posineq theorem : ~(0 < t) = 0 < 1-t*)
   1.271 +(* ------------------------------------------------------------------------- *)
   1.272 +fun adjustcoeffeq_wp  x l fm = 
   1.273 +    case fm of  
   1.274 +  (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
   1.275 +  if (x = y) 
   1.276 +  then let  
   1.277 +       val m = l div (dest_numeral c) 
   1.278 +       val n = abs (m)
   1.279 +       val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
   1.280 +       val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   1.281 +       in (ACPI(n,fm),rs)
   1.282 +       end
   1.283 +  else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )) 
   1.284 +        in (ACPI(1,fm),rs)
   1.285 +        end
   1.286 +
   1.287 +  |(Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
   1.288 +      c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
   1.289 +        let val m = l div (dest_numeral c) 
   1.290 +           val n = (if p = "op <" then abs(m) else m)  
   1.291 +           val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
   1.292 +           val rs = (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   1.293 +	   in (ACAt(n,fm),rs)
   1.294 +	   end
   1.295 +        else (ACfm(fm),fm) 
   1.296 +  |( Const ("Not", _) $ p) => let val (rsp,rsr) = adjustcoeffeq_wp x l p 
   1.297 +                              in (ACNeg(rsp),HOLogic.Not $ rsr) 
   1.298 +                              end
   1.299 +  |( Const ("op &",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
   1.300 +                                     val (rsqp,rsqr) = adjustcoeffeq_wp x l q
   1.301 +
   1.302 +                                  in (ACConst ("CJ",rspp,rsqp), HOLogic.mk_conj (rspr,rsqr)) 
   1.303 +                                  end 
   1.304 +  |( Const ("op |",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
   1.305 +                                     val (rsqp,rsqr) = adjustcoeffeq_wp x l q
   1.306 +
   1.307 +                                  in (ACConst ("DJ",rspp,rsqp), HOLogic.mk_disj (rspr,rsqr)) 
   1.308 +                                  end
   1.309 +
   1.310 +  |_ => (ACfm(fm),fm);
   1.311 +
   1.312 +
   1.313 +(*_________________________________________*)
   1.314 +(*-----------------------------------------*)
   1.315 +(* Protocol generation for the liform step *)
   1.316 +(*_________________________________________*)
   1.317 +(*-----------------------------------------*)
   1.318 +
   1.319 +
   1.320 +fun linform_wp fm = 
   1.321 +  let fun at_linform_wp at =
   1.322 +    case at of
   1.323 +      (Const("op <=",_)$s$t) => LfAt(at)
   1.324 +      |(Const("op <",_)$s$t) => LfAt(at)
   1.325 +      |(Const("op =",_)$s$t) => LfAt(at)
   1.326 +      |(Const("Divides.op dvd",_)$s$t) => LfAtdvd(at)
   1.327 +  in
   1.328 +  if is_arith_rel fm 
   1.329 +  then at_linform_wp fm 
   1.330 +  else case fm of
   1.331 +    (Const("Not",_) $ A) => LfNot(linform_wp A)
   1.332 +   |(Const("op &",_)$ A $ B) => LfConst("CJ",linform_wp A, linform_wp B)
   1.333 +   |(Const("op |",_)$ A $ B) => LfConst("DJ",linform_wp A, linform_wp B)
   1.334 +   |(Const("op -->",_)$ A $ B) => LfConst("IM",linform_wp A, linform_wp B)
   1.335 +   |(Const("op =",Type ("fun",[Type ("bool", []),_]))$ A $ B) => LfConst("EQ",linform_wp A, linform_wp B)
   1.336 +   |Const("Ex",_)$Abs(x,T,p) => 
   1.337 +     let val (xn,p1) = variant_abs(x,T,p)
   1.338 +     in LfQ("Ex",xn,T,linform_wp p1)
   1.339 +     end 
   1.340 +   |Const("All",_)$Abs(x,T,p) => 
   1.341 +     let val (xn,p1) = variant_abs(x,T,p)
   1.342 +     in LfQ("All",xn,T,linform_wp p1)
   1.343 +     end 
   1.344 +end;
   1.345 +
   1.346 +
   1.347 +(* ------------------------------------------------------------------------- *)
   1.348 +(*For simlified formulas we just notice the original formula, for whitch we habe been
   1.349 +intendes to make the proof.*)
   1.350 +(* ------------------------------------------------------------------------- *)
   1.351 +fun simpl_wp (fm,pr) = let val fm2 = simpl fm
   1.352 +				in (fm2,Simp(fm,pr))
   1.353 +				end;
   1.354 +
   1.355 +	
   1.356 +(* ------------------------------------------------------------------------- *)
   1.357 +(*Help function for the generation of the proof EX.P_{minus \infty} --> EX. P(x) *)
   1.358 +(* ------------------------------------------------------------------------- *)
   1.359 +fun minusinf_wph x fm = let fun mk_atomar_minusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
   1.360 +  
   1.361 +	      fun combine_minusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
   1.362 +		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
   1.363 +		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
   1.364 +	in 
   1.365 + 
   1.366 + case fm of 
   1.367 + (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.368 +     if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_minusinf_proof x fm))
   1.369 +        else (fm ,(mk_atomar_minusinf_proof x fm))
   1.370 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.371 +  	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
   1.372 +	 then (HOLogic.false_const ,(mk_atomar_minusinf_proof x fm))
   1.373 +	 				 else (fm,(mk_atomar_minusinf_proof x fm)) 
   1.374 + |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
   1.375 +       if (y=x) andalso (c1 = zero) then 
   1.376 +        if c2 = one then (HOLogic.false_const,(mk_atomar_minusinf_proof x fm)) else
   1.377 +	(HOLogic.true_const,(mk_atomar_minusinf_proof x fm))
   1.378 +	else (fm,(mk_atomar_minusinf_proof x fm))
   1.379 +  
   1.380 +  |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_minusinf_proof x fm)
   1.381 +  
   1.382 +  |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_minusinf_proof x fm)
   1.383 +  
   1.384 +  |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
   1.385 +  				    val (qfm,qpr) = minusinf_wph x q
   1.386 +				    val pr = (combine_minusinf_proofs "CJ" ppr qpr)
   1.387 +				     in 
   1.388 +				     (HOLogic.conj $ pfm $qfm , pr)
   1.389 +				     end 
   1.390 +  |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
   1.391 +  				     val (qfm,qpr) = minusinf_wph x q
   1.392 +				     val pr = (combine_minusinf_proofs "DJ" ppr qpr)
   1.393 +				     in 
   1.394 +				     (HOLogic.disj $ pfm $qfm , pr)
   1.395 +				     end 
   1.396 +
   1.397 +  |_ => (fm,(mk_atomar_minusinf_proof x fm))
   1.398 +  
   1.399 +  end;					 
   1.400 +(* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
   1.401 +(* Just combines the to protokols *)
   1.402 +(* ------------------------------------------------------------------------- *)
   1.403 +fun minusinf_wp x fm  = let val (fm2,pr) = (minusinf_wph x fm)
   1.404 +                       in (fm2,Minusinf(pr))
   1.405 +                        end;
   1.406 +
   1.407 +(* ------------------------------------------------------------------------- *)
   1.408 +(*Help function for the generation of the proof EX.P_{plus \infty} --> EX. P(x) *)
   1.409 +(* ------------------------------------------------------------------------- *)
   1.410 +
   1.411 +fun plusinf_wph x fm = let fun mk_atomar_plusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
   1.412 +  
   1.413 +	      fun combine_plusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
   1.414 +		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
   1.415 +		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
   1.416 +	in 
   1.417 + 
   1.418 + case fm of 
   1.419 + (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.420 +     if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_plusinf_proof x fm))
   1.421 +        else (fm ,(mk_atomar_plusinf_proof x fm))
   1.422 + |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.423 +  	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
   1.424 +	 then (HOLogic.false_const ,(mk_atomar_plusinf_proof x fm))
   1.425 +	 				 else (fm,(mk_atomar_plusinf_proof x fm)) 
   1.426 + |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
   1.427 +       if (y=x) andalso (c1 = zero) then 
   1.428 +        if c2 = one then (HOLogic.true_const,(mk_atomar_plusinf_proof x fm)) else
   1.429 +	(HOLogic.false_const,(mk_atomar_plusinf_proof x fm))
   1.430 +	else (fm,(mk_atomar_plusinf_proof x fm))
   1.431 +  
   1.432 +  |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_plusinf_proof x fm)
   1.433 +  
   1.434 +  |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_plusinf_proof x fm)
   1.435 +  
   1.436 +  |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
   1.437 +  				    val (qfm,qpr) = plusinf_wph x q
   1.438 +				    val pr = (combine_plusinf_proofs "CJ" ppr qpr)
   1.439 +				     in 
   1.440 +				     (HOLogic.conj $ pfm $qfm , pr)
   1.441 +				     end 
   1.442 +  |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
   1.443 +  				     val (qfm,qpr) = plusinf_wph x q
   1.444 +				     val pr = (combine_plusinf_proofs "DJ" ppr qpr)
   1.445 +				     in 
   1.446 +				     (HOLogic.disj $ pfm $qfm , pr)
   1.447 +				     end 
   1.448 +
   1.449 +  |_ => (fm,(mk_atomar_plusinf_proof x fm))
   1.450 +  
   1.451 +  end;					 
   1.452 +(* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
   1.453 +(* Just combines the to protokols *)
   1.454 +(* ------------------------------------------------------------------------- *)
   1.455 +fun plusinf_wp x fm  = let val (fm2,pr) = (plusinf_wph x fm)
   1.456 +                       in (fm2,Minusinf(pr))
   1.457 +                        end;
   1.458 +
   1.459 +
   1.460 +(* ------------------------------------------------------------------------- *)
   1.461 +(*Protocol that we here uses Bset.*)
   1.462 +(* ------------------------------------------------------------------------- *)
   1.463 +fun bset_wp x fm = let val bs = bset x fm in
   1.464 +				(bs,Bset(x,fm,bs,mk_numeral (divlcm x fm)))
   1.465 +				end;
   1.466 +
   1.467 +(* ------------------------------------------------------------------------- *)
   1.468 +(*Protocol that we here uses Aset.*)
   1.469 +(* ------------------------------------------------------------------------- *)
   1.470 +fun aset_wp x fm = let val ast = aset x fm in
   1.471 +				(ast,Aset(x,fm,ast,mk_numeral (divlcm x fm)))
   1.472 +				end;
   1.473 + 
   1.474 +
   1.475 +
   1.476 +(* ------------------------------------------------------------------------- *)
   1.477 +(*function list to Set, constructs a set containing all elements of a given list.*)
   1.478 +(* ------------------------------------------------------------------------- *)
   1.479 +fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in 
   1.480 +	case l of 
   1.481 +		[] => Const ("{}",T)
   1.482 +		|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
   1.483 +		end;
   1.484 +		
   1.485 +
   1.486 +(*====================================================================*)
   1.487 +(* ------------------------------------------------------------------------- *)
   1.488 +(* ------------------------------------------------------------------------- *)
   1.489 +(*Protocol for the proof of the backward direction of the cooper theorem.*)
   1.490 +(* Helpfunction - Protokols evereything about the proof reconstruction*)
   1.491 +(* ------------------------------------------------------------------------- *)
   1.492 +fun not_bst_p_wph fm = case fm of
   1.493 +	Const("Not",_) $ R => if (is_arith_rel R) then (Not_bst_p_atomic (fm)) else CpLogError
   1.494 +	|Const("op &",_) $ ls $ rs => Not_bst_p_conjI((not_bst_p_wph ls),(not_bst_p_wph rs))
   1.495 +	|Const("op |",_) $ ls $ rs => Not_bst_p_disjI((not_bst_p_wph ls),(not_bst_p_wph rs))
   1.496 +	|_ => Not_bst_p_atomic (fm);
   1.497 +(* ------------------------------------------------------------------------- *)	
   1.498 +(* 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*)
   1.499 +(* ------------------------------------------------------------------------- *)
   1.500 +fun not_bst_p_wp x fm = let val prt = not_bst_p_wph fm
   1.501 +			    val D = mk_numeral (divlcm x fm)
   1.502 +			    val B = map norm_zero_one (bset x fm)
   1.503 +			in (Not_bst_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
   1.504 +			end;
   1.505 +(*====================================================================*)
   1.506 +(* ------------------------------------------------------------------------- *)
   1.507 +(* ------------------------------------------------------------------------- *)
   1.508 +(*Protocol for the proof of the backward direction of the cooper theorem.*)
   1.509 +(* Helpfunction - Protokols evereything about the proof reconstruction*)
   1.510 +(* ------------------------------------------------------------------------- *)
   1.511 +fun not_ast_p_wph fm = case fm of
   1.512 +	Const("Not",_) $ R => if (is_arith_rel R) then (Not_ast_p_atomic (fm)) else CpLogError
   1.513 +	|Const("op &",_) $ ls $ rs => Not_ast_p_conjI((not_ast_p_wph ls),(not_ast_p_wph rs))
   1.514 +	|Const("op |",_) $ ls $ rs => Not_ast_p_disjI((not_ast_p_wph ls),(not_ast_p_wph rs))
   1.515 +	|_ => Not_ast_p_atomic (fm);
   1.516 +(* ------------------------------------------------------------------------- *)	
   1.517 +(* 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*)
   1.518 +(* ------------------------------------------------------------------------- *)
   1.519 +fun not_ast_p_wp x fm = let val prt = not_ast_p_wph fm
   1.520 +			    val D = mk_numeral (divlcm x fm)
   1.521 +			    val B = map norm_zero_one (aset x fm)
   1.522 +			in (Not_ast_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
   1.523 +			end;
   1.524 +
   1.525 +(*======================================================*)
   1.526 +(* Protokolgeneration for the formula evaluation process*)
   1.527 +(*======================================================*)
   1.528 +
   1.529 +fun evalc_wp fm = 
   1.530 +  let fun evalc_atom_wp at =case at of  
   1.531 +    (Const (p,_) $ s $ t) =>(  
   1.532 +    case assoc (operations,p) of 
   1.533 +        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)))  
   1.534 +		   handle _ => Evalfm(at)) 
   1.535 +        | _ =>  Evalfm(at)) 
   1.536 +     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   1.537 +       case assoc (operations,p) of 
   1.538 +         Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
   1.539 +	  EvalAt(HOLogic.mk_eq(at, HOLogic.false_const))  else EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)))  
   1.540 +		      handle _ => Evalfm(at)) 
   1.541 +         | _ => Evalfm(at)) 
   1.542 +     | _ => Evalfm(at)  
   1.543 + 
   1.544 +  in
   1.545 +   case fm of
   1.546 +    (Const("op &",_)$A$B) => EvalConst("CJ",evalc_wp A,evalc_wp B)
   1.547 +   |(Const("op |",_)$A$B) => EvalConst("DJ",evalc_wp A,evalc_wp B) 
   1.548 +   |(Const("op -->",_)$A$B) => EvalConst("IM",evalc_wp A,evalc_wp B) 
   1.549 +   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => EvalConst("EQ",evalc_wp A,evalc_wp B) 
   1.550 +   |_ => evalc_atom_wp fm
   1.551 +  end;
   1.552 +
   1.553 +
   1.554 +
   1.555 +(*======================================================*)
   1.556 +(* Protokolgeneration for the NNF Transformation        *)
   1.557 +(*======================================================*)
   1.558 +
   1.559 +fun cnnf_wp f = 
   1.560 +  let fun hcnnf_wp fm =
   1.561 +    case fm of
   1.562 +    (Const ("op &",_) $ p $ q) => NNFConst("CJ",hcnnf_wp p,hcnnf_wp q) 
   1.563 +    | (Const ("op |",_) $ p $ q) =>  NNFConst("DJ",hcnnf_wp p,hcnnf_wp q)
   1.564 +    | (Const ("op -->",_) $ p $q) => NNFConst("IM",hcnnf_wp (HOLogic.Not $ p),hcnnf_wp q)
   1.565 +    | (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)))) 
   1.566 +
   1.567 +    | (Const ("Not",_) $ (Const("Not",_) $ p)) => NNFNN(hcnnf_wp p) 
   1.568 +    | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => NNFConst ("NCJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
   1.569 +    | (Const ("Not",_) $(Const ("op |",_) $ (A as (Const ("op &",_) $ p $ q)) $  
   1.570 +    			(B as (Const ("op &",_) $ p1 $ r)))) => if p1 = negate p then 
   1.571 +		         NNFConst("SDJ",  
   1.572 +			   NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q)),
   1.573 +			   NNFConst("CJ",hcnnf_wp p1,hcnnf_wp(HOLogic.Not $ r)))
   1.574 +			 else  NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ A)),(hcnnf_wp(HOLogic.Not $ B))) 
   1.575 +
   1.576 +    | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
   1.577 +    | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) =>  NNFConst ("NIM",(hcnnf_wp(p)),(hcnnf_wp(HOLogic.Not $ q))) 
   1.578 +    | (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))) 
   1.579 +    | _ => NNFAt(fm)  
   1.580 +  in NNFSimp(hcnnf_wp f)
   1.581 +end; 
   1.582 +   
   1.583 +
   1.584 +
   1.585 +
   1.586 +
   1.587 +
   1.588 +(* ------------------------------------------------------------------------- *)
   1.589 +(*Cooper decision Procedure with proof protocoling*)
   1.590 +(* ------------------------------------------------------------------------- *)
   1.591 +
   1.592 +fun coopermi_wp vars fm =
   1.593 +  case fm of
   1.594 +   Const ("Ex",_) $ Abs(xo,T,po) => let 
   1.595 +    val (xn,np) = variant_abs(xo,T,po) 
   1.596 +    val x = (Free(xn , T))
   1.597 +    val p = np     (* Is this a legal proof for the P=NP Problem??*)
   1.598 +    val (p_inf,miprt) = simpl_wp (minusinf_wp x p)
   1.599 +    val (bset,bsprt) = bset_wp x p
   1.600 +    val nbst_p_prt = not_bst_p_wp x p
   1.601 +    val dlcm = divlcm x p 
   1.602 +    val js = 1 upto dlcm 
   1.603 +    fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p 
   1.604 +    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset) 
   1.605 +   in (list_disj (map stage js),Cooper(mk_numeral dlcm,miprt,bsprt,nbst_p_prt))
   1.606 +   end
   1.607 +   
   1.608 +  | _ => (error "cooper: not an existential formula",No);
   1.609 +				
   1.610 +fun cooperpi_wp vars fm =
   1.611 +  case fm of
   1.612 +   Const ("Ex",_) $ Abs(xo,T,po) => let 
   1.613 +    val (xn,np) = variant_abs(xo,T,po) 
   1.614 +    val x = (Free(xn , T))
   1.615 +    val p = np     (* Is this a legal proof for the P=NP Problem??*)
   1.616 +    val (p_inf,piprt) = simpl_wp (plusinf_wp x p)
   1.617 +    val (aset,asprt) = aset_wp x p
   1.618 +    val nast_p_prt = not_ast_p_wp x p
   1.619 +    val dlcm = divlcm x p 
   1.620 +    val js = 1 upto dlcm 
   1.621 +    fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p 
   1.622 +    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset) 
   1.623 +   in (list_disj (map stage js),Cooper(mk_numeral dlcm,piprt,asprt,nast_p_prt))
   1.624 +   end
   1.625 +  | _ => (error "cooper: not an existential formula",No);
   1.626 +				
   1.627 +
   1.628 +
   1.629 +
   1.630 +
   1.631 +(*-----------------------------------------------------------------*)
   1.632 +(*-----------------------------------------------------------------*)
   1.633 +(*-----------------------------------------------------------------*)
   1.634 +(*---                                                           ---*)
   1.635 +(*---                                                           ---*)
   1.636 +(*---      Interpretation and Proofgeneration Part              ---*)
   1.637 +(*---                                                           ---*)
   1.638 +(*---      Protocole interpretation functions                   ---*)
   1.639 +(*---                                                           ---*)
   1.640 +(*---      and proofgeneration functions                        ---*)
   1.641 +(*---                                                           ---*)
   1.642 +(*---                                                           ---*)
   1.643 +(*---                                                           ---*)
   1.644 +(*---                                                           ---*)
   1.645 +(*-----------------------------------------------------------------*)
   1.646 +(*-----------------------------------------------------------------*)
   1.647 +(*-----------------------------------------------------------------*)
   1.648 +
   1.649 +(* ------------------------------------------------------------------------- *)
   1.650 +(* Returns both sides of an equvalence in the theorem*)
   1.651 +(* ------------------------------------------------------------------------- *)
   1.652 +fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
   1.653 +
   1.654 +
   1.655 +(*-------------------------------------------------------------*)
   1.656 +(*-------------------------------------------------------------*)
   1.657 +(*-------------------------------------------------------------*)
   1.658 +(*-------------------------------------------------------------*)
   1.659 +
   1.660 +(* ------------------------------------------------------------------------- *)
   1.661 +(* Modified version of the simple version with minimal amount of checking and postprocessing*)
   1.662 +(* ------------------------------------------------------------------------- *)
   1.663 +
   1.664 +fun simple_prove_goal_cterm2 G tacs =
   1.665 +  let
   1.666 +    fun check None = error "prove_goal: tactic failed"
   1.667 +      | check (Some (thm, _)) = (case nprems_of thm of
   1.668 +            0 => thm
   1.669 +          | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   1.670 +  in check (Seq.pull (EVERY tacs (trivial G))) end;
   1.671 +
   1.672 +(*-------------------------------------------------------------*)
   1.673 +(*-------------------------------------------------------------*)
   1.674 +(*-------------------------------------------------------------*)
   1.675 +(*-------------------------------------------------------------*)
   1.676 +(*-------------------------------------------------------------*)
   1.677 +
   1.678 +fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
   1.679 +
   1.680 +(* ------------------------------------------------------------------------- *)
   1.681 +(*This function proove elementar will be used to generate proofs at runtime*)
   1.682 +(*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
   1.683 +(*prove properties such as a dvd b (essentially) that are only to make at
   1.684 +runtime.*)
   1.685 +(* ------------------------------------------------------------------------- *)
   1.686 +fun prove_elementar sg s fm2 = case s of 
   1.687 +  (*"ss" like simplification with simpset*)
   1.688 +  "ss" =>
   1.689 +    let
   1.690 +      val ss = presburger_ss addsimps
   1.691 +        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
   1.692 +      val ct =  cert_Trueprop sg fm2
   1.693 +    in 
   1.694 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   1.695 +    end
   1.696 +
   1.697 +  (*"bl" like blast tactic*)
   1.698 +  (* Is only used in the harrisons like proof procedure *)
   1.699 +  | "bl" =>
   1.700 +     let val ct = cert_Trueprop sg fm2
   1.701 +     in
   1.702 +       simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
   1.703 +     end
   1.704 +
   1.705 +  (*"ed" like Existence disjunctions ...*)
   1.706 +  (* Is only used in the harrisons like proof procedure *)
   1.707 +  | "ed" =>
   1.708 +    let
   1.709 +      val ex_disj_tacs =
   1.710 +        let
   1.711 +          val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1]
   1.712 +          val tac2 = EVERY[etac exE 1, rtac exI 1,
   1.713 +            REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1]
   1.714 +	in [rtac iffI 1,
   1.715 +          etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
   1.716 +          REPEAT(EVERY[etac disjE 1, tac2]), tac2]
   1.717 +        end
   1.718 +
   1.719 +      val ct = cert_Trueprop sg fm2
   1.720 +    in 
   1.721 +      simple_prove_goal_cterm2 ct ex_disj_tacs
   1.722 +    end
   1.723 +
   1.724 +  | "fa" =>
   1.725 +    let val ct = cert_Trueprop sg fm2
   1.726 +    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
   1.727 +    end
   1.728 +
   1.729 +  | "sa" =>
   1.730 +    let
   1.731 +      val ss = presburger_ss addsimps zadd_ac
   1.732 +      val ct = cert_Trueprop sg fm2
   1.733 +    in 
   1.734 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   1.735 +    end
   1.736 +
   1.737 +  | "ac" =>
   1.738 +    let
   1.739 +      val ss = HOL_basic_ss addsimps zadd_ac
   1.740 +      val ct = cert_Trueprop sg fm2
   1.741 +    in 
   1.742 +      simple_prove_goal_cterm2 ct [simp_tac ss 1]
   1.743 +    end
   1.744 +
   1.745 +  | "lf" =>
   1.746 +    let
   1.747 +      val ss = presburger_ss addsimps zadd_ac
   1.748 +      val ct = cert_Trueprop sg fm2
   1.749 +    in 
   1.750 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   1.751 +    end;
   1.752 +
   1.753 +
   1.754 +
   1.755 +(* ------------------------------------------------------------------------- *)
   1.756 +(* This function return an Isabelle proof, of the adjustcoffeq result.*)
   1.757 +(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   1.758 +(* ------------------------------------------------------------------------- *)
   1.759 +fun proof_of_adjustcoeffeq sg (prt,rs) = case prt of
   1.760 +   ACfm fm => instantiate' [Some cboolT]
   1.761 +    [Some (cterm_of sg fm)] refl
   1.762 + | ACAt (k,at as (Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
   1.763 +      c $ x ) $t ))) => 
   1.764 +   let
   1.765 +     val ck = cterm_of sg (mk_numeral k)
   1.766 +     val cc = cterm_of sg c
   1.767 +     val ct = cterm_of sg t
   1.768 +     val cx = cterm_of sg x
   1.769 +     val ca = cterm_of sg a
   1.770 +   in case p of
   1.771 +     "op <" => let val pre = prove_elementar sg "ss" 
   1.772 +	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
   1.773 +	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
   1.774 +		      in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   1.775 +                   end
   1.776 +    |"op =" =>let val pre = prove_elementar sg "ss" 
   1.777 +	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   1.778 +	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
   1.779 +	             in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   1.780 +                      end
   1.781 +                  end
   1.782 +    |"Divides.op dvd" =>let val pre = prove_elementar sg "ss" 
   1.783 +	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   1.784 +	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
   1.785 +                         in [th1,(prove_elementar sg "ss" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   1.786 +                        
   1.787 +                          end
   1.788 +  end
   1.789 + |ACPI(k,at as (Const("Not",_)$(Const("op <",_) $a $( Const ("op +", _)$(Const ("op *",_) $ c $ x ) $t )))) => 
   1.790 +   let
   1.791 +     val ck = cterm_of sg (mk_numeral k)
   1.792 +     val cc = cterm_of sg c
   1.793 +     val ct = cterm_of sg t
   1.794 +     val cx = cterm_of sg x
   1.795 +     val pre = prove_elementar sg "ss" 
   1.796 +       (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
   1.797 +       val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
   1.798 +
   1.799 +         in [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   1.800 +   end
   1.801 + |ACNeg(pr) => let val (Const("Not",_)$nrs) = rs
   1.802 +               in (proof_of_adjustcoeffeq sg (pr,nrs)) RS (qe_Not) 
   1.803 +               end
   1.804 + |ACConst(s,pr1,pr2) =>
   1.805 +   let val (Const(_,_)$rs1$rs2) = rs
   1.806 +       val th1 = proof_of_adjustcoeffeq sg (pr1,rs1)
   1.807 +       val th2 = proof_of_adjustcoeffeq sg (pr2,rs2)
   1.808 +       in case s of 
   1.809 +	 "CJ" => [th1,th2] MRS (qe_conjI)
   1.810 +         |"DJ" => [th1,th2] MRS (qe_disjI)
   1.811 +         |"IM" => [th1,th2] MRS (qe_impI)
   1.812 +         |"EQ" => [th1,th2] MRS (qe_eqI)
   1.813 +   end;
   1.814 +
   1.815 +
   1.816 +
   1.817 +
   1.818 +
   1.819 +
   1.820 +(* ------------------------------------------------------------------------- *)
   1.821 +(* This function return an Isabelle proof, of some properties on the atoms*)
   1.822 +(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   1.823 +(* This function doese only instantiate the the theorems in the theory *)
   1.824 +(* ------------------------------------------------------------------------- *)
   1.825 +fun atomar_minf_proof_of sg dlcm (Modd_minf (x,fm1)) =
   1.826 +  let
   1.827 +    (*Some certified Terms*)
   1.828 +    
   1.829 +   val ctrue = cterm_of sg HOLogic.true_const
   1.830 +   val cfalse = cterm_of sg HOLogic.false_const
   1.831 +   val fm = norm_zero_one fm1
   1.832 +  in  case fm1 of 
   1.833 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.834 +         if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   1.835 +           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.836 +
   1.837 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.838 +  	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
   1.839 +	   then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf))
   1.840 +	 	 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)) 
   1.841 +
   1.842 +      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.843 +           if (y=x) andalso (c1 = zero) then 
   1.844 +            if (pm1 = one) then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf)) else
   1.845 +	     (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   1.846 +	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.847 +  
   1.848 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.849 +         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.850 +			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.851 +	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
   1.852 +		      end
   1.853 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.854 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   1.855 +      c $ y ) $ z))) => 
   1.856 +         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.857 +			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.858 +	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
   1.859 +		      end
   1.860 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.861 +		
   1.862 +    
   1.863 +   |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
   1.864 +   end	
   1.865 +
   1.866 + |atomar_minf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
   1.867 +       (*Some certified types*)
   1.868 +   val fm = norm_zero_one fm1
   1.869 +    in  case fm1 of 
   1.870 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.871 +         if  (x=y) andalso (c1=zero) andalso (c2=one) 
   1.872 +	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   1.873 +           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.874 +
   1.875 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.876 +  	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
   1.877 +	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
   1.878 +	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf)) 
   1.879 +
   1.880 +      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.881 +           if (y=x) andalso (c1 =zero) then 
   1.882 +            if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
   1.883 +	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_minf))
   1.884 +	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.885 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.886 +         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.887 +	 		  val cz = cterm_of sg (norm_zero_one z)
   1.888 +	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_minf)) 
   1.889 +		      end
   1.890 +
   1.891 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.892 +		
   1.893 +      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.894 +         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.895 +	 		  val cz = cterm_of sg (norm_zero_one z)
   1.896 +	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_minf))
   1.897 +		      end
   1.898 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.899 +
   1.900 +      		
   1.901 +    |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.902 + end;
   1.903 +
   1.904 +
   1.905 +(* ------------------------------------------------------------------------- *)
   1.906 +(* This function combines proofs of some special form already synthetised from the subtrees to make*)
   1.907 +(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
   1.908 +(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
   1.909 +(* These are Theorems for the Property of P_{-infty}*)
   1.910 +(* ------------------------------------------------------------------------- *)
   1.911 +fun combine_minf_proof s pr1 pr2 = case s of
   1.912 +    "ECJ" => [pr1 , pr2] MRS (eq_minf_conjI)
   1.913 +
   1.914 +   |"EDJ" => [pr1 , pr2] MRS (eq_minf_disjI)
   1.915 +   
   1.916 +   |"MCJ" => [pr1 , pr2] MRS (modd_minf_conjI)
   1.917 +
   1.918 +   |"MDJ" => [pr1 , pr2] MRS (modd_minf_disjI);
   1.919 +
   1.920 +(* ------------------------------------------------------------------------- *)
   1.921 +(*This function return an isabelle Proof for the minusinfinity theorem*)
   1.922 +(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
   1.923 +(* ------------------------------------------------------------------------- *)
   1.924 +fun minf_proof_ofh sg dlcm prl = case prl of 
   1.925 +
   1.926 +    Eq_minf (_) => atomar_minf_proof_of sg dlcm prl
   1.927 +    
   1.928 +   |Modd_minf (_) => atomar_minf_proof_of sg dlcm prl
   1.929 +   
   1.930 +   |Eq_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   1.931 +   				    val pr2 = minf_proof_ofh sg dlcm prl2
   1.932 +				 in (combine_minf_proof "ECJ" pr1 pr2)
   1.933 +				 end
   1.934 +				 
   1.935 +   |Eq_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   1.936 +   				    val pr2 = minf_proof_ofh sg dlcm prl2
   1.937 +				 in (combine_minf_proof "EDJ" pr1 pr2)
   1.938 +				 end
   1.939 +				 
   1.940 +   |Modd_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   1.941 +   				    val pr2 = minf_proof_ofh sg dlcm prl2
   1.942 +				 in (combine_minf_proof "MCJ" pr1 pr2)
   1.943 +				 end
   1.944 +				 
   1.945 +   |Modd_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   1.946 +   				    val pr2 = minf_proof_ofh sg dlcm prl2
   1.947 +				 in (combine_minf_proof "MDJ" pr1 pr2)
   1.948 +				 end;
   1.949 +(* ------------------------------------------------------------------------- *)
   1.950 +(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
   1.951 +(* ------------------------------------------------------------------------- *)
   1.952 +fun  minf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
   1.953 +  let val pr1 = minf_proof_ofh sg dlcm prl1
   1.954 +      val pr2 = minf_proof_ofh sg dlcm prl2
   1.955 +  in (pr1, pr2)
   1.956 +end;
   1.957 +				 
   1.958 +
   1.959 +
   1.960 +
   1.961 +(* ------------------------------------------------------------------------- *)
   1.962 +(* This function return an Isabelle proof, of some properties on the atoms*)
   1.963 +(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   1.964 +(* This function doese only instantiate the the theorems in the theory *)
   1.965 +(* ------------------------------------------------------------------------- *)
   1.966 +fun atomar_pinf_proof_of sg dlcm (Modd_minf (x,fm1)) =
   1.967 + let
   1.968 +    (*Some certified Terms*)
   1.969 +    
   1.970 +  val ctrue = cterm_of sg HOLogic.true_const
   1.971 +  val cfalse = cterm_of sg HOLogic.false_const
   1.972 +  val fm = norm_zero_one fm1
   1.973 + in  case fm1 of 
   1.974 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.975 +         if ((x=y) andalso (c1= zero) andalso (c2= one))
   1.976 +	 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
   1.977 +         else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.978 +
   1.979 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.980 +  	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
   1.981 +	then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   1.982 +	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.983 +
   1.984 +      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.985 +        if ((y=x) andalso (c1 = zero)) then 
   1.986 +          if (pm1 = one) 
   1.987 +	  then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf)) 
   1.988 +	  else (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   1.989 +	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.990 +  
   1.991 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.992 +         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.993 +			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.994 +	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
   1.995 +		      end
   1.996 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.997 +      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   1.998 +      c $ y ) $ z))) => 
   1.999 +         if y=x then  let val cz = cterm_of sg (norm_zero_one z)
  1.1000 +			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
  1.1001 +	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
  1.1002 +		      end
  1.1003 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
  1.1004 +		
  1.1005 +    
  1.1006 +   |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
  1.1007 +   end	
  1.1008 +
  1.1009 + |atomar_pinf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
  1.1010 +					val fm = norm_zero_one fm1
  1.1011 +    in  case fm1 of 
  1.1012 +      (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1.1013 +         if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1.1014 +	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
  1.1015 +           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1.1016 +
  1.1017 +      |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1.1018 +  	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
  1.1019 +	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
  1.1020 +	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf)) 
  1.1021 +
  1.1022 +      |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1.1023 +           if (y=x) andalso (c1 =zero) then 
  1.1024 +            if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
  1.1025 +	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
  1.1026 +	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1.1027 +      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1028 +         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  1.1029 +	 		  val cz = cterm_of sg (norm_zero_one z)
  1.1030 +	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_pinf)) 
  1.1031 +		      end
  1.1032 +
  1.1033 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1.1034 +		
  1.1035 +      |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1036 +         if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  1.1037 +	 		  val cz = cterm_of sg (norm_zero_one z)
  1.1038 +	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_pinf))
  1.1039 +		      end
  1.1040 +		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1.1041 +
  1.1042 +      		
  1.1043 +    |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1.1044 + end;
  1.1045 +
  1.1046 +
  1.1047 +(* ------------------------------------------------------------------------- *)
  1.1048 +(* This function combines proofs of some special form already synthetised from the subtrees to make*)
  1.1049 +(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
  1.1050 +(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
  1.1051 +(* These are Theorems for the Property of P_{+infty}*)
  1.1052 +(* ------------------------------------------------------------------------- *)
  1.1053 +fun combine_pinf_proof s pr1 pr2 = case s of
  1.1054 +    "ECJ" => [pr1 , pr2] MRS (eq_pinf_conjI)
  1.1055 +
  1.1056 +   |"EDJ" => [pr1 , pr2] MRS (eq_pinf_disjI)
  1.1057 +   
  1.1058 +   |"MCJ" => [pr1 , pr2] MRS (modd_pinf_conjI)
  1.1059 +
  1.1060 +   |"MDJ" => [pr1 , pr2] MRS (modd_pinf_disjI);
  1.1061 +
  1.1062 +(* ------------------------------------------------------------------------- *)
  1.1063 +(*This function return an isabelle Proof for the minusinfinity theorem*)
  1.1064 +(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
  1.1065 +(* ------------------------------------------------------------------------- *)
  1.1066 +fun pinf_proof_ofh sg dlcm prl = case prl of 
  1.1067 +
  1.1068 +    Eq_minf (_) => atomar_pinf_proof_of sg dlcm prl
  1.1069 +    
  1.1070 +   |Modd_minf (_) => atomar_pinf_proof_of sg dlcm prl
  1.1071 +   
  1.1072 +   |Eq_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1.1073 +   				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1.1074 +				 in (combine_pinf_proof "ECJ" pr1 pr2)
  1.1075 +				 end
  1.1076 +				 
  1.1077 +   |Eq_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1.1078 +   				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1.1079 +				 in (combine_pinf_proof "EDJ" pr1 pr2)
  1.1080 +				 end
  1.1081 +				 
  1.1082 +   |Modd_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1.1083 +   				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1.1084 +				 in (combine_pinf_proof "MCJ" pr1 pr2)
  1.1085 +				 end
  1.1086 +				 
  1.1087 +   |Modd_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1.1088 +   				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1.1089 +				 in (combine_pinf_proof "MDJ" pr1 pr2)
  1.1090 +				 end;
  1.1091 +(* ------------------------------------------------------------------------- *)
  1.1092 +(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
  1.1093 +(* ------------------------------------------------------------------------- *)
  1.1094 +fun pinf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
  1.1095 +  let val pr1 = pinf_proof_ofh sg dlcm prl1
  1.1096 +      val pr2 = pinf_proof_ofh sg dlcm prl2
  1.1097 +  in (pr1, pr2)
  1.1098 +end;
  1.1099 +				 
  1.1100 +
  1.1101 +
  1.1102 +
  1.1103 +(* ------------------------------------------------------------------------- *)
  1.1104 +(* Here we generate the theorem for the Bset Property in the simple direction*)
  1.1105 +(* It is just an instantiation*)
  1.1106 +(* ------------------------------------------------------------------------- *)
  1.1107 +fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
  1.1108 +  let
  1.1109 +    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1.1110 +    val cdlcm = cterm_of sg dlcm
  1.1111 +    val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
  1.1112 +  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
  1.1113 +    end;
  1.1114 +
  1.1115 +
  1.1116 +
  1.1117 +
  1.1118 +(* ------------------------------------------------------------------------- *)
  1.1119 +(* Here we generate the theorem for the Bset Property in the simple direction*)
  1.1120 +(* It is just an instantiation*)
  1.1121 +(* ------------------------------------------------------------------------- *)
  1.1122 +fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
  1.1123 +  let
  1.1124 +    val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1.1125 +    val cdlcm = cterm_of sg dlcm
  1.1126 +    val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
  1.1127 +  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
  1.1128 +end;
  1.1129 +
  1.1130 +
  1.1131 +
  1.1132 +
  1.1133 +(* ------------------------------------------------------------------------- *)    
  1.1134 +(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
  1.1135 +
  1.1136 +(* For the generation of atomic Theorems*)
  1.1137 +(* Prove the premisses on runtime and then make RS*)
  1.1138 +(* ------------------------------------------------------------------------- *)
  1.1139 +fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = 
  1.1140 +  let
  1.1141 +    val cdlcm = cterm_of sg dlcm
  1.1142 +    val cB = cterm_of sg B
  1.1143 +    val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1.1144 +    val cat = cterm_of sg (norm_zero_one at)
  1.1145 +  in
  1.1146 +  case at of 
  1.1147 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1.1148 +      if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1.1149 +	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
  1.1150 +	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  1.1151 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1152 +	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
  1.1153 +	 end
  1.1154 +         else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1155 +
  1.1156 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1.1157 +     if (is_arith_rel at) andalso (x=y)
  1.1158 +	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
  1.1159 +	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
  1.1160 +	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  1.1161 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1162 +	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
  1.1163 +	 end
  1.1164 +       end
  1.1165 +         else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1166 +
  1.1167 +   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1.1168 +        if (y=x) andalso (c1 =zero) then 
  1.1169 +        if pm1 = one then 
  1.1170 +	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
  1.1171 +              val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
  1.1172 +	  in  (instantiate' [] [Some cfma,  Some cdlcm]([th1,th2] MRS (not_bst_p_gt)))
  1.1173 +	    end
  1.1174 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1175 +	      in (instantiate' [] [Some cfma, Some cB,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
  1.1176 +	      end
  1.1177 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1178 +
  1.1179 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1180 +      if y=x then  
  1.1181 +           let val cz = cterm_of sg (norm_zero_one z)
  1.1182 +	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  1.1183 + 	     in (instantiate' []  [Some cfma, Some cB,Some cz] (th1 RS (not_bst_p_ndvd)))
  1.1184 +	     end
  1.1185 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1186 +
  1.1187 +   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1188 +       if y=x then  
  1.1189 +	 let val cz = cterm_of sg (norm_zero_one z)
  1.1190 +	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  1.1191 + 	    in (instantiate' []  [Some cfma,Some cB,Some cz] (th1 RS (not_bst_p_dvd)))
  1.1192 +	  end
  1.1193 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1194 +      		
  1.1195 +   |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1.1196 +      		
  1.1197 +    end;
  1.1198 +    
  1.1199 +(* ------------------------------------------------------------------------- *)    
  1.1200 +(* Main interpretation function for this backwards dirction*)
  1.1201 +(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
  1.1202 +(*Help Function*)
  1.1203 +(* ------------------------------------------------------------------------- *)
  1.1204 +fun not_bst_p_proof_of_h sg x fm dlcm B prt = case prt of 
  1.1205 +	(Not_bst_p_atomic(fm2)) => (generate_atomic_not_bst_p sg x fm dlcm B fm2)
  1.1206 +	
  1.1207 +	|(Not_bst_p_conjI(pr1,pr2)) => 
  1.1208 +			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
  1.1209 +			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
  1.1210 +			    in ([th1,th2] MRS (not_bst_p_conjI))
  1.1211 +			    end
  1.1212 +
  1.1213 +	|(Not_bst_p_disjI(pr1,pr2)) => 
  1.1214 +			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
  1.1215 +			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
  1.1216 +			    in ([th1,th2] MRS not_bst_p_disjI)
  1.1217 +			    end;
  1.1218 +(* Main function*)
  1.1219 +fun not_bst_p_proof_of sg (Not_bst_p(x as Free(xn,xT),fm,dlcm,B,prl)) =
  1.1220 +  let val th =  not_bst_p_proof_of_h sg x fm dlcm B prl
  1.1221 +      val fma = absfree (xn,xT, norm_zero_one fm)
  1.1222 +  in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
  1.1223 +     in [th,th1] MRS (not_bst_p_Q_elim)
  1.1224 +     end
  1.1225 +  end;
  1.1226 +
  1.1227 +
  1.1228 +(* ------------------------------------------------------------------------- *)    
  1.1229 +(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
  1.1230 +
  1.1231 +(* For the generation of atomic Theorems*)
  1.1232 +(* Prove the premisses on runtime and then make RS*)
  1.1233 +(* ------------------------------------------------------------------------- *)
  1.1234 +fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = 
  1.1235 +  let
  1.1236 +    val cdlcm = cterm_of sg dlcm
  1.1237 +    val cA = cterm_of sg A
  1.1238 +    val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1.1239 +    val cat = cterm_of sg (norm_zero_one at)
  1.1240 +  in
  1.1241 +  case at of 
  1.1242 +   (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1.1243 +      if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1.1244 +	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
  1.1245 +	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
  1.1246 +		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1247 +	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
  1.1248 +	 end
  1.1249 +         else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1250 +
  1.1251 +   |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1.1252 +     if (is_arith_rel at) andalso (x=y)
  1.1253 +	then let val ast_z = norm_zero_one (linear_sub [] one z )
  1.1254 +	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
  1.1255 +	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
  1.1256 +		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1257 +	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
  1.1258 +       end
  1.1259 +         else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1260 +
  1.1261 +   |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1.1262 +        if (y=x) andalso (c1 =zero) then 
  1.1263 +        if pm1 = (mk_numeral ~1) then 
  1.1264 +	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
  1.1265 +              val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
  1.1266 +	  in  (instantiate' [] [Some cfma]([th2,th1] MRS (not_ast_p_lt)))
  1.1267 +	    end
  1.1268 +	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1.1269 +	      in (instantiate' [] [Some cfma, Some cA,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
  1.1270 +	      end
  1.1271 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1272 +
  1.1273 +   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1274 +      if y=x then  
  1.1275 +           let val cz = cterm_of sg (norm_zero_one z)
  1.1276 +	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  1.1277 + 	     in (instantiate' []  [Some cfma, Some cA,Some cz] (th1 RS (not_ast_p_ndvd)))
  1.1278 +	     end
  1.1279 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1280 +
  1.1281 +   |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1.1282 +       if y=x then  
  1.1283 +	 let val cz = cterm_of sg (norm_zero_one z)
  1.1284 +	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  1.1285 + 	    in (instantiate' []  [Some cfma,Some cA,Some cz] (th1 RS (not_ast_p_dvd)))
  1.1286 +	  end
  1.1287 +      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1288 +      		
  1.1289 +   |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1.1290 +      		
  1.1291 +    end;
  1.1292 +    
  1.1293 +(* ------------------------------------------------------------------------- *)    
  1.1294 +(* Main interpretation function for this backwards dirction*)
  1.1295 +(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
  1.1296 +(*Help Function*)
  1.1297 +(* ------------------------------------------------------------------------- *)
  1.1298 +fun not_ast_p_proof_of_h sg x fm dlcm A prt = case prt of 
  1.1299 +	(Not_ast_p_atomic(fm2)) => (generate_atomic_not_ast_p sg x fm dlcm A fm2)
  1.1300 +	
  1.1301 +	|(Not_ast_p_conjI(pr1,pr2)) => 
  1.1302 +			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
  1.1303 +			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
  1.1304 +			    in ([th1,th2] MRS (not_ast_p_conjI))
  1.1305 +			    end
  1.1306 +
  1.1307 +	|(Not_ast_p_disjI(pr1,pr2)) => 
  1.1308 +			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
  1.1309 +			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
  1.1310 +			    in ([th1,th2] MRS (not_ast_p_disjI))
  1.1311 +			    end;
  1.1312 +(* Main function*)
  1.1313 +fun not_ast_p_proof_of sg (Not_ast_p(x as Free(xn,xT),fm,dlcm,A,prl)) =
  1.1314 +  let val th =  not_ast_p_proof_of_h sg x fm dlcm A prl
  1.1315 +      val fma = absfree (xn,xT, norm_zero_one fm)
  1.1316 +      val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
  1.1317 +  in [th,th1] MRS (not_ast_p_Q_elim)
  1.1318 +end;
  1.1319 +
  1.1320 +
  1.1321 +
  1.1322 +
  1.1323 +(* ------------------------------------------------------------------------- *)
  1.1324 +(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
  1.1325 +(* ------------------------------------------------------------------------- *)
  1.1326 +
  1.1327 +
  1.1328 +fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
  1.1329 +  (* Get the Bset thm*)
  1.1330 +  let val bst = bsetproof_of sg bsprt
  1.1331 +      val (mit1,mit2) = minf_proof_of sg dlcm miprt
  1.1332 +      val fm1 = norm_zero_one (simpl fm) 
  1.1333 +      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
  1.1334 +      val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
  1.1335 +    (* Return the four theorems needed to proove the whole Cooper Theorem*)
  1.1336 +  in (dpos,mit2,bst,nbstpthm,mit1)
  1.1337 +end;
  1.1338 +
  1.1339 +
  1.1340 +(* ------------------------------------------------------------------------- *)
  1.1341 +(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
  1.1342 +(* ------------------------------------------------------------------------- *)
  1.1343 +
  1.1344 +
  1.1345 +fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
  1.1346 +  let val ast = asetproof_of sg bsprt
  1.1347 +      val (mit1,mit2) = pinf_proof_of sg dlcm miprt
  1.1348 +      val fm1 = norm_zero_one (simpl fm) 
  1.1349 +      val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
  1.1350 +      val nastpthm = not_ast_p_proof_of sg nast_p_prt
  1.1351 +  in (dpos,mit2,ast,nastpthm,mit1)
  1.1352 +end;
  1.1353 +
  1.1354 +
  1.1355 +(* ------------------------------------------------------------------------- *)
  1.1356 +(* Interpretaion of Protocols of the cooper procedure : full version*)
  1.1357 +(* ------------------------------------------------------------------------- *)
  1.1358 +
  1.1359 +
  1.1360 +
  1.1361 +fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
  1.1362 +  "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
  1.1363 +	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
  1.1364 +		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
  1.1365 +           end
  1.1366 +  |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
  1.1367 +	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
  1.1368 +		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
  1.1369 +                end
  1.1370 + |_ => error "parameter error";
  1.1371 +
  1.1372 +(* ------------------------------------------------------------------------- *)
  1.1373 +(* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
  1.1374 +(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
  1.1375 +(* ------------------------------------------------------------------------- *)
  1.1376 +
  1.1377 +fun cooper_prv sg (x as Free(xn,xT)) efm vars = let 
  1.1378 +   val l = formlcm x efm
  1.1379 +   val ac_thm = proof_of_adjustcoeffeq sg (adjustcoeffeq_wp  x l efm)
  1.1380 +   val fm = snd (qe_get_terms ac_thm)
  1.1381 +   val  cfm = unitycoeff x fm
  1.1382 +   val afm = adjustcoeff x l fm
  1.1383 +   val P = absfree(xn,xT,afm)
  1.1384 +   val ss = presburger_ss addsimps
  1.1385 +     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
  1.1386 +   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
  1.1387 +   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
  1.1388 +   val cms = if ((length (aset x cfm)) < (length (bset x cfm))) then "pi" else "mi"
  1.1389 +   val cp_thm = cooper_thm sg cms x vars cfm
  1.1390 +   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
  1.1391 +   val (lsuth,rsuth) = qe_get_terms (uth)
  1.1392 +   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
  1.1393 +   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
  1.1394 +   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
  1.1395 + in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
  1.1396 +   end
  1.1397 +|cooper_prv _ _ _ _ = error "Parameters format";
  1.1398 +
  1.1399 +
  1.1400 +(*====================================================*)
  1.1401 +(*Interpretation function for the evaluation protokol *)
  1.1402 +(*====================================================*)
  1.1403 +
  1.1404 +fun proof_of_evalc sg fm =
  1.1405 +let
  1.1406 +fun proof_of_evalch prt = case prt of
  1.1407 +  EvalAt(at) => prove_elementar sg "ss" at
  1.1408 + |Evalfm(fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
  1.1409 + |EvalConst(s,pr1,pr2) => 
  1.1410 +   let val th1 = proof_of_evalch pr1
  1.1411 +       val th2 = proof_of_evalch pr2
  1.1412 +   in case s of
  1.1413 +     "CJ" =>[th1,th2] MRS (qe_conjI)
  1.1414 +    |"DJ" =>[th1,th2] MRS (qe_disjI)
  1.1415 +    |"IM" =>[th1,th2] MRS (qe_impI)
  1.1416 +    |"EQ" =>[th1,th2] MRS (qe_eqI)
  1.1417 +    end
  1.1418 +in proof_of_evalch (evalc_wp fm)
  1.1419 +end;
  1.1420 +
  1.1421 +(*============================================================*)
  1.1422 +(*Interpretation function for the NNF-Transformation protokol *)
  1.1423 +(*============================================================*)
  1.1424 +
  1.1425 +fun proof_of_cnnf sg fm pf = 
  1.1426 +let fun proof_of_cnnfh prt pat = case prt of
  1.1427 +  NNFAt(at) => pat at
  1.1428 + |NNFSimp (pr) => let val th1 = proof_of_cnnfh pr pat
  1.1429 +                  in let val fm2 = snd (qe_get_terms th1) 
  1.1430 +		     in [th1,prove_elementar sg "ss" (HOLogic.mk_eq(fm2 ,simpl fm2))] MRS trans
  1.1431 +                     end
  1.1432 +                  end
  1.1433 + |NNFNN (pr) => (proof_of_cnnfh pr pat) RS (nnf_nn)
  1.1434 + |NNFConst (s,pr1,pr2) =>
  1.1435 +   let val th1 = proof_of_cnnfh pr1 pat
  1.1436 +       val th2 = proof_of_cnnfh pr2 pat
  1.1437 +   in case s of
  1.1438 +     "CJ" => [th1,th2] MRS (qe_conjI)
  1.1439 +    |"DJ" => [th1,th2] MRS (qe_disjI)
  1.1440 +    |"IM" => [th1,th2] MRS (nnf_im)
  1.1441 +    |"EQ" => [th1,th2] MRS (nnf_eq)
  1.1442 +    |"SDJ" => let val (Const("op &",_)$A$_) = fst (qe_get_terms th1)
  1.1443 +	          val (Const("op &",_)$C$_) = fst (qe_get_terms th2)
  1.1444 +	      in [th1,th2,prove_elementar sg "ss" (HOLogic.mk_eq (A,HOLogic.Not $ C))] MRS (nnf_sdj)
  1.1445 +	      end
  1.1446 +    |"NCJ" => [th1,th2] MRS (nnf_ncj)
  1.1447 +    |"NIM" => [th1,th2] MRS (nnf_nim)
  1.1448 +    |"NEQ" => [th1,th2] MRS (nnf_neq)
  1.1449 +    |"NDJ" => [th1,th2] MRS (nnf_ndj)
  1.1450 +   end
  1.1451 +in proof_of_cnnfh (cnnf_wp fm) pf
  1.1452 +end;
  1.1453 +
  1.1454 +
  1.1455 +
  1.1456 +
  1.1457 +(*====================================================*)
  1.1458 +(* Interpretation function for the linform protokol   *)
  1.1459 +(*====================================================*)
  1.1460 +
  1.1461 +
  1.1462 +fun proof_of_linform sg vars f = 
  1.1463 +  let fun proof_of_linformh prt = 
  1.1464 +  case prt of
  1.1465 +    (LfAt (at)) =>  prove_elementar sg "lf" (HOLogic.mk_eq (at, linform vars at))
  1.1466 +   |(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))
  1.1467 +   |(Lffm (fm)) => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
  1.1468 +   |(LfConst (s,pr1,pr2)) =>
  1.1469 +     let val th1 = proof_of_linformh pr1
  1.1470 +	 val th2 = proof_of_linformh pr2
  1.1471 +     in case s of
  1.1472 +       "CJ" => [th1,th2] MRS (qe_conjI)
  1.1473 +      |"DJ" =>[th1,th2] MRS (qe_disjI)
  1.1474 +      |"IM" =>[th1,th2] MRS (qe_impI)
  1.1475 +      |"EQ" =>[th1,th2] MRS (qe_eqI)
  1.1476 +     end
  1.1477 +   |(LfNot(pr)) => 
  1.1478 +     let val th = proof_of_linformh pr
  1.1479 +     in (th RS (qe_Not))
  1.1480 +     end
  1.1481 +   |(LfQ(s,xn,xT,pr)) => 
  1.1482 +     let val th = forall_intr (cterm_of sg (Free(xn,xT)))(proof_of_linformh pr)
  1.1483 +     in if s = "Ex" 
  1.1484 +        then (th COMP(qe_exI) )
  1.1485 +        else (th COMP(qe_ALLI) )
  1.1486 +     end
  1.1487 +in
  1.1488 + proof_of_linformh (linform_wp f)
  1.1489 +end;
  1.1490 +
  1.1491 +end;