31 | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2) |
31 | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2) |
32 | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2) |
32 | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2) |
33 | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i => |
33 | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i => |
34 Mul (i,num_of_term vs t2) |
34 Mul (i,num_of_term vs t2) |
35 | _ => error "num_of_term: unsupported Multiplication") |
35 | _ => error "num_of_term: unsupported Multiplication") |
36 | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
36 | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
37 | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
37 | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
38 | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t)); |
38 | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t)); |
39 |
39 |
40 (* pseudo reification : term -> fm *) |
40 (* pseudo reification : term -> fm *) |
41 fun fm_of_term vs t = |
41 fun fm_of_term vs t = |
42 case t of |
42 case t of |