src/HOL/Integ/presburger.ML
changeset 23146 0bc590051d95
parent 23145 5d8faadf3ecf
child 23147 a5db2f7d7654
     1.1 --- a/src/HOL/Integ/presburger.ML	Thu May 31 11:00:06 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,372 +0,0 @@
     1.4 -(*  Title:      HOL/Integ/presburger.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Amine Chaieb and Stefan Berghofer, TU Muenchen
     1.7 -
     1.8 -Tactic for solving arithmetical Goals in Presburger Arithmetic.
     1.9 -
    1.10 -This version of presburger deals with occurences of functional symbols
    1.11 -in the subgoal and abstract over them to try to prove the more general
    1.12 -formula. It then resolves with the subgoal. To enable this feature
    1.13 -call the procedure with the parameter abs.
    1.14 -*)
    1.15 -
    1.16 -signature PRESBURGER =
    1.17 -sig
    1.18 - val presburger_tac : bool -> bool -> int -> tactic
    1.19 - val setup : theory -> theory
    1.20 - val trace : bool ref
    1.21 -end;
    1.22 -
    1.23 -structure Presburger: PRESBURGER =
    1.24 -struct
    1.25 -
    1.26 -val trace = ref false;
    1.27 -fun trace_msg s = if !trace then tracing s else ();
    1.28 -
    1.29 -(*-----------------------------------------------------------------*)
    1.30 -(*cooper_pp: provefunction for the one-existance quantifier elimination*)
    1.31 -(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
    1.32 -(*-----------------------------------------------------------------*)
    1.33 -
    1.34 -
    1.35 -val presburger_ss = simpset ();
    1.36 -val binarith = map thm
    1.37 -  ["Pls_0_eq", "Min_1_eq",
    1.38 - "pred_Pls","pred_Min","pred_1","pred_0",
    1.39 -  "succ_Pls", "succ_Min", "succ_1", "succ_0",
    1.40 -  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
    1.41 -  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1",
    1.42 -  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0",
    1.43 -  "add_Pls_right", "add_Min_right"];
    1.44 - val intarithrel =
    1.45 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
    1.46 -                "int_le_number_of_eq","int_iszero_number_of_0",
    1.47 -                "int_less_number_of_eq_neg"]) @
    1.48 -     (map (fn s => thm s RS thm "lift_bool")
    1.49 -          ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    1.50 -           "int_neg_number_of_Min"])@
    1.51 -     (map (fn s => thm s RS thm "nlift_bool")
    1.52 -          ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    1.53 -
    1.54 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    1.55 -                        "int_number_of_diff_sym", "int_number_of_mult_sym"];
    1.56 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    1.57 -                        "mult_nat_number_of", "eq_nat_number_of",
    1.58 -                        "less_nat_number_of"]
    1.59 -val powerarith =
    1.60 -    (map thm ["nat_number_of", "zpower_number_of_even",
    1.61 -              "zpower_Pls", "zpower_Min"]) @
    1.62 -    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
    1.63 -                           thm "one_eq_Numeral1_nring"]
    1.64 -  (thm "zpower_number_of_odd"))]
    1.65 -
    1.66 -val comp_arith = binarith @ intarith @ intarithrel @ natarith
    1.67 -            @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    1.68 -
    1.69 -fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
    1.70 -  let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
    1.71 -  in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    1.72 -
    1.73 -fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
    1.74 -  (CooperProof.proof_of_evalc sg);
    1.75 -
    1.76 -fun tmproof_of_int_qelim sg fm =
    1.77 -  Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
    1.78 -    (CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
    1.79 -
    1.80 -
    1.81 -(* Theorems to be used in this tactic*)
    1.82 -
    1.83 -val zdvd_int = thm "zdvd_int";
    1.84 -val zdiff_int_split = thm "zdiff_int_split";
    1.85 -val all_nat = thm "all_nat";
    1.86 -val ex_nat = thm "ex_nat";
    1.87 -val number_of1 = thm "number_of1";
    1.88 -val number_of2 = thm "number_of2";
    1.89 -val split_zdiv = thm "split_zdiv";
    1.90 -val split_zmod = thm "split_zmod";
    1.91 -val mod_div_equality' = thm "mod_div_equality'";
    1.92 -val split_div' = thm "split_div'";
    1.93 -val Suc_plus1 = thm "Suc_plus1";
    1.94 -val imp_le_cong = thm "imp_le_cong";
    1.95 -val conj_le_cong = thm "conj_le_cong";
    1.96 -val nat_mod_add_eq = mod_add1_eq RS sym;
    1.97 -val nat_mod_add_left_eq = mod_add_left_eq RS sym;
    1.98 -val nat_mod_add_right_eq = mod_add_right_eq RS sym;
    1.99 -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
   1.100 -val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
   1.101 -val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
   1.102 -val nat_div_add_eq = @{thm div_add1_eq} RS sym;
   1.103 -val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
   1.104 -val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
   1.105 -val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
   1.106 -
   1.107 -
   1.108 -(* extract all the constants in a term*)
   1.109 -fun add_term_typed_consts (Const (c, T), cs) = insert (op =) (c, T) cs
   1.110 -  | add_term_typed_consts (t $ u, cs) =
   1.111 -      add_term_typed_consts (t, add_term_typed_consts (u, cs))
   1.112 -  | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
   1.113 -  | add_term_typed_consts (_, cs) = cs;
   1.114 -
   1.115 -fun term_typed_consts t = add_term_typed_consts(t,[]);
   1.116 -
   1.117 -(* Some Types*)
   1.118 -val bT = HOLogic.boolT;
   1.119 -val bitT = HOLogic.bitT;
   1.120 -val iT = HOLogic.intT;
   1.121 -val nT = HOLogic.natT;
   1.122 -
   1.123 -(* Allowed Consts in formulae for presburger tactic*)
   1.124 -
   1.125 -val allowed_consts =
   1.126 -  [("All", (iT --> bT) --> bT),
   1.127 -   ("Ex", (iT --> bT) --> bT),
   1.128 -   ("All", (nT --> bT) --> bT),
   1.129 -   ("Ex", (nT --> bT) --> bT),
   1.130 -
   1.131 -   ("op &", bT --> bT --> bT),
   1.132 -   ("op |", bT --> bT --> bT),
   1.133 -   ("op -->", bT --> bT --> bT),
   1.134 -   ("op =", bT --> bT --> bT),
   1.135 -   ("Not", bT --> bT),
   1.136 -
   1.137 -   (@{const_name Orderings.less_eq}, iT --> iT --> bT),
   1.138 -   ("op =", iT --> iT --> bT),
   1.139 -   (@{const_name Orderings.less}, iT --> iT --> bT),
   1.140 -   (@{const_name Divides.dvd}, iT --> iT --> bT),
   1.141 -   (@{const_name Divides.div}, iT --> iT --> iT),
   1.142 -   (@{const_name Divides.mod}, iT --> iT --> iT),
   1.143 -   (@{const_name HOL.plus}, iT --> iT --> iT),
   1.144 -   (@{const_name HOL.minus}, iT --> iT --> iT),
   1.145 -   (@{const_name HOL.times}, iT --> iT --> iT),
   1.146 -   (@{const_name HOL.abs}, iT --> iT),
   1.147 -   (@{const_name HOL.uminus}, iT --> iT),
   1.148 -   (@{const_name Orderings.max}, iT --> iT --> iT),
   1.149 -   (@{const_name Orderings.min}, iT --> iT --> iT),
   1.150 -
   1.151 -   (@{const_name Orderings.less_eq}, nT --> nT --> bT),
   1.152 -   ("op =", nT --> nT --> bT),
   1.153 -   (@{const_name Orderings.less}, nT --> nT --> bT),
   1.154 -   (@{const_name Divides.dvd}, nT --> nT --> bT),
   1.155 -   (@{const_name Divides.div}, nT --> nT --> nT),
   1.156 -   (@{const_name Divides.mod}, nT --> nT --> nT),
   1.157 -   (@{const_name HOL.plus}, nT --> nT --> nT),
   1.158 -   (@{const_name HOL.minus}, nT --> nT --> nT),
   1.159 -   (@{const_name HOL.times}, nT --> nT --> nT),
   1.160 -   (@{const_name Suc}, nT --> nT),
   1.161 -   (@{const_name Orderings.max}, nT --> nT --> nT),
   1.162 -   (@{const_name Orderings.min}, nT --> nT --> nT),
   1.163 -
   1.164 -   (@{const_name Numeral.bit.B0}, bitT),
   1.165 -   (@{const_name Numeral.bit.B1}, bitT),
   1.166 -   (@{const_name Numeral.Bit}, iT --> bitT --> iT),
   1.167 -   (@{const_name Numeral.Pls}, iT),
   1.168 -   (@{const_name Numeral.Min}, iT),
   1.169 -   (@{const_name Numeral.number_of}, iT --> iT),
   1.170 -   (@{const_name Numeral.number_of}, iT --> nT),
   1.171 -   (@{const_name HOL.zero}, nT),
   1.172 -   (@{const_name HOL.zero}, iT),
   1.173 -   (@{const_name HOL.one}, nT),
   1.174 -   (@{const_name HOL.one}, iT),
   1.175 -   (@{const_name False}, bT),
   1.176 -   (@{const_name True}, bT)];
   1.177 -
   1.178 -(* Preparation of the formula to be sent to the Integer quantifier *)
   1.179 -(* elimination procedure                                           *)
   1.180 -(* Transforms meta implications and meta quantifiers to object     *)
   1.181 -(* implications and object quantifiers                             *)
   1.182 -
   1.183 -
   1.184 -(*==================================*)
   1.185 -(* Abstracting on subterms  ========*)
   1.186 -(*==================================*)
   1.187 -(* Returns occurences of terms that are function application of type int or nat*)
   1.188 -
   1.189 -fun getfuncs fm = case strip_comb fm of
   1.190 -    (Free (_, T), ts as _ :: _) =>
   1.191 -      if body_type T mem [iT, nT]
   1.192 -         andalso not (ts = []) andalso forall (null o loose_bnos) ts
   1.193 -      then [fm]
   1.194 -      else Library.foldl op union ([], map getfuncs ts)
   1.195 -  | (Var (_, T), ts as _ :: _) =>
   1.196 -      if body_type T mem [iT, nT]
   1.197 -         andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
   1.198 -      else Library.foldl op union ([], map getfuncs ts)
   1.199 -  | (Const (s, T), ts) =>
   1.200 -      if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
   1.201 -      then Library.foldl op union ([], map getfuncs ts)
   1.202 -      else [fm]
   1.203 -  | (Abs (s, T, t), _) => getfuncs t
   1.204 -  | _ => [];
   1.205 -
   1.206 -
   1.207 -fun abstract_pres sg fm =
   1.208 -  foldr (fn (t, u) =>
   1.209 -      let val T = fastype_of t
   1.210 -      in all T $ Abs ("x", T, abstract_over (t, u)) end)
   1.211 -         fm (getfuncs fm);
   1.212 -
   1.213 -
   1.214 -
   1.215 -(* hasfuncs_on_bounds dont care of the type of the functions applied!
   1.216 - It returns true if there is a subterm coresponding to the application of
   1.217 - a function on a bounded variable.
   1.218 -
   1.219 - Function applications are allowed only for well predefined functions a
   1.220 - consts*)
   1.221 -
   1.222 -fun has_free_funcs fm  = case strip_comb fm of
   1.223 -    (Free (_, T), ts as _ :: _) =>
   1.224 -      if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
   1.225 -      then true
   1.226 -      else exists (fn x => x) (map has_free_funcs ts)
   1.227 -  | (Var (_, T), ts as _ :: _) =>
   1.228 -      if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
   1.229 -      then true
   1.230 -      else exists (fn x => x) (map has_free_funcs ts)
   1.231 -  | (Const (s, T), ts) =>  exists (fn x => x) (map has_free_funcs ts)
   1.232 -  | (Abs (s, T, t), _) => has_free_funcs t
   1.233 -  |_ => false;
   1.234 -
   1.235 -
   1.236 -(*returns true if the formula is relevant for presburger arithmetic tactic
   1.237 -The constants occuring in term t should be a subset of the allowed_consts
   1.238 - There also should be no occurences of application of functions on bounded
   1.239 - variables. Whenever this function will be used, it will be ensured that t
   1.240 - will not contain subterms with function symbols that could have been
   1.241 - abstracted over.*)
   1.242 -
   1.243 -fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
   1.244 -  map (fn i => snd (List.nth (ps, i))) (loose_bnos t) @
   1.245 -  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
   1.246 -  subset [iT, nT]
   1.247 -  andalso not (has_free_funcs t);
   1.248 -
   1.249 -
   1.250 -fun prepare_for_presburger sg q fm =
   1.251 -  let
   1.252 -    val ps = Logic.strip_params fm
   1.253 -    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
   1.254 -    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
   1.255 -    val _ = if relevant (rev ps) c then ()
   1.256 -               else  (trace_msg ("Conclusion is not a presburger term:\n" ^
   1.257 -             Sign.string_of_term sg c); raise CooperDec.COOPER)
   1.258 -    fun mk_all ((s, T), (P,n)) =
   1.259 -      if 0 mem loose_bnos P then
   1.260 -        (HOLogic.all_const T $ Abs (s, T, P), n)
   1.261 -      else (incr_boundvars ~1 P, n-1)
   1.262 -    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
   1.263 -    val (rhs,irhs) = List.partition (relevant (rev ps)) hs
   1.264 -    val np = length ps
   1.265 -    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   1.266 -      (foldr HOLogic.mk_imp c rhs, np) ps
   1.267 -    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   1.268 -      (term_frees fm' @ term_vars fm');
   1.269 -    val fm2 = foldr mk_all2 fm' vs
   1.270 -  in (fm2, np + length vs, length rhs) end;
   1.271 -
   1.272 -(*Object quantifier to meta --*)
   1.273 -fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
   1.274 -
   1.275 -(* object implication to meta---*)
   1.276 -fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
   1.277 -
   1.278 -(* the presburger tactic*)
   1.279 -
   1.280 -(* Parameters : q = flag for quantify ofer free variables ;
   1.281 -                a = flag for abstracting over function occurences
   1.282 -                i = subgoal  *)
   1.283 -
   1.284 -fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
   1.285 -  let
   1.286 -    val g = List.nth (prems_of st, i - 1)
   1.287 -    val sg = Thm.theory_of_thm st
   1.288 -    (* The Abstraction step *)
   1.289 -    val g' = if a then abstract_pres sg g else g
   1.290 -    (* Transform the term*)
   1.291 -    val (t,np,nh) = prepare_for_presburger sg q g'
   1.292 -    (* Some simpsets for dealing with mod div abs and nat*)
   1.293 -    val mod_div_simpset = Simplifier.theory_context sg HOL_basic_ss
   1.294 -                        addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
   1.295 -                                  nat_mod_add_right_eq, int_mod_add_eq,
   1.296 -                                  int_mod_add_right_eq, int_mod_add_left_eq,
   1.297 -                                  nat_div_add_eq, int_div_add_eq,
   1.298 -                                  mod_self, @{thm zmod_self},
   1.299 -                                  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
   1.300 -                                  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
   1.301 -                                  @{thm zdiv_zero}, @{thm zmod_zero}, div_0,mod_0,
   1.302 -                                  @{thm zdiv_1}, @{thm zmod_1}, @{thm div_1}, @{thm mod_1},
   1.303 -                                  Suc_plus1]
   1.304 -                        addsimps add_ac
   1.305 -                        addsimprocs [cancel_div_mod_proc]
   1.306 -    val simpset0 = HOL_basic_ss
   1.307 -      addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}]
   1.308 -      addsimps comp_arith
   1.309 -      addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}]
   1.310 -    (* Simp rules for changing (n::int) to int n *)
   1.311 -    val simpset1 = HOL_basic_ss
   1.312 -      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
   1.313 -        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
   1.314 -      addsplits [zdiff_int_split]
   1.315 -    (*simp rules for elimination of int n*)
   1.316 -
   1.317 -    val simpset2 = HOL_basic_ss
   1.318 -      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
   1.319 -      addcongs [conj_le_cong, imp_le_cong]
   1.320 -    (* simp rules for elimination of abs *)
   1.321 -    val simpset3 = HOL_basic_ss addsplits [abs_split]
   1.322 -    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
   1.323 -    (* Theorem for the nat --> int transformation *)
   1.324 -    val pre_thm = Seq.hd (EVERY
   1.325 -      [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
   1.326 -       TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
   1.327 -       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
   1.328 -      (trivial ct))
   1.329 -    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
   1.330 -    (* The result of the quantifier elimination *)
   1.331 -    val (th, tac) = case (prop_of pre_thm) of
   1.332 -        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
   1.333 -    let val pth =
   1.334 -          (* If quick_and_dirty then run without proof generation as oracle*)
   1.335 -             if !quick_and_dirty
   1.336 -             then presburger_oracle sg (Pattern.eta_long [] t1)
   1.337 -(*
   1.338 -assume (cterm_of sg
   1.339 -               (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
   1.340 -*)
   1.341 -             else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
   1.342 -    in
   1.343 -          (trace_msg ("calling procedure with term:\n" ^
   1.344 -             Sign.string_of_term sg t1);
   1.345 -           ((pth RS iffD2) RS pre_thm,
   1.346 -            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
   1.347 -    end
   1.348 -      | _ => (pre_thm, assm_tac i)
   1.349 -  in (rtac (((mp_step nh) o (spec_step np)) th) i
   1.350 -      THEN tac) st
   1.351 -  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
   1.352 -
   1.353 -val presburger_meth =
   1.354 - let val parse_flag =
   1.355 -         Args.$$$ "no_quantify" >> K (apfst (K false))
   1.356 -      || Args.$$$ "no_abs" >> K (apsnd (K false));
   1.357 - in
   1.358 -   Method.simple_args
   1.359 -     (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   1.360 -      curry (Library.foldl op |>) (true, true))
   1.361 -     (fn (q,a) => K (Method.SIMPLE_METHOD' (presburger_tac q a)))
   1.362 -  end;
   1.363 -
   1.364 -val presburger_arith_tac = mk_arith_tactic "presburger" (fn i => fn st =>
   1.365 -  (warning "Trying full Presburger arithmetic ...";
   1.366 -   presburger_tac true true i st));
   1.367 -
   1.368 -val setup =
   1.369 -  Method.add_method ("presburger", presburger_meth,
   1.370 -    "decision procedure for Presburger arithmetic") #>
   1.371 -  arith_tactic_add presburger_arith_tac;
   1.372 -
   1.373 -end;
   1.374 -
   1.375 -val presburger_tac = Presburger.presburger_tac true true;