src/HOL/Tools/Qelim/cooper.ML
author haftmann
Wed, 05 May 2010 18:25:34 +0200
changeset 36692 54b64d4ad524
parent 36527 68a837d1a754
child 36717 2a72455be88b
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
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
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     3
*)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     4
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     5
signature COOPER =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     6
 sig
23484
731658208196 made type conv pervasive;
wenzelm
parents: 23466
diff changeset
     7
  val cooper_conv : Proof.context -> conv
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     8
  exception COOPER of string * exn
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     9
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    10
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    11
structure Cooper: COOPER =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    12
struct
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
    13
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    14
open Conv;
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
    15
open Normalizer;
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
    16
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    17
exception COOPER of string * exn;
27018
b3e63f39fc0f proper context for simp_thms_conv;
wenzelm
parents: 26928
diff changeset
    18
fun simp_thms_conv ctxt =
35410
1ea89d2a1bd4 more antiquotations;
wenzelm
parents: 35267
diff changeset
    19
  Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
23484
731658208196 made type conv pervasive;
wenzelm
parents: 23466
diff changeset
    20
val FWD = Drule.implies_elim_list;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    21
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    22
val true_tm = @{cterm "True"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    23
val false_tm = @{cterm "False"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    24
val zdvd1_eq = @{thm "zdvd1_eq"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    25
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
    26
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
    27
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    28
val iT = HOLogic.intT
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    29
val bT = HOLogic.boolT;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    30
val dest_numeral = HOLogic.dest_number #> snd;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    31
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    32
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
    33
    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    34
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    35
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    36
    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    37
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    38
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
    39
    map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    40
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    41
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    42
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    43
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    44
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    45
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    46
      asetgt, asetge, asetdvd, asetndvd,asetP],
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    47
     [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    48
      bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    49
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    50
val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    51
                                @{thm "plusinfinity"}, @{thm "cppi"}];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    52
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    53
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    54
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    55
val [zdvd_mono,simp_from_to,all_not_ex] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    56
     [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    57
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    58
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    59
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    60
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
    61
val eval_conv = Simplifier.rewrite eval_ss;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    62
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
    63
(* recognising cterm without moving to terms *)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    64
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    65
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
    66
            | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    67
            | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    68
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    69
fun whatis x ct =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    70
( case (term_of ct) of
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    71
  Const("op &",_)$_$_ => And (Thm.dest_binop ct)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    72
| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    73
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    74
| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    75
  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
    76
| Const (@{const_name Orderings.less}, _) $ y$ z =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    77
   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
    78
   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
    79
| Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    80
   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
    81
   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
    82
| 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
    83
   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
    84
| 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
    85
   if term_of x aconv y then
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    86
   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
    87
| _ => Nox)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    88
  handle CTERM _ => Nox;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    89
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    90
fun get_pmi_term t =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
    91
  let val (x,eq) =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    92
     (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
    93
        (Thm.dest_arg t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    94
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
    95
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    96
val get_pmi = get_pmi_term o cprop_of;
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 p_v' = @{cpat "?P' :: int => bool"};
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    99
val q_v' = @{cpat "?Q' :: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   100
val p_v = @{cpat "?P:: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   101
val q_v = @{cpat "?Q:: int => bool"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   102
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   103
fun myfwd (th1, th2, th3) p q
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   104
      [(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
   105
  let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   106
   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
   107
   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
   108
                   [th_1, th_1']
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   109
   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
   110
   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
   111
  in (mi_th, set_th, infD_th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   112
  end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   113
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   114
val inst' = fn cts => instantiate' [] (map SOME cts);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   115
val infDTrue = instantiate' [] [SOME true_tm] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   116
val infDFalse = instantiate' [] [SOME false_tm] infDP;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   117
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   118
val cadd =  @{cterm "op + :: int => _"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   119
val cmulC =  @{cterm "op * :: int => _"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   120
val cminus =  @{cterm "op - :: int => _"}
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   121
val cone =  @{cterm "1 :: int"}
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   122
val cneg = @{cterm "uminus :: int => _"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   123
val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   124
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   125
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   126
val is_numeral = can dest_numeral;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   127
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   128
fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   129
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   130
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   131
val [minus1,plus1] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   132
    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
   133
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   134
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   135
                           asetgt, asetge,asetdvd,asetndvd,asetP,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   136
                           infDdvd, infDndvd, asetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   137
                           asetdisj, infDconj, infDdisj] cp =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   138
 case (whatis x cp) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   139
  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
   140
| 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
   141
| 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
   142
| 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
   143
| 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
   144
| 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
   145
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   146
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   147
| Dvd (d,s) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   148
   ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   149
       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
   150
| NDvd(d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   151
        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
   152
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   153
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   154
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   155
                           bsetge,bsetdvd,bsetndvd,bsetP,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   156
                           infDdvd, infDndvd, bsetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   157
                           bsetdisj, infDconj, infDdisj] cp =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   158
 case (whatis x cp) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   159
  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
   160
| 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
   161
| 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
   162
| 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
   163
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   164
| Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   165
| 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
   166
| 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
   167
| Dvd (d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   168
        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
   169
| NDvd (d,s) => ([],let val dd = dvd d
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   170
        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
   171
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   172
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   173
    (* Canonical linear form for terms, formulae etc.. *)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   174
fun provelin ctxt t = Goal.prove ctxt [] [] t
31101
26c7bb764a38 qualified names for Lin_Arith tactics and simprocs
haftmann
parents: 30686
diff changeset
   175
  (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
   176
fun linear_cmul 0 tm = zero
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   177
  | linear_cmul n tm = case tm of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   178
      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
   179
    | 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
   180
    | 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
   181
    | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   182
    | _ => numeral1 (fn m => n * m) tm;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   183
fun earlier [] x y = false
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   184
  | earlier (h::t) x y =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   185
    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
   186
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   187
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
   188
    (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
   189
    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
   190
   if x1 = x2 then
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 32603
diff changeset
   191
     let val c = numeral2 Integer.add c1 c2
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   192
      in if c = zero then linear_add vars r1 r2
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   193
         else addC$(mulC$c$x1)$(linear_add vars r1 r2)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   194
     end
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   195
     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
   196
   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
   197
 | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   198
      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
   199
 | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   200
      addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
33002
f3f02f36a3e2 uniform use of Integer.add/mult/sum/prod;
wenzelm
parents: 32603
diff changeset
   201
 | (_, _) => numeral2 Integer.add tm1 tm2;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   202
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   203
fun linear_neg tm = linear_cmul ~1 tm;
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   204
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
   205
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   206
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   207
fun lint vars tm =  if is_numeral tm then tm  else case tm of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   208
  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
   209
| 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
   210
| 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
   211
| Const (@{const_name Groups.times}, _) $ s $ t =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   212
  let val s' = lint vars s
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   213
      val t' = lint vars t
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   214
  in if is_numeral s' then (linear_cmul (dest_numeral s') t')
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   215
     else if is_numeral t' then (linear_cmul (dest_numeral t') s')
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   216
     else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   217
  end
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   218
 | _ => addC $ (mulC $ one $ tm) $ zero;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   219
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   220
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
   221
    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
   222
  | 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
   223
    lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   224
  | 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
   225
  | 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
   226
    HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   227
  | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   228
     (case lint vs (subC$t$s) of
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   229
      (t as a$(m$c$y)$r) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   230
        if x <> y then b$zero$t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   231
        else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   232
        else b$(m$c$y)$(linear_neg r)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   233
      | t => b$zero$t)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   234
  | lin (vs as x::_) (b$s$t) =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   235
     (case lint vs (subC$t$s) of
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   236
      (t as a$(m$c$y)$r) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   237
        if x <> y then b$zero$t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   238
        else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   239
        else b$(linear_neg r)$(m$c$y)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   240
      | t => b$zero$t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   241
  | lin vs fm = fm;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   242
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   243
fun lint_conv ctxt vs ct =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   244
let val t = term_of ct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   245
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
   246
             RS eq_reflection
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   247
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   248
32398
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   249
fun is_intrel_type T = T = @{typ "int => int => bool"};
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   250
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   251
fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
40a0760a00ea stricter condition for (binary) integer relation
boehmes
parents: 32264
diff changeset
   252
  | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   253
  | is_intrel _ = false;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   254
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   255
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
   256
  Const(@{const_name Rings.dvd},_)$d$t =>
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   257
  let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   258
    val th = binop_conv (lint_conv ctxt vs) ct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   259
    val (d',t') = Thm.dest_binop (Thm.rhs_of th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   260
    val (dt',tt') = (term_of d', term_of t')
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   261
  in if is_numeral dt' andalso is_numeral tt'
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   262
     then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   263
     else
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   264
     let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   265
      val dth =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   266
      ((if dest_numeral (term_of d') < 0 then
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   267
          Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   268
                           (Thm.transitive th (inst' [d',t'] dvd_uminus))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   269
        else th) handle TERM _ => th)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   270
      val d'' = Thm.rhs_of dth |> Thm.dest_arg1
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   271
     in
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   272
      case tt' of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   273
        Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   274
        let val x = dest_numeral c
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   275
        in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   276
                                       (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   277
        else dth end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   278
      | _ => dth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   279
     end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   280
  end
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   281
| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   282
| t => if is_intrel t
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   283
      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
   284
       RS eq_reflection
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   285
      else reflexive ct;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   286
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   287
val dvdc = @{cterm "op dvd :: int => _"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   288
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   289
fun unify ctxt q =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   290
 let
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   291
  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
   292
  val x = term_of cx
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   293
  val ins = insert (op = : int * int -> bool)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   294
  fun h (acc,dacc) t =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   295
   case (term_of t) of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   296
    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
   297
    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
   298
      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   299
    then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   300
  | 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
   301
    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
   302
       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   303
    then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   304
  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   305
    if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   306
  | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   307
  | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   308
  | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   309
  | _ => (acc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   310
  val (cs,ds) = h ([],[]) p
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
   311
  val l = Integer.lcms (union (op =) cs ds)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   312
  fun cv k ct =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   313
    let val (tm as b$s$t) = term_of ct
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   314
    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
   315
         |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   316
  fun nzprop x =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   317
   let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   318
    val th =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   319
     Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   320
      (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   321
           (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
   322
           @{cterm "0::int"})))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   323
   in equal_elim (Thm.symmetric th) TrueI end;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   324
  val notz =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   325
    let val tab = fold Inttab.update
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   326
          (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   327
    in
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   328
      fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   329
        handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   330
          (writeln ("noz: Theorems-Table contains no entry for " ^
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   331
              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   332
    end
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   333
  fun unit_conv t =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   334
   case (term_of t) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   335
   Const("op &",_)$_$_ => binop_conv unit_conv t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   336
  | Const("op |",_)$_$_ => binop_conv unit_conv t
25768
1c1ca4b20ec6 some more antiquotations
haftmann
parents: 24630
diff changeset
   337
  | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   338
  | 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
   339
    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
   340
      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   341
    then cv (l div dest_numeral c) t else Thm.reflexive t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   342
  | 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
   343
    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
   344
      [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   345
    then cv (l div dest_numeral c) t else Thm.reflexive t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   346
  | 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
   347
    if x=y then
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   348
      let
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   349
       val k = l div dest_numeral c
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   350
       val kt = HOLogic.mk_number iT k
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   351
       val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   352
             ((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
   353
       val (d',t') = (mulC$kt$d, mulC$kt$r)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   354
       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
   355
                   RS eq_reflection
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   356
       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
   357
                 RS eq_reflection
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   358
      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
   359
    else Thm.reflexive t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   360
  | _ => Thm.reflexive t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   361
  val uth = unit_conv p
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   362
  val clt =  Numeral.mk_cnumber @{ctyp "int"} l
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   363
  val ltx = Thm.capply (Thm.capply cmulC clt) cx
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   364
  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
   365
  val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   366
  val thf = transitive th
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   367
      (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   368
  val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   369
                  ||> beta_conversion true |>> Thm.symmetric
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   370
 in transitive (transitive lth thf) rth end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   371
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   372
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   373
val emptyIS = @{cterm "{}::int set"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   374
val insert_tm = @{cterm "insert :: int => _"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   375
val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] ---> bT);
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   376
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
   377
val cTrp = @{cterm "Trueprop"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   378
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   379
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
   380
                                      |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   381
                      [asetP,bsetP];
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   382
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   383
val D_tm = @{cpat "?D::int"};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   384
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   385
fun cooperex_conv ctxt vs q =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   386
let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   387
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   388
 val uth = unify ctxt q
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   389
 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
   390
 val ins = insert (op aconvc)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   391
 fun h t (bacc,aacc,dacc) =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   392
  case (whatis x t) of
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   393
    And (p,q) => h q (h p (bacc,aacc,dacc))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   394
  | Or (p,q) => h q  (h p (bacc,aacc,dacc))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   395
  | Eq t => (ins (minus1 t) bacc,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   396
             ins (plus1 t) aacc,dacc)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   397
  | NEq t => (ins t bacc,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   398
              ins t aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   399
  | Lt t => (bacc, ins t aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   400
  | Le t => (bacc, ins (plus1 t) aacc,dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   401
  | Gt t => (ins t bacc, aacc,dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   402
  | Ge t => (ins (minus1 t) bacc, aacc,dacc)
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   403
  | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   404
  | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   405
  | _ => (bacc, aacc, dacc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   406
 val (b0,a0,ds) = h p ([],[],[])
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   407
 val d = Integer.lcms ds
23582
94d0dd87cc24 avoid polymorphic equality;
wenzelm
parents: 23523
diff changeset
   408
 val cd = Numeral.mk_cnumber @{ctyp "int"} d
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   409
 val dt = term_of cd
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   410
 fun divprop x =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   411
   let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   412
    val th =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   413
     Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   414
      (Thm.capply @{cterm Trueprop}
23582
94d0dd87cc24 avoid polymorphic equality;
wenzelm
parents: 23523
diff changeset
   415
           (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   416
   in equal_elim (Thm.symmetric th) TrueI end;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   417
 val dvd =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   418
   let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   419
     fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   420
       handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   421
        (writeln ("dvd: Theorems-Table contains no entry for" ^
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   422
            Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   423
   end
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   424
 val dp =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   425
   let val th = Simplifier.rewrite lin_ss
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   426
      (Thm.capply @{cterm Trueprop}
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   427
           (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   428
   in equal_elim (Thm.symmetric th) TrueI end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   429
    (* A and B set *)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   430
   local
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   431
     val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   432
     val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   433
   in
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   434
    fun provein x S =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   435
     case term_of S of
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 31101
diff changeset
   436
        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
   437
      | Const(@{const_name insert}, _) $ y $ _ =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   438
         let val (cy,S') = Thm.dest_binop S
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   439
         in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   440
         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   441
                           (provein x S')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   442
         end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   443
   end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   444
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   445
 val al = map (lint vs o term_of) a0
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   446
 val bl = map (lint vs o term_of) b0
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   447
 val (sl,s0,f,abths,cpth) =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   448
   if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   449
   then
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   450
    (bl,b0,decomp_minf,
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   451
     fn B => (map (fn th => 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
   452
                     [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   453
                   (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   454
                        [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   455
                         bsetdisj,infDconj, infDdisj]),
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   456
                       cpmi)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   457
     else (al,a0,decomp_pinf,fn A =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   458
          (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   459
                   [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   460
                   (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   461
                   [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   462
                         asetdisj,infDconj, infDdisj]),cppi)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   463
 val cpth =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   464
  let
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   465
   val sths = map (fn (tl,t0) =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   466
                      if tl = term_of t0
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   467
                      then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   468
                      else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   469
                                 |> HOLogic.mk_Trueprop))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   470
                   (sl ~~ s0)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   471
   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
   472
   val S = mkISet csl
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   473
   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
   474
                    csl Termtab.empty
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   475
   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
   476
   val inS =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   477
     let
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   478
      fun transmem th0 th1 =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   479
       Thm.equal_elim
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   480
        (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   481
               ((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   482
      val tab = fold Termtab.update
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   483
        (map (fn eq =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   484
                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
   485
                    val th = if term_of s = term_of t
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   486
                             then the (Termtab.lookup inStab (term_of s))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   487
                             else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   488
                                [eq, the (Termtab.lookup inStab (term_of s))]
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   489
                 in (term_of t, th) end)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   490
                  sths) Termtab.empty
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   491
        in
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 33002
diff changeset
   492
          fn ct => the (Termtab.lookup tab (term_of ct))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   493
            handle Option =>
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   494
              (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
   495
                raise Option)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   496
        end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   497
       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
   498
   in [dp, inf, nb, pd] MRS cpth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   499
   end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   500
 val cpth' = Thm.transitive uth (cpth RS eq_reflection)
27018
b3e63f39fc0f proper context for simp_thms_conv;
wenzelm
parents: 26928
diff changeset
   501
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
   502
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   503
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   504
fun literals_conv bops uops env cv =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   505
 let fun h t =
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   506
  case (term_of t) of
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   507
   b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   508
 | u$_ => if member (op aconv) uops u then arg_conv h t else cv env t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   509
 | _ => cv env t
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   510
 in h end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   511
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   512
fun integer_nnf_conv ctxt env =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   513
 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
   514
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   515
local
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   516
 val pcv = Simplifier.rewrite
35410
1ea89d2a1bd4 more antiquotations;
wenzelm
parents: 35267
diff changeset
   517
     (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
1ea89d2a1bd4 more antiquotations;
wenzelm
parents: 35267
diff changeset
   518
                      @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   519
 val postcv = Simplifier.rewrite presburger_ss
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   520
 fun conv ctxt p =
24298
229fdfc1ddd9 removed dead code;
wenzelm
parents: 24075
diff changeset
   521
  let val _ = ()
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   522
  in
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   523
   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   524
      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   525
      (cooperex_conv ctxt) p
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   526
  end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   527
  handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   528
        | THM s => raise COOPER ("Cooper Failed", THM s)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   529
        | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   530
in val cooper_conv = conv
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   531
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   532
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   533
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   534
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   535
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   536
structure Coopereif =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   537
struct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   538
36527
68a837d1a754 modernized structure name
haftmann
parents: 35410
diff changeset
   539
open Generated_Cooper;
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   540
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36527
diff changeset
   541
fun member eq = Library.member eq;
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36527
diff changeset
   542
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   543
fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   544
fun i_of_term vs t = case t
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   545
 of Free (xn, xT) => (case AList.lookup (op aconv) vs t
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   546
     of NONE   => cooper "Variable not found in the list!"
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   547
      | SOME n => Bound n)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   548
  | @{term "0::int"} => C 0
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   549
  | @{term "1::int"} => C 1
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   550
  | Term.Bound i => Bound i
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   551
  | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t')
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   552
  | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   553
  | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   554
  | Const(@{const_name Groups.times},_)$t1$t2 =>
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   555
     (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   556
    handle TERM _ =>
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   557
       (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   558
        handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   559
  | _ => (C (HOLogic.dest_number t |> snd)
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   560
           handle TERM _ => cooper "Reification: unknown term");
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   561
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   562
fun qf_of_term ps vs t =  case t
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   563
 of Const("True",_) => T
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   564
  | Const("False",_) => F
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   565
  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35050
diff changeset
   566
  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   567
  | Const(@{const_name Rings.dvd},_)$t1$t2 =>
28397
389c5e494605 handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents: 28290
diff changeset
   568
      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   569
  | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   570
  | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   571
  | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   572
  | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   573
  | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   574
  | Const (@{const_name Not},_)$t' => Not(qf_of_term ps vs t')
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   575
  | Const("Ex",_)$Abs(xn,xT,p) =>
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   576
     let val (xn',p') = variant_abs (xn,xT,p)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   577
         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   578
     in E (qf_of_term ps vs' p')
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   579
     end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   580
  | Const("All",_)$Abs(xn,xT,p) =>
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   581
     let val (xn',p') = variant_abs (xn,xT,p)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   582
         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   583
     in A (qf_of_term ps vs' p')
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   584
     end
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   585
  | _ =>(case AList.lookup (op aconv) ps t of
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   586
           NONE => cooper "Reification: unknown term!"
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   587
         | SOME n => Closed n);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   588
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   589
local
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   590
 val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   591
             @{term "op = :: int => _"}, @{term "op < :: int => _"},
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   592
             @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   593
             @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   594
fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   595
in
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   596
fun term_bools acc t =
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   597
case t of
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36527
diff changeset
   598
    (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   599
            else insert (op aconv) t acc
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36527
diff changeset
   600
  | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   601
            else insert (op aconv) t acc
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   602
  | Abs p => term_bools acc (snd (variant_abs p))
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36527
diff changeset
   603
  | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   604
end;
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   605
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   606
fun myassoc2 l v =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   607
    case l of
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   608
  [] => NONE
23689
0410269099dc replaced code generator framework for reflected cooper
haftmann
parents: 23582
diff changeset
   609
      | (x,v')::xs => if v = v' then SOME x
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   610
          else myassoc2 xs v;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   611
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   612
fun term_of_i vs t = case t
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   613
 of C i => HOLogic.mk_number HOLogic.intT i
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   614
  | Bound n => the (myassoc2 vs n)
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   615
  | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   616
  | Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   617
  | Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   618
  | Mul (i, t2) => @{term "op * :: int => _"} $
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   619
      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   620
  | Cn (n, i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   621
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   622
fun term_of_qf ps vs t =
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   623
 case t of
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   624
   T => HOLogic.true_const
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   625
 | F => HOLogic.false_const
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   626
 | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   627
 | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   628
 | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   629
 | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   630
 | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   631
 | NEq t' => term_of_qf ps vs (Not (Eq t'))
32429
54758ca53fd6 modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents: 32398
diff changeset
   632
 | Dvd(i,t') => @{term "op dvd :: int => _ "} $
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   633
    HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   634
 | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   635
 | Not t' => HOLogic.Not$(term_of_qf ps vs t')
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   636
 | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   637
 | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   638
 | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   639
 | Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   640
 | Closed n => the (myassoc2 ps n)
29787
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   641
 | NClosed n => term_of_qf ps vs (Not (Closed n))
23bf900a21db regenerated presburger code
haftmann
parents: 29265
diff changeset
   642
 | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   643
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 27651
diff changeset
   644
fun cooper_oracle ct =
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   645
  let
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 27651
diff changeset
   646
    val thy = Thm.theory_of_cterm ct;
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 27651
diff changeset
   647
    val t = Thm.term_of ct;
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 28397
diff changeset
   648
    val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   649
  in
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 27651
diff changeset
   650
    Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 27651
diff changeset
   651
      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
23713
db10cf19f1f8 now works with SML/NJ
haftmann
parents: 23689
diff changeset
   652
  end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   653
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   654
end;