# HG changeset patch
# User haftmann
# Date 1273487149 -7200
# Node ID cb074cec7a3012f3299207b79422dcb77377fb4b
# Parent  739a9379e29b06bfa24d1026a2455dde13f1c0f2
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)

diff -r 739a9379e29b -r cb074cec7a30 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sun May 09 22:51:11 2010 -0700
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 12:25:49 2010 +0200
@@ -11,8 +11,6 @@
 structure Cooper: COOPER =
 struct
 
-open Conv;
-
 exception COOPER of string * exn;
 fun simp_thms_conv ctxt =
   Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
@@ -46,8 +44,7 @@
      [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
       bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
 
-val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
-                                @{thm "plusinfinity"}, @{thm "cppi"}];
+val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
 
 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
 
@@ -69,7 +66,7 @@
 ( case (term_of ct) of
   Const("op &",_)$_$_ => And (Thm.dest_binop ct)
 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
-| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
 | Const (@{const_name Orderings.less}, _) $ y$ z =>
@@ -118,8 +115,7 @@
 val cmulC =  @{cterm "op * :: int => _"}
 val cminus =  @{cterm "op - :: int => _"}
 val cone =  @{cterm "1 :: int"}
-val cneg = @{cterm "uminus :: int => _"}
-val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]
+val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
 val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
 
 val is_numeral = can dest_numeral;
@@ -254,16 +250,16 @@
 fun linearize_conv ctxt vs ct = case term_of ct of
   Const(@{const_name Rings.dvd},_)$d$t =>
   let
-    val th = binop_conv (lint_conv ctxt vs) ct
+    val th = Conv.binop_conv (lint_conv ctxt vs) ct
     val (d',t') = Thm.dest_binop (Thm.rhs_of th)
     val (dt',tt') = (term_of d', term_of t')
   in if is_numeral dt' andalso is_numeral tt'
-     then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th
+     then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
      else
      let
       val dth =
       ((if dest_numeral (term_of d') < 0 then
-          Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))
+          Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
                            (Thm.transitive th (inst' [d',t'] dvd_uminus))
         else th) handle TERM _ => th)
       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
@@ -271,13 +267,13 @@
       case tt' of
         Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
         let val x = dest_numeral c
-        in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
+        in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
         else dth end
       | _ => dth
      end
   end
-| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
+| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct
 | t => if is_intrel t
       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
        RS eq_reflection
@@ -331,9 +327,9 @@
     end
   fun unit_conv t =
    case (term_of t) of
-   Const("op &",_)$_$_ => binop_conv unit_conv t
-  | Const("op |",_)$_$_ => binop_conv unit_conv t
-  | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
+   Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
+  | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
+  | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
     if x=y andalso member (op =)
       ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
@@ -371,9 +367,7 @@
 
 val emptyIS = @{cterm "{}::int set"};
 val insert_tm = @{cterm "insert :: int => _"};
-val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] ---> bT);
 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
-val cTrp = @{cterm "Trueprop"};
 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
 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
                                       |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
@@ -399,13 +393,12 @@
   | Le t => (bacc, ins (plus1 t) aacc,dacc)
   | Gt t => (ins t bacc, aacc,dacc)
   | Ge t => (ins (minus1 t) bacc, aacc,dacc)
-  | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
-  | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
+  | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
+  | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
   | _ => (bacc, aacc, dacc)
  val (b0,a0,ds) = h p ([],[],[])
  val d = Integer.lcms ds
  val cd = Numeral.mk_cnumber @{ctyp "int"} d
- val dt = term_of cd
  fun divprop x =
    let
     val th =
@@ -474,10 +467,6 @@
    val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
    val inS =
      let
