src/HOL/Tools/Qelim/presburger.ML
author nipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 31790 05c92381363c
parent 30936 d13cecf4ed4c
child 32603 e08fdd615333
permissions -rw-r--r--
corrected and unified thm names
haftmann@24584
     1
(*  Title:      HOL/Tools/Qelim/presburger.ML
wenzelm@23466
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23466
     3
*)
wenzelm@23466
     4
wenzelm@23466
     5
signature PRESBURGER =
wenzelm@23499
     6
sig
wenzelm@23499
     7
  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
wenzelm@23466
     8
end;
wenzelm@23466
     9
wenzelm@23466
    10
structure Presburger : PRESBURGER = 
wenzelm@23466
    11
struct
wenzelm@23466
    12
wenzelm@23466
    13
open Conv;
wenzelm@23466
    14
val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
wenzelm@23466
    15
wenzelm@23499
    16
fun strip_objimp ct =
wenzelm@23499
    17
  (case Thm.term_of ct of
wenzelm@23499
    18
    Const ("op -->", _) $ _ $ _ =>
wenzelm@23499
    19
      let val (A, B) = Thm.dest_binop ct
wenzelm@23499
    20
      in A :: strip_objimp B end
wenzelm@23499
    21
  | _ => [ct]);
wenzelm@23466
    22
wenzelm@23466
    23
fun strip_objall ct = 
wenzelm@23466
    24
 case term_of ct of 
wenzelm@23466
    25
  Const ("All", _) $ Abs (xn,xT,p) => 
wenzelm@23466
    26
   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
