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