18 (*-------------------------from InsSort.thy 8.3.01----------------------*) |
18 (*-------------------------from InsSort.thy 8.3.01----------------------*) |
19 |
19 |
20 |
20 |
21 (*-------------------------from InsSort.ML 8.3.01----------------------*) |
21 (*-------------------------from InsSort.ML 8.3.01----------------------*) |
22 |
22 |
23 theory' := (!theory') @ [("InsSort.thy",InsSort.thy)]; |
23 theory' := (!theory') @ [("InsSort",InsSort.thy)]; |
24 |
24 |
25 val ins_sort = |
25 val ins_sort = |
26 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
26 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
27 rules = [Thm ("foldr_base",(*num_str*) foldr_base), |
27 rules = [Thm ("foldr_base",(*num_str*) foldr_base), |
28 Thm ("foldr_rec",foldr_rec), |
28 Thm ("foldr_rec",foldr_rec), |
40 |
40 |
41 |
41 |
42 |
42 |
43 |
43 |
44 (* |
44 (* |
45 > get_pbt ["Script.thy","squareroot","univariate","equation"]; |
45 > get_pbt ["Script","squareroot","univariate","equation"]; |
46 > get_met ("Script.thy","max_on_interval_by_calculus"); |
46 > get_met ("Script","max_on_interval_by_calculus"); |
47 *) |
47 *) |
48 pbltypes:= (!pbltypes) @ |
48 pbltypes:= (!pbltypes) @ |
49 [ |
49 [ |
50 prep_pbt InsSort.thy |
50 prep_pbt InsSort.thy |
51 (["InsSort.thy","inssort"]:pblID, |
51 (["InsSort","inssort"]:pblID, |
52 [("#Given" ,"unsorted u_"), |
52 [("#Given" ,"unsorted u_"), |
53 ("#Find" ,"sorted s_") |
53 ("#Find" ,"sorted s_") |
54 ]) |
54 ]) |
55 ]; |
55 ]; |
56 |
56 |
57 methods:= (!methods) @ |
57 methods:= (!methods) @ |
58 [ |
58 [ |
59 (*, -------17.6.00, |
59 (*, -------17.6.00, |
60 (("InsSort.thy","inssort"):metID, |
60 (("InsSort","inssort"):metID, |
61 {ppc = prep_met |
61 {ppc = prep_met |
62 [("#Given" ,"unsorted u_"), |
62 [("#Given" ,"unsorted u_"), |
63 ("#Find" ,"sorted s_") |
63 ("#Find" ,"sorted s_") |
64 ], |
64 ], |
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
66 scr=Script (((inst_abs (assoc_thm "InsSort.thy")) |
66 scr=Script (((inst_abs (assoc_thm "InsSort")) |
67 o term_of o the o (parse thy)) (*for [#1,#3,#2] only*) |
67 o term_of o the o (parse thy)) (*for [#1,#3,#2] only*) |
68 "Script Ins_sort (u_::'a list) = \ |
68 "Script Ins_sort (u_::'a list) = \ |
69 \ (let u_ = Rewrite sort_def False u_; \ |
69 \ (let u_ = Rewrite sort_def False u_; \ |
70 \ u_ = Rewrite foldr_rec False u_; \ |
70 \ u_ = Rewrite foldr_rec False u_; \ |
71 \ u_ = Rewrite ins_base False u_; \ |
71 \ u_ = Rewrite ins_base False u_; \ |
83 \ u_ = Rewrite if_False False u_; \ |
83 \ u_ = Rewrite if_False False u_; \ |
84 \ u_ = Rewrite foldr_base False u_ \ |
84 \ u_ = Rewrite foldr_base False u_ \ |
85 \ in u_)") |
85 \ in u_)") |
86 } : met), |
86 } : met), |
87 |
87 |
88 (("InsSort.thy","sort"):metID, |
88 (("InsSort","sort"):metID, |
89 {ppc = prep_met |
89 {ppc = prep_met |
90 [("#Given" ,"unsorted u_"), |
90 [("#Given" ,"unsorted u_"), |
91 ("#Find" ,"sorted s_") |
91 ("#Find" ,"sorted s_") |
92 ], |
92 ], |
93 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
93 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |