src/HOL/ex/SVC_Oracle.thy
 changeset 34974 18b41bba42b5 parent 32740 9dd0a2f83429 child 35084 e25eedfc15ce
```     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:43 2010 +0100
1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:49 2010 +0100
1.3 @@ -63,21 +63,21 @@
1.4      (*abstraction of a numeric literal*)
1.5      fun lit t = if can HOLogic.dest_number t then t else replace t;
1.6      (*abstraction of a real/rational expression*)
1.7 -    fun rat ((c as Const(@{const_name HOL.plus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.8 -      | rat ((c as Const(@{const_name HOL.minus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.9 -      | rat ((c as Const(@{const_name HOL.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.10 -      | rat ((c as Const(@{const_name HOL.times}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.11 -      | rat ((c as Const(@{const_name HOL.uminus}, _)) \$ x) = c \$ (rat x)
1.12 +    fun rat ((c as Const(@{const_name Algebras.plus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.13 +      | rat ((c as Const(@{const_name Algebras.minus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.14 +      | rat ((c as Const(@{const_name Algebras.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.15 +      | rat ((c as Const(@{const_name Algebras.times}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
1.16 +      | rat ((c as Const(@{const_name Algebras.uminus}, _)) \$ x) = c \$ (rat x)
1.17        | rat t = lit t
1.18      (*abstraction of an integer expression: no div, mod*)
1.19 -    fun int ((c as Const(@{const_name HOL.plus}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.20 -      | int ((c as Const(@{const_name HOL.minus}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.21 -      | int ((c as Const(@{const_name HOL.times}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.22 -      | int ((c as Const(@{const_name HOL.uminus}, _)) \$ x) = c \$ (int x)
1.23 +    fun int ((c as Const(@{const_name Algebras.plus}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.24 +      | int ((c as Const(@{const_name Algebras.minus}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.25 +      | int ((c as Const(@{const_name Algebras.times}, _)) \$ x \$ y) = c \$ (int x) \$ (int y)
1.26 +      | int ((c as Const(@{const_name Algebras.uminus}, _)) \$ x) = c \$ (int x)
1.27        | int t = lit t
1.28      (*abstraction of a natural number expression: no minus*)
1.29 -    fun nat ((c as Const(@{const_name HOL.plus}, _)) \$ x \$ y) = c \$ (nat x) \$ (nat y)
1.30 -      | nat ((c as Const(@{const_name HOL.times}, _)) \$ x \$ y) = c \$ (nat x) \$ (nat y)
1.31 +    fun nat ((c as Const(@{const_name Algebras.plus}, _)) \$ x \$ y) = c \$ (nat x) \$ (nat y)
1.32 +      | nat ((c as Const(@{const_name Algebras.times}, _)) \$ x \$ y) = c \$ (nat x) \$ (nat y)
1.33        | nat ((c as Const(@{const_name Suc}, _)) \$ x) = c \$ (nat x)
1.34        | nat t = lit t
1.35      (*abstraction of a relation: =, <, <=*)
1.36 @@ -95,8 +95,8 @@
1.37        | fm ((c as Const("True", _))) = c
1.38        | fm ((c as Const("False", _))) = c
1.39        | fm (t as Const("op =",  Type ("fun", [T,_])) \$ _ \$ _) = rel (T, t)
1.40 -      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) \$ _ \$ _) = rel (T, t)
1.41 -      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) \$ _ \$ _) = rel (T, t)
1.42 +      | fm (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) \$ _ \$ _) = rel (T, t)
1.43 +      | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) \$ _ \$ _) = rel (T, t)
1.44        | fm t = replace t
1.45      (*entry point, and abstraction of a meta-formula*)
1.46      fun mt ((c as Const("Trueprop", _)) \$ p) = c \$ (fm p)
```