src/HOL/Tools/Qelim/presburger.ML
author wenzelm
Mon, 25 Jun 2007 00:36:37 +0200
changeset 23488 342029af73d1
parent 23469 3f309f885d0b
child 23499 7e27947d92d7
permissions -rw-r--r--
Thm.eta_long_conversion;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     1
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     2
(*  Title:      HOL/Tools/Presburger/presburger.ML
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     3
    ID:         $Id$
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     4
    Author:     Amine Chaieb, TU Muenchen
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
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     7
signature PRESBURGER =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     8
 sig
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     9
  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> Tactical.tactic
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    10
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    11
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    12
structure Presburger : PRESBURGER = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    13
struct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    14
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    15
open Conv;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    16
val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    17
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    18
fun strip_imp_cprems ct = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    19
 case term_of ct of 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    20
  Const ("==>", _) $ _ $ _ => Thm.dest_arg1 ct :: strip_imp_cprems (Thm.dest_arg ct)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    21
| _ => [];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    22
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    23
val cprems_of = strip_imp_cprems o cprop_of;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    24
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    25
fun strip_objimp ct = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    26
 case term_of ct of 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    27
  Const ("op -->", _) $ _ $ _ => Thm.dest_arg1 ct :: strip_objimp (Thm.dest_arg ct)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    28
| _ => [ct];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    29
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    30
fun strip_objall ct = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    31
 case term_of ct of 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    32
  Const ("All", _) $ Abs (xn,xT,p) => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    33
   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
    34
   in apfst (cons (a,v)) (strip_objall t')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    35
   end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    36
| _ => ([],ct);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    37
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    38
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    39
  val all_maxscope_ss = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    40
     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
    41
in
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    42
fun thin_prems_tac P i =  simp_tac all_maxscope_ss i THEN
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    43
  (fn st => case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    44
    NONE => no_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    45
  | SOME p' => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    46
    let
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    47
     val (qvs, p) = strip_objall (Thm.dest_arg p')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    48
     val (ps, c) = split_last (strip_objimp p)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    49
     val qs = filter P ps
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    50
     val q = if P c then c else @{cterm "False"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    51
     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
    52
         (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
    53
     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
    54
     val ntac = (case qs of [] => q aconvc @{cterm "False"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    55
                         | _ => false)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    56
    in 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    57
    if ntac then no_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    58
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i st 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    59
    end)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    60
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    61
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    62
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    63
 fun ty cts t = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    64
 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    65
    else case term_of t of 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    66
      c$_$_ => not (member (op aconv) cts c)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    67
    | c$_ => not (member (op aconv) cts c)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    68
    | c => not (member (op aconv) cts c)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    69
    | _ => true
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    70
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    71
 val term_constants =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    72
  let fun h acc t = case t of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    73
    Const _ => insert (op aconv) t acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    74
  | a$b => h (h acc a) b
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    75
  | Abs (_,_,t) => h acc t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    76
  | _ => acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    77
 in h [] end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    78
in 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    79
fun is_relevant ctxt ct = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    80
  gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    81
 andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    82
 andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct));
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    83
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    84
fun int_nat_terms ctxt ct =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    85
 let 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    86
  val cts = snd (CooperData.get ctxt)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    87
  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
    88
   case (term_of t) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    89
    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    90
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    91
  | _ => acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    92
 in h [] ct end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    93
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    94
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    95
fun generalize_tac ctxt f i st = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    96
 case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    97
    NONE => all_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    98
  | SOME p => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    99
   let 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   100
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   101
   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
   102
   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
   103
   val p' = fold_rev gen ts p
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   104
 in Seq.of_list [implies_intr p' (implies_elim st (fold forall_elim ts (assume p')))]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   105
 end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   106
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   107
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   108
val ss1 = comp_ss
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   109
  addsimps simp_thms @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   110
      @ map (fn r => r RS sym) 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   111
        [@{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
   112
         @{thm "zmult_int"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   113
    addsplits [@{thm "zdiff_int_split"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   114
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   115
val ss2 = HOL_basic_ss
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   116
  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   117
            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   118
            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   119
  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   120
val div_mod_ss = HOL_basic_ss addsimps simp_thms 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   121
  @ map (symmetric o mk_meta_eq) 
23469
3f309f885d0b add thm antiquotations
huffman
parents: 23466
diff changeset
   122
    [@{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
   123
     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   124
     @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   125
     @{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
   126
  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   127
     @{thm "DIVISION_BY_ZERO_DIV"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   128
     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   129
     @{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
   130
     @{thm "mod_1"}, @{thm "Suc_plus1"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   131
  @ add_ac
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   132
 addsimprocs [cancel_div_mod_proc]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   133
 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   134
     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   135
      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   136
in
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   137
fun nat_to_int_tac ctxt i = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   138
  simp_tac (Simplifier.context ctxt ss1) i THEN 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   139
  simp_tac (Simplifier.context ctxt ss2) i THEN 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   140
  TRY (simp_tac (Simplifier.context ctxt comp_ss) i);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   141
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   142
fun div_mod_tac  ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   143
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
   144
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   145
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   146
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   147
fun eta_beta_tac ctxt i st = case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   148
   NONE => no_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   149
 | SOME p => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   150
   let
23488
342029af73d1 Thm.eta_long_conversion;
wenzelm
parents: 23469
diff changeset
   151
    val eq = (Thm.eta_long_conversion then_conv Thm.beta_conversion true) p
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   152
    val p' = Thm.rhs_of eq
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   153
    val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   154
   in rtac th i st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   155
   end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   156
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   157
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   158
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   159
fun core_cooper_tac ctxt i st = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   160
 case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   161
   NONE => all_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   162
 | SOME p => 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   163
   let 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   164
    val cpth = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   165
       if !quick_and_dirty 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   166
       then linzqe_oracle (ProofContext.theory_of ctxt) 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   167
             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   168
       else arg_conv (Cooper.cooper_conv ctxt) p
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   169
    val p' = Thm.rhs_of cpth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   170
    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   171
   in rtac th i st end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   172
   handle Cooper.COOPER _ => no_tac st;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   173
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   174
fun nogoal_tac i st = case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   175
   NONE => no_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   176
 | SOME _ => all_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   177
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   178
fun finish_tac q i st = case try (nth (cprems_of st)) (i - 1) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   179
   NONE => all_tac st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   180
 | SOME _ => (if q then I else TRY) (rtac TrueI i) st
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   181
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   182
fun cooper_tac elim add_ths del_ths ctxt i = 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   183
let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   184
in
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   185
nogoal_tac i 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   186
THEN (EVERY o (map TRY))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   187
 [ObjectLogic.full_atomize_tac i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   188
  eta_beta_tac ctxt i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   189
  simp_tac ss  i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   190
  generalize_tac ctxt (int_nat_terms ctxt) i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   191
  ObjectLogic.full_atomize_tac i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   192
  div_mod_tac ctxt i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   193
  splits_tac ctxt i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   194
  simp_tac ss i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   195
  eta_beta_tac ctxt i,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   196
  nat_to_int_tac ctxt i, 
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   197
  thin_prems_tac (is_relevant ctxt) i]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   198
THEN core_cooper_tac ctxt i THEN finish_tac elim i
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   199
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   200
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   201
end;