50 val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * eval_fn; |
50 val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * eval_fn; |
51 val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * eval_fn; |
51 val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * eval_fn; |
52 |
52 |
53 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t); |
53 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t); |
54 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
54 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
55 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t; |
55 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
56 if term2str t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
56 if term2str t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
57 |
57 |
58 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); |
58 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); |
59 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; |
59 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; |
60 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t; |
60 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
61 if term2str t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed"; |
61 if term2str t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed"; |
62 |
62 |
63 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); |
63 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); |
64 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
64 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
65 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t; |
65 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
66 if term2str t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed"; |
66 if term2str t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed"; |
67 |
67 |
68 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); |
68 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); |
69 val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; |
69 val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; |
70 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t; |
70 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
71 if term2str t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; |
71 if term2str t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; |
72 |
72 |
73 "----------- calculate from Prog --------------------------------- -----------------------------"; |
73 "----------- calculate from Prog --------------------------------- -----------------------------"; |
74 "----------- calculate from Prog --------------------------------- -----------------------------"; |
74 "----------- calculate from Prog --------------------------------- -----------------------------"; |
75 "----------- calculate from Prog --------------------------------- -----------------------------"; |
75 "----------- calculate from Prog --------------------------------- -----------------------------"; |