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