54 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn; |
54 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn; |
55 val pow = (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn; |
55 val pow = (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn; |
56 |
56 |
57 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); |
57 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); |
58 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
58 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
59 val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
59 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
60 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
60 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
61 |
61 |
62 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); |
62 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); |
63 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; |
63 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; |
64 val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
64 val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
65 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed"; |
65 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed"; |
66 |
66 |
67 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); |
67 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); |
68 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
68 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
69 val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
69 val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
70 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed"; |
70 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed"; |
71 |
71 |
72 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); |
72 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); |
73 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; |
73 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; |
74 val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
74 val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; |
75 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; |
75 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; |
76 |
76 |
77 "----------- calculate from Prog --------------------------------- -----------------------------"; |
77 "----------- calculate from Prog --------------------------------- -----------------------------"; |
78 "----------- calculate from Prog --------------------------------- -----------------------------"; |
78 "----------- calculate from Prog --------------------------------- -----------------------------"; |
79 "----------- calculate from Prog --------------------------------- -----------------------------"; |
79 "----------- calculate from Prog --------------------------------- -----------------------------"; |