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