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