2 theory scrtools |
2 theory scrtools |
3 imports Isac.Build_Thydata |
3 imports Isac.Build_Thydata |
4 begin |
4 begin |
5 |
5 |
6 subsection \<open> Compare with scrtools.sml: "--- test auto-generated script" \<close> |
6 subsection \<open> Compare with scrtools.sml: "--- test auto-generated script" \<close> |
|
7 |
|
8 partial_function (tailrec) stepwise_test :: "real => real" |
|
9 where |
|
10 "stepwise_test t_t = |
|
11 (Try (Rewrite_Set ''discard_minus'' False) @@ |
|
12 Try (Rewrite_Set ''expand_poly'' False) @@ |
|
13 Try (Repeat (Calculate ''TIMES'')) @@ |
|
14 Try (Rewrite_Set ''order_mult_rls'' False) @@ |
|
15 Try (Rewrite_Set ''simplify_power'' False) @@ |
|
16 Try (Rewrite_Set ''calc_add_mult_pow'' False) @@ |
|
17 Try (Rewrite_Set ''reduce_012_mult'' False) @@ |
|
18 Try (Rewrite_Set ''order_add_rls'' False) @@ |
|
19 Try (Rewrite_Set ''collect_numerals'' False) @@ |
|
20 Try (Rewrite_Set ''reduce_012'' False) @@ |
|
21 Try (Rewrite_Set ''discard_parentheses'' False)) |
|
22 t_t" |
7 setup \<open>KEStore_Elems.add_mets |
23 setup \<open>KEStore_Elems.add_mets |
8 [Specify.prep_met @{theory "Test"} "met_testinter" [] Celem.e_metID |
24 [Specify.prep_met @{theory "Test"} "met_testinter" [] Celem.e_metID |
9 (["Test","test_interSteps_1"], |
25 (["Test","test_interSteps_1"], |
10 [("#Given" ,["Term t_t"]), ("#Find" ,["normalform n_n"])], |
26 [("#Given" ,["Term t_t"]), ("#Find" ,["normalform n_n"])], |
11 {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
27 {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
12 crls=tval_rls, errpats = [], nrls = Rule.e_rls}, |
28 crls=tval_rls, errpats = [], nrls = Rule.e_rls}, |
13 "Script Stepwise t_t = \ |
29 @{thm stepwise_test.simps} |
|
30 (*"Script Stepwise t_t = \ |
14 \(Try (Rewrite_Set ''discard_minus'' False) @@ \ |
31 \(Try (Rewrite_Set ''discard_minus'' False) @@ \ |
15 \ Try (Rewrite_Set ''expand_poly'' False) @@ \ |
32 \ Try (Rewrite_Set ''expand_poly'' False) @@ \ |
16 \ Try (Repeat (Calculate ''TIMES'')) @@ \ |
33 \ Try (Repeat (Calculate ''TIMES'')) @@ \ |
17 \ Try (Rewrite_Set ''order_mult_rls'' False) @@ \ |
34 \ Try (Rewrite_Set ''order_mult_rls'' False) @@ \ |
18 \ Try (Rewrite_Set ''simplify_power'' False) @@ \ |
35 \ Try (Rewrite_Set ''simplify_power'' False) @@ \ |
20 \ Try (Rewrite_Set ''reduce_012_mult'' False) @@ \ |
37 \ Try (Rewrite_Set ''reduce_012_mult'' False) @@ \ |
21 \ Try (Rewrite_Set ''order_add_rls'' False) @@ \ |
38 \ Try (Rewrite_Set ''order_add_rls'' False) @@ \ |
22 \ Try (Rewrite_Set ''collect_numerals'' False) @@ \ |
39 \ Try (Rewrite_Set ''collect_numerals'' False) @@ \ |
23 \ Try (Rewrite_Set ''reduce_012'' False) @@ \ |
40 \ Try (Rewrite_Set ''reduce_012'' False) @@ \ |
24 \ Try (Rewrite_Set ''discard_parentheses'' False)) \ |
41 \ Try (Rewrite_Set ''discard_parentheses'' False)) \ |
25 \ t_t" |
42 \ t_t"*) |
26 (*presently this script cannot become equal in types to auto_script, because: |
43 (*presently this script cannot become equal in types to auto_script, because: |
27 this t_t must be either 'real' or 'bool' #1#, |
44 this t_t must be either 'real' or 'bool' #1#, |
28 while the auto_script must be 'z and type-instantiated before usage*))] |
45 while the auto_script must be 'z and type-instantiated before usage*))] |
29 \<close> |
46 \<close> |
30 text \<open> see scrtools.sml "--- test auto-generated script" \<close> |
47 text \<open> see scrtools.sml "--- test auto-generated script" \<close> |