5843 @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
5843 @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
5844 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = |
5844 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = |
5845 @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
5845 @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
5846 | fm_of_term vs (@{term "Not"} $ t') = |
5846 | fm_of_term vs (@{term "Not"} $ t') = |
5847 @{code NOT} (fm_of_term vs t') |
5847 @{code NOT} (fm_of_term vs t') |
5848 | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) = |
5848 | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) = |
5849 @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
5849 @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
5850 | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) = |
5850 | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) = |
5851 @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
5851 @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
5852 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
5852 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
5853 |
5853 |
5854 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
5854 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
5855 | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) |
5855 | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) |