src/HOL/Integ/presburger.ML
author wenzelm
Sat, 08 Jul 2006 12:54:41 +0200
changeset 20053 7f32ce6354d6
parent 19277 f7602e74d948
child 20194 c9dbce9a23a1
permissions -rw-r--r--
presburger_ss: proper context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Integ/presburger.ML
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
     3
    Author:     Amine Chaieb and Stefan Berghofer, TU Muenchen
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
     4
17465
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
     5
Tactic for solving arithmetical Goals in Presburger Arithmetic.
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
     6
17465
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
     7
This version of presburger deals with occurences of functional symbols
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
     8
in the subgoal and abstract over them to try to prove the more general
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
     9
formula. It then resolves with the subgoal. To enable this feature
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
    10
call the procedure with the parameter abs.
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    11
*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    12
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    13
signature PRESBURGER = 
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    14
sig
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    15
 val presburger_tac : bool -> bool -> int -> tactic
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    16
 val presburger_method : bool -> bool -> int -> Proof.method
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
    17
 val setup : theory -> theory
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    18
 val trace : bool ref
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    19
end;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    20
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    21
structure Presburger: PRESBURGER =
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    22
struct
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    23
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    24
val trace = ref false;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    25
fun trace_msg s = if !trace then tracing s else ();
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    26
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    27
(*-----------------------------------------------------------------*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    28
(*cooper_pp: provefunction for the one-exstance quantifier elimination*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    29
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    30
(*-----------------------------------------------------------------*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    31
14941
1edb674e0c33 Oracle corrected
chaieb
parents: 14920
diff changeset
    32
20053
7f32ce6354d6 presburger_ss: proper context;
wenzelm
parents: 19277
diff changeset
    33
val presburger_ss = simpset ();
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    34
val binarith = map thm
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    35
  ["Pls_0_eq", "Min_1_eq",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    36
 "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    37
  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    38
  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    39
  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    40
  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    41
  "bin_add_Pls_right", "bin_add_Min_right"];
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    42
 val intarithrel = 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    43
     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    44
		"int_le_number_of_eq","int_iszero_number_of_0",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    45
		"int_less_number_of_eq_neg"]) @
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    46
     (map (fn s => thm s RS thm "lift_bool") 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    47
	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    48
	   "int_neg_number_of_Min"])@
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    49
     (map (fn s => thm s RS thm "nlift_bool") 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    50
	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    51
     
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    52
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    53
			"int_number_of_diff_sym", "int_number_of_mult_sym"];
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    54
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    55
			"mult_nat_number_of", "eq_nat_number_of",
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    56
			"less_nat_number_of"]
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    57
val powerarith = 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    58
    (map thm ["nat_number_of", "zpower_number_of_even", 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    59
	      "zpower_Pls", "zpower_Min"]) @ 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    60
    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    61
			   thm "one_eq_Numeral1_nring"] 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    62
  (thm "zpower_number_of_odd"))]
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    63
18393
af72cbfa00a5 deals with Suc in mod expressions
chaieb
parents: 18202
diff changeset
    64
val comp_arith = binarith @ intarith @ intarithrel @ natarith 
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    65
	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
