# HG changeset patch
# User haftmann
# Date 1273596363 -7200
# Node ID e6078ef937df2de6e25df67c622faff4cee70580
# Parent  3037d6810fca6f680f021660fcdbeee5c0725701
tuned reification functions

diff -r 3037d6810fca -r e6078ef937df src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 18:31:36 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 18:46:03 2010 +0200
@@ -582,81 +582,96 @@
     | _ => if skip orelse is_op t then I else insert (op aconv) t
   end;
 
+fun descend vs (abs as (_, xT, _)) =
+  let
+    val (xn', p') = variant_abs abs;
+    val vs' = ((xn', xT), 0) :: (map o apsnd) (fn n => n + 1) vs;
+  in (vs', p') end;
+
 local structure Proc = Cooper_Procedure in
 
-fun i_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
-  | i_of_term vs (Term.Bound i) = Proc.Bound i
-  | i_of_term vs @{term "0::int"} = Proc.C 0
-  | i_of_term vs @{term "1::int"} = Proc.C 1
-  | i_of_term vs (t as Const (@{const_name number_of}, _) $ _) = Proc.C (dest_number t)
-  | i_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') = Proc.Neg (i_of_term vs t')
-  | i_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) = Proc.Add (i_of_term vs t1, i_of_term vs t2)
-  | i_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) = Proc.Sub (i_of_term vs t1, i_of_term vs t2)
-  | i_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) = (case perhaps_number t1
-     of SOME n => Proc.Mul (n, i_of_term vs t2)
-      | NONE => (case perhaps_number t2
-         of SOME n => Proc.Mul (n, i_of_term vs t1)
-          | NONE => raise COOPER "reification: unsupported kind of multiplication"))
-  | i_of_term _ _ = raise COOPER "reification: unknown term";
+fun num_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
+  | num_of_term vs (Term.Bound i) = Proc.Bound i
+  | num_of_term vs @{term "0::int"} = Proc.C 0
+  | num_of_term vs @{term "1::int"} = Proc.C 1
+  | num_of_term vs (t as Const (@{const_name number_of}, _) $ _) =
+      Proc.C (dest_number t)
+  | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
+      Proc.Neg (num_of_term vs t')
+  | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
+      Proc.Add (num_of_term vs t1, num_of_term vs t2)
+  | num_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) =
+      Proc.Sub (num_of_term vs t1, num_of_term vs t2)
+  | num_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) =
+     (case perhaps_number t1
+       of SOME n => Proc.Mul (n, num_of_term vs t2)
+        | NONE => (case perhaps_number t2
+           of SOME n => Proc.Mul (n, num_of_term vs t1)
+            | NONE => raise COOPER "reification: unsupported kind of multiplication"))
+  | num_of_term _ _ = raise COOPER "reification: bad term";
 
