--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Jan 05 17:24:33 2019 +0100
@@ -2466,76 +2466,76 @@
val mk_Bound = @{code Bound} o @{code nat_of_integer};
fun num_of_term vs (Free vT) = mk_Bound (find_index (fn vT' => vT = vT') vs)
- | num_of_term vs @{term "real_of_int (0::int)"} = mk_C 0
- | num_of_term vs @{term "real_of_int (1::int)"} = mk_C 1
- | num_of_term vs @{term "0::real"} = mk_C 0
- | num_of_term vs @{term "1::real"} = mk_C 1
+ | num_of_term vs \<^term>\<open>real_of_int (0::int)\<close> = mk_C 0
+ | num_of_term vs \<^term>\<open>real_of_int (1::int)\<close> = mk_C 1
+ | num_of_term vs \<^term>\<open>0::real\<close> = mk_C 0
+ | num_of_term vs \<^term>\<open>1::real\<close> = mk_C 1
| num_of_term vs (Bound i) = mk_Bound i
- | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
- | num_of_term vs (@{term "(+) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ | num_of_term vs (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ t') = @{code Neg} (num_of_term vs t')
+ | num_of_term vs (\<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
@{code Add} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+ | num_of_term vs (\<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
+ | num_of_term vs (\<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) = (case num_of_term vs t1
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported multiplication")
- | num_of_term vs (@{term "real_of_int :: int \<Rightarrow> real"} $ t') =
+ | num_of_term vs (\<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $ t') =
(mk_C (snd (HOLogic.dest_number t'))
handle TERM _ => error ("num_of_term: unknown term"))
| num_of_term vs t' =
(mk_C (snd (HOLogic.dest_number t'))
handle TERM _ => error ("num_of_term: unknown term"));
-fun fm_of_term vs @{term True} = @{code T}
- | fm_of_term vs @{term False} = @{code F}
- | fm_of_term vs (@{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+fun fm_of_term vs \<^term>\<open>True\<close> = @{code T}
+ | fm_of_term vs \<^term>\<open>False\<close> = @{code F}
+ | fm_of_term vs (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
@{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ | fm_of_term vs (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
@{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "(=) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
+ | fm_of_term vs (\<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (@{term "(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
+ | fm_of_term vs (\<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (\<^term>\<open>Not\<close> $ t') = @{code NOT} (fm_of_term vs t')
+ | fm_of_term vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
+ | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
-fun term_of_num vs (@{code C} i) = @{term "real_of_int :: int \<Rightarrow> real"} $
+fun term_of_num vs (@{code C} i) = \<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $
HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
| term_of_num vs (@{code Bound} n) = Free (nth vs (@{code integer_of_nat} n))
- | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} $ term_of_num vs t'
- | term_of_num vs (@{code Add} (t1, t2)) = @{term "(+) :: real \<Rightarrow> real \<Rightarrow> real"} $
+ | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ term_of_num vs t'
+ | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
+ | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
+ | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm vs @{code T} = @{term True}
- | term_of_fm vs @{code F} = @{term False}
- | term_of_fm vs (@{code Lt} t) = @{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} $
- term_of_num vs t $ @{term "0::real"}
- | term_of_fm vs (@{code Le} t) = @{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} $
- term_of_num vs t $ @{term "0::real"}
- | term_of_fm vs (@{code Gt} t) = @{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} $
- @{term "0::real"} $ term_of_num vs t
- | term_of_fm vs (@{code Ge} t) = @{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} $
- @{term "0::real"} $ term_of_num vs t
- | term_of_fm vs (@{code Eq} t) = @{term "(=) :: real \<Rightarrow> real \<Rightarrow> bool"} $
- term_of_num vs t $ @{term "0::real"}
+fun term_of_fm vs @{code T} = \<^term>\<open>True\<close>
+ | term_of_fm vs @{code F} = \<^term>\<open>False\<close>
+ | term_of_fm vs (@{code Lt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
+ term_of_num vs t $ \<^term>\<open>0::real\<close>
+ | term_of_fm vs (@{code Le} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
+ term_of_num vs t $ \<^term>\<open>0::real\<close>
+ | term_of_fm vs (@{code Gt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
+ \<^term>\<open>0::real\<close> $ term_of_num vs t
+ | term_of_fm vs (@{code Ge} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
+ \<^term>\<open>0::real\<close> $ term_of_num vs t
+ | term_of_fm vs (@{code Eq} t) = \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
+ term_of_num vs t $ \<^term>\<open>0::real\<close>
| term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t))
| term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t'
| term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $
+ | term_of_fm vs (@{code Iff} (t1, t2)) = \<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $
term_of_fm vs t1 $ term_of_fm vs t2;
in fn (ctxt, t) =>