14801
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
    66
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    67
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    68
  let val (xn1,p1) = variant_abs (xn,xT,p)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    69
  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    70
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    71
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    72
  (CooperProof.proof_of_evalc sg);
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    73
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    74
fun tmproof_of_int_qelim sg fm =
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    75
  Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    76
    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    77
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
    78
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    79
(* Theorems to be used in this tactic*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    80
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    81
val zdvd_int = thm "zdvd_int";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    82
val zdiff_int_split = thm "zdiff_int_split";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    83
val all_nat = thm "all_nat";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    84
val ex_nat = thm "ex_nat";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    85
val number_of1 = thm "number_of1";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    86
val number_of2 = thm "number_of2";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    87
val split_zdiv = thm "split_zdiv";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    88
val split_zmod = thm "split_zmod";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    89
val mod_div_equality' = thm "mod_div_equality'";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    90
val split_div' = thm "split_div'";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    91
val Suc_plus1 = thm "Suc_plus1";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    92
val imp_le_cong = thm "imp_le_cong";
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
    93
val conj_le_cong = thm "conj_le_cong";
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    94
val nat_mod_add_eq = mod_add1_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    95
val nat_mod_add_left_eq = mod_add_left_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    96
val nat_mod_add_right_eq = mod_add_right_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    97
val int_mod_add_eq = zmod_zadd1_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    98
val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
    99
val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   100
val nat_div_add_eq = div_add1_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   101
val int_div_add_eq = zdiv_zadd1_eq RS sym;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   102
val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   103
val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   104
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   105
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   106
(* extract all the constants in a term*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   107
fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   108
  | add_term_typed_consts (t $ u, cs) =
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   109
      add_term_typed_consts (t, add_term_typed_consts (u, cs))
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   110
  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   111
  | add_term_typed_consts (_, cs) = cs;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   112
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   113
fun term_typed_consts t = add_term_typed_consts(t,[]);
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   114
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15620
diff changeset
   115
(* Some Types*)
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   116
val bT = HOLogic.boolT;
15620
8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals
paulson
parents: 15574
diff changeset
   117
val bitT = HOLogic.bitT;
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   118
val iT = HOLogic.intT;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   119
val binT = HOLogic.binT;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   120
val nT = HOLogic.natT;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   121
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   122
(* Allowed Consts in formulae for presburger tactic*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   123
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   124
val allowed_consts =
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   125
  [("All", (iT --> bT) --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   126
   ("Ex", (iT --> bT) --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   127
   ("All", (nT --> bT) --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   128
   ("Ex", (nT --> bT) --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   129
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   130
   ("op &", bT --> bT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   131
   ("op |", bT --> bT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   132
   ("op -->", bT --> bT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   133
   ("op =", bT --> bT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   134
   ("Not", bT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   135
19277
f7602e74d948 renamed op < <= to Orderings.less(_eq)
haftmann
parents: 19233
diff changeset
   136
   ("Orderings.less_eq", iT --> iT --> bT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   137
   ("op =", iT --> iT --> bT),
19277
f7602e74d948 renamed op < <= to Orderings.less(_eq)
haftmann
parents: 19233
diff changeset
   138
   ("Orderings.less", iT --> iT --> bT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   139
   ("Divides.op dvd", iT --> iT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   140
   ("Divides.op div", iT --> iT --> iT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   141
   ("Divides.op mod", iT --> iT --> iT),
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   142
   ("HOL.plus", iT --> iT --> iT),
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   143
   ("HOL.minus", iT --> iT --> iT),
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   144
   ("HOL.times", iT --> iT --> iT), 
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   145
   ("HOL.abs", iT --> iT),
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   146
   ("HOL.uminus", iT --> iT),
14801
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
   147
   ("HOL.max", iT --> iT --> iT),
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
   148
   ("HOL.min", iT --> iT --> iT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   149
19277
f7602e74d948 renamed op < <= to Orderings.less(_eq)
haftmann
parents: 19233
diff changeset
   150
   ("Orderings.less_eq", nT --> nT --> bT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   151
   ("op =", nT --> nT --> bT),
19277
f7602e74d948 renamed op < <= to Orderings.less(_eq)
haftmann
parents: 19233
diff changeset
   152
   ("Orderings.less", nT --> nT --> bT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   153
   ("Divides.op dvd", nT --> nT --> bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   154
   ("Divides.op div", nT --> nT --> nT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   155
   ("Divides.op mod", nT --> nT --> nT),
19233
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   156
   ("HOL.plus", nT --> nT --> nT),
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   157
   ("HOL.minus", nT --> nT --> nT),
77ca20b0ed77 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents: 18708
diff changeset
   158
   ("HOL.times", nT --> nT --> nT), 
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   159
   ("Suc", nT --> nT),
14801
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
   160
   ("HOL.max", nT --> nT --> nT),
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
   161
   ("HOL.min", nT --> nT --> nT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   162
15620
8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals
paulson
parents: 15574
diff changeset
   163
   ("Numeral.bit.B0", bitT),
8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals
paulson
parents: 15574
diff changeset
   164
   ("Numeral.bit.B1", bitT),
8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals
paulson
parents: 15574
diff changeset
   165
   ("Numeral.Bit", binT --> bitT --> binT),
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14981
diff changeset
   166
   ("Numeral.Pls", binT),
34264f5e4691 new treatment of binary numerals
paulson
parents: 14981
diff changeset
   167
   ("Numeral.Min", binT),
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   168
   ("Numeral.number_of", binT --> iT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   169
   ("Numeral.number_of", binT --> nT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   170
   ("0", nT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   171
   ("0", iT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   172
   ("1", nT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   173
   ("1", iT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   174
   ("False", bT),
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   175
   ("True", bT)];
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   176
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   177
(* Preparation of the formula to be sent to the Integer quantifier *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   178
(* elimination procedure                                           *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   179
(* Transforms meta implications and meta quantifiers to object     *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   180
(* implications and object quantifiers                             *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   181
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   182
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   183
(*==================================*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   184
(* Abstracting on subterms  ========*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   185
(*==================================*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   186
(* Returns occurences of terms that are function application of type int or nat*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   187
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   188
fun getfuncs fm = case strip_comb fm of
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   189
    (Free (_, T), ts as _ :: _) =>
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   190
      if body_type T mem [iT, nT] 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   191
         andalso not (ts = []) andalso forall (null o loose_bnos) ts 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   192
      then [fm]
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   193
      else Library.foldl op union ([], map getfuncs ts)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   194
  | (Var (_, T), ts as _ :: _) =>
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   195
      if body_type T mem [iT, nT] 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   196
         andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   197
      else Library.foldl op union ([], map getfuncs ts)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   198
  | (Const (s, T), ts) =>
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   199
      if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   200
      then Library.foldl op union ([], map getfuncs ts)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   201
      else [fm]
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   202
  | (Abs (s, T, t), _) => getfuncs t
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   203
  | _ => [];
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   204
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   205
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   206
fun abstract_pres sg fm = 
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   207
  foldr (fn (t, u) =>
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   208
      let val T = fastype_of t
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   209
      in all T $ Abs ("x", T, abstract_over (t, u)) end)
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   210
         fm (getfuncs fm);
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   211
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   212
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   213
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   214
(* hasfuncs_on_bounds dont care of the type of the functions applied!
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   215
 It returns true if there is a subterm coresponding to the application of
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   216
 a function on a bounded variable.
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   217
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   218
 Function applications are allowed only for well predefined functions a 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   219
 consts*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   220
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   221
fun has_free_funcs fm  = case strip_comb fm of
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   222
    (Free (_, T), ts as _ :: _) => 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   223
      if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   224
      then true
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   225
      else exists (fn x => x) (map has_free_funcs ts)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   226
  | (Var (_, T), ts as _ :: _) =>
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   227
      if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   228
      then true
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   229
      else exists (fn x => x) (map has_free_funcs ts)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   230
  | (Const (s, T), ts) =>  exists (fn x => x) (map has_free_funcs ts)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   231
  | (Abs (s, T, t), _) => has_free_funcs t
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   232
  |_ => false;
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   233
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   234
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   235
(*returns true if the formula is relevant for presburger arithmetic tactic
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   236
The constants occuring in term t should be a subset of the allowed_consts
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   237
 There also should be no occurences of application of functions on bounded 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   238
 variables. Whenever this function will be used, it will be ensured that t 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   239
 will not contain subterms with function symbols that could have been 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   240
 abstracted over.*)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   241
 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   242
fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   243
  map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   244
  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   245
  subset [iT, nT]
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   246
  andalso not (has_free_funcs t);
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   247
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   248
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   249
fun prepare_for_presburger sg q fm = 
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   250
  let
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   251
    val ps = Logic.strip_params fm
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   252
    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   253
    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   254
    val _ = if relevant (rev ps) c then () 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   255
               else  (trace_msg ("Conclusion is not a presburger term:\n" ^
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   256
             Sign.string_of_term sg c); raise CooperDec.COOPER)
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   257
    fun mk_all ((s, T), (P,n)) =
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   258
      if 0 mem loose_bnos P then
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   259
        (HOLogic.all_const T $ Abs (s, T, P), n)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   260
      else (incr_boundvars ~1 P, n-1)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   261
    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   262
    val (rhs,irhs) = List.partition (relevant (rev ps)) hs
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   263
    val np = length ps
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   264
    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   265
      (foldr HOLogic.mk_imp c rhs, np) ps
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   266
    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   267
      (term_frees fm' @ term_vars fm');
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   268
    val fm2 = foldr mk_all2 fm' vs
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   269
  in (fm2, np + length vs, length rhs) end;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   270
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   271
(*Object quantifier to meta --*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   272
fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   273
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   274
(* object implication to meta---*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   275
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   276
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   277
(* the presburger tactic*)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   278
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   279
(* Parameters : q = flag for quantify ofer free variables ; 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   280
                a = flag for abstracting over function occurences
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   281
                i = subgoal  *)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   282
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   283
fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   284
  let
17465
93fc1211603f removed obsolete BasisLibrary;
wenzelm
parents: 16836
diff changeset
   285
    val g = List.nth (prems_of st, i - 1)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   286
    val sg = sign_of_thm st
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   287
    (* The Abstraction step *)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   288
    val g' = if a then abstract_pres sg g else g
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   289
    (* Transform the term*)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   290
    val (t,np,nh) = prepare_for_presburger sg q g'
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15620
diff changeset
   291
    (* Some simpsets for dealing with mod div abs and nat*)
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   292
    val mod_div_simpset = HOL_basic_ss 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   293
			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   294
				  nat_mod_add_right_eq, int_mod_add_eq, 
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   295
				  int_mod_add_right_eq, int_mod_add_left_eq,
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   296
				  nat_div_add_eq, int_div_add_eq,
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   297
				  mod_self, zmod_self,
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   298
				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   299
				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   300
				  zdiv_zero,zmod_zero,div_0,mod_0,
18393
af72cbfa00a5 deals with Suc in mod expressions
chaieb
parents: 18202
diff changeset
   301
				  zdiv_1,zmod_1,div_1,mod_1,
af72cbfa00a5 deals with Suc in mod expressions
chaieb
parents: 18202
diff changeset
   302
				  Suc_plus1]
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   303
			addsimps add_ac
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   304
			addsimprocs [cancel_div_mod_proc]
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   305
    val simpset0 = HOL_basic_ss
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   306
      addsimps [mod_div_equality', Suc_plus1]
18393
af72cbfa00a5 deals with Suc in mod expressions
chaieb
parents: 18202
diff changeset
   307
      addsimps comp_arith
13997
3d53dcd77877 - Added split_min and split_max to preprocessor
berghofe
parents: 13892
diff changeset
   308
      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   309
    (* Simp rules for changing (n::int) to int n *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   310
    val simpset1 = HOL_basic_ss
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   311
      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   312
        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   313
      addsplits [zdiff_int_split]
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   314
    (*simp rules for elimination of int n*)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   315
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   316
    val simpset2 = HOL_basic_ss
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   317
      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   318
      addcongs [conj_le_cong, imp_le_cong]
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   319
    (* simp rules for elimination of abs *)
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14130
diff changeset
   320
    val simpset3 = HOL_basic_ss addsplits [abs_split]
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   321
    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   322
    (* Theorem for the nat --> int transformation *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   323
    val pre_thm = Seq.hd (EVERY
18202
46af82efd311 presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents: 18155
diff changeset
   324
      [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   325
       TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
14801
2d27b5ebc447 - deleted unneeded function eta_long (now in Pure/pattern.ML
berghofe
parents: 14758
diff changeset
   326
       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   327
      (trivial ct))
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   328
    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   329
    (* The result of the quantifier elimination *)
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   330
    val (th, tac) = case (prop_of pre_thm) of
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   331
        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
14920
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   332
    let val pth = 
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   333
          (* If quick_and_dirty then run without proof generation as oracle*)
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   334
             if !quick_and_dirty 
16836
45a3dc4688bc improved oracle setup;
wenzelm
parents: 15661
diff changeset
   335
             then presburger_oracle sg (Pattern.eta_long [] t1)
14941
1edb674e0c33 Oracle corrected
chaieb
parents: 14920
diff changeset
   336
(*
1edb674e0c33 Oracle corrected
chaieb
parents: 14920
diff changeset
   337
assume (cterm_of sg 
14920
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   338
	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
14941
1edb674e0c33 Oracle corrected
chaieb
parents: 14920
diff changeset
   339
*)
14920
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   340
	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   341
    in 
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   342
          (trace_msg ("calling procedure with term:\n" ^
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   343
             Sign.string_of_term sg t1);
14920
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   344
           ((pth RS iffD2) RS pre_thm,
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   345
            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
14920
a7525235e20f An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents: 14882
diff changeset
   346
    end
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   347
      | _ => (pre_thm, assm_tac i)
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   348
  in (rtac (((mp_step nh) o (spec_step np)) th) i 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   349
      THEN tac) st
14130
398bc4a885d6 Fixed two bugs:
berghofe
parents: 13997
diff changeset
   350
  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   351
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   352
fun presburger_args meth =
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   353
 let val parse_flag = 
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   354
         Args.$$$ "no_quantify" >> K (apfst (K false))
18155
e5ab63ca6b0f old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents: 17465
diff changeset
   355
      || Args.$$$ "no_abs" >> K (apsnd (K false));
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   356
 in
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   357
   Method.simple_args 
14882
e0e2361b9a30 avoid Args.list (lost update?);
wenzelm
parents: 14877
diff changeset
   358
  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
18155
e5ab63ca6b0f old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents: 17465
diff changeset
   359
    curry (Library.foldl op |>) (true, true))
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   360
    (fn (q,a) => fn _ => meth q a 1)
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   361
  end;
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   362
14758
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   363
fun presburger_method q a i = Method.METHOD (fn facts =>
af3b71a46a1c A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents: 14353
diff changeset
   364
  Method.insert_tac facts 1 THEN presburger_tac q a i)
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   365
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   366
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   367
  Method.add_method ("presburger",
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   368
    presburger_args presburger_method,
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   369
    "decision procedure for Presburger arithmetic") #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   370
  ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   371
    {splits = splits, inj_consts = inj_consts, discrete = discrete,
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18393
diff changeset
   372
      presburger = SOME (presburger_tac true true)});
13876
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   373
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   374
end;
68f4ed8311ac New decision procedure for Presburger arithmetic.
berghofe
parents:
diff changeset
   375
18155
e5ab63ca6b0f old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
chaieb
parents: 17465
diff changeset
   376
val presburger_tac = Presburger.presburger_tac true true;