src/HOL/ex/coopereif.ML
changeset 24000 467e77e4e276
parent 23996 306aba3e5118
child 24423 ae9cd0e92423
equal deleted inserted replaced
23999:393dd64d0d04 24000:467e77e4e276
    90   | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
    90   | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
    91   | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
    91   | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
    92       term_of_i vs t1 $ term_of_i vs t2
    92       term_of_i vs t1 $ term_of_i vs t2
    93   | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
    93   | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
    94       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
    94       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
    95   | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound (nat n)), t'));
    95   | Cn (n,i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
    96 
    96 
    97 fun term_of_qf ps vs t = case t
    97 fun term_of_qf ps vs t = case t
    98  of T => HOLogic.true_const 
    98  of T => HOLogic.true_const 
    99   | F => HOLogic.false_const
    99   | F => HOLogic.false_const
   100   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   100   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}