47 |
47 |
48 val one_to_of_int_one_simproc = |
48 val one_to_of_int_one_simproc = |
49 make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc", |
49 make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc", |
50 proc = proc1, identifier = []}; |
50 proc = proc1, identifier = []}; |
51 |
51 |
52 fun check (Const (@{const_name HOL.one}, @{typ int})) = false |
52 fun check (Const (@{const_name Algebras.one}, @{typ int})) = false |
53 | check (Const (@{const_name HOL.one}, _)) = true |
53 | check (Const (@{const_name Algebras.one}, _)) = true |
54 | check (Const (s, _)) = member (op =) [@{const_name "op ="}, |
54 | check (Const (s, _)) = member (op =) [@{const_name "op ="}, |
55 @{const_name HOL.times}, @{const_name HOL.uminus}, |
55 @{const_name Algebras.times}, @{const_name Algebras.uminus}, |
56 @{const_name HOL.minus}, @{const_name HOL.plus}, |
56 @{const_name Algebras.minus}, @{const_name Algebras.plus}, |
57 @{const_name HOL.zero}, |
57 @{const_name Algebras.zero}, |
58 @{const_name HOL.less}, @{const_name HOL.less_eq}] s |
58 @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s |
59 | check (a $ b) = check a andalso check b |
59 | check (a $ b) = check a andalso check b |
60 | check _ = false; |
60 | check _ = false; |
61 |
61 |
62 val conv = |
62 val conv = |
63 Simplifier.rewrite |
63 Simplifier.rewrite |