12 "-----------------------------------------------------------------------------------------------"; |
12 "-----------------------------------------------------------------------------------------------"; |
13 |
13 |
14 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
14 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
15 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
15 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
16 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
16 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
17 val (t1, t2) = (@{term 3}, @{term "2::real"}); |
|
18 val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2); |
|
19 |
17 |
20 eval_binop "" "" t ""; |
18 fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t))); |
21 "~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *) |
|
22 ((), (), t, ()); |
|
23 (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*); |
|
24 val res = calcul op0 (t1, t2); |
|
25 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); |
|
26 (*in*) |
|
27 val xxx = SOME ("#: " ^ UnparseC.term prop, prop); |
|
28 (*end*) |
|
29 |
19 |
30 case xxx of |
20 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>; |
31 SOME |
21 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>; |
32 ("#: (3::'a) + 2 = (5::'a)", |
22 test \<^theory> \<^term>\<open>10 * 20 :: real\<close>; |
33 Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
23 test \<^theory> \<^term>\<open>10 powr 20 :: real\<close>; |
34 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
24 |
35 (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ _ $ |
25 test \<^theory> \<^term>\<open>10 + 20 :: int\<close>; |
36 (Const (\<^const_name>\<open>numeral\<close>, _) $ _ )) $ |
26 test \<^theory> \<^term>\<open>10 - 20 :: int\<close>; |
37 _ )) => () |
27 test \<^theory> \<^term>\<open>10 * 20 :: int\<close>; |
38 | _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED" |
28 |
|
29 test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>; |
|
30 test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>; |
|
31 test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>; |