only one module fpr presburger method
authorhaftmann
Mon May 10 14:55:06 2010 +0200 (2010-05-10)
changeset 368025f9fe7b3295d
parent 36801 3560de0fe851
child 36803 2cad8904c4ff
only one module fpr presburger method
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
     1.1 --- a/src/HOL/Presburger.thy	Mon May 10 14:55:04 2010 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon May 10 14:55:06 2010 +0200
     1.3 @@ -218,16 +218,6 @@
     1.4  lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
     1.5  by(induct rule: int_gr_induct, simp_all add:int_distrib)
     1.6  
     1.7 -theorem int_induct[case_names base step1 step2]:
     1.8 -  assumes 
     1.9 -  base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and
    1.10 -  step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
    1.11 -  shows "P i"
    1.12 -proof -
    1.13 -  have "i \<le> k \<or> i\<ge> k" by arith
    1.14 -  thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast
    1.15 -qed
    1.16 -
    1.17  lemma decr_mult_lemma:
    1.18    assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
    1.19    shows "ALL x. P x \<longrightarrow> P(x - k*d)"
    1.20 @@ -402,29 +392,8 @@
    1.21  use "Tools/Qelim/cooper.ML"
    1.22  
    1.23  setup Cooper.setup
    1.24 -oracle linzqe_oracle = Cooper.cooper_oracle
    1.25  
    1.26 -use "Tools/Qelim/presburger.ML"
    1.27 -
    1.28 -setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
    1.29 -
    1.30 -method_setup presburger = {*
    1.31 -let
    1.32 - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.33 - fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
    1.34 - val addN = "add"
    1.35 - val delN = "del"
    1.36 - val elimN = "elim"
    1.37 - val any_keyword = keyword addN || keyword delN || simple_keyword elimN
    1.38 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.39 -in
    1.40 -  Scan.optional (simple_keyword elimN >> K false) true --
    1.41 -  Scan.optional (keyword addN |-- thms) [] --
    1.42 -  Scan.optional (keyword delN |-- thms) [] >>
    1.43 -  (fn ((elim, add_ths), del_ths) => fn ctxt =>
    1.44 -    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
    1.45 -end
    1.46 -*} "Cooper's algorithm for Presburger arithmetic"
    1.47 +method_setup presburger = "Cooper.cooper_method" "Cooper's algorithm for Presburger arithmetic"
    1.48  
    1.49  declare dvd_eq_mod_eq_0[symmetric, presburger]
    1.50  declare mod_1[presburger] 
     2.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:55:04 2010 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:55:06 2010 +0200
     2.3 @@ -1,5 +1,7 @@
     2.4  (*  Title:      HOL/Tools/Qelim/cooper.ML
     2.5      Author:     Amine Chaieb, TU Muenchen
     2.6 +
     2.7 +Presburger arithmetic by Cooper's algorithm.
     2.8  *)
     2.9  
    2.10  signature COOPER =
    2.11 @@ -8,10 +10,12 @@
    2.12    val get: Proof.context -> entry
    2.13    val del: term list -> attribute
    2.14    val add: term list -> attribute 
    2.15 +  val cooper_conv: Proof.context -> conv
    2.16 +  val cooper_oracle: cterm -> thm
    2.17 +  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    2.18 +  val cooper_method: (Proof.context -> Method.method) context_parser
    2.19 +  exception COOPER of string * exn
    2.20    val setup: theory -> theory
    2.21 -  val cooper_conv: Proof.context -> conv
    2.22 -  val cooper_oracle: cterm -> cterm
    2.23 -  exception COOPER of string * exn
    2.24  end;
    2.25  
    2.26  structure Cooper: COOPER =
    2.27 @@ -25,7 +29,6 @@
    2.28     @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    2.29     @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    2.30     @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    2.31 -   @{term "Int.Bit0"}, @{term "Int.Bit1"},
    2.32     @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    2.33     @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    2.34     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    2.35 @@ -64,30 +67,6 @@
    2.36    context |> Data.map (fn (ss,ts') => 
    2.37       (ss delsimps [th], subtract (op aconv) ts' ts ))) 
    2.38  
    2.39 -
    2.40 -(* theory setup *)
    2.41 -
    2.42 -local
    2.43 -
    2.44 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    2.45 -
    2.46 -val constsN = "consts";
    2.47 -val any_keyword = keyword constsN
    2.48 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    2.49 -val terms = thms >> map (term_of o Drule.dest_term);
    2.50 -
    2.51 -fun optional scan = Scan.optional scan [];
    2.52 -
    2.53 -in
    2.54 -
    2.55 -val setup =
    2.56 -  Attrib.setup @{binding presburger}
    2.57 -    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    2.58 -      optional (keyword constsN |-- terms) >> add) "Cooper data";
    2.59 -
    2.60 -end;
    2.61 -
    2.62 -exception COOPER of string * exn;
    2.63  fun simp_thms_conv ctxt =
    2.64    Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
    2.65  val FWD = Drule.implies_elim_list;
    2.66 @@ -274,6 +253,9 @@
    2.67  fun linear_neg tm = linear_cmul ~1 tm;
    2.68  fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
    2.69  
    2.70 +exception COOPER of string * exn;
    2.71 +
    2.72 +fun cooper s = raise COOPER ("Cooper failed", ERROR s);
    2.73  
    2.74  fun lint vars tm =  if is_numeral tm then tm  else case tm of
    2.75    Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
    2.76 @@ -594,7 +576,6 @@
    2.77  in val cooper_conv = conv
    2.78  end;
    2.79  
    2.80 -fun cooper s = raise COOPER ("Cooper oracle failed", ERROR s);
    2.81  fun i_of_term vs t = case t
    2.82   of Free (xn, xT) => (case AList.lookup (op aconv) vs t
    2.83       of NONE   => cooper "Variable not found in the list!"
    2.84 @@ -619,7 +600,7 @@
    2.85    | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
    2.86    | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
    2.87    | Const(@{const_name Rings.dvd},_)$t1$t2 =>
    2.88 -      (Cooper_Procedure.Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
    2.89 +      (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle TERM _ => cooper "Reification: unsupported dvd")
    2.90    | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
    2.91    | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
    2.92    | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    2.93 @@ -695,7 +676,7 @@
    2.94   | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
    2.95   | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
    2.96  
    2.97 -fun cooper_oracle ct =
    2.98 +fun raw_cooper_oracle ct =
    2.99    let
   2.100      val thy = Thm.theory_of_cterm ct;
   2.101      val t = Thm.term_of ct;
   2.102 @@ -705,4 +686,218 @@
   2.103        HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
   2.104    end;
   2.105  
   2.106 +val (_, cooper_oracle) = Context.>>> (Context.map_theory_result
   2.107 +  (Thm.add_oracle (Binding.name "cooper", raw_cooper_oracle)));
   2.108 +
   2.109 +val comp_ss = HOL_ss addsimps @{thms semiring_norm};
   2.110 +
   2.111 +fun strip_objimp ct =
   2.112 +  (case Thm.term_of ct of
   2.113 +    Const ("op -->", _) $ _ $ _ =>
   2.114 +      let val (A, B) = Thm.dest_binop ct
   2.115 +      in A :: strip_objimp B end
   2.116 +  | _ => [ct]);
   2.117 +
   2.118 +fun strip_objall ct = 
   2.119 + case term_of ct of 
   2.120 +  Const ("All", _) $ Abs (xn,xT,p) => 
   2.121 +   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
   2.122 +   in apfst (cons (a,v)) (strip_objall t')
   2.123 +   end
   2.124 +| _ => ([],ct);
   2.125 +
   2.126 +local
   2.127 +  val all_maxscope_ss = 
   2.128 +     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
   2.129 +in
   2.130 +fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
   2.131 +  CSUBGOAL (fn (p', i) =>
   2.132 +    let
   2.133 +     val (qvs, p) = strip_objall (Thm.dest_arg p')
   2.134 +     val (ps, c) = split_last (strip_objimp p)
   2.135 +     val qs = filter P ps
   2.136 +     val q = if P c then c else @{cterm "False"}
   2.137 +     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
   2.138 +         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
   2.139 +     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
   2.140 +     val ntac = (case qs of [] => q aconvc @{cterm "False"}
   2.141 +                         | _ => false)
   2.142 +    in 
   2.143 +    if ntac then no_tac
   2.144 +      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
   2.145 +    end)
   2.146  end;
   2.147 +
   2.148 +local
   2.149 + fun isnum t = case t of 
   2.150 +   Const(@{const_name Groups.zero},_) => true
   2.151 + | Const(@{const_name Groups.one},_) => true
   2.152 + | @{term "Suc"}$s => isnum s
   2.153 + | @{term "nat"}$s => isnum s
   2.154 + | @{term "int"}$s => isnum s
   2.155 + | Const(@{const_name Groups.uminus},_)$s => isnum s
   2.156 + | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
   2.157 + | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
   2.158 + | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
   2.159 + | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
   2.160 + | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
   2.161 + | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
   2.162 + | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
   2.163 +
   2.164 + fun ty cts t = 
   2.165 + if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
   2.166 +    else case term_of t of 
   2.167 +      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
   2.168 +               then not (isnum l orelse isnum r)
   2.169 +               else not (member (op aconv) cts c)
   2.170 +    | c$_ => not (member (op aconv) cts c)
   2.171 +    | c => not (member (op aconv) cts c)
   2.172 +
   2.173 + val term_constants =
   2.174 +  let fun h acc t = case t of
   2.175 +    Const _ => insert (op aconv) t acc
   2.176 +  | a$b => h (h acc a) b
   2.177 +  | Abs (_,_,t) => h acc t
   2.178 +  | _ => acc
   2.179 + in h [] end;
   2.180 +in 
   2.181 +fun is_relevant ctxt ct = 
   2.182 + subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
   2.183 + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
   2.184 + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
   2.185 +
   2.186 +fun int_nat_terms ctxt ct =
   2.187 + let 
   2.188 +  val cts = snd (get ctxt)
   2.189 +  fun h acc t = if ty cts t then insert (op aconvc) t acc else
   2.190 +   case (term_of t) of
   2.191 +    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   2.192 +  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
   2.193 +  | _ => acc
   2.194 + in h [] ct end
   2.195 +end;
   2.196 +
   2.197 +fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
   2.198 + let 
   2.199 +   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   2.200 +   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   2.201 +   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   2.202 +   val p' = fold_rev gen ts p
   2.203 + in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   2.204 +
   2.205 +local
   2.206 +val ss1 = comp_ss
   2.207 +  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
   2.208 +      @ map (fn r => r RS sym) 
   2.209 +        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
   2.210 +         @{thm "zmult_int"}]
   2.211 +    addsplits [@{thm "zdiff_int_split"}]
   2.212 +
   2.213 +val ss2 = HOL_basic_ss
   2.214 +  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
   2.215 +            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
   2.216 +            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   2.217 +  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   2.218 +val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
   2.219 +  @ map (symmetric o mk_meta_eq) 
   2.220 +    [@{thm "dvd_eq_mod_eq_0"},
   2.221 +     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   2.222 +     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   2.223 +  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   2.224 +     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   2.225 +     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   2.226 +     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   2.227 +     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   2.228 +  @ @{thms add_ac}
   2.229 + addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
   2.230 + val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
   2.231 +     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   2.232 +      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
   2.233 +in
   2.234 +fun nat_to_int_tac ctxt = 
   2.235 +  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
   2.236 +  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
   2.237 +  simp_tac (Simplifier.context ctxt comp_ss);
   2.238 +
   2.239 +fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
   2.240 +fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
   2.241 +end;
   2.242 +
   2.243 +fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
   2.244 +   let 
   2.245 +    val cpth = 
   2.246 +       if !quick_and_dirty 
   2.247 +       then cooper_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
   2.248 +             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
   2.249 +       else Conv.arg_conv (cooper_conv ctxt) p
   2.250 +    val p' = Thm.rhs_of cpth
   2.251 +    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
   2.252 +   in rtac th i end
   2.253 +   handle COOPER _ => no_tac);
   2.254 +
   2.255 +fun finish_tac q = SUBGOAL (fn (_, i) =>
   2.256 +  (if q then I else TRY) (rtac TrueI i));
   2.257 +
   2.258 +fun cooper_tac elim add_ths del_ths ctxt =
   2.259 +let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
   2.260 +    val aprems = Arith_Data.get_arith_facts ctxt
   2.261 +in
   2.262 +  Method.insert_tac aprems
   2.263 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
   2.264 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   2.265 +  THEN_ALL_NEW simp_tac ss
   2.266 +  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   2.267 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
   2.268 +  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
   2.269 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
   2.270 +  THEN_ALL_NEW div_mod_tac ctxt
   2.271 +  THEN_ALL_NEW splits_tac ctxt
   2.272 +  THEN_ALL_NEW simp_tac ss
   2.273 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   2.274 +  THEN_ALL_NEW nat_to_int_tac ctxt
   2.275 +  THEN_ALL_NEW (core_cooper_tac ctxt)
   2.276 +  THEN_ALL_NEW finish_tac elim
   2.277 +end;
   2.278 +
   2.279 +val cooper_method =
   2.280 +  let
   2.281 +    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   2.282 +    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   2.283 +    val addN = "add"
   2.284 +    val delN = "del"
   2.285 +    val elimN = "elim"
   2.286 +    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   2.287 +    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   2.288 +  in
   2.289 +    Scan.optional (simple_keyword elimN >> K false) true --
   2.290 +    Scan.optional (keyword addN |-- thms) [] --
   2.291 +    Scan.optional (keyword delN |-- thms) [] >>
   2.292 +    (fn ((elim, add_ths), del_ths) => fn ctxt =>
   2.293 +      SIMPLE_METHOD' (cooper_tac elim add_ths del_ths ctxt))
   2.294 +  end;
   2.295 +
   2.296 +
   2.297 +(* theory setup *)
   2.298 +
   2.299 +local
   2.300 +
   2.301 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   2.302 +
   2.303 +val constsN = "consts";
   2.304 +val any_keyword = keyword constsN
   2.305 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   2.306 +val terms = thms >> map (term_of o Drule.dest_term);
   2.307 +
   2.308 +fun optional scan = Scan.optional scan [];
   2.309 +
   2.310 +in
   2.311 +
   2.312 +val setup =
   2.313 +  Attrib.setup @{binding presburger}
   2.314 +    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
   2.315 +      optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
   2.316 +  #> Arith_Data.add_tactic "Presburger arithmetic" (K (cooper_tac true [] []));
   2.317 +
   2.318 +end;
   2.319 +
   2.320 +end;
     3.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 14:55:04 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,184 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Qelim/presburger.ML
     3.5 -    Author:     Amine Chaieb, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -signature PRESBURGER =
     3.9 -sig
    3.10 -  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    3.11 -end;
    3.12 -
    3.13 -structure Presburger : PRESBURGER = 
    3.14 -struct
    3.15 -
    3.16 -val comp_ss = HOL_ss addsimps @{thms semiring_norm};
    3.17 -
    3.18 -fun strip_objimp ct =
    3.19 -  (case Thm.term_of ct of
    3.20 -    Const ("op -->", _) $ _ $ _ =>
    3.21 -      let val (A, B) = Thm.dest_binop ct
    3.22 -      in A :: strip_objimp B end
    3.23 -  | _ => [ct]);
    3.24 -
    3.25 -fun strip_objall ct = 
    3.26 - case term_of ct of 
    3.27 -  Const ("All", _) $ Abs (xn,xT,p) => 
    3.28 -   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
    3.29 -   in apfst (cons (a,v)) (strip_objall t')
    3.30 -   end
    3.31 -| _ => ([],ct);
    3.32 -
    3.33 -local
    3.34 -  val all_maxscope_ss = 
    3.35 -     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
    3.36 -in
    3.37 -fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
    3.38 -  CSUBGOAL (fn (p', i) =>
    3.39 -    let
    3.40 -     val (qvs, p) = strip_objall (Thm.dest_arg p')
    3.41 -     val (ps, c) = split_last (strip_objimp p)
    3.42 -     val qs = filter P ps
    3.43 -     val q = if P c then c else @{cterm "False"}
    3.44 -     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
    3.45 -         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
    3.46 -     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
    3.47 -     val ntac = (case qs of [] => q aconvc @{cterm "False"}
    3.48 -                         | _ => false)
    3.49 -    in 
    3.50 -    if ntac then no_tac
    3.51 -      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
    3.52 -    end)
    3.53 -end;
    3.54 -
    3.55 -local
    3.56 - fun isnum t = case t of 
    3.57 -   Const(@{const_name Groups.zero},_) => true
    3.58 - | Const(@{const_name Groups.one},_) => true
    3.59 - | @{term "Suc"}$s => isnum s
    3.60 - | @{term "nat"}$s => isnum s
    3.61 - | @{term "int"}$s => isnum s
    3.62 - | Const(@{const_name Groups.uminus},_)$s => isnum s
    3.63 - | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
    3.64 - | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
    3.65 - | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
    3.66 - | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
    3.67 - | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
    3.68 - | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    3.69 - | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
    3.70 -
    3.71 - fun ty cts t = 
    3.72 - if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
    3.73 -    else case term_of t of 
    3.74 -      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
    3.75 -               then not (isnum l orelse isnum r)
    3.76 -               else not (member (op aconv) cts c)
    3.77 -    | c$_ => not (member (op aconv) cts c)
    3.78 -    | c => not (member (op aconv) cts c)
    3.79 -
    3.80 - val term_constants =
    3.81 -  let fun h acc t = case t of
    3.82 -    Const _ => insert (op aconv) t acc
    3.83 -  | a$b => h (h acc a) b
    3.84 -  | Abs (_,_,t) => h acc t
    3.85 -  | _ => acc
    3.86 - in h [] end;
    3.87 -in 
    3.88 -fun is_relevant ctxt ct = 
    3.89 - subset (op aconv) (term_constants (term_of ct) , snd (Cooper.get ctxt))
    3.90 - andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
    3.91 - andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
    3.92 -
    3.93 -fun int_nat_terms ctxt ct =
    3.94 - let 
    3.95 -  val cts = snd (Cooper.get ctxt)
    3.96 -  fun h acc t = if ty cts t then insert (op aconvc) t acc else
    3.97 -   case (term_of t) of
    3.98 -    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
    3.99 -  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
   3.100 -  | _ => acc
   3.101 - in h [] ct end
   3.102 -end;
   3.103 -
   3.104 -fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
   3.105 - let 
   3.106 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   3.107 -   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   3.108 -   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   3.109 -   val p' = fold_rev gen ts p
   3.110 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   3.111 -
   3.112 -local
   3.113 -val ss1 = comp_ss
   3.114 -  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
   3.115 -      @ map (fn r => r RS sym) 
   3.116 -        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
   3.117 -         @{thm "zmult_int"}]
   3.118 -    addsplits [@{thm "zdiff_int_split"}]
   3.119 -
   3.120 -val ss2 = HOL_basic_ss
   3.121 -  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
   3.122 -            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
   3.123 -            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   3.124 -  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   3.125 -val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
   3.126 -  @ map (symmetric o mk_meta_eq) 
   3.127 -    [@{thm "dvd_eq_mod_eq_0"},
   3.128 -     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   3.129 -     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   3.130 -  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   3.131 -     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   3.132 -     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   3.133 -     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   3.134 -     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   3.135 -  @ @{thms add_ac}
   3.136 - addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
   3.137 - val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
   3.138 -     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   3.139 -      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
   3.140 -in
   3.141 -fun nat_to_int_tac ctxt = 
   3.142 -  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
   3.143 -  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
   3.144 -  simp_tac (Simplifier.context ctxt comp_ss);
   3.145 -
   3.146 -fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
   3.147 -fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
   3.148 -end;
   3.149 -
   3.150 -
   3.151 -fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
   3.152 -   let 
   3.153 -    val cpth = 
   3.154 -       if !quick_and_dirty 
   3.155 -       then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
   3.156 -             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
   3.157 -       else Conv.arg_conv (Cooper.cooper_conv ctxt) p
   3.158 -    val p' = Thm.rhs_of cpth
   3.159 -    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
   3.160 -   in rtac th i end
   3.161 -   handle Cooper.COOPER _ => no_tac);
   3.162 -
   3.163 -fun finish_tac q = SUBGOAL (fn (_, i) =>
   3.164 -  (if q then I else TRY) (rtac TrueI i));
   3.165 -
   3.166 -fun cooper_tac elim add_ths del_ths ctxt =
   3.167 -let val ss = Simplifier.context ctxt (fst (Cooper.get ctxt)) delsimps del_ths addsimps add_ths
   3.168 -    val aprems = Arith_Data.get_arith_facts ctxt
   3.169 -in
   3.170 -  Method.insert_tac aprems
   3.171 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
   3.172 -  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   3.173 -  THEN_ALL_NEW simp_tac ss
   3.174 -  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   3.175 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
   3.176 -  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
   3.177 -  THEN_ALL_NEW Object_Logic.full_atomize_tac
   3.178 -  THEN_ALL_NEW div_mod_tac ctxt
   3.179 -  THEN_ALL_NEW splits_tac ctxt
   3.180 -  THEN_ALL_NEW simp_tac ss
   3.181 -  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   3.182 -  THEN_ALL_NEW nat_to_int_tac ctxt
   3.183 -  THEN_ALL_NEW (core_cooper_tac ctxt)
   3.184 -  THEN_ALL_NEW finish_tac elim
   3.185 -end;
   3.186 -
   3.187 -end;