src/HOL/Tools/Qelim/cooper.ML
changeset 23713 db10cf19f1f8
parent 23689 0410269099dc
child 23881 851c74f1bb69
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 10 17:30:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 10 17:30:54 2007 +0200
     1.3 @@ -535,55 +535,53 @@
     1.4  structure Coopereif =
     1.5  struct
     1.6  
     1.7 -open GeneratedCooper.Reflected_Presburger;
     1.8 +open GeneratedCooper;
     1.9 +
    1.10 +fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
    1.11 +fun i_of_term vs t = case t
    1.12 + of Free (xn, xT) => (case AList.lookup (op aconv) vs t
    1.13 +     of NONE   => cooper "Variable not found in the list!"
    1.14 +      | SOME n => Bound n)
    1.15 +  | @{term "0::int"} => C 0
    1.16 +  | @{term "1::int"} => C 1
    1.17 +  | Term.Bound i => Bound (Integer.int i)
    1.18 +  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
    1.19 +  | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    1.20 +  | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
    1.21 +  | Const(@{const_name HOL.times},_)$t1$t2 => 
    1.22 +     (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
    1.23 +    handle TERM _ => 
    1.24 +       (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
    1.25 +        handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
    1.26 +  | _ => (C (HOLogic.dest_number t |> snd) 
    1.27 +           handle TERM _ => cooper "Reification: unknown term");
    1.28  
    1.29 -fun cooper s = raise Cooper.COOPER ("Cooper Oracle Failed", ERROR s);
    1.30 -fun i_of_term vs t = 
    1.31 -    case t of
    1.32 -	Free(xn,xT) => (case AList.lookup (op aconv) vs t of 
    1.33 -			   NONE   => cooper "Variable not found in the list!!"
    1.34 -			 | SOME n => Bound n)
    1.35 -      | @{term "0::int"} => C 0
    1.36 -      | @{term "1::int"} => C 1
    1.37 -      | Term.Bound i => Bound i
    1.38 -      | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
    1.39 -      | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
    1.40 -      | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
    1.41 -      | Const(@{const_name "HOL.times"},_)$t1$t2 => 
    1.42 -	     (Mul (HOLogic.dest_number t1 |> snd |> Integer.machine_int,i_of_term vs t2)
    1.43 -        handle TERM _ => 
    1.44 -           (Mul (HOLogic.dest_number t2 |> snd |> Integer.machine_int,i_of_term vs t1)
    1.45 -            handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
    1.46 -      | _ => (C (HOLogic.dest_number t |> snd |> Integer.machine_int) 
    1.47 -               handle TERM _ => cooper "Reification: unknown term");
    1.48 -	
    1.49 -fun qf_of_term ps vs t = 
    1.50 -    case t of 
    1.51 -	Const("True",_) => T
    1.52 -      | Const("False",_) => F
    1.53 -      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    1.54 -      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    1.55 -      | Const(@{const_name Divides.dvd},_)$t1$t2 => 
    1.56 -	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
    1.57 -      | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    1.58 -      | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.59 -      | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.60 -      | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.61 -      | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.62 -      | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
    1.63 -      | Const("Ex",_)$Abs(xn,xT,p) => 
    1.64 -         let val (xn',p') = variant_abs (xn,xT,p)
    1.65 -             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.66 -         in E (qf_of_term ps vs' p')
    1.67 -         end
    1.68 -      | Const("All",_)$Abs(xn,xT,p) => 
    1.69 -         let val (xn',p') = variant_abs (xn,xT,p)
    1.70 -             val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.71 -         in A (qf_of_term ps vs' p')
    1.72 -         end
    1.73 -      | _ =>(case AList.lookup (op aconv) ps t of 
    1.74 -               NONE => cooper "Reification: unknown term!"
    1.75 -             | SOME n => Closed n);
    1.76 +fun qf_of_term ps vs t =  case t
    1.77 + of Const("True",_) => T
    1.78 +  | Const("False",_) => F
    1.79 +  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    1.80 +  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    1.81 +  | Const(@{const_name Divides.dvd},_)$t1$t2 => 
    1.82 +      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
    1.83 +  | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    1.84 +  | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.85 +  | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.86 +  | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.87 +  | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.88 +  | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
    1.89 +  | Const("Ex",_)$Abs(xn,xT,p) => 
    1.90 +     let val (xn',p') = variant_abs (xn,xT,p)
    1.91 +         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.92 +     in E (qf_of_term ps vs' p')
    1.93 +     end
    1.94 +  | Const("All",_)$Abs(xn,xT,p) => 
    1.95 +     let val (xn',p') = variant_abs (xn,xT,p)
    1.96 +         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.97 +     in A (qf_of_term ps vs' p')
    1.98 +     end
    1.99 +  | _ =>(case AList.lookup (op aconv) ps t of 
   1.100 +           NONE => cooper "Reification: unknown term!"
   1.101 +         | SOME n => Closed n);
   1.102  
   1.103  local
   1.104   val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   1.105 @@ -602,33 +600,21 @@
   1.106    | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
   1.107  end;
   1.108   
   1.109 -
   1.110 -fun start_vs t =
   1.111 -let
   1.112 - val fs = term_frees t
   1.113 - val ps = term_bools [] t
   1.114 -in (fs ~~ (0 upto  (length fs - 1)), ps ~~ (0 upto  (length ps - 1)))
   1.115 -end ;
   1.116 -
   1.117 -val iT = HOLogic.intT;
   1.118 -val bT = HOLogic.boolT;
   1.119  fun myassoc2 l v =
   1.120      case l of
   1.121  	[] => NONE
   1.122        | (x,v')::xs => if v = v' then SOME x
   1.123  		      else myassoc2 xs v;
   1.124  
   1.125 -fun term_of_i vs t =
   1.126 -    case t of 
   1.127 -	C i => HOLogic.mk_number HOLogic.intT (Integer.int i)
   1.128 -      | Bound n => valOf (myassoc2 vs n)
   1.129 -      | Neg t' => @{term "uminus :: int => _"}$(term_of_i vs t')
   1.130 -      | Add(t1,t2) => @{term "op +:: int => _"}$ (term_of_i vs t1)$(term_of_i vs t2)
   1.131 -      | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[iT,iT] ---> iT)$
   1.132 -			   (term_of_i vs t1)$(term_of_i vs t2)
   1.133 -      | Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$
   1.134 -			   (HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t2)
   1.135 -      | Cx(i,t')=> term_of_i vs (Add(Mul (i, Bound 0),t'));
   1.136 +fun term_of_i vs t = case t
   1.137 + of C i => HOLogic.mk_number HOLogic.intT i
   1.138 +  | Bound n => the (myassoc2 vs n)
   1.139 +  | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   1.140 +  | Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.141 +  | Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.142 +  | Mul (i, t2) => @{term "op * :: int => _"} $
   1.143 +      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   1.144 +  | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound 0), t'));
   1.145  
   1.146  fun term_of_qf ps vs t = 
   1.147   case t of 
   1.148 @@ -639,24 +625,26 @@
   1.149   | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   1.150   | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   1.151   | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   1.152 - | NEq t' => term_of_qf ps vs (Nota(Eq t'))
   1.153 - | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
   1.154 -                 (HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t')
   1.155 + | NEq t' => term_of_qf ps vs (Nota (Eq t'))
   1.156 + | Dvd(i,t') => @{term "op dvd :: int => _ "} $ 
   1.157 +    HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
   1.158   | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
   1.159   | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
   1.160   | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.161   | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.162   | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.163 - | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2)
   1.164 - | Closed n => valOf (myassoc2 ps n)
   1.165 + | Iffa(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.166 + | Closed n => the (myassoc2 ps n)
   1.167   | NClosed n => term_of_qf ps vs (Nota (Closed n))
   1.168   | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   1.169  
   1.170 -(* The oracle *)
   1.171  fun cooper_oracle thy t = 
   1.172 -    let val (vs,ps) = start_vs t
   1.173 -    in (equals propT) $ (HOLogic.mk_Trueprop t) $ 
   1.174 -            (HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
   1.175 -    end;
   1.176 +  let
   1.177 +    val (vs, ps) = pairself (map_index (swap o apfst Integer.int))
   1.178 +      (term_frees t, term_bools [] t);
   1.179 +  in
   1.180 +    equals propT $ HOLogic.mk_Trueprop t $
   1.181 +      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
   1.182 +  end;
   1.183  
   1.184  end;