1 (* Title: ~~test/../Interpret/ptyps.thy
6 imports Isac.Build_Isac
10 *setup* KEStore_Elems.add_pbts is impossible in *.sml files.
11 The respective test/../ptyps.sml is called in Test_Isac.thy.
14 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
15 setup \<open>KEStore_Elems.add_pbts
16 [(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
17 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
18 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
19 (["pbla", "refine", "test"],
20 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
21 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
22 (["pbla1","pbla", "refine", "test"],
23 [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
24 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
25 (["pbla2","pbla", "refine", "test"],
26 [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
27 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
28 (["pbla2x","pbla2","pbla", "refine", "test"],
29 [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
30 Rule_Set.empty, NONE, [])),
31 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
32 (["pbla2y","pbla2","pbla", "refine", "test"],
33 [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
34 Rule_Set.empty, NONE, [])),
35 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
36 (["pbla2z","pbla2","pbla", "refine", "test"],
37 [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
38 Rule_Set.empty, NONE, [])),
39 (Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
40 (["pbla3","pbla", "refine", "test"],
41 [("#Given" ,["fixedValues a_a","relations a_3"])],
42 Rule_Set.empty, NONE, []))]
45 (*ML_file "ptyps.sml" ... is called in Test_Isac.thy *)