1 (* Title: ~~test/../ProgLang/calculate.thy
6 imports Isac.Build_Thydata
10 *setup* KEStore_Elems.add_pbts / add_mets is impossible in *.sml files.
11 The respective test/../calculate.sml is called in Test_Isac.thy.
15 "-calculate.thy: provides 'setup' -----------------------";
16 "-calculate.thy: provides 'setup' -----------------------";
17 "-calculate.thy: provides 'setup' -----------------------";
20 setup \<open>KEStore_Elems.add_pbts
21 [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Celem.e_pblID (["test"], [], Rule_Set.empty, NONE, []),
22 Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Celem.e_pblID
23 (["calculate", "test"],
24 [("#Given", ["realTestGiven t_t"]),
25 ("#Find", ["realTestFind s_s"])],
26 Rule_Set.empty, NONE, [["Test", "test_calculate"]])]\<close>
28 partial_function (tailrec) calc_test :: "real \<Rightarrow> real"
32 ((Try (Repeat (Calculate ''PLUS''))) #>
33 (Try (Repeat (Calculate ''TIMES''))) #>
34 (Try (Repeat (Calculate ''DIVIDE''))) #>
35 (Try (Repeat (Calculate ''POWER''))))) t_t"
36 setup \<open>KEStore_Elems.add_mets
37 [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Celem.e_metID
38 (["Test","test_calculate"],
39 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
40 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
41 calc=[("PLUS", ("op +", eval_binop "#add_")),
42 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
43 ("DIVIDE", ("HOL.divide", Prog_Expr.eval_cancel "#divide_")),
44 ("POWER", ("Prog_Expr.pow", eval_binop "#power_"))],
45 crls=tval_rls, errpats = [], nrls= Rule_Set.empty (*, asm_rls=[],asm_thm=[]*)},
46 @{thm calc_test.simps})]