# HG changeset patch
# User haftmann
# Date 1199283264 -3600
# Node ID 1c1ca4b20ec69de20815c55a19e03f08c2b5caa6
# Parent  852bce03412ac9b535f099bbd07a0fb5309ca8b5
some more antiquotations

diff -r 852bce03412a -r 1c1ca4b20ec6 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Jan 02 15:14:23 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Jan 02 15:14:24 2008 +0100
@@ -71,7 +71,7 @@
   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("Not",_) $ (Const ("op =",_)$y$_) => 
+| 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 HOL.less}, _) $ y$ z =>
    if term_of x aconv y then Lt (Thm.dest_arg ct) 
@@ -81,7 +81,7 @@
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox 
-| Const("Not",_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
    if term_of x aconv y then 
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox 
 | _ => Nox)
@@ -173,59 +173,55 @@
     (* Canonical linear form for terms, formulae etc.. *)
 fun provelin ctxt t = Goal.prove ctxt [] [] t 
   (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
-fun linear_cmul 0 tm =  zero 
-  | linear_cmul n tm = 
-    case tm of  
-      Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)
-    | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (fn m => n * m) c)$x
-    | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)
-    | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)
-    | _ =>  numeral1 (fn m => n * m) tm;
+fun linear_cmul 0 tm = zero 
+  | linear_cmul n tm = case tm of  
+      Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
+    | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
+    | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
+    | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
+    | _ => numeral1 (fn m => n * m) tm;
 fun earlier [] x y = false 
 	| earlier (h::t) x y = 
     if h aconv y then false else if h aconv x then true else earlier t x y; 
 
-fun linear_add vars tm1 tm2 = 
- case (tm1,tm2) of 
-	 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,
-    Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
+fun linear_add vars tm1 tm2 = case (tm1, tm2) of 
+    (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
+    Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
    if x1 = x2 then 
      let val c = numeral2 (curry op +) c1 c2
-	   in if c = zero then linear_add vars r1  r2  
-	      else addC$(mulC$c$x1)$(linear_add vars  r1 r2)
+      in if c = zero then linear_add vars r1 r2
+         else addC$(mulC$c$x1)$(linear_add vars r1 r2)
      end 
-	 else if earlier vars x1 x2 then addC$(mulC$ c1 $ x1)$(linear_add vars r1 tm2)
-   else addC$(mulC$c2$x2)$(linear_add vars tm1 r2)
- | (Const("HOL.plus_class.plus",_) $ (Const("HOL.times_class.times",_)$c1$x1)$r1 ,_) => 
-    	  addC$(mulC$c1$x1)$(linear_add vars r1 tm2)
- | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
-      	  addC$(mulC$c2$x2)$(linear_add vars tm1 r2) 
- | (_,_) => numeral2 (curry op +) tm1 tm2;
+     else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
+   else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
+ | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
+      addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
+ | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => 
+      addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
+ | (_, _) => numeral2 (curry op +) tm1 tm2;
  
 fun linear_neg tm = linear_cmul ~1 tm; 
 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
 
 
-fun lint vars tm = 
-if is_numeral tm then tm 
-else case tm of 
- Const("HOL.minus_class.uminus",_)$t => linear_neg (lint vars t)
-| Const("HOL.plus_class.plus",_) $ s $ t => linear_add vars (lint vars s) (lint vars t) 
-| Const("HOL.minus_class.minus",_) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
-| Const ("HOL.times_class.times",_) $ s $ t => 
+fun lint vars tm =  if is_numeral tm then tm  else case tm of 
+  Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
+| Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
+| Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
+| Const (@{const_name HOL.times}, _) $ s $ t =>
   let val s' = lint vars s  
       val t' = lint vars t  
   in if is_numeral s' then (linear_cmul (dest_numeral s') t') 
      else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
      else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
   end 
- | _ => addC$(mulC$one$tm)$zero;
+ | _ => addC $ (mulC $ one $ tm) $ zero;
 
-fun lin (vs as x::_) (Const("Not", _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
-    lin vs (Const(@{const_name HOL.less_eq}, T) $ t $ s)
-  | lin (vs as x::_) (Const("Not",_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
-    lin vs (Const(@{const_name HOL.less}, T) $ t $ s)
-  | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
+    lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
+  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
+    lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
+  | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = 
     HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
   | lin (vs as x::_) ((b as Const("op =",_))$s$t) = 
@@ -254,8 +250,7 @@
   | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
   | is_intrel _ = false;
  
-fun linearize_conv ctxt vs ct =  
- case (term_of ct) of 
+fun linearize_conv ctxt vs ct = case term_of ct of
   Const(@{const_name Divides.dvd},_)$d$t => 
   let 
     val th = binop_conv (lint_conv ctxt vs) ct
@@ -273,7 +268,7 @@
       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
      in
       case tt' of 
-        Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$_)$_ => 
+        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ => 
         let val x = dest_numeral c
         in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
@@ -281,7 +276,7 @@
       | _ => dth
      end
   end
-| Const("Not",_)$(Const(@{const_name Divides.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
+| Const (@{const_name Not},_)$(Const(@{const_name Divides.dvd},_)$_$_) => 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
@@ -296,19 +291,19 @@
   val ins = insert (op = : int * int -> bool)
   fun h (acc,dacc) t = 
    case (term_of t) of
-    Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
+    Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => 
     if x aconv y andalso member (op =)
       ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
-  | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
+  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => 
     if x aconv y andalso member (op =)
        [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
-  | Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) => 
+  | Const(@{const_name Divides.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) => 
     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
-  | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
+  | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   | _ => (acc, dacc)
   val (cs,ds) = h ([],[]) p
   val l = Integer.lcms (cs union ds)
@@ -335,16 +330,16 @@
    case (term_of t) of
    Const("op &",_)$_$_ => binop_conv unit_conv t
   | Const("op |",_)$_$_ => binop_conv unit_conv t
-  | Const("Not",_)$_ => arg_conv unit_conv t
-  | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
+  | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
+  | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ => 
     if x=y andalso member (op =)
       ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
+  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) => 
     if x=y andalso member (op =)
       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
+  | Const(@{const_name Divides.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) => 
     if x=y then 
       let 
        val k = l div dest_numeral c
@@ -567,7 +562,7 @@
   | 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 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
-  | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
+  | Const (@{const_name Not},_)$t' => Nota(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)
diff -r 852bce03412a -r 1c1ca4b20ec6 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Wed Jan 02 15:14:23 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Jan 02 15:14:24 2008 +0100
@@ -58,7 +58,7 @@
  | @{term "Suc"}$s => isnum s
  | @{term "nat"}$s => isnum s
  | @{term "int"}$s => isnum s
- | Const(@{const_name "uminus"},_)$s => isnum s
+ | Const(@{const_name "HOL.uminus"},_)$s => isnum s
  | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r