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)