src/HOL/Integ/cooper_proof.ML
author berghofe
Tue Apr 08 09:44:21 2003 +0200 (2003-04-08)
changeset 13905 3e496c70f2f3
parent 13876 68f4ed8311ac
child 14139 ca3dd7ed5ac5
permissions -rw-r--r--
Fixed bug in adjustcoeffeq_wp.
     1 (*  Title:      HOL/Integ/cooper_proof.ML
     2     ID:         $Id$
     3     Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 File containing the implementation of the proof
     7 generation for Cooper Algorithm
     8 *)
     9 
    10 signature COOPER_PROOF =
    11 sig
    12   val qe_Not : thm
    13   val qe_conjI : thm
    14   val qe_disjI : thm
    15   val qe_impI : thm
    16   val qe_eqI : thm
    17   val qe_exI : thm
    18   val qe_get_terms : thm -> term * term
    19   val cooper_prv : Sign.sg -> term -> term -> string list -> thm
    20   val proof_of_evalc : Sign.sg -> term -> thm
    21   val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
    22   val proof_of_linform : Sign.sg -> string list -> term -> thm
    23 end;
    24 
    25 structure CooperProof : COOPER_PROOF =
    26 struct
    27 
    28 open CooperDec;
    29 
    30 (*-----------------------------------------------------------------*)
    31 (*-----------------------------------------------------------------*)
    32 (*-----------------------------------------------------------------*)
    33 (*---                                                           ---*)
    34 (*---                                                           ---*)
    35 (*---         Protocoling part                                  ---*)
    36 (*---                                                           ---*)
    37 (*---           includes the protocolling datastructure         ---*)
    38 (*---                                                           ---*)
    39 (*---          and the protocolling fuctions                    ---*)
    40 (*---                                                           ---*)
    41 (*---                                                           ---*)
    42 (*-----------------------------------------------------------------*)
    43 (*-----------------------------------------------------------------*)
    44 (*-----------------------------------------------------------------*)
    45 
    46 val presburger_ss = simpset_of (theory "Presburger")
    47   addsimps [zdiff_def] delsimps [symmetric zdiff_def];
    48 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    49 
    50 (*Theorems that will be used later for the proofgeneration*)
    51 
    52 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
    53 val unity_coeff_ex = thm "unity_coeff_ex";
    54 
    55 (* Thorems for proving the adjustment of the coeffitients*)
    56 
    57 val ac_lt_eq =  thm "ac_lt_eq";
    58 val ac_eq_eq = thm "ac_eq_eq";
    59 val ac_dvd_eq = thm "ac_dvd_eq";
    60 val ac_pi_eq = thm "ac_pi_eq";
    61 
    62 (* The logical compination of the sythetised properties*)
    63 val qe_Not = thm "qe_Not";
    64 val qe_conjI = thm "qe_conjI";
    65 val qe_disjI = thm "qe_disjI";
    66 val qe_impI = thm "qe_impI";
    67 val qe_eqI = thm "qe_eqI";
    68 val qe_exI = thm "qe_exI";
    69 val qe_ALLI = thm "qe_ALLI";
    70 
    71 (*Modulo D property for Pminusinf an Plusinf *)
    72 val fm_modd_minf = thm "fm_modd_minf";
    73 val not_dvd_modd_minf = thm "not_dvd_modd_minf";
    74 val dvd_modd_minf = thm "dvd_modd_minf";
    75 
    76 val fm_modd_pinf = thm "fm_modd_pinf";
    77 val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
    78 val dvd_modd_pinf = thm "dvd_modd_pinf";
    79 
    80 (* the minusinfinity proprty*)
    81 
    82 val fm_eq_minf = thm "fm_eq_minf";
    83 val neq_eq_minf = thm "neq_eq_minf";
    84 val eq_eq_minf = thm "eq_eq_minf";
    85 val le_eq_minf = thm "le_eq_minf";
    86 val len_eq_minf = thm "len_eq_minf";
    87 val not_dvd_eq_minf = thm "not_dvd_eq_minf";
    88 val dvd_eq_minf = thm "dvd_eq_minf";
    89 
    90 (* the Plusinfinity proprty*)
    91 
    92 val fm_eq_pinf = thm "fm_eq_pinf";
    93 val neq_eq_pinf = thm "neq_eq_pinf";
    94 val eq_eq_pinf = thm "eq_eq_pinf";
    95 val le_eq_pinf = thm "le_eq_pinf";
    96 val len_eq_pinf = thm "len_eq_pinf";
    97 val not_dvd_eq_pinf = thm "not_dvd_eq_pinf";
    98 val dvd_eq_pinf = thm "dvd_eq_pinf";
    99 
   100 (*Logical construction of the Property*)
   101 val eq_minf_conjI = thm "eq_minf_conjI";
   102 val eq_minf_disjI = thm "eq_minf_disjI";
   103 val modd_minf_disjI = thm "modd_minf_disjI";
   104 val modd_minf_conjI = thm "modd_minf_conjI";
   105 
   106 val eq_pinf_conjI = thm "eq_pinf_conjI";
   107 val eq_pinf_disjI = thm "eq_pinf_disjI";
   108 val modd_pinf_disjI = thm "modd_pinf_disjI";
   109 val modd_pinf_conjI = thm "modd_pinf_conjI";
   110 
   111 (*A/B - set Theorem *)
   112 
   113 val bst_thm = thm "bst_thm";
   114 val ast_thm = thm "ast_thm";
   115 
   116 (*Cooper Backwards...*)
   117 (*Bset*)
   118 val not_bst_p_fm = thm "not_bst_p_fm";
   119 val not_bst_p_ne = thm "not_bst_p_ne";
   120 val not_bst_p_eq = thm "not_bst_p_eq";
   121 val not_bst_p_gt = thm "not_bst_p_gt";
   122 val not_bst_p_lt = thm "not_bst_p_lt";
   123 val not_bst_p_ndvd = thm "not_bst_p_ndvd";
   124 val not_bst_p_dvd = thm "not_bst_p_dvd";
   125 
   126 (*Aset*)
   127 val not_ast_p_fm = thm "not_ast_p_fm";
   128 val not_ast_p_ne = thm "not_ast_p_ne";
   129 val not_ast_p_eq = thm "not_ast_p_eq";
   130 val not_ast_p_gt = thm "not_ast_p_gt";
   131 val not_ast_p_lt = thm "not_ast_p_lt";
   132 val not_ast_p_ndvd = thm "not_ast_p_ndvd";
   133 val not_ast_p_dvd = thm "not_ast_p_dvd";
   134 
   135 (*Logical construction of the prop*)
   136 (*Bset*)
   137 val not_bst_p_conjI = thm "not_bst_p_conjI";
   138 val not_bst_p_disjI = thm "not_bst_p_disjI";
   139 val not_bst_p_Q_elim = thm "not_bst_p_Q_elim";
   140 
   141 (*Aset*)
   142 val not_ast_p_conjI = thm "not_ast_p_conjI";
   143 val not_ast_p_disjI = thm "not_ast_p_disjI";
   144 val not_ast_p_Q_elim = thm "not_ast_p_Q_elim";
   145 
   146 (*Cooper*)
   147 val cppi_eq = thm "cppi_eq";
   148 val cpmi_eq = thm "cpmi_eq";
   149 
   150 (*Others*)
   151 val simp_from_to = thm "simp_from_to";
   152 val P_eqtrue = thm "P_eqtrue";
   153 val P_eqfalse = thm "P_eqfalse";
   154 
   155 (*For Proving NNF*)
   156 
   157 val nnf_nn = thm "nnf_nn";
   158 val nnf_im = thm "nnf_im";
   159 val nnf_eq = thm "nnf_eq";
   160 val nnf_sdj = thm "nnf_sdj";
   161 val nnf_ncj = thm "nnf_ncj";
   162 val nnf_nim = thm "nnf_nim";
   163 val nnf_neq = thm "nnf_neq";
   164 val nnf_ndj = thm "nnf_ndj";
   165 
   166 (*For Proving term linearizition*)
   167 val linearize_dvd = thm "linearize_dvd";
   168 val lf_lt = thm "lf_lt";
   169 val lf_eq = thm "lf_eq";
   170 val lf_dvd = thm "lf_dvd";
   171 
   172 
   173 
   174 (* ------------------------------------------------------------------------- *)
   175 (*Datatatype declarations for Proofprotocol for the cooperprocedure.*)
   176 (* ------------------------------------------------------------------------- *)
   177 
   178 
   179 
   180 (* ------------------------------------------------------------------------- *)
   181 (*Datatatype declarations for Proofprotocol for the adjustcoeff step.*)
   182 (* ------------------------------------------------------------------------- *)
   183 datatype CpLog = No
   184                 |Simp of term*CpLog
   185 		|Blast of CpLog*CpLog
   186 		|Aset of (term*term*(term list)*term)
   187 		|Bset of (term*term*(term list)*term)
   188 		|Minusinf of CpLog*CpLog
   189 		|Cooper of term*CpLog*CpLog*CpLog
   190 		|Eq_minf of term*term
   191 		|Modd_minf of term*term
   192 		|Eq_minf_conjI of CpLog*CpLog
   193 		|Modd_minf_conjI of CpLog*CpLog	
   194 		|Modd_minf_disjI of CpLog*CpLog
   195 		|Eq_minf_disjI of CpLog*CpLog	
   196 		|Not_bst_p of term*term*term*term*CpLog
   197 		|Not_bst_p_atomic of term
   198 		|Not_bst_p_conjI of CpLog*CpLog
   199 		|Not_bst_p_disjI of CpLog*CpLog
   200 		|Not_ast_p of term*term*term*term*CpLog
   201 		|Not_ast_p_atomic of term
   202 		|Not_ast_p_conjI of CpLog*CpLog
   203 		|Not_ast_p_disjI of CpLog*CpLog
   204 		|CpLogError;
   205 
   206 
   207 
   208 datatype ACLog = ACAt of int*term
   209                 |ACPI of int*term
   210                 |ACfm of term
   211                 |ACNeg of ACLog
   212 		|ACConst of string*ACLog*ACLog;
   213 
   214 
   215 
   216 (* ------------------------------------------------------------------------- *)
   217 (*Datatatype declarations for Proofprotocol for the CNNF step.*)
   218 (* ------------------------------------------------------------------------- *)
   219 
   220 
   221 datatype NNFLog = NNFAt of term
   222                 |NNFSimp of NNFLog
   223                 |NNFNN of NNFLog
   224 		|NNFConst of string*NNFLog*NNFLog;
   225 
   226 (* ------------------------------------------------------------------------- *)
   227 (*Datatatype declarations for Proofprotocol for the linform  step.*)
   228 (* ------------------------------------------------------------------------- *)
   229 
   230 
   231 datatype LfLog = LfAt of term
   232                 |LfAtdvd of term
   233                 |Lffm of term
   234                 |LfConst of string*LfLog*LfLog
   235 		|LfNot of LfLog
   236 		|LfQ of string*string*typ*LfLog;
   237 
   238 
   239 (* ------------------------------------------------------------------------- *)
   240 (*Datatatype declarations for Proofprotocol for the evaluation- evalc-  step.*)
   241 (* ------------------------------------------------------------------------- *)
   242 
   243 
   244 datatype EvalLog = EvalAt of term
   245                 |Evalfm of term
   246 		|EvalConst of string*EvalLog*EvalLog;
   247 
   248 (* ------------------------------------------------------------------------- *)
   249 (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
   250 (*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
   251 (*this is necessary because the theorems use this representation.*)
   252 (* This function should be elminated in next versions...*)
   253 (* ------------------------------------------------------------------------- *)
   254 
   255 fun norm_zero_one fm = case fm of
   256   (Const ("op *",_) $ c $ t) => 
   257     if c = one then (norm_zero_one t)
   258     else if (dest_numeral c = ~1) 
   259          then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   260          else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   261   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   262   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   263   |_ => fm;
   264 
   265 
   266 (* ------------------------------------------------------------------------- *)
   267 (* Intended to tell that here we changed the structure of the formula with respect to the posineq theorem : ~(0 < t) = 0 < 1-t*)
   268 (* ------------------------------------------------------------------------- *)
   269 fun adjustcoeffeq_wp  x l fm = 
   270     case fm of  
   271   (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
   272   if (x = y) 
   273   then let  
   274        val m = l div (dest_numeral c) 
   275        val n = abs (m)
   276        val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
   277        val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   278        in (ACPI(n,fm),rs)
   279        end
   280   else  let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )) 
   281         in (ACPI(1,fm),rs)
   282         end
   283 
   284   |(Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ 
   285       c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then  
   286         let val m = l div (dest_numeral c) 
   287            val n = (if p = "op <" then abs(m) else m)  
   288            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
   289            val rs = (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   290 	   in (ACAt(n,fm),rs)
   291 	   end
   292         else (ACfm(fm),fm) 
   293   |( Const ("Not", _) $ p) => let val (rsp,rsr) = adjustcoeffeq_wp x l p 
   294                               in (ACNeg(rsp),HOLogic.Not $ rsr) 
   295                               end
   296   |( Const ("op &",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
   297                                      val (rsqp,rsqr) = adjustcoeffeq_wp x l q
   298 
   299                                   in (ACConst ("CJ",rspp,rsqp), HOLogic.mk_conj (rspr,rsqr)) 
   300                                   end 
   301   |( Const ("op |",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
   302                                      val (rsqp,rsqr) = adjustcoeffeq_wp x l q
   303 
   304                                   in (ACConst ("DJ",rspp,rsqp), HOLogic.mk_disj (rspr,rsqr)) 
   305                                   end
   306 
   307   |_ => (ACfm(fm),fm);
   308 
   309 
   310 (*_________________________________________*)
   311 (*-----------------------------------------*)
   312 (* Protocol generation for the liform step *)
   313 (*_________________________________________*)
   314 (*-----------------------------------------*)
   315 
   316 
   317 fun linform_wp fm = 
   318   let fun at_linform_wp at =
   319     case at of
   320       (Const("op <=",_)$s$t) => LfAt(at)
   321       |(Const("op <",_)$s$t) => LfAt(at)
   322       |(Const("op =",_)$s$t) => LfAt(at)
   323       |(Const("Divides.op dvd",_)$s$t) => LfAtdvd(at)
   324   in
   325   if is_arith_rel fm 
   326   then at_linform_wp fm 
   327   else case fm of
   328     (Const("Not",_) $ A) => LfNot(linform_wp A)
   329    |(Const("op &",_)$ A $ B) => LfConst("CJ",linform_wp A, linform_wp B)
   330    |(Const("op |",_)$ A $ B) => LfConst("DJ",linform_wp A, linform_wp B)
   331    |(Const("op -->",_)$ A $ B) => LfConst("IM",linform_wp A, linform_wp B)
   332    |(Const("op =",Type ("fun",[Type ("bool", []),_]))$ A $ B) => LfConst("EQ",linform_wp A, linform_wp B)
   333    |Const("Ex",_)$Abs(x,T,p) => 
   334      let val (xn,p1) = variant_abs(x,T,p)
   335      in LfQ("Ex",xn,T,linform_wp p1)
   336      end 
   337    |Const("All",_)$Abs(x,T,p) => 
   338      let val (xn,p1) = variant_abs(x,T,p)
   339      in LfQ("All",xn,T,linform_wp p1)
   340      end 
   341 end;
   342 
   343 
   344 (* ------------------------------------------------------------------------- *)
   345 (*For simlified formulas we just notice the original formula, for whitch we habe been
   346 intendes to make the proof.*)
   347 (* ------------------------------------------------------------------------- *)
   348 fun simpl_wp (fm,pr) = let val fm2 = simpl fm
   349 				in (fm2,Simp(fm,pr))
   350 				end;
   351 
   352 	
   353 (* ------------------------------------------------------------------------- *)
   354 (*Help function for the generation of the proof EX.P_{minus \infty} --> EX. P(x) *)
   355 (* ------------------------------------------------------------------------- *)
   356 fun minusinf_wph x fm = let fun mk_atomar_minusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
   357   
   358 	      fun combine_minusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
   359 		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
   360 		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
   361 	in 
   362  
   363  case fm of 
   364  (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   365      if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_minusinf_proof x fm))
   366         else (fm ,(mk_atomar_minusinf_proof x fm))
   367  |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   368   	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
   369 	 then (HOLogic.false_const ,(mk_atomar_minusinf_proof x fm))
   370 	 				 else (fm,(mk_atomar_minusinf_proof x fm)) 
   371  |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
   372        if (y=x) andalso (c1 = zero) then 
   373         if c2 = one then (HOLogic.false_const,(mk_atomar_minusinf_proof x fm)) else
   374 	(HOLogic.true_const,(mk_atomar_minusinf_proof x fm))
   375 	else (fm,(mk_atomar_minusinf_proof x fm))
   376   
   377   |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_minusinf_proof x fm)
   378   
   379   |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_minusinf_proof x fm)
   380   
   381   |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
   382   				    val (qfm,qpr) = minusinf_wph x q
   383 				    val pr = (combine_minusinf_proofs "CJ" ppr qpr)
   384 				     in 
   385 				     (HOLogic.conj $ pfm $qfm , pr)
   386 				     end 
   387   |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
   388   				     val (qfm,qpr) = minusinf_wph x q
   389 				     val pr = (combine_minusinf_proofs "DJ" ppr qpr)
   390 				     in 
   391 				     (HOLogic.disj $ pfm $qfm , pr)
   392 				     end 
   393 
   394   |_ => (fm,(mk_atomar_minusinf_proof x fm))
   395   
   396   end;					 
   397 (* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
   398 (* Just combines the to protokols *)
   399 (* ------------------------------------------------------------------------- *)
   400 fun minusinf_wp x fm  = let val (fm2,pr) = (minusinf_wph x fm)
   401                        in (fm2,Minusinf(pr))
   402                         end;
   403 
   404 (* ------------------------------------------------------------------------- *)
   405 (*Help function for the generation of the proof EX.P_{plus \infty} --> EX. P(x) *)
   406 (* ------------------------------------------------------------------------- *)
   407 
   408 fun plusinf_wph x fm = let fun mk_atomar_plusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
   409   
   410 	      fun combine_plusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of 
   411 		 "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
   412 		|"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
   413 	in 
   414  
   415  case fm of 
   416  (Const ("Not", _) $  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   417      if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_plusinf_proof x fm))
   418         else (fm ,(mk_atomar_plusinf_proof x fm))
   419  |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   420   	 if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
   421 	 then (HOLogic.false_const ,(mk_atomar_plusinf_proof x fm))
   422 	 				 else (fm,(mk_atomar_plusinf_proof x fm)) 
   423  |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
   424        if (y=x) andalso (c1 = zero) then 
   425         if c2 = one then (HOLogic.true_const,(mk_atomar_plusinf_proof x fm)) else
   426 	(HOLogic.false_const,(mk_atomar_plusinf_proof x fm))
   427 	else (fm,(mk_atomar_plusinf_proof x fm))
   428   
   429   |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_plusinf_proof x fm)
   430   
   431   |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_plusinf_proof x fm)
   432   
   433   |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
   434   				    val (qfm,qpr) = plusinf_wph x q
   435 				    val pr = (combine_plusinf_proofs "CJ" ppr qpr)
   436 				     in 
   437 				     (HOLogic.conj $ pfm $qfm , pr)
   438 				     end 
   439   |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
   440   				     val (qfm,qpr) = plusinf_wph x q
   441 				     val pr = (combine_plusinf_proofs "DJ" ppr qpr)
   442 				     in 
   443 				     (HOLogic.disj $ pfm $qfm , pr)
   444 				     end 
   445 
   446   |_ => (fm,(mk_atomar_plusinf_proof x fm))
   447   
   448   end;					 
   449 (* ------------------------------------------------------------------------- *)	    (* Protokol for the Proof of the property of the minusinfinity formula*)
   450 (* Just combines the to protokols *)
   451 (* ------------------------------------------------------------------------- *)
   452 fun plusinf_wp x fm  = let val (fm2,pr) = (plusinf_wph x fm)
   453                        in (fm2,Minusinf(pr))
   454                         end;
   455 
   456 
   457 (* ------------------------------------------------------------------------- *)
   458 (*Protocol that we here uses Bset.*)
   459 (* ------------------------------------------------------------------------- *)
   460 fun bset_wp x fm = let val bs = bset x fm in
   461 				(bs,Bset(x,fm,bs,mk_numeral (divlcm x fm)))
   462 				end;
   463 
   464 (* ------------------------------------------------------------------------- *)
   465 (*Protocol that we here uses Aset.*)
   466 (* ------------------------------------------------------------------------- *)
   467 fun aset_wp x fm = let val ast = aset x fm in
   468 				(ast,Aset(x,fm,ast,mk_numeral (divlcm x fm)))
   469 				end;
   470  
   471 
   472 
   473 (* ------------------------------------------------------------------------- *)
   474 (*function list to Set, constructs a set containing all elements of a given list.*)
   475 (* ------------------------------------------------------------------------- *)
   476 fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in 
   477 	case l of 
   478 		[] => Const ("{}",T)
   479 		|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
   480 		end;
   481 		
   482 
   483 (*====================================================================*)
   484 (* ------------------------------------------------------------------------- *)
   485 (* ------------------------------------------------------------------------- *)
   486 (*Protocol for the proof of the backward direction of the cooper theorem.*)
   487 (* Helpfunction - Protokols evereything about the proof reconstruction*)
   488 (* ------------------------------------------------------------------------- *)
   489 fun not_bst_p_wph fm = case fm of
   490 	Const("Not",_) $ R => if (is_arith_rel R) then (Not_bst_p_atomic (fm)) else CpLogError
   491 	|Const("op &",_) $ ls $ rs => Not_bst_p_conjI((not_bst_p_wph ls),(not_bst_p_wph rs))
   492 	|Const("op |",_) $ ls $ rs => Not_bst_p_disjI((not_bst_p_wph ls),(not_bst_p_wph rs))
   493 	|_ => Not_bst_p_atomic (fm);
   494 (* ------------------------------------------------------------------------- *)	
   495 (* 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*)
   496 (* ------------------------------------------------------------------------- *)
   497 fun not_bst_p_wp x fm = let val prt = not_bst_p_wph fm
   498 			    val D = mk_numeral (divlcm x fm)
   499 			    val B = map norm_zero_one (bset x fm)
   500 			in (Not_bst_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
   501 			end;
   502 (*====================================================================*)
   503 (* ------------------------------------------------------------------------- *)
   504 (* ------------------------------------------------------------------------- *)
   505 (*Protocol for the proof of the backward direction of the cooper theorem.*)
   506 (* Helpfunction - Protokols evereything about the proof reconstruction*)
   507 (* ------------------------------------------------------------------------- *)
   508 fun not_ast_p_wph fm = case fm of
   509 	Const("Not",_) $ R => if (is_arith_rel R) then (Not_ast_p_atomic (fm)) else CpLogError
   510 	|Const("op &",_) $ ls $ rs => Not_ast_p_conjI((not_ast_p_wph ls),(not_ast_p_wph rs))
   511 	|Const("op |",_) $ ls $ rs => Not_ast_p_disjI((not_ast_p_wph ls),(not_ast_p_wph rs))
   512 	|_ => Not_ast_p_atomic (fm);
   513 (* ------------------------------------------------------------------------- *)	
   514 (* 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*)
   515 (* ------------------------------------------------------------------------- *)
   516 fun not_ast_p_wp x fm = let val prt = not_ast_p_wph fm
   517 			    val D = mk_numeral (divlcm x fm)
   518 			    val B = map norm_zero_one (aset x fm)
   519 			in (Not_ast_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
   520 			end;
   521 
   522 (*======================================================*)
   523 (* Protokolgeneration for the formula evaluation process*)
   524 (*======================================================*)
   525 
   526 fun evalc_wp fm = 
   527   let fun evalc_atom_wp at =case at of  
   528     (Const (p,_) $ s $ t) =>(  
   529     case assoc (operations,p) of 
   530         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)))  
   531 		   handle _ => Evalfm(at)) 
   532         | _ =>  Evalfm(at)) 
   533      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   534        case assoc (operations,p) of 
   535          Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
   536 	  EvalAt(HOLogic.mk_eq(at, HOLogic.false_const))  else EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)))  
   537 		      handle _ => Evalfm(at)) 
   538          | _ => Evalfm(at)) 
   539      | _ => Evalfm(at)  
   540  
   541   in
   542    case fm of
   543     (Const("op &",_)$A$B) => EvalConst("CJ",evalc_wp A,evalc_wp B)
   544    |(Const("op |",_)$A$B) => EvalConst("DJ",evalc_wp A,evalc_wp B) 
   545    |(Const("op -->",_)$A$B) => EvalConst("IM",evalc_wp A,evalc_wp B) 
   546    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => EvalConst("EQ",evalc_wp A,evalc_wp B) 
   547    |_ => evalc_atom_wp fm
   548   end;
   549 
   550 
   551 
   552 (*======================================================*)
   553 (* Protokolgeneration for the NNF Transformation        *)
   554 (*======================================================*)
   555 
   556 fun cnnf_wp f = 
   557   let fun hcnnf_wp fm =
   558     case fm of
   559     (Const ("op &",_) $ p $ q) => NNFConst("CJ",hcnnf_wp p,hcnnf_wp q) 
   560     | (Const ("op |",_) $ p $ q) =>  NNFConst("DJ",hcnnf_wp p,hcnnf_wp q)
   561     | (Const ("op -->",_) $ p $q) => NNFConst("IM",hcnnf_wp (HOLogic.Not $ p),hcnnf_wp q)
   562     | (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)))) 
   563 
   564     | (Const ("Not",_) $ (Const("Not",_) $ p)) => NNFNN(hcnnf_wp p) 
   565     | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => NNFConst ("NCJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
   566     | (Const ("Not",_) $(Const ("op |",_) $ (A as (Const ("op &",_) $ p $ q)) $  
   567     			(B as (Const ("op &",_) $ p1 $ r)))) => if p1 = negate p then 
   568 		         NNFConst("SDJ",  
   569 			   NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q)),
   570 			   NNFConst("CJ",hcnnf_wp p1,hcnnf_wp(HOLogic.Not $ r)))
   571 			 else  NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ A)),(hcnnf_wp(HOLogic.Not $ B))) 
   572 
   573     | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q))) 
   574     | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) =>  NNFConst ("NIM",(hcnnf_wp(p)),(hcnnf_wp(HOLogic.Not $ q))) 
   575     | (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))) 
   576     | _ => NNFAt(fm)  
   577   in NNFSimp(hcnnf_wp f)
   578 end; 
   579    
   580 
   581 
   582 
   583 
   584 
   585 (* ------------------------------------------------------------------------- *)
   586 (*Cooper decision Procedure with proof protocoling*)
   587 (* ------------------------------------------------------------------------- *)
   588 
   589 fun coopermi_wp vars fm =
   590   case fm of
   591    Const ("Ex",_) $ Abs(xo,T,po) => let 
   592     val (xn,np) = variant_abs(xo,T,po) 
   593     val x = (Free(xn , T))
   594     val p = np     (* Is this a legal proof for the P=NP Problem??*)
   595     val (p_inf,miprt) = simpl_wp (minusinf_wp x p)
   596     val (bset,bsprt) = bset_wp x p
   597     val nbst_p_prt = not_bst_p_wp x p
   598     val dlcm = divlcm x p 
   599     val js = 1 upto dlcm 
   600     fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p 
   601     fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset) 
   602    in (list_disj (map stage js),Cooper(mk_numeral dlcm,miprt,bsprt,nbst_p_prt))
   603    end
   604    
   605   | _ => (error "cooper: not an existential formula",No);
   606 				
   607 fun cooperpi_wp vars fm =
   608   case fm of
   609    Const ("Ex",_) $ Abs(xo,T,po) => let 
   610     val (xn,np) = variant_abs(xo,T,po) 
   611     val x = (Free(xn , T))
   612     val p = np     (* Is this a legal proof for the P=NP Problem??*)
   613     val (p_inf,piprt) = simpl_wp (plusinf_wp x p)
   614     val (aset,asprt) = aset_wp x p
   615     val nast_p_prt = not_ast_p_wp x p
   616     val dlcm = divlcm x p 
   617     val js = 1 upto dlcm 
   618     fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p 
   619     fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset) 
   620    in (list_disj (map stage js),Cooper(mk_numeral dlcm,piprt,asprt,nast_p_prt))
   621    end
   622   | _ => (error "cooper: not an existential formula",No);
   623 				
   624 
   625 
   626 
   627 
   628 (*-----------------------------------------------------------------*)
   629 (*-----------------------------------------------------------------*)
   630 (*-----------------------------------------------------------------*)
   631 (*---                                                           ---*)
   632 (*---                                                           ---*)
   633 (*---      Interpretation and Proofgeneration Part              ---*)
   634 (*---                                                           ---*)
   635 (*---      Protocole interpretation functions                   ---*)
   636 (*---                                                           ---*)
   637 (*---      and proofgeneration functions                        ---*)
   638 (*---                                                           ---*)
   639 (*---                                                           ---*)
   640 (*---                                                           ---*)
   641 (*---                                                           ---*)
   642 (*-----------------------------------------------------------------*)
   643 (*-----------------------------------------------------------------*)
   644 (*-----------------------------------------------------------------*)
   645 
   646 (* ------------------------------------------------------------------------- *)
   647 (* Returns both sides of an equvalence in the theorem*)
   648 (* ------------------------------------------------------------------------- *)
   649 fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
   650 
   651 
   652 (*-------------------------------------------------------------*)
   653 (*-------------------------------------------------------------*)
   654 (*-------------------------------------------------------------*)
   655 (*-------------------------------------------------------------*)
   656 
   657 (* ------------------------------------------------------------------------- *)
   658 (* Modified version of the simple version with minimal amount of checking and postprocessing*)
   659 (* ------------------------------------------------------------------------- *)
   660 
   661 fun simple_prove_goal_cterm2 G tacs =
   662   let
   663     fun check None = error "prove_goal: tactic failed"
   664       | check (Some (thm, _)) = (case nprems_of thm of
   665             0 => thm
   666           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   667   in check (Seq.pull (EVERY tacs (trivial G))) end;
   668 
   669 (*-------------------------------------------------------------*)
   670 (*-------------------------------------------------------------*)
   671 (*-------------------------------------------------------------*)
   672 (*-------------------------------------------------------------*)
   673 (*-------------------------------------------------------------*)
   674 
   675 fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
   676 
   677 (* ------------------------------------------------------------------------- *)
   678 (*This function proove elementar will be used to generate proofs at runtime*)
   679 (*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
   680 (*prove properties such as a dvd b (essentially) that are only to make at
   681 runtime.*)
   682 (* ------------------------------------------------------------------------- *)
   683 fun prove_elementar sg s fm2 = case s of 
   684   (*"ss" like simplification with simpset*)
   685   "ss" =>
   686     let
   687       val ss = presburger_ss addsimps
   688         [zdvd_iff_zmod_eq_0,unity_coeff_ex]
   689       val ct =  cert_Trueprop sg fm2
   690     in 
   691       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   692     end
   693 
   694   (*"bl" like blast tactic*)
   695   (* Is only used in the harrisons like proof procedure *)
   696   | "bl" =>
   697      let val ct = cert_Trueprop sg fm2
   698      in
   699        simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
   700      end
   701 
   702   (*"ed" like Existence disjunctions ...*)
   703   (* Is only used in the harrisons like proof procedure *)
   704   | "ed" =>
   705     let
   706       val ex_disj_tacs =
   707         let
   708           val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1]
   709           val tac2 = EVERY[etac exE 1, rtac exI 1,
   710             REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1]
   711 	in [rtac iffI 1,
   712           etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
   713           REPEAT(EVERY[etac disjE 1, tac2]), tac2]
   714         end
   715 
   716       val ct = cert_Trueprop sg fm2
   717     in 
   718       simple_prove_goal_cterm2 ct ex_disj_tacs
   719     end
   720 
   721   | "fa" =>
   722     let val ct = cert_Trueprop sg fm2
   723     in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
   724     end
   725 
   726   | "sa" =>
   727     let
   728       val ss = presburger_ss addsimps zadd_ac
   729       val ct = cert_Trueprop sg fm2
   730     in 
   731       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   732     end
   733 
   734   | "ac" =>
   735     let
   736       val ss = HOL_basic_ss addsimps zadd_ac
   737       val ct = cert_Trueprop sg fm2
   738     in 
   739       simple_prove_goal_cterm2 ct [simp_tac ss 1]
   740     end
   741 
   742   | "lf" =>
   743     let
   744       val ss = presburger_ss addsimps zadd_ac
   745       val ct = cert_Trueprop sg fm2
   746     in 
   747       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   748     end;
   749 
   750 
   751 
   752 (* ------------------------------------------------------------------------- *)
   753 (* This function return an Isabelle proof, of the adjustcoffeq result.*)
   754 (* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   755 (* ------------------------------------------------------------------------- *)
   756 fun proof_of_adjustcoeffeq sg (prt,rs) = case prt of
   757    ACfm fm => instantiate' [Some cboolT]
   758     [Some (cterm_of sg fm)] refl
   759  | ACAt (k,at as (Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
   760       c $ x ) $t ))) => 
   761    let
   762      val ck = cterm_of sg (mk_numeral k)
   763      val cc = cterm_of sg c
   764      val ct = cterm_of sg t
   765      val cx = cterm_of sg x
   766      val ca = cterm_of sg a
   767    in case p of
   768      "op <" => let val pre = prove_elementar sg "lf" 
   769 	                  (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
   770 	           val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
   771 		      in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   772                    end
   773     |"op =" =>let val pre = prove_elementar sg "lf" 
   774 	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   775 	          in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
   776 	             in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   777                       end
   778                   end
   779     |"Divides.op dvd" =>let val pre = prove_elementar sg "lf" 
   780 	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   781 	                 val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
   782                          in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   783                         
   784                           end
   785   end
   786  |ACPI(k,at as (Const("Not",_)$(Const("op <",_) $a $( Const ("op +", _)$(Const ("op *",_) $ c $ x ) $t )))) => 
   787    let
   788      val ck = cterm_of sg (mk_numeral k)
   789      val cc = cterm_of sg c
   790      val ct = cterm_of sg t
   791      val cx = cterm_of sg x
   792      val pre = prove_elementar sg "lf" 
   793        (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
   794        val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
   795 
   796          in [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
   797    end
   798  |ACNeg(pr) => let val (Const("Not",_)$nrs) = rs
   799                in (proof_of_adjustcoeffeq sg (pr,nrs)) RS (qe_Not) 
   800                end
   801  |ACConst(s,pr1,pr2) =>
   802    let val (Const(_,_)$rs1$rs2) = rs
   803        val th1 = proof_of_adjustcoeffeq sg (pr1,rs1)
   804        val th2 = proof_of_adjustcoeffeq sg (pr2,rs2)
   805        in case s of 
   806 	 "CJ" => [th1,th2] MRS (qe_conjI)
   807          |"DJ" => [th1,th2] MRS (qe_disjI)
   808          |"IM" => [th1,th2] MRS (qe_impI)
   809          |"EQ" => [th1,th2] MRS (qe_eqI)
   810    end;
   811 
   812 
   813 
   814 
   815 
   816 
   817 (* ------------------------------------------------------------------------- *)
   818 (* This function return an Isabelle proof, of some properties on the atoms*)
   819 (* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   820 (* This function doese only instantiate the the theorems in the theory *)
   821 (* ------------------------------------------------------------------------- *)
   822 fun atomar_minf_proof_of sg dlcm (Modd_minf (x,fm1)) =
   823   let
   824     (*Some certified Terms*)
   825     
   826    val ctrue = cterm_of sg HOLogic.true_const
   827    val cfalse = cterm_of sg HOLogic.false_const
   828    val fm = norm_zero_one fm1
   829   in  case fm1 of 
   830       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   831          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   832            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   833 
   834       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   835   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
   836 	   then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf))
   837 	 	 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)) 
   838 
   839       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   840            if (y=x) andalso (c1 = zero) then 
   841             if (pm1 = one) then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf)) else
   842 	     (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   843 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   844   
   845       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   846          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   847 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   848 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
   849 		      end
   850 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   851       |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   852       c $ y ) $ z))) => 
   853          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   854 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   855 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
   856 		      end
   857 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   858 		
   859     
   860    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
   861    end	
   862 
   863  |atomar_minf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
   864        (*Some certified types*)
   865    val fm = norm_zero_one fm1
   866     in  case fm1 of 
   867       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   868          if  (x=y) andalso (c1=zero) andalso (c2=one) 
   869 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   870            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   871 
   872       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   873   	   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))
   874 	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
   875 	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf)) 
   876 
   877       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   878            if (y=x) andalso (c1 =zero) then 
   879             if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
   880 	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_minf))
   881 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   882       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   883          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   884 	 		  val cz = cterm_of sg (norm_zero_one z)
   885 	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_minf)) 
   886 		      end
   887 
   888 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   889 		
   890       |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   891          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   892 	 		  val cz = cterm_of sg (norm_zero_one z)
   893 	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_minf))
   894 		      end
   895 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   896 
   897       		
   898     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   899  end;
   900 
   901 
   902 (* ------------------------------------------------------------------------- *)
   903 (* This function combines proofs of some special form already synthetised from the subtrees to make*)
   904 (* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
   905 (*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
   906 (* These are Theorems for the Property of P_{-infty}*)
   907 (* ------------------------------------------------------------------------- *)
   908 fun combine_minf_proof s pr1 pr2 = case s of
   909     "ECJ" => [pr1 , pr2] MRS (eq_minf_conjI)
   910 
   911    |"EDJ" => [pr1 , pr2] MRS (eq_minf_disjI)
   912    
   913    |"MCJ" => [pr1 , pr2] MRS (modd_minf_conjI)
   914 
   915    |"MDJ" => [pr1 , pr2] MRS (modd_minf_disjI);
   916 
   917 (* ------------------------------------------------------------------------- *)
   918 (*This function return an isabelle Proof for the minusinfinity theorem*)
   919 (* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
   920 (* ------------------------------------------------------------------------- *)
   921 fun minf_proof_ofh sg dlcm prl = case prl of 
   922 
   923     Eq_minf (_) => atomar_minf_proof_of sg dlcm prl
   924     
   925    |Modd_minf (_) => atomar_minf_proof_of sg dlcm prl
   926    
   927    |Eq_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   928    				    val pr2 = minf_proof_ofh sg dlcm prl2
   929 				 in (combine_minf_proof "ECJ" pr1 pr2)
   930 				 end
   931 				 
   932    |Eq_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   933    				    val pr2 = minf_proof_ofh sg dlcm prl2
   934 				 in (combine_minf_proof "EDJ" pr1 pr2)
   935 				 end
   936 				 
   937    |Modd_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   938    				    val pr2 = minf_proof_ofh sg dlcm prl2
   939 				 in (combine_minf_proof "MCJ" pr1 pr2)
   940 				 end
   941 				 
   942    |Modd_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
   943    				    val pr2 = minf_proof_ofh sg dlcm prl2
   944 				 in (combine_minf_proof "MDJ" pr1 pr2)
   945 				 end;
   946 (* ------------------------------------------------------------------------- *)
   947 (* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
   948 (* ------------------------------------------------------------------------- *)
   949 fun  minf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
   950   let val pr1 = minf_proof_ofh sg dlcm prl1
   951       val pr2 = minf_proof_ofh sg dlcm prl2
   952   in (pr1, pr2)
   953 end;
   954 				 
   955 
   956 
   957 
   958 (* ------------------------------------------------------------------------- *)
   959 (* This function return an Isabelle proof, of some properties on the atoms*)
   960 (* The proofs are in Presburger.thy and are generally based on the arithmetic *)
   961 (* This function doese only instantiate the the theorems in the theory *)
   962 (* ------------------------------------------------------------------------- *)
   963 fun atomar_pinf_proof_of sg dlcm (Modd_minf (x,fm1)) =
   964  let
   965     (*Some certified Terms*)
   966     
   967   val ctrue = cterm_of sg HOLogic.true_const
   968   val cfalse = cterm_of sg HOLogic.false_const
   969   val fm = norm_zero_one fm1
   970  in  case fm1 of 
   971       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   972          if ((x=y) andalso (c1= zero) andalso (c2= one))
   973 	 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
   974          else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   975 
   976       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   977   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
   978 	then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   979 	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   980 
   981       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   982         if ((y=x) andalso (c1 = zero)) then 
   983           if (pm1 = one) 
   984 	  then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf)) 
   985 	  else (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   986 	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   987   
   988       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   989          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   990 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   991 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
   992 		      end
   993 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   994       |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   995       c $ y ) $ z))) => 
   996          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   997 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   998 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
   999 		      end
  1000 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
  1001 		
  1002     
  1003    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
  1004    end	
  1005 
  1006  |atomar_pinf_proof_of sg dlcm (Eq_minf (x,fm1)) =  let
  1007 					val fm = norm_zero_one fm1
  1008     in  case fm1 of 
  1009       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1010          if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1011 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
  1012            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1013 
  1014       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1015   	   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))
  1016 	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
  1017 	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf)) 
  1018 
  1019       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1020            if (y=x) andalso (c1 =zero) then 
  1021             if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
  1022 	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
  1023 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1024       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1025          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  1026 	 		  val cz = cterm_of sg (norm_zero_one z)
  1027 	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_pinf)) 
  1028 		      end
  1029 
  1030 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1031 		
  1032       |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1033          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
  1034 	 		  val cz = cterm_of sg (norm_zero_one z)
  1035 	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_pinf))
  1036 		      end
  1037 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1038 
  1039       		
  1040     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
  1041  end;
  1042 
  1043 
  1044 (* ------------------------------------------------------------------------- *)
  1045 (* This function combines proofs of some special form already synthetised from the subtrees to make*)
  1046 (* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
  1047 (*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
  1048 (* These are Theorems for the Property of P_{+infty}*)
  1049 (* ------------------------------------------------------------------------- *)
  1050 fun combine_pinf_proof s pr1 pr2 = case s of
  1051     "ECJ" => [pr1 , pr2] MRS (eq_pinf_conjI)
  1052 
  1053    |"EDJ" => [pr1 , pr2] MRS (eq_pinf_disjI)
  1054    
  1055    |"MCJ" => [pr1 , pr2] MRS (modd_pinf_conjI)
  1056 
  1057    |"MDJ" => [pr1 , pr2] MRS (modd_pinf_disjI);
  1058 
  1059 (* ------------------------------------------------------------------------- *)
  1060 (*This function return an isabelle Proof for the minusinfinity theorem*)
  1061 (* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
  1062 (* ------------------------------------------------------------------------- *)
  1063 fun pinf_proof_ofh sg dlcm prl = case prl of 
  1064 
  1065     Eq_minf (_) => atomar_pinf_proof_of sg dlcm prl
  1066     
  1067    |Modd_minf (_) => atomar_pinf_proof_of sg dlcm prl
  1068    
  1069    |Eq_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1070    				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1071 				 in (combine_pinf_proof "ECJ" pr1 pr2)
  1072 				 end
  1073 				 
  1074    |Eq_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1075    				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1076 				 in (combine_pinf_proof "EDJ" pr1 pr2)
  1077 				 end
  1078 				 
  1079    |Modd_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1080    				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1081 				 in (combine_pinf_proof "MCJ" pr1 pr2)
  1082 				 end
  1083 				 
  1084    |Modd_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
  1085    				    val pr2 = pinf_proof_ofh sg dlcm prl2
  1086 				 in (combine_pinf_proof "MDJ" pr1 pr2)
  1087 				 end;
  1088 (* ------------------------------------------------------------------------- *)
  1089 (* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)				 
  1090 (* ------------------------------------------------------------------------- *)
  1091 fun pinf_proof_of sg dlcm (Minusinf (prl1,prl2))  = 
  1092   let val pr1 = pinf_proof_ofh sg dlcm prl1
  1093       val pr2 = pinf_proof_ofh sg dlcm prl2
  1094   in (pr1, pr2)
  1095 end;
  1096 				 
  1097 
  1098 
  1099 
  1100 (* ------------------------------------------------------------------------- *)
  1101 (* Here we generate the theorem for the Bset Property in the simple direction*)
  1102 (* It is just an instantiation*)
  1103 (* ------------------------------------------------------------------------- *)
  1104 fun bsetproof_of sg (Bset(x as Free(xn,xT),fm,bs,dlcm))   = 
  1105   let
  1106     val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1107     val cdlcm = cterm_of sg dlcm
  1108     val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
  1109   in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
  1110     end;
  1111 
  1112 
  1113 
  1114 
  1115 (* ------------------------------------------------------------------------- *)
  1116 (* Here we generate the theorem for the Bset Property in the simple direction*)
  1117 (* It is just an instantiation*)
  1118 (* ------------------------------------------------------------------------- *)
  1119 fun asetproof_of sg (Aset(x as Free(xn,xT),fm,ast,dlcm))   = 
  1120   let
  1121     val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1122     val cdlcm = cterm_of sg dlcm
  1123     val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
  1124   in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
  1125 end;
  1126 
  1127 
  1128 
  1129 
  1130 (* ------------------------------------------------------------------------- *)    
  1131 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
  1132 
  1133 (* For the generation of atomic Theorems*)
  1134 (* Prove the premisses on runtime and then make RS*)
  1135 (* ------------------------------------------------------------------------- *)
  1136 fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = 
  1137   let
  1138     val cdlcm = cterm_of sg dlcm
  1139     val cB = cterm_of sg B
  1140     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1141     val cat = cterm_of sg (norm_zero_one at)
  1142   in
  1143   case at of 
  1144    (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1145       if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1146 	 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)
  1147 	          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)))
  1148 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1149 	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
  1150 	 end
  1151          else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1152 
  1153    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1154      if (is_arith_rel at) andalso (x=y)
  1155 	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
  1156 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
  1157 	          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))))
  1158 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1159 	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
  1160 	 end
  1161        end
  1162          else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1163 
  1164    |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1165         if (y=x) andalso (c1 =zero) then 
  1166         if pm1 = one then 
  1167 	  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)
  1168               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)))
  1169 	  in  (instantiate' [] [Some cfma,  Some cdlcm]([th1,th2] MRS (not_bst_p_gt)))
  1170 	    end
  1171 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1172 	      in (instantiate' [] [Some cfma, Some cB,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
  1173 	      end
  1174       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1175 
  1176    |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1177       if y=x then  
  1178            let val cz = cterm_of sg (norm_zero_one z)
  1179 	       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)
  1180  	     in (instantiate' []  [Some cfma, Some cB,Some cz] (th1 RS (not_bst_p_ndvd)))
  1181 	     end
  1182       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1183 
  1184    |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1185        if y=x then  
  1186 	 let val cz = cterm_of sg (norm_zero_one z)
  1187 	     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)
  1188  	    in (instantiate' []  [Some cfma,Some cB,Some cz] (th1 RS (not_bst_p_dvd)))
  1189 	  end
  1190       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1191       		
  1192    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
  1193       		
  1194     end;
  1195     
  1196 (* ------------------------------------------------------------------------- *)    
  1197 (* Main interpretation function for this backwards dirction*)
  1198 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
  1199 (*Help Function*)
  1200 (* ------------------------------------------------------------------------- *)
  1201 fun not_bst_p_proof_of_h sg x fm dlcm B prt = case prt of 
  1202 	(Not_bst_p_atomic(fm2)) => (generate_atomic_not_bst_p sg x fm dlcm B fm2)
  1203 	
  1204 	|(Not_bst_p_conjI(pr1,pr2)) => 
  1205 			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
  1206 			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
  1207 			    in ([th1,th2] MRS (not_bst_p_conjI))
  1208 			    end
  1209 
  1210 	|(Not_bst_p_disjI(pr1,pr2)) => 
  1211 			let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
  1212 			    val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
  1213 			    in ([th1,th2] MRS not_bst_p_disjI)
  1214 			    end;
  1215 (* Main function*)
  1216 fun not_bst_p_proof_of sg (Not_bst_p(x as Free(xn,xT),fm,dlcm,B,prl)) =
  1217   let val th =  not_bst_p_proof_of_h sg x fm dlcm B prl
  1218       val fma = absfree (xn,xT, norm_zero_one fm)
  1219   in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
  1220      in [th,th1] MRS (not_bst_p_Q_elim)
  1221      end
  1222   end;
  1223 
  1224 
  1225 (* ------------------------------------------------------------------------- *)    
  1226 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
  1227 
  1228 (* For the generation of atomic Theorems*)
  1229 (* Prove the premisses on runtime and then make RS*)
  1230 (* ------------------------------------------------------------------------- *)
  1231 fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = 
  1232   let
  1233     val cdlcm = cterm_of sg dlcm
  1234     val cA = cterm_of sg A
  1235     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
  1236     val cat = cterm_of sg (norm_zero_one at)
  1237   in
  1238   case at of 
  1239    (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
  1240       if  (x=y) andalso (c1=zero) andalso (c2=one) 
  1241 	 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)
  1242 	          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)))
  1243 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1244 	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
  1245 	 end
  1246          else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1247 
  1248    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
  1249      if (is_arith_rel at) andalso (x=y)
  1250 	then let val ast_z = norm_zero_one (linear_sub [] one z )
  1251 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
  1252 	         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))))
  1253 		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1254 	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
  1255        end
  1256          else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1257 
  1258    |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
  1259         if (y=x) andalso (c1 =zero) then 
  1260         if pm1 = (mk_numeral ~1) then 
  1261 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
  1262               val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
  1263 	  in  (instantiate' [] [Some cfma]([th2,th1] MRS (not_ast_p_lt)))
  1264 	    end
  1265 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
  1266 	      in (instantiate' [] [Some cfma, Some cA,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
  1267 	      end
  1268       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1269 
  1270    |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1271       if y=x then  
  1272            let val cz = cterm_of sg (norm_zero_one z)
  1273 	       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)
  1274  	     in (instantiate' []  [Some cfma, Some cA,Some cz] (th1 RS (not_ast_p_ndvd)))
  1275 	     end
  1276       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1277 
  1278    |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
  1279        if y=x then  
  1280 	 let val cz = cterm_of sg (norm_zero_one z)
  1281 	     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)
  1282  	    in (instantiate' []  [Some cfma,Some cA,Some cz] (th1 RS (not_ast_p_dvd)))
  1283 	  end
  1284       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1285       		
  1286    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
  1287       		
  1288     end;
  1289     
  1290 (* ------------------------------------------------------------------------- *)    
  1291 (* Main interpretation function for this backwards dirction*)
  1292 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
  1293 (*Help Function*)
  1294 (* ------------------------------------------------------------------------- *)
  1295 fun not_ast_p_proof_of_h sg x fm dlcm A prt = case prt of 
  1296 	(Not_ast_p_atomic(fm2)) => (generate_atomic_not_ast_p sg x fm dlcm A fm2)
  1297 	
  1298 	|(Not_ast_p_conjI(pr1,pr2)) => 
  1299 			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
  1300 			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
  1301 			    in ([th1,th2] MRS (not_ast_p_conjI))
  1302 			    end
  1303 
  1304 	|(Not_ast_p_disjI(pr1,pr2)) => 
  1305 			let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
  1306 			    val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
  1307 			    in ([th1,th2] MRS (not_ast_p_disjI))
  1308 			    end;
  1309 (* Main function*)
  1310 fun not_ast_p_proof_of sg (Not_ast_p(x as Free(xn,xT),fm,dlcm,A,prl)) =
  1311   let val th =  not_ast_p_proof_of_h sg x fm dlcm A prl
  1312       val fma = absfree (xn,xT, norm_zero_one fm)
  1313       val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
  1314   in [th,th1] MRS (not_ast_p_Q_elim)
  1315 end;
  1316 
  1317 
  1318 
  1319 
  1320 (* ------------------------------------------------------------------------- *)
  1321 (* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
  1322 (* ------------------------------------------------------------------------- *)
  1323 
  1324 
  1325 fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
  1326   (* Get the Bset thm*)
  1327   let val bst = bsetproof_of sg bsprt
  1328       val (mit1,mit2) = minf_proof_of sg dlcm miprt
  1329       val fm1 = norm_zero_one (simpl fm) 
  1330       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
  1331       val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
  1332     (* Return the four theorems needed to proove the whole Cooper Theorem*)
  1333   in (dpos,mit2,bst,nbstpthm,mit1)
  1334 end;
  1335 
  1336 
  1337 (* ------------------------------------------------------------------------- *)
  1338 (* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
  1339 (* ------------------------------------------------------------------------- *)
  1340 
  1341 
  1342 fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
  1343   let val ast = asetproof_of sg bsprt
  1344       val (mit1,mit2) = pinf_proof_of sg dlcm miprt
  1345       val fm1 = norm_zero_one (simpl fm) 
  1346       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
  1347       val nastpthm = not_ast_p_proof_of sg nast_p_prt
  1348   in (dpos,mit2,ast,nastpthm,mit1)
  1349 end;
  1350 
  1351 
  1352 (* ------------------------------------------------------------------------- *)
  1353 (* Interpretaion of Protocols of the cooper procedure : full version*)
  1354 (* ------------------------------------------------------------------------- *)
  1355 
  1356 
  1357 
  1358 fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
  1359   "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
  1360 	      val (dpsthm,th1,th2,nbpth,th3) = cooperpi_proof_of sg x prt
  1361 		   in [dpsthm,th1,th2,nbpth,th3] MRS (cppi_eq)
  1362            end
  1363   |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
  1364 	       val (dpsthm,th1,th2,nbpth,th3) = coopermi_proof_of sg x prt
  1365 		   in [dpsthm,th1,th2,nbpth,th3] MRS (cpmi_eq)
  1366                 end
  1367  |_ => error "parameter error";
  1368 
  1369 (* ------------------------------------------------------------------------- *)
  1370 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
  1371 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
  1372 (* ------------------------------------------------------------------------- *)
  1373 
  1374 fun cooper_prv sg (x as Free(xn,xT)) efm vars = let 
  1375    val l = formlcm x efm
  1376    val ac_thm = proof_of_adjustcoeffeq sg (adjustcoeffeq_wp  x l efm)
  1377    val fm = snd (qe_get_terms ac_thm)
  1378    val  cfm = unitycoeff x fm
  1379    val afm = adjustcoeff x l fm
  1380    val P = absfree(xn,xT,afm)
  1381    val ss = presburger_ss addsimps
  1382      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
  1383    val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
  1384    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
  1385    val cms = if ((length (aset x cfm)) < (length (bset x cfm))) then "pi" else "mi"
  1386    val cp_thm = cooper_thm sg cms x vars cfm
  1387    val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
  1388    val (lsuth,rsuth) = qe_get_terms (uth)
  1389    val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
  1390    val (lscth,rscth) = qe_get_terms (exp_cp_thm)
  1391    val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
  1392  in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
  1393    end
  1394 |cooper_prv _ _ _ _ = error "Parameters format";
  1395 
  1396 
  1397 (*====================================================*)
  1398 (*Interpretation function for the evaluation protokol *)
  1399 (*====================================================*)
  1400 
  1401 fun proof_of_evalc sg fm =
  1402 let
  1403 fun proof_of_evalch prt = case prt of
  1404   EvalAt(at) => prove_elementar sg "ss" at
  1405  |Evalfm(fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
  1406  |EvalConst(s,pr1,pr2) => 
  1407    let val th1 = proof_of_evalch pr1
  1408        val th2 = proof_of_evalch pr2
  1409    in case s of
  1410      "CJ" =>[th1,th2] MRS (qe_conjI)
  1411     |"DJ" =>[th1,th2] MRS (qe_disjI)
  1412     |"IM" =>[th1,th2] MRS (qe_impI)
  1413     |"EQ" =>[th1,th2] MRS (qe_eqI)
  1414     end
  1415 in proof_of_evalch (evalc_wp fm)
  1416 end;
  1417 
  1418 (*============================================================*)
  1419 (*Interpretation function for the NNF-Transformation protokol *)
  1420 (*============================================================*)
  1421 
  1422 fun proof_of_cnnf sg fm pf = 
  1423 let fun proof_of_cnnfh prt pat = case prt of
  1424   NNFAt(at) => pat at
  1425  |NNFSimp (pr) => let val th1 = proof_of_cnnfh pr pat
  1426                   in let val fm2 = snd (qe_get_terms th1) 
  1427 		     in [th1,prove_elementar sg "ss" (HOLogic.mk_eq(fm2 ,simpl fm2))] MRS trans
  1428                      end
  1429                   end
  1430  |NNFNN (pr) => (proof_of_cnnfh pr pat) RS (nnf_nn)
  1431  |NNFConst (s,pr1,pr2) =>
  1432    let val th1 = proof_of_cnnfh pr1 pat
  1433        val th2 = proof_of_cnnfh pr2 pat
  1434    in case s of
  1435      "CJ" => [th1,th2] MRS (qe_conjI)
  1436     |"DJ" => [th1,th2] MRS (qe_disjI)
  1437     |"IM" => [th1,th2] MRS (nnf_im)
  1438     |"EQ" => [th1,th2] MRS (nnf_eq)
  1439     |"SDJ" => let val (Const("op &",_)$A$_) = fst (qe_get_terms th1)
  1440 	          val (Const("op &",_)$C$_) = fst (qe_get_terms th2)
  1441 	      in [th1,th2,prove_elementar sg "ss" (HOLogic.mk_eq (A,HOLogic.Not $ C))] MRS (nnf_sdj)
  1442 	      end
  1443     |"NCJ" => [th1,th2] MRS (nnf_ncj)
  1444     |"NIM" => [th1,th2] MRS (nnf_nim)
  1445     |"NEQ" => [th1,th2] MRS (nnf_neq)
  1446     |"NDJ" => [th1,th2] MRS (nnf_ndj)
  1447    end
  1448 in proof_of_cnnfh (cnnf_wp fm) pf
  1449 end;
  1450 
  1451 
  1452 
  1453 
  1454 (*====================================================*)
  1455 (* Interpretation function for the linform protokol   *)
  1456 (*====================================================*)
  1457 
  1458 
  1459 fun proof_of_linform sg vars f = 
  1460   let fun proof_of_linformh prt = 
  1461   case prt of
  1462     (LfAt (at)) =>  prove_elementar sg "lf" (HOLogic.mk_eq (at, linform vars at))
  1463    |(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))
  1464    |(Lffm (fm)) => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
  1465    |(LfConst (s,pr1,pr2)) =>
  1466      let val th1 = proof_of_linformh pr1
  1467 	 val th2 = proof_of_linformh pr2
  1468      in case s of
  1469        "CJ" => [th1,th2] MRS (qe_conjI)
  1470       |"DJ" =>[th1,th2] MRS (qe_disjI)
  1471       |"IM" =>[th1,th2] MRS (qe_impI)
  1472       |"EQ" =>[th1,th2] MRS (qe_eqI)
  1473      end
  1474    |(LfNot(pr)) => 
  1475      let val th = proof_of_linformh pr
  1476      in (th RS (qe_Not))
  1477      end
  1478    |(LfQ(s,xn,xT,pr)) => 
  1479      let val th = forall_intr (cterm_of sg (Free(xn,xT)))(proof_of_linformh pr)
  1480      in if s = "Ex" 
  1481         then (th COMP(qe_exI) )
  1482         else (th COMP(qe_ALLI) )
  1483      end
  1484 in
  1485  proof_of_linformh (linform_wp f)
  1486 end;
  1487 
  1488 end;