src/HOL/Integ/cooper_proof.ML
author chaieb
Wed May 19 11:23:59 2004 +0200 (2004-05-19)
changeset 14758 af3b71a46a1c
parent 14479 0eca4aabf371
child 14877 28084696907f
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
     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 -> 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   val prove_elementar : Sign.sg -> string -> term -> thm
    24   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    25 end;
    26 
    27 structure CooperProof : COOPER_PROOF =
    28 struct
    29 open CooperDec;
    30 
    31 (*
    32 val presburger_ss = simpset_of (theory "Presburger")
    33   addsimps [zdiff_def] delsimps [symmetric zdiff_def];
    34 *)
    35 
    36 val presburger_ss = simpset_of (theory "Presburger")
    37   addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
    38 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    39 
    40 (*Theorems that will be used later for the proofgeneration*)
    41 
    42 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
    43 val unity_coeff_ex = thm "unity_coeff_ex";
    44 
    45 (* Thorems for proving the adjustment of the coeffitients*)
    46 
    47 val ac_lt_eq =  thm "ac_lt_eq";
    48 val ac_eq_eq = thm "ac_eq_eq";
    49 val ac_dvd_eq = thm "ac_dvd_eq";
    50 val ac_pi_eq = thm "ac_pi_eq";
    51 
    52 (* The logical compination of the sythetised properties*)
    53 val qe_Not = thm "qe_Not";
    54 val qe_conjI = thm "qe_conjI";
    55 val qe_disjI = thm "qe_disjI";
    56 val qe_impI = thm "qe_impI";
    57 val qe_eqI = thm "qe_eqI";
    58 val qe_exI = thm "qe_exI";
    59 val qe_ALLI = thm "qe_ALLI";
    60 
    61 (*Modulo D property for Pminusinf an Plusinf *)
    62 val fm_modd_minf = thm "fm_modd_minf";
    63 val not_dvd_modd_minf = thm "not_dvd_modd_minf";
    64 val dvd_modd_minf = thm "dvd_modd_minf";
    65 
    66 val fm_modd_pinf = thm "fm_modd_pinf";
    67 val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
    68 val dvd_modd_pinf = thm "dvd_modd_pinf";
    69 
    70 (* the minusinfinity proprty*)
    71 
    72 val fm_eq_minf = thm "fm_eq_minf";
    73 val neq_eq_minf = thm "neq_eq_minf";
    74 val eq_eq_minf = thm "eq_eq_minf";
    75 val le_eq_minf = thm "le_eq_minf";
    76 val len_eq_minf = thm "len_eq_minf";
    77 val not_dvd_eq_minf = thm "not_dvd_eq_minf";
    78 val dvd_eq_minf = thm "dvd_eq_minf";
    79 
    80 (* the Plusinfinity proprty*)
    81 
    82 val fm_eq_pinf = thm "fm_eq_pinf";
    83 val neq_eq_pinf = thm "neq_eq_pinf";
    84 val eq_eq_pinf = thm "eq_eq_pinf";
    85 val le_eq_pinf = thm "le_eq_pinf";
    86 val len_eq_pinf = thm "len_eq_pinf";
    87 val not_dvd_eq_pinf = thm "not_dvd_eq_pinf";
    88 val dvd_eq_pinf = thm "dvd_eq_pinf";
    89 
    90 (*Logical construction of the Property*)
    91 val eq_minf_conjI = thm "eq_minf_conjI";
    92 val eq_minf_disjI = thm "eq_minf_disjI";
    93 val modd_minf_disjI = thm "modd_minf_disjI";
    94 val modd_minf_conjI = thm "modd_minf_conjI";
    95 
    96 val eq_pinf_conjI = thm "eq_pinf_conjI";
    97 val eq_pinf_disjI = thm "eq_pinf_disjI";
    98 val modd_pinf_disjI = thm "modd_pinf_disjI";
    99 val modd_pinf_conjI = thm "modd_pinf_conjI";
   100 
   101 (*Cooper Backwards...*)
   102 (*Bset*)
   103 val not_bst_p_fm = thm "not_bst_p_fm";
   104 val not_bst_p_ne = thm "not_bst_p_ne";
   105 val not_bst_p_eq = thm "not_bst_p_eq";
   106 val not_bst_p_gt = thm "not_bst_p_gt";
   107 val not_bst_p_lt = thm "not_bst_p_lt";
   108 val not_bst_p_ndvd = thm "not_bst_p_ndvd";
   109 val not_bst_p_dvd = thm "not_bst_p_dvd";
   110 
   111 (*Aset*)
   112 val not_ast_p_fm = thm "not_ast_p_fm";
   113 val not_ast_p_ne = thm "not_ast_p_ne";
   114 val not_ast_p_eq = thm "not_ast_p_eq";
   115 val not_ast_p_gt = thm "not_ast_p_gt";
   116 val not_ast_p_lt = thm "not_ast_p_lt";
   117 val not_ast_p_ndvd = thm "not_ast_p_ndvd";
   118 val not_ast_p_dvd = thm "not_ast_p_dvd";
   119 
   120 (*Logical construction of the prop*)
   121 (*Bset*)
   122 val not_bst_p_conjI = thm "not_bst_p_conjI";
   123 val not_bst_p_disjI = thm "not_bst_p_disjI";
   124 val not_bst_p_Q_elim = thm "not_bst_p_Q_elim";
   125 
   126 (*Aset*)
   127 val not_ast_p_conjI = thm "not_ast_p_conjI";
   128 val not_ast_p_disjI = thm "not_ast_p_disjI";
   129 val not_ast_p_Q_elim = thm "not_ast_p_Q_elim";
   130 
   131 (*Cooper*)
   132 val cppi_eq = thm "cppi_eq";
   133 val cpmi_eq = thm "cpmi_eq";
   134 
   135 (*Others*)
   136 val simp_from_to = thm "simp_from_to";
   137 val P_eqtrue = thm "P_eqtrue";
   138 val P_eqfalse = thm "P_eqfalse";
   139 
   140 (*For Proving NNF*)
   141 
   142 val nnf_nn = thm "nnf_nn";
   143 val nnf_im = thm "nnf_im";
   144 val nnf_eq = thm "nnf_eq";
   145 val nnf_sdj = thm "nnf_sdj";
   146 val nnf_ncj = thm "nnf_ncj";
   147 val nnf_nim = thm "nnf_nim";
   148 val nnf_neq = thm "nnf_neq";
   149 val nnf_ndj = thm "nnf_ndj";
   150 
   151 (*For Proving term linearizition*)
   152 val linearize_dvd = thm "linearize_dvd";
   153 val lf_lt = thm "lf_lt";
   154 val lf_eq = thm "lf_eq";
   155 val lf_dvd = thm "lf_dvd";
   156 
   157 
   158 (* ------------------------------------------------------------------------- *)
   159 (*This function norm_zero_one  replaces the occurences of Numeral1 and Numeral0*)
   160 (*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
   161 (*this is necessary because the theorems use this representation.*)
   162 (* This function should be elminated in next versions...*)
   163 (* ------------------------------------------------------------------------- *)
   164 
   165 fun norm_zero_one fm = case fm of
   166   (Const ("op *",_) $ c $ t) => 
   167     if c = one then (norm_zero_one t)
   168     else if (dest_numeral c = ~1) 
   169          then (Const("uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t))
   170          else (HOLogic.mk_binop "op *" (norm_zero_one c,norm_zero_one t))
   171   |(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest))
   172   |(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
   173   |_ => fm;
   174 
   175 (* ------------------------------------------------------------------------- *)
   176 (*function list to Set, constructs a set containing all elements of a given list.*)
   177 (* ------------------------------------------------------------------------- *)
   178 fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in 
   179 	case l of 
   180 		[] => Const ("{}",T)
   181 		|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
   182 		end;
   183 		
   184 (* ------------------------------------------------------------------------- *)
   185 (* Returns both sides of an equvalence in the theorem*)
   186 (* ------------------------------------------------------------------------- *)
   187 fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
   188 
   189 (* ------------------------------------------------------------------------- *)
   190 (* Modified version of the simple version with minimal amount of checking and postprocessing*)
   191 (* ------------------------------------------------------------------------- *)
   192 
   193 fun simple_prove_goal_cterm2 G tacs =
   194   let
   195     fun check None = error "prove_goal: tactic failed"
   196       | check (Some (thm, _)) = (case nprems_of thm of
   197             0 => thm
   198           | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
   199   in check (Seq.pull (EVERY tacs (trivial G))) end;
   200 
   201 (*-------------------------------------------------------------*)
   202 (*-------------------------------------------------------------*)
   203 
   204 fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
   205 
   206 (* ------------------------------------------------------------------------- *)
   207 (*This function proove elementar will be used to generate proofs at runtime*)
   208 (*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
   209 (*prove properties such as a dvd b (essentially) that are only to make at
   210 runtime.*)
   211 (* ------------------------------------------------------------------------- *)
   212 fun prove_elementar sg s fm2 = case s of 
   213   (*"ss" like simplification with simpset*)
   214   "ss" =>
   215     let
   216       val ss = presburger_ss addsimps
   217         [zdvd_iff_zmod_eq_0,unity_coeff_ex]
   218       val ct =  cert_Trueprop sg fm2
   219     in 
   220       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   221     end
   222 
   223   (*"bl" like blast tactic*)
   224   (* Is only used in the harrisons like proof procedure *)
   225   | "bl" =>
   226      let val ct = cert_Trueprop sg fm2
   227      in
   228        simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
   229      end
   230 
   231   (*"ed" like Existence disjunctions ...*)
   232   (* Is only used in the harrisons like proof procedure *)
   233   | "ed" =>
   234     let
   235       val ex_disj_tacs =
   236         let
   237           val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1]
   238           val tac2 = EVERY[etac exE 1, rtac exI 1,
   239             REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1]
   240 	in [rtac iffI 1,
   241           etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
   242           REPEAT(EVERY[etac disjE 1, tac2]), tac2]
   243         end
   244 
   245       val ct = cert_Trueprop sg fm2
   246     in 
   247       simple_prove_goal_cterm2 ct ex_disj_tacs
   248     end
   249 
   250   | "fa" =>
   251     let val ct = cert_Trueprop sg fm2
   252     in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
   253     end
   254 
   255   | "sa" =>
   256     let
   257       val ss = presburger_ss addsimps zadd_ac
   258       val ct = cert_Trueprop sg fm2
   259     in 
   260       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   261     end
   262   (* like Existance Conjunction *)
   263   | "ec" =>
   264     let
   265       val ss = presburger_ss addsimps zadd_ac
   266       val ct = cert_Trueprop sg fm2
   267     in 
   268       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
   269     end
   270 
   271   | "ac" =>
   272     let
   273       val ss = HOL_basic_ss addsimps zadd_ac
   274       val ct = cert_Trueprop sg fm2
   275     in 
   276       simple_prove_goal_cterm2 ct [simp_tac ss 1]
   277     end
   278 
   279   | "lf" =>
   280     let
   281       val ss = presburger_ss addsimps zadd_ac
   282       val ct = cert_Trueprop sg fm2
   283     in 
   284       simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
   285     end;
   286 
   287 (*=============================================================*)
   288 (*-------------------------------------------------------------*)
   289 (*              The new compact model                          *)
   290 (*-------------------------------------------------------------*)
   291 (*=============================================================*)
   292 
   293 fun thm_of sg decomp t = 
   294     let val (ts,recomb) = decomp t 
   295     in recomb (map (thm_of sg decomp) ts) 
   296     end;
   297 
   298 (*==================================================*)
   299 (*     Compact Version for adjustcoeffeq            *)
   300 (*==================================================*)
   301 
   302 fun decomp_adjustcoeffeq sg x l fm = case fm of
   303     (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $    c $ y ) $z )))) => 
   304      let  
   305         val m = l div (dest_numeral c) 
   306         val n = if (x = y) then abs (m) else 1
   307         val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) 
   308         val rs = if (x = y) 
   309                  then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) 
   310                  else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
   311         val ck = cterm_of sg (mk_numeral n)
   312         val cc = cterm_of sg c
   313         val ct = cterm_of sg z
   314         val cx = cterm_of sg y
   315         val pre = prove_elementar sg "lf" 
   316             (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
   317         val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
   318         in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   319         end
   320 
   321   |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $ 
   322       c $ y ) $t )) => 
   323    if (is_arith_rel fm) andalso (x = y) 
   324    then  
   325         let val m = l div (dest_numeral c) 
   326            val k = (if p = "op <" then abs(m) else m)  
   327            val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
   328            val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) )))) 
   329 
   330            val ck = cterm_of sg (mk_numeral k)
   331            val cc = cterm_of sg c
   332            val ct = cterm_of sg t
   333            val cx = cterm_of sg x
   334            val ca = cterm_of sg a
   335 
   336 	   in 
   337 	case p of
   338 	  "op <" => 
   339 	let val pre = prove_elementar sg "lf" 
   340 	    (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
   341             val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
   342 	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   343          end
   344 
   345            |"op =" =>
   346 	     let val pre = prove_elementar sg "lf" 
   347 	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   348 	         val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
   349 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   350              end
   351 
   352              |"Divides.op dvd" =>
   353 	       let val pre = prove_elementar sg "lf" 
   354 	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
   355                    val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
   356                in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
   357                         
   358                end
   359               end
   360   else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
   361 
   362  |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
   363   |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   364   |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
   365 
   366   |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
   367 
   368 (*==================================================*)
   369 (*   Finding rho for modd_minusinfinity             *)
   370 (*==================================================*)
   371 fun rho_for_modd_minf x dlcm sg fm1 =
   372 let
   373     (*Some certified Terms*)
   374     
   375    val ctrue = cterm_of sg HOLogic.true_const
   376    val cfalse = cterm_of sg HOLogic.false_const
   377    val fm = norm_zero_one fm1
   378   in  case fm1 of 
   379       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   380          if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   381            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   382 
   383       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   384   	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
   385 	   then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf))
   386 	 	 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)) 
   387 
   388       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   389            if (y=x) andalso (c1 = zero) then 
   390             if (pm1 = one) then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf)) else
   391 	     (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
   392 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   393   
   394       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   395          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   396 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   397 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
   398 		      end
   399 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   400       |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   401       c $ y ) $ z))) => 
   402          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   403 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   404 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
   405 		      end
   406 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   407 		
   408     
   409    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
   410    end;	 
   411 (*=========================================================================*)
   412 (*=========================================================================*)
   413 fun rho_for_eq_minf x dlcm  sg fm1 =  
   414    let
   415    val fm = norm_zero_one fm1
   416     in  case fm1 of 
   417       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   418          if  (x=y) andalso (c1=zero) andalso (c2=one) 
   419 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   420            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   421 
   422       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   423   	   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))
   424 	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
   425 	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf)) 
   426 
   427       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   428            if (y=x) andalso (c1 =zero) then 
   429             if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
   430 	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_minf))
   431 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   432       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   433          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   434 	 		  val cz = cterm_of sg (norm_zero_one z)
   435 	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_minf)) 
   436 		      end
   437 
   438 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   439 		
   440       |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   441          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   442 	 		  val cz = cterm_of sg (norm_zero_one z)
   443 	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_minf))
   444 		      end
   445 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   446 
   447       		
   448     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   449  end;
   450 
   451 (*=====================================================*)
   452 (*=====================================================*)
   453 (*=========== minf proofs with the compact version==========*)
   454 fun decomp_minf_eq x dlcm sg t =  case t of
   455    Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
   456    |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
   457    |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
   458 
   459 fun decomp_minf_modd x dlcm sg t = case t of
   460    Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
   461    |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
   462    |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
   463 
   464 (* -------------------------------------------------------------*)
   465 (*                    Finding rho for pinf_modd                 *)
   466 (* -------------------------------------------------------------*)
   467 fun rho_for_modd_pinf x dlcm sg fm1 = 
   468 let
   469     (*Some certified Terms*)
   470     
   471   val ctrue = cterm_of sg HOLogic.true_const
   472   val cfalse = cterm_of sg HOLogic.false_const
   473   val fm = norm_zero_one fm1
   474  in  case fm1 of 
   475       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   476          if ((x=y) andalso (c1= zero) andalso (c2= one))
   477 	 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
   478          else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   479 
   480       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   481   	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
   482 	then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   483 	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   484 
   485       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   486         if ((y=x) andalso (c1 = zero)) then 
   487           if (pm1 = one) 
   488 	  then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf)) 
   489 	  else (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   490 	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   491   
   492       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   493          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   494 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   495 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
   496 		      end
   497 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   498       |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   499       c $ y ) $ z))) => 
   500          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   501 			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   502 	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
   503 		      end
   504 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   505 		
   506     
   507    |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
   508    end;	
   509 (* -------------------------------------------------------------*)
   510 (*                    Finding rho for pinf_eq                 *)
   511 (* -------------------------------------------------------------*)
   512 fun rho_for_eq_pinf x dlcm sg fm1 = 
   513   let
   514 					val fm = norm_zero_one fm1
   515     in  case fm1 of 
   516       (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   517          if  (x=y) andalso (c1=zero) andalso (c2=one) 
   518 	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
   519            else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   520 
   521       |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   522   	   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))
   523 	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
   524 	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf)) 
   525 
   526       |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   527            if (y=x) andalso (c1 =zero) then 
   528             if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
   529 	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
   530 	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   531       |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   532          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   533 	 		  val cz = cterm_of sg (norm_zero_one z)
   534 	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_pinf)) 
   535 		      end
   536 
   537 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   538 		
   539       |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   540          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   541 	 		  val cz = cterm_of sg (norm_zero_one z)
   542 	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_pinf))
   543 		      end
   544 		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   545 
   546       		
   547     |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   548  end;
   549 
   550 
   551 
   552 fun  minf_proof_of_c sg x dlcm t =
   553   let val minf_eqth   = thm_of sg (decomp_minf_eq x dlcm sg) t
   554       val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
   555   in (minf_eqth, minf_moddth)
   556 end;
   557 
   558 (*=========== pinf proofs with the compact version==========*)
   559 fun decomp_pinf_eq x dlcm sg t = case t of
   560    Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
   561    |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
   562    |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
   563 
   564 fun decomp_pinf_modd x dlcm sg t =  case t of
   565    Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
   566    |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
   567    |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
   568 
   569 fun  pinf_proof_of_c sg x dlcm t =
   570   let val pinf_eqth   = thm_of sg (decomp_pinf_eq x dlcm sg) t
   571       val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
   572   in (pinf_eqth,pinf_moddth)
   573 end;
   574 
   575 
   576 (* ------------------------------------------------------------------------- *)
   577 (* Here we generate the theorem for the Bset Property in the simple direction*)
   578 (* It is just an instantiation*)
   579 (* ------------------------------------------------------------------------- *)
   580 (*
   581 fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm   = 
   582   let
   583     val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   584     val cdlcm = cterm_of sg dlcm
   585     val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
   586   in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
   587 end;
   588 
   589 fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = 
   590   let
   591     val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   592     val cdlcm = cterm_of sg dlcm
   593     val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
   594   in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
   595 end;
   596 *)
   597 
   598 (* For the generation of atomic Theorems*)
   599 (* Prove the premisses on runtime and then make RS*)
   600 (* ------------------------------------------------------------------------- *)
   601 
   602 (*========= this is rho ============*)
   603 fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = 
   604   let
   605     val cdlcm = cterm_of sg dlcm
   606     val cB = cterm_of sg B
   607     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   608     val cat = cterm_of sg (norm_zero_one at)
   609   in
   610   case at of 
   611    (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   612       if  (x=y) andalso (c1=zero) andalso (c2=one) 
   613 	 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)
   614 	          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)))
   615 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   616 	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
   617 	 end
   618          else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   619 
   620    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
   621      if (is_arith_rel at) andalso (x=y)
   622 	then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
   623 	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
   624 	          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))))
   625 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   626 	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
   627 	 end
   628        end
   629          else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   630 
   631    |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   632         if (y=x) andalso (c1 =zero) then 
   633         if pm1 = one then 
   634 	  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)
   635               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)))
   636 	  in  (instantiate' [] [Some cfma,  Some cdlcm]([th1,th2] MRS (not_bst_p_gt)))
   637 	    end
   638 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   639 	      in (instantiate' [] [Some cfma, Some cB,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
   640 	      end
   641       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   642 
   643    |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   644       if y=x then  
   645            let val cz = cterm_of sg (norm_zero_one z)
   646 	       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)
   647  	     in (instantiate' []  [Some cfma, Some cB,Some cz] (th1 RS (not_bst_p_ndvd)))
   648 	     end
   649       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   650 
   651    |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   652        if y=x then  
   653 	 let val cz = cterm_of sg (norm_zero_one z)
   654 	     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)
   655  	    in (instantiate' []  [Some cfma,Some cB,Some cz] (th1 RS (not_bst_p_dvd)))
   656 	  end
   657       else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   658       		
   659    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   660       		
   661     end;
   662     
   663 
   664 (* ------------------------------------------------------------------------- *)    
   665 (* Main interpretation function for this backwards dirction*)
   666 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
   667 (*Help Function*)
   668 (* ------------------------------------------------------------------------- *)
   669 
   670 (*==================== Proof with the compact version   *)
   671 
   672 fun decomp_nbstp sg x dlcm B fm t = case t of 
   673    Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
   674   |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
   675   |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
   676 
   677 fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
   678   let 
   679        val th =  thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
   680       val fma = absfree (xn,xT, norm_zero_one fm)
   681   in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
   682      in [th,th1] MRS (not_bst_p_Q_elim)
   683      end
   684   end;
   685 
   686 
   687 (* ------------------------------------------------------------------------- *)    
   688 (* Protokol interpretation function for the backwards direction for cooper's Theorem*)
   689 
   690 (* For the generation of atomic Theorems*)
   691 (* Prove the premisses on runtime and then make RS*)
   692 (* ------------------------------------------------------------------------- *)
   693 (*========= this is rho ============*)
   694 fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = 
   695   let
   696     val cdlcm = cterm_of sg dlcm
   697     val cA = cterm_of sg A
   698     val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   699     val cat = cterm_of sg (norm_zero_one at)
   700   in
   701   case at of 
   702    (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   703       if  (x=y) andalso (c1=zero) andalso (c2=one) 
   704 	 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)
   705 	          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)))
   706 		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   707 	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
   708 	 end
   709          else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   710 
   711    |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
   712      if (is_arith_rel at) andalso (x=y)
   713 	then let val ast_z = norm_zero_one (linear_sub [] one z )
   714 	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
   715 	         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))))
   716 		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   717 	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
   718        end
   719          else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   720 
   721    |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   722         if (y=x) andalso (c1 =zero) then 
   723         if pm1 = (mk_numeral ~1) then 
   724 	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
   725               val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
   726 	  in  (instantiate' [] [Some cfma]([th2,th1] MRS (not_ast_p_lt)))
   727 	    end
   728 	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   729 	      in (instantiate' [] [Some cfma, Some cA,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
   730 	      end
   731       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   732 
   733    |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   734       if y=x then  
   735            let val cz = cterm_of sg (norm_zero_one z)
   736 	       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)
   737  	     in (instantiate' []  [Some cfma, Some cA,Some cz] (th1 RS (not_ast_p_ndvd)))
   738 	     end
   739       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   740 
   741    |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   742        if y=x then  
   743 	 let val cz = cterm_of sg (norm_zero_one z)
   744 	     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)
   745  	    in (instantiate' []  [Some cfma,Some cA,Some cz] (th1 RS (not_ast_p_dvd)))
   746 	  end
   747       else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   748       		
   749    |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   750       		
   751     end;
   752 
   753 (* ------------------------------------------------------------------------ *)
   754 (* Main interpretation function for this backwards dirction*)
   755 (* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
   756 (*Help Function*)
   757 (* ------------------------------------------------------------------------- *)
   758 
   759 fun decomp_nastp sg x dlcm A fm t = case t of 
   760    Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
   761   |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
   762   |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
   763 
   764 fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
   765   let 
   766        val th =  thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
   767       val fma = absfree (xn,xT, norm_zero_one fm)
   768   in let val th1 =  prove_elementar sg "ss"  (HOLogic.mk_eq (fma,fma))
   769      in [th,th1] MRS (not_ast_p_Q_elim)
   770      end
   771   end;
   772 
   773 
   774 (* -------------------------------*)
   775 (* Finding rho and beta for evalc *)
   776 (* -------------------------------*)
   777 
   778 fun rho_for_evalc sg at = case at of  
   779     (Const (p,_) $ s $ t) =>(  
   780     case assoc (operations,p) of 
   781         Some f => 
   782            ((if (f ((dest_numeral s),(dest_numeral t))) 
   783              then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
   784              else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
   785 		   handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl
   786         | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )) 
   787      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   788        case assoc (operations,p) of 
   789          Some f => 
   790            ((if (f ((dest_numeral s),(dest_numeral t))) 
   791              then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
   792              else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
   793 		      handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl) 
   794          | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ) 
   795      | _ =>   instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
   796 
   797 
   798 (*=========================================================*)
   799 fun decomp_evalc sg t = case t of
   800    (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   801    |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
   802    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
   803    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   804    |_ => ([], fn [] => rho_for_evalc sg t);
   805 
   806 
   807 fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
   808 
   809 (*==================================================*)
   810 (*     Proof of linform with the compact model      *)
   811 (*==================================================*)
   812 
   813 
   814 fun decomp_linform sg vars t = case t of
   815    (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   816    |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
   817    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
   818    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   819    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
   820    |(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)))
   821    |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
   822 
   823 fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
   824 
   825 (* ------------------------------------------------------------------------- *)
   826 (* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
   827 (* ------------------------------------------------------------------------- *)
   828 fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
   829   (* Get the Bset thm*)
   830   let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm 
   831       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
   832       val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
   833   in (dpos,minf_eqth,nbstpthm,minf_moddth)
   834 end;
   835 
   836 (* ------------------------------------------------------------------------- *)
   837 (* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
   838 (* ------------------------------------------------------------------------- *)
   839 fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
   840   let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
   841       val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
   842       val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
   843   in (dpos,pinf_eqth,nastpthm,pinf_moddth)
   844 end;
   845 
   846 (* ------------------------------------------------------------------------- *)
   847 (* Interpretaion of Protocols of the cooper procedure : full version*)
   848 (* ------------------------------------------------------------------------- *)
   849 fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
   850   "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm 
   851 	      in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
   852            end
   853   |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
   854 	       in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
   855                 end
   856  |_ => error "parameter error";
   857 
   858 (* ------------------------------------------------------------------------- *)
   859 (* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*)
   860 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
   861 (* ------------------------------------------------------------------------- *)
   862 
   863 fun cooper_prv sg (x as Free(xn,xT)) efm = let 
   864    val lfm_thm = proof_of_linform sg [xn] efm
   865    val efm2 = snd(qe_get_terms lfm_thm)
   866    val l = formlcm x efm2
   867    val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
   868    val fm = snd (qe_get_terms ac_thm)
   869    val  cfm = unitycoeff x fm
   870    val afm = adjustcoeff x l fm
   871    val P = absfree(xn,xT,afm)
   872    val ss = presburger_ss addsimps
   873      [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
   874    val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
   875    val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
   876    val A = aset x cfm
   877    val B = bset x cfm
   878    val dlcm = mk_numeral (divlcm x cfm)
   879    val cms = if ((length A) < (length B )) then "pi" else "mi"
   880    val cp_thm = cooper_thm sg cms x cfm dlcm A B
   881    val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
   882    val (lsuth,rsuth) = qe_get_terms (uth)
   883    val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
   884    val (lscth,rscth) = qe_get_terms (exp_cp_thm)
   885    val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
   886  in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
   887    end
   888 |cooper_prv _ _ _ =  error "Parameters format";
   889 
   890 
   891 
   892 fun decomp_cnnf sg lfnp P = case P of 
   893      Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
   894    |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS  qe_disjI)
   895    |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
   896    |Const("Not",_) $ (Const(opn,T) $ p $ q) => 
   897      if opn = "op |" 
   898       then case (p,q) of 
   899          (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
   900           if r1 = negate r 
   901           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)
   902 
   903           else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
   904         |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
   905       else (
   906          case (opn,T) of 
   907            ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
   908            |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
   909            |("op =",Type ("fun",[Type ("bool", []),_])) => 
   910            ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
   911             |(_,_) => ([], fn [] => lfnp P)
   912 )
   913 
   914    |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
   915 
   916    |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
   917      ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
   918    |_ => ([], fn [] => lfnp P);
   919 
   920 
   921 
   922 
   923 fun proof_of_cnnf sg p lfnp = 
   924  let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
   925      val rs = snd(qe_get_terms th1)
   926      val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
   927   in [th1,th2] MRS trans
   928   end;
   929 
   930 end;