63 (*abstraction of a numeric literal*) |
63 (*abstraction of a numeric literal*) |
64 fun lit t = if can HOLogic.dest_number t then t else replace t; |
64 fun lit t = if can HOLogic.dest_number t then t else replace t; |
65 (*abstraction of a real/rational expression*) |
65 (*abstraction of a real/rational expression*) |
66 fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
66 fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
67 | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
67 | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
68 | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
68 | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
69 | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
69 | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) |
70 | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x) |
70 | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x) |
71 | rat t = lit t |
71 | rat t = lit t |
72 (*abstraction of an integer expression: no div, mod*) |
72 (*abstraction of an integer expression: no div, mod*) |
73 fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y) |
73 fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y) |