-fun qf_of_term ps vs t = case t
- of Const (@{const_name True}, _) => Proc.T
-  | Const (@{const_name False}, _) => Proc.F
-  | Const (@{const_name Orderings.less}, _) $ t1 $ t2 => Proc.Lt (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
-  | Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2 => Proc.Le (Proc.Sub(i_of_term vs t1, i_of_term vs t2))
-  | Const (@{const_name Rings.dvd}, _) $ t1 $ t2 =>
-      (Proc.Dvd (dest_number t1, i_of_term vs t2)
-        handle TERM _ => raise COOPER "reification: unsupported dvd")
-  | @{term "op = :: int => _"} $ t1 $ t2 => Proc.Eq (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
-  | @{term "op = :: bool => _ "} $ t1 $ t2 => Proc.Iff (qf_of_term ps vs t1, qf_of_term ps vs t2)
-  | Const ("op &", _) $ t1 $t2 => Proc.And (qf_of_term ps vs t1, qf_of_term ps vs t2)
-  | Const ("op |", _) $ t1 $ t2 => Proc.Or (qf_of_term ps vs t1, qf_of_term ps vs t2)
-  | Const ("op -->", _) $ t1 $t2 => Proc.Imp (qf_of_term ps vs t1, qf_of_term ps vs t2)
-  | Const (@{const_name Not}, _) $ t' => Proc.Not (qf_of_term ps vs t')
-  | Const ("Ex", _) $ Abs (xn, xT, p) =>
-     let val (xn',p') = variant_abs (xn,xT,p)
-         val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
-     in Proc.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' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
-     in Proc.A (qf_of_term ps vs' p')
-     end
-  | _ =>(case AList.lookup (op aconv) ps t of
-           NONE => raise COOPER "reification: unknown term"
-         | SOME n => Proc.Closed n);
+fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
+  | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
+  | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
+      Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
+      Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
+      Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
+      Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
+      Proc.Not (fm_of_term ps vs t')
+  | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
+      Proc.E (uncurry (fm_of_term ps) (descend vs abs))
+  | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
+      Proc.A (uncurry (fm_of_term ps) (descend vs abs))
+  | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
+      Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+  | fm_of_term ps vs (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
+      Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+  | fm_of_term ps vs (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
+      Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+  | fm_of_term ps vs (Const (@{const_name Rings.dvd}, _) $ t1 $ t2) =
+     (case perhaps_number t1
+       of SOME n => Proc.Dvd (n, num_of_term vs t2)
+        | NONE => raise COOPER "reification: unsupported dvd")
+  | fm_of_term ps vs t =
+     (case AList.lookup (op aconv) ps t
+       of SOME n => Proc.Closed n
+        | NONE => raise COOPER "reification: unknown term");
 
-fun term_of_i vs t = case t
- of Proc.C i => HOLogic.mk_number HOLogic.intT i
-  | Proc.Bound n => Free (the (AList.lookup (op =) vs n))
-  | Proc.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
-  | Proc.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
-  | Proc.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
-  | Proc.Mul (i, t2) => @{term "op * :: int => _"} $
-      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
-  | Proc.Cn (n, i, t') => term_of_i vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
+fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i
+  | term_of_num vs (Proc.Bound n) = Free (the (AList.lookup (op =) vs n))
+  | term_of_num vs (Proc.Neg t') =
+      @{term "uminus :: int => _"} $ term_of_num vs t'
+  | term_of_num vs (Proc.Add (t1, t2)) =
+      @{term "op + :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
+  | term_of_num vs (Proc.Sub (t1, t2)) =
+      @{term "op - :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
+  | term_of_num vs (Proc.Mul (i, t2)) =
+      @{term "op * :: int => _"} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t2
+  | term_of_num vs (Proc.Cn (n, i, t')) =
+      term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
 
-fun term_of_qf ps vs t =
- case t of
-   Proc.T => HOLogic.true_const
- | Proc.F => HOLogic.false_const
- | Proc.Lt t' => @{term "op < :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
- | Proc.Le t' => @{term "op <= :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
- | Proc.Gt t' => @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
- | Proc.Ge t' => @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
- | Proc.Eq t' => @{term "op = :: int => _ "} $ term_of_i vs t'$ @{term "0::int"}
- | Proc.NEq t' => term_of_qf ps vs (Proc.Not (Proc.Eq t'))
- | Proc.Dvd (i, t') => @{term "op dvd :: int => _ "} $
-    HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
- | Proc.NDvd (i, t')=> term_of_qf ps vs (Proc.Not (Proc.Dvd (i, t')))
- | Proc.Not t' => HOLogic.Not $ term_of_qf ps vs t'
- | Proc.And (t1, t2) => HOLogic.conj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Proc.Or (t1, t2) => HOLogic.disj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Proc.Imp (t1, t2) => HOLogic.imp $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Proc.Iff (t1, t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Proc.Closed n => the (AList.lookup (op =) ps n)
- | Proc.NClosed n => term_of_qf ps vs (Proc.Not (Proc.Closed n));
+fun term_of_fm ps vs Proc.T = HOLogic.true_const
+  | term_of_fm ps vs Proc.F = HOLogic.false_const
+  | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (Proc.Iff (t1, t2)) = @{term "op = :: bool => _"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
+  | term_of_fm ps vs (Proc.Eq t') = @{term "op = :: int => _ "} $ term_of_num vs t'$ @{term "0::int"}
+  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
+  | term_of_fm ps vs (Proc.Lt t') = @{term "op < :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
+  | term_of_fm ps vs (Proc.Le t') = @{term "op <= :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
+  | term_of_fm ps vs (Proc.Gt t') = @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
+  | term_of_fm ps vs (Proc.Ge t') = @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
+  | term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $
+      HOLogic.mk_number HOLogic.intT i $ term_of_num vs t'
+  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
+  | term_of_fm ps vs (Proc.Closed n) = the (AList.lookup (op =) ps n)
+  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
 
 fun invoke t =
   let
@@ -664,7 +679,7 @@
     val ps = map_index swap (add_bools t []);
   in
     Logic.mk_equals (HOLogic.mk_Trueprop t,
-      HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Proc.pa (qf_of_term ps vs t))))
+      HOLogic.mk_Trueprop (term_of_fm (map swap ps) (map swap vs) (Proc.pa (fm_of_term ps vs t))))
   end;
 
 end;