src/HOL/Tools/Qelim/presburger.ML
author wenzelm
Thu, 29 May 2008 23:46:40 +0200
changeset 27019 9ad9d6554d05
parent 25843 af0c90f54ebe
child 27651 16a26996c30e
permissions -rw-r--r--
proper context for ss;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24403
diff changeset
     1
(*  Title:      HOL/Tools/Qelim/presburger.ML
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     3
    Author:     Amine Chaieb, TU Muenchen
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     4
*)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     5
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     6
signature PRESBURGER =
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
     7
sig
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
     8
  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     9
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    10
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    11
structure Presburger : PRESBURGER = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    12
struct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    13
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    14
open Conv;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    15
val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    16
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    17
fun strip_objimp ct =
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    18
  (case Thm.term_of ct of
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    19
    Const ("op -->", _) $ _ $ _ =>
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    20
      let val (A, B) = Thm.dest_binop ct
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    21
      in A :: strip_objimp B end
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    22
  | _ => [ct]);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    23
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    24
fun strip_objall ct = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    25
 case term_of ct of 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    26
  Const ("All", _) $ Abs (xn,xT,p) => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    27
   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    28
   in apfst (cons (a,v)) (strip_objall t')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    29
   end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    30
| _ => ([],ct);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    31
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    32
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    33
  val all_maxscope_ss = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    34
     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    35
in
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    36
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    37
  CSUBGOAL (fn (p', i) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    38
    let
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    39
     val (qvs, p) = strip_objall (Thm.dest_arg p')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    40
     val (ps, c) = split_last (strip_objimp p)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    41
     val qs = filter P ps
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    42
     val q = if P c then c else @{cterm "False"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    43
     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    44
         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    45
     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    46
     val ntac = (case qs of [] => q aconvc @{cterm "False"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    47
                         | _ => false)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    48
    in 
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    49
    if ntac then no_tac
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
    50
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    51
    end)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    52
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    53
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    54
local
24403
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    55
 fun isnum t = case t of 
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    56
   Const(@{const_name "HOL.zero"},_) => true
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    57
 | Const(@{const_name "HOL.one"},_) => true
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    58
 | @{term "Suc"}$s => isnum s
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    59
 | @{term "nat"}$s => isnum s
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    60
 | @{term "int"}$s => isnum s
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24996
diff changeset
    61
 | Const(@{const_name "HOL.uminus"},_)$s => isnum s
24403
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    62
 | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    63
 | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    64
 | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
24996
ebd5f4cc7118 moved class power to theory Power
haftmann
parents: 24584
diff changeset
    65
 | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
24403
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    66
 | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    67
 | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    68
 | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    69
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    70
 fun ty cts t = 
25843
af0c90f54ebe Tuned relevant premises selection
chaieb
parents: 25811
diff changeset
    71
 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    72
    else case term_of t of 
24403
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    73
      c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    74
               then not (isnum l orelse isnum r)
b7c3ee2ca184 More selective generalization : a*b is generalized whenever none of a and b is a number
chaieb
parents: 23880
diff changeset
    75
               else not (member (op aconv) cts c)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    76
    | c$_ => not (member (op aconv) cts c)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    77
    | c => not (member (op aconv) cts c)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    78
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    79
 val term_constants =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    80
  let fun h acc t = case t of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    81
    Const _ => insert (op aconv) t acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    82
  | a$b => h (h acc a) b
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    83
  | Abs (_,_,t) => h acc t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    84
  | _ => acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    85
 in h [] end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    86
in 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    87
fun is_relevant ctxt ct = 
25811
f7c048eafa90 tuned relevance test for presburger
chaieb
parents: 25800
diff changeset
    88
 gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
f7c048eafa90 tuned relevance test for presburger
chaieb
parents: 25800
diff changeset
    89
 andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct))
f7c048eafa90 tuned relevance test for presburger
chaieb
parents: 25800
diff changeset
    90
 andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    91
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    92
fun int_nat_terms ctxt ct =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    93
 let 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    94
  val cts = snd (CooperData.get ctxt)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    95
  fun h acc t = if ty cts t then insert (op aconvc) t acc else
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    96
   case (term_of t) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    97
    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    98
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    99
  | _ => acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   100
 in h [] ct end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   101
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   102
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   103
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   104
 let 
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   105
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   106
   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   107
   val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   108
   val p' = fold_rev gen ts p
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   109
 in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   110
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   111
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   112
val ss1 = comp_ss
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   113
  addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   114
      @ map (fn r => r RS sym) 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   115
        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   116
         @{thm "zmult_int"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   117
    addsplits [@{thm "zdiff_int_split"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   118
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   119
val ss2 = HOL_basic_ss
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   120
  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   121
            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   122
            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   123
  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   124
val div_mod_ss = HOL_basic_ss addsimps simp_thms 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   125
  @ map (symmetric o mk_meta_eq) 
23469
3f309f885d0b add thm antiquotations
huffman
parents: 23466
diff changeset
   126
    [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
3f309f885d0b add thm antiquotations
huffman
parents: 23466
diff changeset
   127
     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   128
     @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   129
     @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   130
  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   131
     @{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   132
     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   133
     @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   134
     @{thm "mod_1"}, @{thm "Suc_plus1"}]
23880
64b9806e160b dropped Nat.ML legacy bindings
haftmann
parents: 23530
diff changeset
   135
  @ @{thms add_ac}
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   136
 addsimprocs [cancel_div_mod_proc]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   137
 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   138
     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   139
      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   140
in
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   141
fun nat_to_int_tac ctxt = 
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   142
  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   143
  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   144
  simp_tac (Simplifier.context ctxt comp_ss);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   145
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   146
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   147
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   148
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   149
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   150
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   151
fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   152
   let 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   153
    val cpth = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   154
       if !quick_and_dirty 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   155
       then linzqe_oracle (ProofContext.theory_of ctxt) 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   156
             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   157
       else arg_conv (Cooper.cooper_conv ctxt) p
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   158
    val p' = Thm.rhs_of cpth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   159
    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   160
   in rtac th i end
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   161
   handle Cooper.COOPER _ => no_tac);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   162
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   163
fun finish_tac q = SUBGOAL (fn (_, i) =>
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   164
  (if q then I else TRY) (rtac TrueI i));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   165
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   166
fun cooper_tac elim add_ths del_ths ctxt =
27019
9ad9d6554d05 proper context for ss;
wenzelm
parents: 25843
diff changeset
   167
let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   168
in
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   169
  ObjectLogic.full_atomize_tac
23530
438c5d2db482 CONVERSION tactical;
wenzelm
parents: 23499
diff changeset
   170
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   171
  THEN_ALL_NEW simp_tac ss
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   172
  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
25843
af0c90f54ebe Tuned relevant premises selection
chaieb
parents: 25811
diff changeset
   173
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
25800
0298341876d0 Changed order of tactics in presburger --- thinning before case splits
chaieb
parents: 25768
diff changeset
   174
  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   175
  THEN_ALL_NEW ObjectLogic.full_atomize_tac
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   176
  THEN_ALL_NEW div_mod_tac ctxt
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   177
  THEN_ALL_NEW splits_tac ctxt
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   178
  THEN_ALL_NEW simp_tac ss
23530
438c5d2db482 CONVERSION tactical;
wenzelm
parents: 23499
diff changeset
   179
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
23499
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   180
  THEN_ALL_NEW nat_to_int_tac ctxt
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   181
  THEN_ALL_NEW core_cooper_tac ctxt
7e27947d92d7 tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
wenzelm
parents: 23488
diff changeset
   182
  THEN_ALL_NEW finish_tac elim
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   183
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   184
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   185
end;