wneuper/isa: src/HOL/Tools/Qelim/cooper.ML@db10cf19f1f8

     1 (*  Title:      HOL/Tools/Presburger/cooper.ML

     2     ID:         $Id$

     3     Author:     Amine Chaieb, TU Muenchen

     4 *)

     6 signature COOPER =

     7  sig

     8   val cooper_conv : Proof.context -> conv

     9   exception COOPER of string * exn

    10 end;

    12 structure Cooper: COOPER =

    13 struct

    15 open Conv;

    16 open Normalizer;

    17 structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);

    19 exception COOPER of string * exn;

    20 val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);

    21 val FWD = Drule.implies_elim_list;

    23 val true_tm = @{cterm "True"};

    24 val false_tm = @{cterm "False"};

    25 val zdvd1_eq = @{thm "zdvd1_eq"};

    26 val presburger_ss = @{simpset} addsimps [zdvd1_eq];

    27 val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});

    29 val iT = HOLogic.intT

    30 val bT = HOLogic.boolT;

    31 val dest_numeral = HOLogic.dest_number #> snd;

    33 val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =

    34     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};

    36 val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =

    37     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};

    39 val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =

    40     map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};

    42 val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];

    44 val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;

    46 val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,

    47       asetgt, asetge, asetdvd, asetndvd,asetP],

    48      [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,

    49       bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];

    51 val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},

    52                                 @{thm "plusinfinity"}, @{thm "cppi"}];

    54 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};

    56 val [zdvd_mono,simp_from_to,all_not_ex] =

    57      [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];

    59 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};

    61 val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv];

    62 val eval_conv = Simplifier.rewrite eval_ss;

    64 (* recognising cterm without moving to terms *)

    66 datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm

    67             | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm

    68             | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox

    70 fun whatis x ct =

    71 ( case (term_of ct) of

    72   Const("op &",_)$_$_ => And (Thm.dest_binop ct)

    73 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)

    74 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox

    75 | Const("Not",_) $ (Const ("op =",_)$y$_) =>

    76   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox

    77 | Const ("Orderings.ord_class.less",_)$y$z =>

    78    if term_of x aconv y then Lt (Thm.dest_arg ct)

    79    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox

    80 | Const ("Orderings.ord_class.less_eq",_)$y$z =>

    81    if term_of x aconv y then Le (Thm.dest_arg ct)

    82    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox

    83 | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>

    84    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox

    85 | Const("Not",_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>

    86    if term_of x aconv y then

    87    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox

    88 | _ => Nox)

    89   handle CTERM _ => Nox;

    91 fun get_pmi_term t =

    92   let val (x,eq) =

    93      (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)

    94         (Thm.dest_arg t)

    95 in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;

    97 val get_pmi = get_pmi_term o cprop_of;

    99 val p_v' = @{cpat "?P' :: int => bool"};

   100 val q_v' = @{cpat "?Q' :: int => bool"};

   101 val p_v = @{cpat "?P:: int => bool"};

   102 val q_v = @{cpat "?Q:: int => bool"};

   104 fun myfwd (th1, th2, th3) p q

   105       [(th_1,th_2,th_3), (th_1',th_2',th_3')] =

   106   let

   107    val (mp', mq') = (get_pmi th_1, get_pmi th_1')

   108    val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)

   109                    [th_1, th_1']

   110    val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']

   111    val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']

   112   in (mi_th, set_th, infD_th)

   113   end;

   115 val inst' = fn cts => instantiate' [] (map SOME cts);

   116 val infDTrue = instantiate' [] [SOME true_tm] infDP;

   117 val infDFalse = instantiate' [] [SOME false_tm] infDP;

   119 val cadd =  @{cterm "op + :: int => _"}

   120 val cmulC =  @{cterm "op * :: int => _"}

   121 val cminus =  @{cterm "op - :: int => _"}

   122 val cone =  @{cterm "1 :: int"}

   123 val cneg = @{cterm "uminus :: int => _"}

   124 val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]

   125 val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];

   127 val is_numeral = can dest_numeral;

   129 fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));

   130 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));

   132 val [minus1,plus1] =

   133     map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];

   135 fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,

   136                            asetgt, asetge,asetdvd,asetndvd,asetP,

   137                            infDdvd, infDndvd, asetconj,

   138                            asetdisj, infDconj, infDdisj] cp =

   139  case (whatis x cp) of

   140   And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))

   141 | Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))

   142 | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))

   143 | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))

   144 | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))

   145 | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))

   146 | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))

   147 | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))

   148 | Dvd (d,s) =>

   149    ([],let val dd = dvd d

   150 	     in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)

   151 | NDvd(d,s) => ([],let val dd = dvd d

   152 	      in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)

   153 | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));

   155 fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,

   156                            bsetge,bsetdvd,bsetndvd,bsetP,

   157                            infDdvd, infDndvd, bsetconj,

   158                            bsetdisj, infDconj, infDdisj] cp =

   159  case (whatis x cp) of

   160   And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))

   161 | Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))

   162 | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))

   163 | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))

   164 | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))

   165 | Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))

   166 | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))

   167 | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))

   168 | Dvd (d,s) => ([],let val dd = dvd d

   169 	      in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)

   170 | NDvd (d,s) => ([],let val dd = dvd d

   171 	      in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)

   172 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))

   174     (* Canonical linear form for terms, formulae etc.. *)

   175 fun provelin ctxt t = Goal.prove ctxt [] [] t

   176                           (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]);

   177 fun linear_cmul 0 tm =  zero

   178   | linear_cmul n tm =

   179     case tm of

   180       Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)

   181     | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x

   182     | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)

   183     | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)

   184     | _ =>  numeral1 (Integer.mult n) tm;

   185 fun earlier [] x y = false

   186 	| earlier (h::t) x y =

   187     if h aconv y then false else if h aconv x then true else earlier t x y;

   189 fun linear_add vars tm1 tm2 =

   190  case (tm1,tm2) of

   191 	 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,

   192     Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>

   193    if x1 = x2 then

   194      let val c = numeral2 Integer.add c1 c2

   195 	   in if c = zero then linear_add vars r1  r2

   196 	      else addC$(mulC$c$x1)$(linear_add vars  r1 r2)

   197      end

   198 	 else if earlier vars x1 x2 then addC$(mulC$ c1 $ x1)$(linear_add vars r1 tm2)

   199    else addC$(mulC$c2$x2)$(linear_add vars tm1 r2)

   200  | (Const("HOL.plus_class.plus",_) $ (Const("HOL.times_class.times",_)$c1$x1)$r1 ,_) =>

   201     	  addC$(mulC$c1$x1)$(linear_add vars r1 tm2)

   202  | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>

   203       	  addC$(mulC$c2$x2)$(linear_add vars tm1 r2)

   204  | (_,_) => numeral2 Integer.add tm1 tm2;

   206 fun linear_neg tm = linear_cmul ~1 tm;

   207 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);

   210 fun lint vars tm =

   211 if is_numeral tm then tm

   212 else case tm of

   213  Const("HOL.minus_class.uminus",_)$t => linear_neg (lint vars t)

   214 | Const("HOL.plus_class.plus",_) $ s $ t => linear_add vars (lint vars s) (lint vars t)

   215 | Const("HOL.minus_class.minus",_) $ s $ t => linear_sub vars (lint vars s) (lint vars t)

   216 | Const ("HOL.times_class.times",_) $ s $ t =>

   217   let val s' = lint vars s

   218       val t' = lint vars t

   219   in if is_numeral s' then (linear_cmul (dest_numeral s') t')

   220      else if is_numeral t' then (linear_cmul (dest_numeral t') s')

   221      else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))

   222   end

   223  | _ => addC$(mulC$one$tm)$zero;

   225 fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) =

   226     lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)

   227   | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) =

   228     lin vs (Const("Orderings.ord_class.less",T)$t$s)

   229   | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)

   230   | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) =

   231     HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)

   232   | lin (vs as x::_) ((b as Const("op =",_))$s$t) =

   233      (case lint vs (subC$t$s) of

   234       (t as a$(m$c$y)$r) =>

   235         if x <> y then b$zero$t

   236         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r

   237         else b$(m$c$y)$(linear_neg r)

   238       | t => b$zero$t)

   239   | lin (vs as x::_) (b$s$t) =

   240      (case lint vs (subC$t$s) of

   241       (t as a$(m$c$y)$r) =>

   242         if x <> y then b$zero$t

   243         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r

   244         else b$(linear_neg r)$(m$c$y)

   245       | t => b$zero$t)

   246   | lin vs fm = fm;

   248 fun lint_conv ctxt vs ct =

   249 let val t = term_of ct

   250 in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))

   251              RS eq_reflection

   252 end;

   254 fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT

   255   | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT

   256   | is_intrel _ = false;

   258 fun linearize_conv ctxt vs ct =

   259  case (term_of ct) of

   260   Const(@{const_name Divides.dvd},_)$d$t =>

   261   let

   262     val th = binop_conv (lint_conv ctxt vs) ct

   263     val (d',t') = Thm.dest_binop (Thm.rhs_of th)

   264     val (dt',tt') = (term_of d', term_of t')

   265   in if is_numeral dt' andalso is_numeral tt'

   266      then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th

   267      else

   268      let

   269       val dth =

   270       ((if dest_numeral (term_of d') < 0 then

   271           Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))

   272                            (Thm.transitive th (inst' [d',t'] dvd_uminus))

   273         else th) handle TERM _ => th)

   274       val d'' = Thm.rhs_of dth |> Thm.dest_arg1

   275      in

   276       case tt' of

   277         Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$_)$_ =>

   278         let val x = dest_numeral c

   279         in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))

   280                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))

   281         else dth end

   282       | _ => dth

   283      end

   284   end

   285 | Const("Not",_)$(Const(@{const_name Divides.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct

   286 | t => if is_intrel t

   287       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))

   288        RS eq_reflection

   289       else reflexive ct;

   291 val dvdc = @{cterm "op dvd :: int => _"};

   293 fun unify ctxt q =

   294  let

   295   val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE

   296   val x = term_of cx

   297   val ins = insert (op = : integer*integer -> bool)

   298   fun h (acc,dacc) t =

   299    case (term_of t) of

   300     Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>

   301     if x aconv y

   302        andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]

   303     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)

   304   | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>

   305     if x aconv y

   306        andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]

   307     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)

   308   | Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) =>

   309     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)

   310   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)

   311   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)

   312   | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)

   313   | _ => (acc, dacc)

   314   val (cs,ds) = h ([],[]) p

   315   val l = fold Integer.lcm (cs union ds) 1

   316   fun cv k ct =

   317     let val (tm as b$s$t) = term_of ct

   318     in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))

   319          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end

   320   fun nzprop x =

   321    let

   322     val th =

   323      Simplifier.rewrite lin_ss

   324       (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}

   325            (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))

   326            @{cterm "0::int"})))

   327    in equal_elim (Thm.symmetric th) TrueI end;

   328   val notz = let val tab = fold Integertab.update

   329                                (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty

   330             in

   331              (fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral))

   332                 handle Option => (writeln "noz: Theorems-Table contains no entry for";

   333                                     print_cterm ct ; raise Option)))

   334            end

   335   fun unit_conv t =

   336    case (term_of t) of

   337    Const("op &",_)$_$_ => binop_conv unit_conv t

   338   | Const("op |",_)$_$_ => binop_conv unit_conv t

   339   | Const("Not",_)$_ => arg_conv unit_conv t

   340   | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>

   341     if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]

   342     then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t

   343   | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>

   344     if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]

   345     then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t

   346   | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) =>

   347     if x=y then

   348       let

   349        val k = Integer.div l (dest_numeral c)

   350        val kt = HOLogic.mk_number iT k

   351        val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]

   352              ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)

   353        val (d',t') = (mulC$kt$d, mulC$kt$r)

   354        val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))

   355                    RS eq_reflection

   356        val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))

   357                  RS eq_reflection

   358       in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end

   359     else Thm.reflexive t

   360   | _ => Thm.reflexive t

   361   val uth = unit_conv p

   362   val clt =  Numeral.mk_cnumber @{ctyp "int"} l

   363   val ltx = Thm.capply (Thm.capply cmulC clt) cx

   364   val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)

   365   val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex

   366   val thf = transitive th

   367       (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')

   368   val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true

   369                   ||> beta_conversion true |>> Thm.symmetric

   370  in transitive (transitive lth thf) rth end;

   373 val emptyIS = @{cterm "{}::int set"};

   374 val insert_tm = @{cterm "insert :: int => _"};

   375 val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] ---> bT);

   376 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;

   377 val cTrp = @{cterm "Trueprop"};

   378 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;

   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

   380                                       |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)

   381                       [asetP,bsetP];

   383 val D_tm = @{cpat "?D::int"};

   385 val int_eq = (op =):integer*integer -> bool;

   386 fun cooperex_conv ctxt vs q =

   387 let

   389  val uth = unify ctxt q

   390  val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))

   391  val ins = insert (op aconvc)

   392  fun h t (bacc,aacc,dacc) =

   393   case (whatis x t) of

   394     And (p,q) => h q (h p (bacc,aacc,dacc))

   395   | Or (p,q) => h q  (h p (bacc,aacc,dacc))

   396   | Eq t => (ins (minus1 t) bacc,

   397              ins (plus1 t) aacc,dacc)

   398   | NEq t => (ins t bacc,

   399               ins t aacc, dacc)

   400   | Lt t => (bacc, ins t aacc, dacc)

   401   | Le t => (bacc, ins (plus1 t) aacc,dacc)

   402   | Gt t => (ins t bacc, aacc,dacc)

   403   | Ge t => (ins (minus1 t) bacc, aacc,dacc)

   404   | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc)

   405   | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)

   406   | _ => (bacc, aacc, dacc)

   407  val (b0,a0,ds) = h p ([],[],[])

   408  val d = fold Integer.lcm ds 1

   409  val cd = Numeral.mk_cnumber @{ctyp "int"} d

   410  val dt = term_of cd

   411  fun divprop x =

   412    let

   413     val th =

   414      Simplifier.rewrite lin_ss

   415       (Thm.capply @{cterm Trueprop}

   416            (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))

   417    in equal_elim (Thm.symmetric th) TrueI end;

   418  val dvd = let val tab = fold Integertab.update

   419                                (ds ~~ (map divprop ds)) Integertab.empty in

   420            (fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral))

   421                     handle Option => (writeln "dvd: Theorems-Table contains no entry for";

   422                                       print_cterm ct ; raise Option)))

   423            end

   424  val dp =

   425    let val th = Simplifier.rewrite lin_ss

   426       (Thm.capply @{cterm Trueprop}

   427            (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))

   428    in equal_elim (Thm.symmetric th) TrueI end;

   429     (* A and B set *)

   430    local

   431      val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}

   432      val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}

   433    in

   434     fun provein x S =

   435      case term_of S of

   436         Const("{}",_) => error "Unexpected error in Cooper please email Amine Chaieb"

   437       | Const("insert",_)$y$_ =>

   438          let val (cy,S') = Thm.dest_binop S

   439          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1

   440          else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)

   441                            (provein x S')

   442          end

   443    end

   445  val al = map (lint vs o term_of) a0

   446  val bl = map (lint vs o term_of) b0

   447  val (sl,s0,f,abths,cpth) =

   448    if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)

   449    then

   450     (bl,b0,decomp_minf,

   451      fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)

   452                      [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@

   453                    (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))

   454                         [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,

   455                          bsetdisj,infDconj, infDdisj]),

   456                        cpmi)

   457      else (al,a0,decomp_pinf,fn A =>

   458           (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)

   459                    [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@

   460                    (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))

   461                    [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,

   462                          asetdisj,infDconj, infDdisj]),cppi)

   463  val cpth =

   464   let

   465    val sths = map (fn (tl,t0) =>

   466                       if tl = term_of t0

   467                       then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl

   468                       else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)

   469                                  |> HOLogic.mk_Trueprop))

   470                    (sl ~~ s0)

   471    val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)

   472    val S = mkISet csl

   473    val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)

   474                     csl Termtab.empty

   475    val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp

   476    val inS =

   477      let

   478       fun transmem th0 th1 =

   479        Thm.equal_elim

   480         (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule

   481                ((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1

   482       val tab = fold Termtab.update

   483         (map (fn eq =>

   484                 let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop

   485                     val th = if term_of s = term_of t

   486                              then valOf(Termtab.lookup inStab (term_of s))

   487                              else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)

   488                                 [eq, valOf(Termtab.lookup inStab (term_of s))]

   489                  in (term_of t, th) end)

   490                   sths) Termtab.empty

   491         in fn ct =>

   492           (valOf (Termtab.lookup tab (term_of ct))

   493            handle Option => (writeln "inS: No theorem for " ; print_cterm ct ; raise Option))

   494         end

   495        val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p

   496    in [dp, inf, nb, pd] MRS cpth

   497    end

   498  val cpth' = Thm.transitive uth (cpth RS eq_reflection)

   499 in Thm.transitive cpth' ((simp_thms_conv then_conv eval_conv) (Thm.rhs_of cpth'))

   500 end;

   502 fun literals_conv bops uops env cv =

   503  let fun h t =

   504   case (term_of t) of

   505    b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t

   506  | u$_ => if member (op aconv) uops u then arg_conv h t else cv env t

   507  | _ => cv env t

   508  in h end;

   510 fun integer_nnf_conv ctxt env =

   511  nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);

   513 (* val my_term = ref (@{cterm "NotaHING"}); *)

   514 local

   515  val pcv = Simplifier.rewrite

   516      (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))

   517                       @ [not_all,all_not_ex, ex_disj_distrib]))

   518  val postcv = Simplifier.rewrite presburger_ss

   519  fun conv ctxt p =

   520   let val _ = () (* my_term := p *)

   521   in

   522    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)

   523       (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)

   524       (cooperex_conv ctxt) p

   525   end

   526   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)

   527         | THM s => raise COOPER ("Cooper Failed", THM s)

   528         | TYPE s => raise COOPER ("Cooper Failed", TYPE s)

   529 in val cooper_conv = conv

   530 end;

   531 end;

   535 structure Coopereif =

   536 struct

   538 open GeneratedCooper;

   540 fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);

   541 fun i_of_term vs t = case t

   542  of Free (xn, xT) => (case AList.lookup (op aconv) vs t

   543      of NONE   => cooper "Variable not found in the list!"

   544       | SOME n => Bound n)

   545   | @{term "0::int"} => C 0

   546   | @{term "1::int"} => C 1

   547   | Term.Bound i => Bound (Integer.int i)

   548   | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')

   549   | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)

   550   | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)

   551   | Const(@{const_name HOL.times},_)$t1$t2 =>

   552      (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)

   553     handle TERM _ =>

   554        (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)

   555         handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))

   556   | _ => (C (HOLogic.dest_number t |> snd)

   557            handle TERM _ => cooper "Reification: unknown term");

   559 fun qf_of_term ps vs t =  case t

   560  of Const("True",_) => T

   561   | Const("False",_) => F

   562   | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))

   563   | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))

   564   | Const(@{const_name Divides.dvd},_)$t1$t2 =>

   565       (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")

   566   | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))

   567   | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)

   568   | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)

   569   | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)

   570   | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)

   571   | Const("Not",_)$t' => Nota(qf_of_term ps vs t')

   572   | Const("Ex",_)$Abs(xn,xT,p) =>

   573      let val (xn',p') = variant_abs (xn,xT,p)

   574          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)

   575      in E (qf_of_term ps vs' p')

   576      end

   577   | Const("All",_)$Abs(xn,xT,p) =>

   578      let val (xn',p') = variant_abs (xn,xT,p)

   579          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)

   580      in A (qf_of_term ps vs' p')

   581      end

   582   | _ =>(case AList.lookup (op aconv) ps t of

   583            NONE => cooper "Reification: unknown term!"

   584          | SOME n => Closed n);

   586 local

   587  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},

   588              @{term "op = :: int => _"}, @{term "op < :: int => _"},

   589              @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},

   590              @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]

   591 fun ty t = Bool.not (fastype_of t = HOLogic.boolT)

   592 in

   593 fun term_bools acc t =

   594 case t of

   595     (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b

   596             else insert (op aconv) t acc

   597   | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a

   598             else insert (op aconv) t acc

   599   | Abs p => term_bools acc (snd (variant_abs p))

   600   | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc

   601 end;

   603 fun myassoc2 l v =

   604     case l of

   605 	[] => NONE

   606       | (x,v')::xs => if v = v' then SOME x

   607 		      else myassoc2 xs v;

   609 fun term_of_i vs t = case t

   610  of C i => HOLogic.mk_number HOLogic.intT i

   611   | Bound n => the (myassoc2 vs n)

   612   | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'

   613   | Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2

   614   | Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2

   615   | Mul (i, t2) => @{term "op * :: int => _"} $

   616       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2

   617   | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound 0), t'));

   619 fun term_of_qf ps vs t =

   620  case t of

   621    T => HOLogic.true_const

   622  | F => HOLogic.false_const

   623  | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}

   624  | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}

   625  | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'

   626  | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'

   627  | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}

   628  | NEq t' => term_of_qf ps vs (Nota (Eq t'))

   629  | Dvd(i,t') => @{term "op dvd :: int => _ "} $

   630     HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'

   631  | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))

   632  | Nota t' => HOLogic.Not$(term_of_qf ps vs t')

   633  | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)

   634  | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)

   635  | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)

   636  | Iffa(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2

   637  | Closed n => the (myassoc2 ps n)

   638  | NClosed n => term_of_qf ps vs (Nota (Closed n))

   639  | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";

   641 fun cooper_oracle thy t =

   642   let

   643     val (vs, ps) = pairself (map_index (swap o apfst Integer.int))

   644       (term_frees t, term_bools [] t);

   645   in

   646     equals propT $ HOLogic.mk_Trueprop t $

   647       HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))

   648   end;

   650 end;

author	haftmann
	Tue, 10 Jul 2007 17:30:54 +0200
changeset 23713	db10cf19f1f8
parent 23689	0410269099dc
child 23881	851c74f1bb69
permissions	-rw-r--r--