src/HOL/Tools/Qelim/cooper.ML
author wenzelm
Fri, 27 Aug 2010 17:59:40 +0200
changeset 38808 89ae86205739
parent 38795 848be46708dc
child 38864 4abe644fcea5
permissions -rw-r--r--
more antiquotations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24298
diff changeset
     1
(*  Title:      HOL/Tools/Qelim/cooper.ML
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
     3
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
     4
Presburger arithmetic by Cooper's algorithm.
23466
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
36799
628fe06cbeff one structure is better than three
haftmann
parents: 36798
diff changeset
     7
signature COOPER =
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
     8
sig
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
     9
  type entry
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    10
  val get: Proof.context -> entry
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    11
  val del: term list -> attribute
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    12
  val add: term list -> attribute 
37117
59cee8807c29 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
wenzelm
parents: 36945
diff changeset
    13
  exception COOPER of string
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
    14
  val conv: Proof.context -> conv
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
    15
  val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
    16
  val method: (Proof.context -> Method.method) context_parser
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    17
  val setup: theory -> theory
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    18
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    19
36799
628fe06cbeff one structure is better than three
haftmann
parents: 36798
diff changeset
    20
structure Cooper: COOPER =
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    21
struct
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    22
36799
628fe06cbeff one structure is better than three
haftmann
parents: 36798
diff changeset
    23
type entry = simpset * term list;
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    24
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    25
val allowed_consts = 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    26
  [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    27
   @{term "op - :: int => _"}, @{term "op - :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    28
   @{term "op * :: int => _"}, @{term "op * :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    29
   @{term "op div :: int => _"}, @{term "op div :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    30
   @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
    31
   @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, 
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    32
   @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    33
   @{term "op < :: int => _"}, @{term "op < :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    34
   @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    35
   @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    36
   @{term "abs :: int => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    37
   @{term "max :: int => _"}, @{term "max :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    38
   @{term "min :: int => _"}, @{term "min :: nat => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    39
   @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 37117
diff changeset
    40
   @{term "Not"}, @{term Suc},
36798
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    41
   @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    42
   @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    43
   @{term "nat"}, @{term "int"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    44
   @{term "Int.Bit0"}, @{term "Int.Bit1"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    45
   @{term "Int.Pls"}, @{term "Int.Min"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    46
   @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    47
   @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    48
   @{term "True"}, @{term "False"}];
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    49
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    50
structure Data = Generic_Data
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    51
(
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    52
  type T = simpset * term list;
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    53
  val empty = (HOL_ss, allowed_consts);
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    54
  val extend  = I;
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    55
  fun merge ((ss1, ts1), (ss2, ts2)) =
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    56
    (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    57
);
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    58
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    59
val get = Data.get o Context.Proof;
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    60
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    61
fun add ts = Thm.declaration_attribute (fn th => fn context => 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    62
  context |> Data.map (fn (ss,ts') => 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    63
     (ss addsimps [th], merge (op aconv) (ts',ts) ))) 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    64
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    65
fun del ts = Thm.declaration_attribute (fn th => fn context => 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    66
  context |> Data.map (fn (ss,ts') => 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    67
     (ss delsimps [th], subtract (op aconv) ts' ts ))) 
3981db162131 less complex organization of cooper source code
haftmann
parents: 36797
diff changeset
    68
27018
b3e63f39fc0f proper context for simp_thms_conv;
wenzelm
parents: 26928
diff changeset
    69
fun simp_thms_conv ctxt =
35410
1ea89d2a1bd4 more antiquotations;
wenzelm
parents: 35267
diff changeset
    70
  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
23484
731658208196 made type conv pervasive;
wenzelm
parents: 23466
diff changeset
    71
val FWD = Drule.implies_elim_list;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    72
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    73
val true_tm = @{cterm "True"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    74
val false_tm = @{cterm "False"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    75
val zdvd1_eq = @{thm "zdvd1_eq"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    76
val presburger_ss = @{simpset} addsimps [zdvd1_eq];
30595
c87a3350f5a9 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
wenzelm
parents: 30448
diff changeset
    77
val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
    78
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    79
val iT = HOLogic.intT
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    80
val bT = HOLogic.boolT;
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
    81
val dest_number = HOLogic.dest_number #> snd;
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
    82
val perhaps_number = try dest_number;
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
    83
val is_number = can dest_number;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    84
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    85
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    86
    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    87
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    88
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    89
    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    90
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    91
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    92
    map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    93
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    94
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    95
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    96
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    97
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    98
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    99
      asetgt, asetge, asetdvd, asetndvd,asetP],
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   100
     [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   101
      bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   102
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   103
val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   104
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   105
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   106
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   107
val [zdvd_mono,simp_from_to,all_not_ex] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   108
     [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   109
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   110
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   111
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   112
val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   113
val eval_conv = Simplifier.rewrite eval_ss;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   114
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   115
(* recognising cterm without moving to terms *)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   116
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   117
datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   118
            | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   119
            | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   120
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   121
fun whatis x ct =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   122
( case (term_of ct) of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   123
  Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   124
| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
38549
d0385f2764d8 use antiquotations for remaining unqualified constants in HOL
haftmann
parents: 37388
diff changeset
   125
| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
d0385f2764d8 use antiquotations for remaining unqualified constants in HOL
haftmann
parents: 37388
diff changeset
   126
| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   127
  if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   128
| Const (@{const_name Orderings.less}, _) $ y$ z =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   129
   if term_of x aconv y then Lt (Thm.dest_arg ct)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   130
   else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   131
| Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   132
   if term_of x aconv y then Le (Thm.dest_arg ct)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   133
   else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   134
| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   135
   if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   136
| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   137
   if term_of x aconv y then
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   138
   NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   139
| _ => Nox)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   140
  handle CTERM _ => Nox;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   141
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   142
fun get_pmi_term t =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   143
  let val (x,eq) =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   144
     (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   145
        (Thm.dest_arg t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   146
in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   147
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   148
val get_pmi = get_pmi_term o cprop_of;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   149
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   150
val p_v' = @{cpat "?P' :: int => bool"};
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   151
val q_v' = @{cpat "?Q' :: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   152
val p_v = @{cpat "?P:: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   153
val q_v = @{cpat "?Q:: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   154
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   155
fun myfwd (th1, th2, th3) p q
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   156
      [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   157
  let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   158
   val (mp', mq') = (get_pmi th_1, get_pmi th_1')
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   159
   val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   160
                   [th_1, th_1']
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   161
   val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   162
   val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   163
  in (mi_th, set_th, infD_th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   164
  end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   165
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   166
val inst' = fn cts => instantiate' [] (map SOME cts);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   167
val infDTrue = instantiate' [] [SOME true_tm] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   168
val infDFalse = instantiate' [] [SOME false_tm] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   169
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   170
val cadd =  @{cterm "op + :: int => _"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   171
val cmulC =  @{cterm "op * :: int => _"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   172
val cminus =  @{cterm "op - :: int => _"}
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   173
val cone =  @{cterm "1 :: int"}
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   174
val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   175
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   176
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   177
fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n));
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   178
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   179
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   180
val [minus1,plus1] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   181
    map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   182
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   183
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   184
                           asetgt, asetge,asetdvd,asetndvd,asetP,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   185
                           infDdvd, infDndvd, asetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   186
                           asetdisj, infDconj, infDdisj] cp =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   187
 case (whatis x cp) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   188
  And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   189
| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   190
| Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   191
| NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   192
| Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   193
| Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   194
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   195
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   196
| Dvd (d,s) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   197
   ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   198
       in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   199
| NDvd(d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   200
        in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   201
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   202
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   203
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   204
                           bsetge,bsetdvd,bsetndvd,bsetP,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   205
                           infDdvd, infDndvd, bsetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   206
                           bsetdisj, infDconj, infDdisj] cp =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   207
 case (whatis x cp) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   208
  And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   209
| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   210
| Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   211
| NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   212
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   213
| Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   214
| Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   215
| Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   216
| Dvd (d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   217
        in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   218
| NDvd (d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   219
        in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   220
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   221
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   222
    (* Canonical linear form for terms, formulae etc.. *)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   223
fun provelin ctxt t = Goal.prove ctxt [] [] t
31101
26c7bb764a38 qualified names for Lin_Arith tactics and simprocs
haftmann
parents: 30686
diff changeset
   224
  (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   225
fun linear_cmul 0 tm = zero
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   226
  | linear_cmul n tm = case tm of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   227
      Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   228
    | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   229
    | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   230
    | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   231
    | _ => numeral1 (fn m => n * m) tm;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   232
fun earlier [] x y = false
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   233
  | earlier (h::t) x y =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   234
    if h aconv y then false else if h aconv x then true else earlier t x y;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   235
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   236
fun linear_add vars tm1 tm2 = case (tm1, tm2) of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   237
    (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   238
    Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   239
   if x1 = x2 then
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 32603
diff changeset
   240
     let val c = numeral2 Integer.add c1 c2
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   241
      in if c = zero then linear_add vars r1 r2
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   242
         else addC$(mulC$c$x1)$(linear_add vars r1 r2)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   243
     end
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   244
     else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   245
   else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   246
 | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   247
      addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   248
 | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   249
      addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 32603
diff changeset
   250
 | (_, _) => numeral2 Integer.add tm1 tm2;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   251
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   252
fun linear_neg tm = linear_cmul ~1 tm;
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   253
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   254
36806
fc27b0465a4c stylized COOPER exception
haftmann
parents: 36805
diff changeset
   255
exception COOPER of string;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   256
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   257
fun lint vars tm =  if is_number tm then tm  else case tm of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   258
  Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   259
| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   260
| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   261
| Const (@{const_name Groups.times}, _) $ s $ t =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   262
  let val s' = lint vars s
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   263
      val t' = lint vars t
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   264
  in case perhaps_number s' of SOME n => linear_cmul n t'
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   265
   | NONE => (case perhaps_number t' of SOME n => linear_cmul n s'
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   266
   | NONE => raise COOPER "lint: not linear")
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   267
  end
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   268
 | _ => addC $ (mulC $ one $ tm) $ zero;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   269
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   270
fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   271
    lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   272
  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   273
    lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   274
  | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   275
  | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   276
    HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
38549
d0385f2764d8 use antiquotations for remaining unqualified constants in HOL
haftmann
parents: 37388
diff changeset
   277
  | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   278
     (case lint vs (subC$t$s) of
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   279
      (t as a$(m$c$y)$r) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   280
        if x <> y then b$zero$t
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   281
        else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   282
        else b$(m$c$y)$(linear_neg r)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   283
      | t => b$zero$t)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   284
  | lin (vs as x::_) (b$s$t) =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   285
     (case lint vs (subC$t$s) of
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   286
      (t as a$(m$c$y)$r) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   287
        if x <> y then b$zero$t
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   288
        else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   289
        else b$(linear_neg r)$(m$c$y)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   290
      | t => b$zero$t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   291
  | lin vs fm = fm;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   292
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   293
fun lint_conv ctxt vs ct =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   294
let val t = term_of ct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   295
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   296
             RS eq_reflection
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   297
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   298
32398
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   299
fun is_intrel_type T = T = @{typ "int => int => bool"};
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   300
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   301
fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   302
  | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   303
  | is_intrel _ = false;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   304
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   305
fun linearize_conv ctxt vs ct = case term_of ct of
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   306
  Const(@{const_name Rings.dvd},_)$d$t =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   307
  let
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   308
    val th = Conv.binop_conv (lint_conv ctxt vs) ct
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   309
    val (d',t') = Thm.dest_binop (Thm.rhs_of th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   310
    val (dt',tt') = (term_of d', term_of t')
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   311
  in if is_number dt' andalso is_number tt'
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   312
     then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   313
     else
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   314
     let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   315
      val dth =
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   316
      ((if dest_number (term_of d') < 0 then
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   317
          Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   318
                           (Thm.transitive th (inst' [d',t'] dvd_uminus))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   319
        else th) handle TERM _ => th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   320
      val d'' = Thm.rhs_of dth |> Thm.dest_arg1
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   321
     in
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   322
      case tt' of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   323
        Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   324
        let val x = dest_number c
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   325
        in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   326
                                       (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   327
        else dth end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   328
      | _ => dth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   329
     end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   330
  end
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   331
| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   332
| t => if is_intrel t
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   333
      then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   334
       RS eq_reflection
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   335
      else Thm.reflexive ct;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   336
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   337
val dvdc = @{cterm "op dvd :: int => _"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   338
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   339
fun unify ctxt q =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   340
 let
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   341
  val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   342
  val x = term_of cx
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   343
  val ins = insert (op = : int * int -> bool)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   344
  fun h (acc,dacc) t =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   345
   case (term_of t) of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   346
    Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23713
diff changeset
   347
    if x aconv y andalso member (op =)
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   348
      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   349
    then (ins (dest_number c) acc,dacc) else (acc,dacc)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   350
  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23713
diff changeset
   351
    if x aconv y andalso member (op =)
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   352
       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   353
    then (ins (dest_number c) acc, dacc) else (acc,dacc)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   354
  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   355
    if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   356
  | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   357
  | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   358
  | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   359
  | _ => (acc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   360
  val (cs,ds) = h ([],[]) p
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
   361
  val l = Integer.lcms (union (op =) cs ds)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   362
  fun cv k ct =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   363
    let val (tm as b$s$t) = term_of ct
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   364
    in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   365
         |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   366
  fun nzprop x =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   367
   let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   368
    val th =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   369
     Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   370
      (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   371
           (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   372
           @{cterm "0::int"})))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   373
   in Thm.equal_elim (Thm.symmetric th) TrueI end;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   374
  val notz =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   375
    let val tab = fold Inttab.update
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   376
          (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   377
    in
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   378
      fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   379
        handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   380
          (writeln ("noz: Theorems-Table contains no entry for " ^
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   381
              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   382
    end
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   383
  fun unit_conv t =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   384
   case (term_of t) of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   385
   Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   386
  | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   387
  | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   388
  | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23713
diff changeset
   389
    if x=y andalso member (op =)
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   390
      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   391
    then cv (l div dest_number c) t else Thm.reflexive t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   392
  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23713
diff changeset
   393
    if x=y andalso member (op =)
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   394
      [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   395
    then cv (l div dest_number c) t else Thm.reflexive t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   396
  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   397
    if x=y then
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   398
      let
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   399
       val k = l div dest_number c
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   400
       val kt = HOLogic.mk_number iT k
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   401
       val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   402
             ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   403
       val (d',t') = (mulC$kt$d, mulC$kt$r)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   404
       val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   405
                   RS eq_reflection
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   406
       val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   407
                 RS eq_reflection
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   408
      in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   409
    else Thm.reflexive t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   410
  | _ => Thm.reflexive t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   411
  val uth = unit_conv p
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   412
  val clt =  Numeral.mk_cnumber @{ctyp "int"} l
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   413
  val ltx = Thm.capply (Thm.capply cmulC clt) cx
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   414
  val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   415
  val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   416
  val thf = Thm.transitive th
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   417
      (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   418
  val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   419
                  ||> Thm.beta_conversion true |>> Thm.symmetric
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   420
 in Thm.transitive (Thm.transitive lth thf) rth end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   421
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   422
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   423
val emptyIS = @{cterm "{}::int set"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   424
val insert_tm = @{cterm "insert :: int => _"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   425
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   426
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   427
val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   428
                                      |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   429
                      [asetP,bsetP];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   430
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   431
val D_tm = @{cpat "?D::int"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   432
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   433
fun cooperex_conv ctxt vs q =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   434
let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   435
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   436
 val uth = unify ctxt q
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   437
 val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   438
 val ins = insert (op aconvc)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   439
 fun h t (bacc,aacc,dacc) =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   440
  case (whatis x t) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   441
    And (p,q) => h q (h p (bacc,aacc,dacc))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   442
  | Or (p,q) => h q  (h p (bacc,aacc,dacc))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   443
  | Eq t => (ins (minus1 t) bacc,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   444
             ins (plus1 t) aacc,dacc)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   445
  | NEq t => (ins t bacc,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   446
              ins t aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   447
  | Lt t => (bacc, ins t aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   448
  | Le t => (bacc, ins (plus1 t) aacc,dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   449
  | Gt t => (ins t bacc, aacc,dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   450
  | Ge t => (ins (minus1 t) bacc, aacc,dacc)
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   451
  | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_number) dacc)
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   452
  | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_number) dacc)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   453
  | _ => (bacc, aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   454
 val (b0,a0,ds) = h p ([],[],[])
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   455
 val d = Integer.lcms ds
23582
94d0dd87cc24 avoid polymorphic equality;
wenzelm
parents: 23523
diff changeset
   456
 val cd = Numeral.mk_cnumber @{ctyp "int"} d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   457
 fun divprop x =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   458
   let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   459
    val th =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   460
     Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   461
      (Thm.capply @{cterm Trueprop}
23582
94d0dd87cc24 avoid polymorphic equality;
wenzelm
parents: 23523
diff changeset
   462
           (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   463
   in Thm.equal_elim (Thm.symmetric th) TrueI end;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   464
 val dvd =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   465
   let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   466
     fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   467
       handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   468
        (writeln ("dvd: Theorems-Table contains no entry for" ^
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   469
            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   470
   end
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   471
 val dp =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   472
   let val th = Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   473
      (Thm.capply @{cterm Trueprop}
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   474
           (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   475
   in Thm.equal_elim (Thm.symmetric th) TrueI end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   476
    (* A and B set *)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   477
   local
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   478
     val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   479
     val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   480
   in
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   481
    fun provein x S =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   482
     case term_of S of
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 31101
diff changeset
   483
        Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   484
      | Const(@{const_name insert}, _) $ y $ _ =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   485
         let val (cy,S') = Thm.dest_binop S
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   486
         in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   487
         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   488
                           (provein x S')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   489
         end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   490
   end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   491
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   492
 val al = map (lint vs o term_of) a0
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   493
 val bl = map (lint vs o term_of) b0
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   494
 val (sl,s0,f,abths,cpth) =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   495
   if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   496
   then
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   497
    (bl,b0,decomp_minf,
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   498
     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   499
                     [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   500
                   (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   501
                        [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   502
                         bsetdisj,infDconj, infDdisj]),
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   503
                       cpmi)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   504
     else (al,a0,decomp_pinf,fn A =>
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   505
          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   506
                   [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   507
                   (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   508
                   [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   509
                         asetdisj,infDconj, infDdisj]),cppi)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   510
 val cpth =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   511
  let
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   512
   val sths = map (fn (tl,t0) =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   513
                      if tl = term_of t0
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   514
                      then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   515
                      else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   516
                                 |> HOLogic.mk_Trueprop))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   517
                   (sl ~~ s0)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   518
   val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   519
   val S = mkISet csl
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   520
   val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   521
                    csl Termtab.empty
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   522
   val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   523
   val inS =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   524
     let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   525
      val tab = fold Termtab.update
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   526
        (map (fn eq =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   527
                let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   528
                    val th = if term_of s = term_of t
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   529
                             then the (Termtab.lookup inStab (term_of s))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   530
                             else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   531
                                [eq, the (Termtab.lookup inStab (term_of s))]
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   532
                 in (term_of t, th) end)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   533
                  sths) Termtab.empty
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   534
        in
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   535
          fn ct => the (Termtab.lookup tab (term_of ct))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   536
            handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   537
              (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   538
                raise Option)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   539
        end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   540
       val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   541
   in [dp, inf, nb, pd] MRS cpth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   542
   end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   543
 val cpth' = Thm.transitive uth (cpth RS eq_reflection)
27018
b3e63f39fc0f proper context for simp_thms_conv;
wenzelm
parents: 26928
diff changeset
   544
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   545
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   546
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   547
fun literals_conv bops uops env cv =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   548
 let fun h t =
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   549
  case (term_of t) of
36797
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   550
   b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t
cb074cec7a30 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents: 36717
diff changeset
   551
 | u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   552
 | _ => cv env t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   553
 in h end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   554
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   555
fun integer_nnf_conv ctxt env =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   556
 nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   557
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   558
val conv_ss = HOL_basic_ss addsimps
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   559
  (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}]);
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   560
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   561
fun conv ctxt p =
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   562
  Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   563
    (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   564
    (cooperex_conv ctxt) p
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   565
  handle CTERM s => raise COOPER "bad cterm"
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   566
       | THM s => raise COOPER "bad thm"
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   567
       | TYPE s => raise COOPER "bad type"
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   568
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   569
fun add_bools t =
36807
abcfc8372694 tuned; dropped strange myassoc2
haftmann
parents: 36806
diff changeset
   570
  let
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   571
    val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   572
      @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   573
      @{term "Not"}, @{term "All :: (int => _) => _"},
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   574
      @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   575
    val is_op = member (op =) ops;
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   576
    val skip = not (fastype_of t = HOLogic.boolT)
36807
abcfc8372694 tuned; dropped strange myassoc2
haftmann
parents: 36806
diff changeset
   577
  in case t of
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   578
      (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   579
              else insert (op aconv) t
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   580
    | f $ a => if skip orelse is_op f then add_bools a o add_bools f
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   581
              else insert (op aconv) t
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   582
    | Abs p => add_bools (snd (variant_abs p))
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   583
    | _ => if skip orelse is_op t then I else insert (op aconv) t
36807
abcfc8372694 tuned; dropped strange myassoc2
haftmann
parents: 36806
diff changeset
   584
  end;
abcfc8372694 tuned; dropped strange myassoc2
haftmann
parents: 36806
diff changeset
   585
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   586
fun descend vs (abs as (_, xT, _)) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   587
  let
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   588
    val (xn', p') = variant_abs abs;
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   589
  in ((xn', xT) :: vs, p') end;
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   590
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   591
local structure Proc = Cooper_Procedure in
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   592
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   593
fun num_of_term vs (Free vT) = Proc.Bound (find_index (fn vT' => vT' = vT) vs)
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   594
  | num_of_term vs (Term.Bound i) = Proc.Bound i
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   595
  | num_of_term vs @{term "0::int"} = Proc.C 0
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   596
  | num_of_term vs @{term "1::int"} = Proc.C 1
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   597
  | num_of_term vs (t as Const (@{const_name number_of}, _) $ _) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   598
      Proc.C (dest_number t)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   599
  | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   600
      Proc.Neg (num_of_term vs t')
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   601
  | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   602
      Proc.Add (num_of_term vs t1, num_of_term vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   603
  | num_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   604
      Proc.Sub (num_of_term vs t1, num_of_term vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   605
  | num_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   606
     (case perhaps_number t1
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   607
       of SOME n => Proc.Mul (n, num_of_term vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   608
        | NONE => (case perhaps_number t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   609
           of SOME n => Proc.Mul (n, num_of_term vs t1)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   610
            | NONE => raise COOPER "reification: unsupported kind of multiplication"))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   611
  | num_of_term _ _ = raise COOPER "reification: bad term";
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   612
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   613
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   614
  | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   615
  | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   616
      Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   617
  | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   618
      Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38558
diff changeset
   619
  | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   620
      Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   621
  | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   622
      Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   623
  | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   624
      Proc.Not (fm_of_term ps vs t')
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   625
  | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) =
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   626
      Proc.E (uncurry (fm_of_term ps) (descend vs abs))
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   627
  | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) =
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   628
      Proc.A (uncurry (fm_of_term ps) (descend vs abs))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   629
  | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   630
      Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   631
  | fm_of_term ps vs (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   632
      Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   633
  | fm_of_term ps vs (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   634
      Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   635
  | fm_of_term ps vs (Const (@{const_name Rings.dvd}, _) $ t1 $ t2) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   636
     (case perhaps_number t1
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   637
       of SOME n => Proc.Dvd (n, num_of_term vs t2)
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   638
        | NONE => raise COOPER "reification: unsupported dvd")
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   639
  | fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   640
      in if n > 0 then Proc.Closed n else raise COOPER "reification: unknown term" end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   641
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   642
fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   643
  | term_of_num vs (Proc.Bound n) = Free (nth vs n)
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   644
  | term_of_num vs (Proc.Neg t') =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   645
      @{term "uminus :: int => _"} $ term_of_num vs t'
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   646
  | term_of_num vs (Proc.Add (t1, t2)) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   647
      @{term "op + :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   648
  | term_of_num vs (Proc.Sub (t1, t2)) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   649
      @{term "op - :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   650
  | term_of_num vs (Proc.Mul (i, t2)) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   651
      @{term "op * :: int => _"} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   652
  | term_of_num vs (Proc.Cn (n, i, t')) =
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   653
      term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   654
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   655
fun term_of_fm ps vs Proc.T = HOLogic.true_const
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   656
  | term_of_fm ps vs Proc.F = HOLogic.false_const
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   657
  | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   658
  | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   659
  | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   660
  | term_of_fm ps vs (Proc.Iff (t1, t2)) = @{term "op = :: bool => _"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   661
  | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   662
  | term_of_fm ps vs (Proc.Eq t') = @{term "op = :: int => _ "} $ term_of_num vs t'$ @{term "0::int"}
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   663
  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   664
  | term_of_fm ps vs (Proc.Lt t') = @{term "op < :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   665
  | term_of_fm ps vs (Proc.Le t') = @{term "op <= :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   666
  | term_of_fm ps vs (Proc.Gt t') = @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   667
  | term_of_fm ps vs (Proc.Ge t') = @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   668
  | term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   669
      HOLogic.mk_number HOLogic.intT i $ term_of_num vs t'
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   670
  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   671
  | term_of_fm ps vs (Proc.Closed n) = nth ps n
36832
e6078ef937df tuned reification functions
haftmann
parents: 36831
diff changeset
   672
  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   673
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   674
fun procedure t =
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   675
  let
36833
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   676
    val vs = Term.add_frees t [];
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   677
    val ps = add_bools t [];
9628f969d843 represent de-Bruin indices simply by position in list
haftmann
parents: 36832
diff changeset
   678
  in (term_of_fm ps vs o Proc.pa o fm_of_term ps vs) t end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   679
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   680
end;
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   681
38808
89ae86205739 more antiquotations;
wenzelm
parents: 38795
diff changeset
   682
val (_, oracle) = Context.>>> (Context.map_theory_result
89ae86205739 more antiquotations;
wenzelm
parents: 38795
diff changeset
   683
  (Thm.add_oracle (@{binding cooper},
89ae86205739 more antiquotations;
wenzelm
parents: 38795
diff changeset
   684
    (fn (ctxt, t) =>
89ae86205739 more antiquotations;
wenzelm
parents: 38795
diff changeset
   685
      (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
89ae86205739 more antiquotations;
wenzelm
parents: 38795
diff changeset
   686
        (t, procedure t)))));
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   687
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   688
val comp_ss = HOL_ss addsimps @{thms semiring_norm};
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   689
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   690
fun strip_objimp ct =
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   691
  (case Thm.term_of ct of
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38558
diff changeset
   692
    Const (@{const_name HOL.implies}, _) $ _ $ _ =>
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   693
      let val (A, B) = Thm.dest_binop ct
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   694
      in A :: strip_objimp B end
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   695
  | _ => [ct]);
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   696
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   697
fun strip_objall ct = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   698
 case term_of ct of 
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   699
  Const (@{const_name All}, _) $ Abs (xn,xT,p) => 
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   700
   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   701
   in apfst (cons (a,v)) (strip_objall t')
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   702
   end
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   703
| _ => ([],ct);
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   704
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   705
local
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   706
  val all_maxscope_ss = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   707
     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   708
in
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   709
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   710
  CSUBGOAL (fn (p', i) =>
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   711
    let
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   712
     val (qvs, p) = strip_objall (Thm.dest_arg p')
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   713
     val (ps, c) = split_last (strip_objimp p)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   714
     val qs = filter P ps
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   715
     val q = if P c then c else @{cterm "False"}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   716
     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38558
diff changeset
   717
         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   718
     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   719
     val ntac = (case qs of [] => q aconvc @{cterm "False"}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   720
                         | _ => false)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   721
    in 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   722
    if ntac then no_tac
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   723
      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   724
    end)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   725
end;
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   726
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   727
local
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   728
 fun isnum t = case t of 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   729
   Const(@{const_name Groups.zero},_) => true
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   730
 | Const(@{const_name Groups.one},_) => true
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 37117
diff changeset
   731
 | @{term Suc}$s => isnum s
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   732
 | @{term "nat"}$s => isnum s
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   733
 | @{term "int"}$s => isnum s
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   734
 | Const(@{const_name Groups.uminus},_)$s => isnum s
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   735
 | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   736
 | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   737
 | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   738
 | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   739
 | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   740
 | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
36831
3037d6810fca tuned code; toward a tightended interface with generated code
haftmann
parents: 36807
diff changeset
   741
 | _ => is_number t orelse can HOLogic.dest_nat t
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   742
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   743
 fun ty cts t = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   744
 if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   745
    else case term_of t of 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   746
      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   747
               then not (isnum l orelse isnum r)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   748
               else not (member (op aconv) cts c)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   749
    | c$_ => not (member (op aconv) cts c)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   750
    | c => not (member (op aconv) cts c)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   751
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   752
 val term_constants =
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   753
  let fun h acc t = case t of
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   754
    Const _ => insert (op aconv) t acc
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   755
  | a$b => h (h acc a) b
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   756
  | Abs (_,_,t) => h acc t
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   757
  | _ => acc
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   758
 in h [] end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   759
in 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   760
fun is_relevant ctxt ct = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   761
 subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   762
 andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   763
 andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   764
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   765
fun int_nat_terms ctxt ct =
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   766
 let 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   767
  val cts = snd (get ctxt)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   768
  fun h acc t = if ty cts t then insert (op aconvc) t acc else
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   769
   case (term_of t) of
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   770
    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   771
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   772
  | _ => acc
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   773
 in h [] ct end
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   774
end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   775
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   776
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   777
 let 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   778
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   779
   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   780
   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   781
   val p' = fold_rev gen ts p
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   782
 in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   783
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   784
local
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   785
val ss1 = comp_ss
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   786
  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   787
      @ map (fn r => r RS sym) 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   788
        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   789
         @{thm "zmult_int"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   790
    addsplits [@{thm "zdiff_int_split"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   791
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   792
val ss2 = HOL_basic_ss
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   793
  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   794
            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   795
            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   796
  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   797
val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   798
  @ map (Thm.symmetric o mk_meta_eq) 
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   799
    [@{thm "dvd_eq_mod_eq_0"},
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   800
     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   801
     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   802
  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   803
     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   804
     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   805
     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   806
     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   807
  @ @{thms add_ac}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   808
 addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   809
 val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   810
     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   811
      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   812
in
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   813
fun nat_to_int_tac ctxt = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   814
  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   815
  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   816
  simp_tac (Simplifier.context ctxt comp_ss);
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   817
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   818
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   819
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   820
end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   821
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   822
fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
36805
929b23461a14 simplified oracle
haftmann
parents: 36804
diff changeset
   823
   let
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   824
    val cpth = 
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   825
       if !quick_and_dirty 
36805
929b23461a14 simplified oracle
haftmann
parents: 36804
diff changeset
   826
       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   827
       else Conv.arg_conv (conv ctxt) p
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   828
    val p' = Thm.rhs_of cpth
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36833
diff changeset
   829
    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   830
   in rtac th i end
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   831
   handle COOPER _ => no_tac);
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   832
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   833
fun finish_tac q = SUBGOAL (fn (_, i) =>
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   834
  (if q then I else TRY) (rtac TrueI i));
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   835
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   836
fun tac elim add_ths del_ths ctxt =
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   837
let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   838
    val aprems = Arith_Data.get_arith_facts ctxt
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   839
in
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   840
  Method.insert_tac aprems
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   841
  THEN_ALL_NEW Object_Logic.full_atomize_tac
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   842
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   843
  THEN_ALL_NEW simp_tac ss
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   844
  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   845
  THEN_ALL_NEW Object_Logic.full_atomize_tac
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   846
  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   847
  THEN_ALL_NEW Object_Logic.full_atomize_tac
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   848
  THEN_ALL_NEW div_mod_tac ctxt
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   849
  THEN_ALL_NEW splits_tac ctxt
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   850
  THEN_ALL_NEW simp_tac ss
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   851
  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   852
  THEN_ALL_NEW nat_to_int_tac ctxt
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   853
  THEN_ALL_NEW (core_tac ctxt)
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   854
  THEN_ALL_NEW finish_tac elim
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   855
end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   856
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   857
val method =
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   858
  let
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   859
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   860
    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   861
    val addN = "add"
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   862
    val delN = "del"
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   863
    val elimN = "elim"
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   864
    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   865
    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   866
  in
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   867
    Scan.optional (simple_keyword elimN >> K false) true --
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   868
    Scan.optional (keyword addN |-- thms) [] --
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   869
    Scan.optional (keyword delN |-- thms) [] >>
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   870
    (fn ((elim, add_ths), del_ths) => fn ctxt =>
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   871
      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   872
  end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   873
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   874
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   875
(* theory setup *)
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   876
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   877
local
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   878
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   879
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   880
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   881
val constsN = "consts";
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   882
val any_keyword = keyword constsN
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   883
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   884
val terms = thms >> map (term_of o Drule.dest_term);
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   885
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   886
fun optional scan = Scan.optional scan [];
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   887
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   888
in
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   889
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   890
val setup =
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   891
  Attrib.setup @{binding presburger}
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   892
    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   893
      optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
36804
f4ad04780669 shorten names
haftmann
parents: 36802
diff changeset
   894
  #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
36802
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   895
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   896
end;
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   897
5f9fe7b3295d only one module fpr presburger method
haftmann
parents: 36799
diff changeset
   898
end;