wenzelm@23466
    27
   in apfst (cons (a,v)) (strip_objall t')
wenzelm@23466
    28
   end
wenzelm@23466
    29
| _ => ([],ct);
wenzelm@23466
    30
wenzelm@23466
    31
local
wenzelm@23466
    32
  val all_maxscope_ss = 
wenzelm@23466
    33
     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
wenzelm@23466
    34
in
wenzelm@23499
    35
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
wenzelm@23499
    36
  CSUBGOAL (fn (p', i) =>
wenzelm@23466
    37
    let
wenzelm@23466
    38
     val (qvs, p) = strip_objall (Thm.dest_arg p')
wenzelm@23466
    39
     val (ps, c) = split_last (strip_objimp p)
wenzelm@23466
    40
     val qs = filter P ps
wenzelm@23466
    41
     val q = if P c then c else @{cterm "False"}
wenzelm@23466
    42
     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
wenzelm@23466
    43
         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
wenzelm@23466
    44
     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
wenzelm@23466
    45
     val ntac = (case qs of [] => q aconvc @{cterm "False"}
wenzelm@23466
    46
                         | _ => false)
wenzelm@23466
    47
    in 
wenzelm@23499
    48
    if ntac then no_tac
wenzelm@23499
    49
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
wenzelm@23466
    50
    end)
wenzelm@23466
    51
end;
wenzelm@23466
    52
wenzelm@23466
    53
local
chaieb@24403
    54
 fun isnum t = case t of 
chaieb@24403
    55
   Const(@{const_name "HOL.zero"},_) => true
chaieb@24403
    56
 | Const(@{const_name "HOL.one"},_) => true
chaieb@24403
    57
 | @{term "Suc"}$s => isnum s
chaieb@24403
    58
 | @{term "nat"}$s => isnum s
chaieb@24403
    59
 | @{term "int"}$s => isnum s
haftmann@25768
    60
 | Const(@{const_name "HOL.uminus"},_)$s => isnum s
chaieb@24403
    61
 | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
chaieb@24403
    62
 | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
chaieb@24403
    63
 | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
haftmann@24996
    64
 | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
chaieb@24403
    65
 | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
chaieb@24403
    66
 | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
chaieb@24403
    67
 | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
chaieb@24403
    68
wenzelm@23466
    69
 fun ty cts t = 
chaieb@25843
    70
 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
wenzelm@23466
    71
    else case term_of t of 
chaieb@24403
    72
      c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
chaieb@24403
    73
               then not (isnum l orelse isnum r)
chaieb@24403
    74
               else not (member (op aconv) cts c)
wenzelm@23466
    75
    | c$_ => not (member (op aconv) cts c)
wenzelm@23466
    76
    | c => not (member (op aconv) cts c)
wenzelm@23466
    77
wenzelm@23466
    78
 val term_constants =
wenzelm@23466
    79
  let fun h acc t = case t of
wenzelm@23466
    80
    Const _ => insert (op aconv) t acc
wenzelm@23466
    81
  | a$b => h (h acc a) b
wenzelm@23466
    82
  | Abs (_,_,t) => h acc t
wenzelm@23466
    83
  | _ => acc
wenzelm@23466
    84
 in h [] end;
wenzelm@23466
    85
in 
wenzelm@23466
    86
fun is_relevant ctxt ct = 
chaieb@25811
    87
 gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
wenzelm@29265
    88
 andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
wenzelm@29265
    89
 andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
wenzelm@23466
    90
wenzelm@23466
    91
fun int_nat_terms ctxt ct =
wenzelm@23466
    92
 let 
wenzelm@23466
    93
  val cts = snd (CooperData.get ctxt)
wenzelm@23466
    94
  fun h acc t = if ty cts t then insert (op aconvc) t acc else
wenzelm@23466
    95
   case (term_of t) of
wenzelm@23466
    96
    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
wenzelm@23466
    97
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
wenzelm@23466
    98
  | _ => acc
wenzelm@23466
    99
 in h [] ct end
wenzelm@23466
   100
end;
wenzelm@23466
   101
wenzelm@23499
   102
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
wenzelm@23499
   103
 let 
wenzelm@23466
   104
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
wenzelm@23466
   105
   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
wenzelm@29269
   106
   val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
wenzelm@23466
   107
   val p' = fold_rev gen ts p
wenzelm@23499
   108
 in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
wenzelm@23466
   109
wenzelm@23466
   110
local
wenzelm@23466
   111
val ss1 = comp_ss
wenzelm@23466
   112
  addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
wenzelm@23466
   113
      @ map (fn r => r RS sym) 
wenzelm@23466
   114
        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
wenzelm@23466
   115
         @{thm "zmult_int"}]
wenzelm@23466
   116
    addsplits [@{thm "zdiff_int_split"}]
wenzelm@23466
   117
wenzelm@23466
   118
val ss2 = HOL_basic_ss
wenzelm@23466
   119
  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
wenzelm@23466
   120
            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
nipkow@31790
   121
            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
wenzelm@23466
   122
  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
wenzelm@23466
   123
val div_mod_ss = HOL_basic_ss addsimps simp_thms 
wenzelm@23466
   124
  @ map (symmetric o mk_meta_eq) 
nipkow@30224
   125
    [@{thm "dvd_eq_mod_eq_0"},
huffman@23469
   126
     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
nipkow@30034
   127
     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
haftmann@27651
   128
  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
haftmann@27651
   129
     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
wenzelm@23466
   130
     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
nipkow@30031
   131
     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
nipkow@31790
   132
     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
haftmann@23880
   133
  @ @{thms add_ac}
haftmann@30936
   134
 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
wenzelm@23466
   135
 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
wenzelm@23466
   136
     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
wenzelm@23466
   137
      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
wenzelm@23466
   138
in
wenzelm@23499
   139
fun nat_to_int_tac ctxt = 
wenzelm@23499
   140
  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
wenzelm@23499
   141
  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
wenzelm@23499
   142
  simp_tac (Simplifier.context ctxt comp_ss);
wenzelm@23466
   143
wenzelm@23499
   144
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
wenzelm@23466
   145
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
wenzelm@23466
   146
end;
wenzelm@23466
   147
wenzelm@23466
   148
wenzelm@23499
   149
fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
wenzelm@23466
   150
   let 
wenzelm@23466
   151
    val cpth = 
wenzelm@23466
   152
       if !quick_and_dirty 
wenzelm@28290
   153
       then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
wenzelm@28290
   154
             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
wenzelm@23466
   155
       else arg_conv (Cooper.cooper_conv ctxt) p
wenzelm@23466
   156
    val p' = Thm.rhs_of cpth
wenzelm@23466
   157
    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
wenzelm@23499
   158
   in rtac th i end
wenzelm@23499
   159
   handle Cooper.COOPER _ => no_tac);
wenzelm@23466
   160
wenzelm@23499
   161
fun finish_tac q = SUBGOAL (fn (_, i) =>
wenzelm@23499
   162
  (if q then I else TRY) (rtac TrueI i));
wenzelm@23466
   163
wenzelm@23499
   164
fun cooper_tac elim add_ths del_ths ctxt =
wenzelm@27019
   165
let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
nipkow@30699
   166
    val aprems = Arith_Data.get_arith_facts ctxt
wenzelm@23466
   167
in
nipkow@30697
   168
  Method.insert_tac aprems
nipkow@30697
   169
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
wenzelm@23530
   170
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
wenzelm@23499
   171
  THEN_ALL_NEW simp_tac ss
wenzelm@23499
   172
  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
chaieb@25843
   173
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
chaieb@30002
   174
  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
wenzelm@23499
   175
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
wenzelm@23499
   176
  THEN_ALL_NEW div_mod_tac ctxt
wenzelm@23499
   177
  THEN_ALL_NEW splits_tac ctxt
wenzelm@23499
   178
  THEN_ALL_NEW simp_tac ss
wenzelm@23530
   179
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
wenzelm@23499
   180
  THEN_ALL_NEW nat_to_int_tac ctxt
chaieb@30002
   181
  THEN_ALL_NEW (core_cooper_tac ctxt)
wenzelm@23499
   182
  THEN_ALL_NEW finish_tac elim
wenzelm@23466
   183
end;
wenzelm@23466
   184
wenzelm@23466
   185
end;