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