-      fun transmem th0 th1 =
-       Thm.equal_elim
-        (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
-               ((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1
       val tab = fold Termtab.update
         (map (fn eq =>
                 let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
@@ -503,8 +492,8 @@
 fun literals_conv bops uops env cv =
  let fun h t =
   case (term_of t) of
-   b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t
- | u$_ => if member (op aconv) uops u then arg_conv h t else cv env t
+   b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t
+ | u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t
  | _ => cv env t
  in h end;
 
@@ -535,55 +524,53 @@
 structure Coopereif =
 struct
 
-open Generated_Cooper;
-
 fun member eq = Library.member eq;
 
 fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
 fun i_of_term vs t = case t
  of Free (xn, xT) => (case AList.lookup (op aconv) vs t
      of NONE   => cooper "Variable not found in the list!"
-      | SOME n => Bound n)
-  | @{term "0::int"} => C 0
-  | @{term "1::int"} => C 1
-  | Term.Bound i => Bound i
-  | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t')
-  | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-  | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+      | SOME n => Generated_Cooper.Bound n)
+  | @{term "0::int"} => Generated_Cooper.C 0
+  | @{term "1::int"} => Generated_Cooper.C 1
+  | Term.Bound i => Generated_Cooper.Bound i
+  | Const(@{const_name Groups.uminus},_)$t' => Generated_Cooper.Neg (i_of_term vs t')
+  | Const(@{const_name Groups.plus},_)$t1$t2 => Generated_Cooper.Add (i_of_term vs t1,i_of_term vs t2)
+  | Const(@{const_name Groups.minus},_)$t1$t2 => Generated_Cooper.Sub (i_of_term vs t1,i_of_term vs t2)
   | Const(@{const_name Groups.times},_)$t1$t2 =>
-     (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
+     (Generated_Cooper.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
     handle TERM _ =>
-       (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
+       (Generated_Cooper.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
         handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
-  | _ => (C (HOLogic.dest_number t |> snd)
+  | _ => (Generated_Cooper.C (HOLogic.dest_number t |> snd)
            handle TERM _ => cooper "Reification: unknown term");
 
 fun qf_of_term ps vs t =  case t
- of Const("True",_) => T
-  | Const("False",_) => F
-  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
-  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+ of Const("True",_) => Generated_Cooper.T
+  | Const("False",_) => Generated_Cooper.F
+  | Const(@{const_name Orderings.less},_)$t1$t2 => Generated_Cooper.Lt (Generated_Cooper.Sub (i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Generated_Cooper.Le (Generated_Cooper.Sub(i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Rings.dvd},_)$t1$t2 =>
-      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
-  | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
-  | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
-  | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
-  | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
-  | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
-  | Const (@{const_name Not},_)$t' => Not(qf_of_term ps vs t')
+      (Generated_Cooper.Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
+  | @{term "op = :: int => _"}$t1$t2 => Generated_Cooper.Eq (Generated_Cooper.Sub (i_of_term vs t1,i_of_term vs t2))
+  | @{term "op = :: bool => _ "}$t1$t2 => Generated_Cooper.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op &",_)$t1$t2 => Generated_Cooper.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op |",_)$t1$t2 => Generated_Cooper.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op -->",_)$t1$t2 => Generated_Cooper.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const (@{const_name Not},_)$t' => Generated_Cooper.Not(qf_of_term ps vs t')
   | Const("Ex",_)$Abs(xn,xT,p) =>
      let val (xn',p') = variant_abs (xn,xT,p)
          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
-     in E (qf_of_term ps vs' p')
+     in Generated_Cooper.E (qf_of_term ps vs' p')
      end
   | Const("All",_)$Abs(xn,xT,p) =>
      let val (xn',p') = variant_abs (xn,xT,p)
          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
-     in A (qf_of_term ps vs' p')
+     in Generated_Cooper.A (qf_of_term ps vs' p')
      end
   | _ =>(case AList.lookup (op aconv) ps t of
            NONE => cooper "Reification: unknown term!"
-         | SOME n => Closed n);
+         | SOME n => Generated_Cooper.Closed n);
 
 local
  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
@@ -609,35 +596,35 @@
           else myassoc2 xs v;
 
 fun term_of_i vs t = case t
- of C i => HOLogic.mk_number HOLogic.intT i
-  | Bound n => the (myassoc2 vs n)
-  | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
-  | Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
-  | Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
-  | Mul (i, t2) => @{term "op * :: int => _"} $
+ of Generated_Cooper.C i => HOLogic.mk_number HOLogic.intT i
+  | Generated_Cooper.Bound n => the (myassoc2 vs n)
+  | Generated_Cooper.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
+  | Generated_Cooper.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+  | Generated_Cooper.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+  | Generated_Cooper.Mul (i, t2) => @{term "op * :: int => _"} $
       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
-  | Cn (n, i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
+  | Generated_Cooper.Cn (n, i, t') => term_of_i vs (Generated_Cooper.Add (Generated_Cooper.Mul (i, Generated_Cooper.Bound n), t'));
 
 fun term_of_qf ps vs t =
  case t of
-   T => HOLogic.true_const
- | F => HOLogic.false_const
- | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
- | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | NEq t' => term_of_qf ps vs (Not (Eq t'))
- | Dvd(i,t') => @{term "op dvd :: int => _ "} $
+   Generated_Cooper.T => HOLogic.true_const
+ | Generated_Cooper.F => HOLogic.false_const
+ | Generated_Cooper.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
+ | Generated_Cooper.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
+ | Generated_Cooper.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
+ | Generated_Cooper.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
+ | Generated_Cooper.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
+ | Generated_Cooper.NEq t' => term_of_qf ps vs (Generated_Cooper.Not (Generated_Cooper.Eq t'))
+ | Generated_Cooper.Dvd(i,t') => @{term "op dvd :: int => _ "} $
     HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
- | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
- | Not t' => HOLogic.Not$(term_of_qf ps vs t')
- | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Closed n => the (myassoc2 ps n)
- | NClosed n => term_of_qf ps vs (Not (Closed n))
+ | Generated_Cooper.NDvd(i,t')=> term_of_qf ps vs (Generated_Cooper.Not(Generated_Cooper.Dvd(i,t')))
+ | Generated_Cooper.Not t' => HOLogic.Not$(term_of_qf ps vs t')
+ | Generated_Cooper.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
+ | Generated_Cooper.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
+ | Generated_Cooper.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
+ | Generated_Cooper.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Generated_Cooper.Closed n => the (myassoc2 ps n)
+ | Generated_Cooper.NClosed n => term_of_qf ps vs (Generated_Cooper.Not (Generated_Cooper.Closed n))
  | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
 
 fun cooper_oracle ct =
@@ -647,7 +634,7 @@
     val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   in
     Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
-      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
+      HOLogic.mk_Trueprop (term_of_qf ps vs (Generated_Cooper.pa (qf_of_term ps vs t)))))
   end;
 
 end;
diff -r 739a9379e29b -r cb074cec7a30 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Sun May 09 22:51:11 2010 -0700
+++ b/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 12:25:49 2010 +0200
@@ -10,7 +10,6 @@
 structure Presburger : PRESBURGER = 
 struct
 
-open Conv;
 val comp_ss = HOL_ss addsimps @{thms semiring_norm};
 
 fun strip_objimp ct =
@@ -152,7 +151,7 @@
        if !quick_and_dirty 
        then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
              (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
-       else arg_conv (Cooper.cooper_conv ctxt) p
+       else Conv.arg_conv (Cooper.cooper_conv ctxt) p
     val p' = Thm.rhs_of cpth
     val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
    in rtac th i end