wneuper@59229
|
1 |
theory InsSort imports "../Interpret/Interpret" Rational(*for norm_Rational?!?*)
|
wneuper@59229
|
2 |
begin
|
neuper@37906
|
3 |
|
wneuper@59229
|
4 |
subsection {* consts *}
|
wneuper@59229
|
5 |
consts
|
wneuper@59235
|
6 |
unsorted :: "int xlist => unl"
|
wneuper@59235
|
7 |
sorted :: "int xlist => unl"
|
neuper@37906
|
8 |
|
wneuper@59229
|
9 |
(* subproblem and script-name *)
|
wneuper@59235
|
10 |
Ins'_sort :: "[int xlist,
|
wneuper@59235
|
11 |
int xlist] => int xlist"
|
neuper@37954
|
12 |
("((Script Ins'_sort (_ =))//
|
neuper@37954
|
13 |
(_))" 9)
|
wneuper@59235
|
14 |
Sortprog :: "[int xlist,
|
wneuper@59235
|
15 |
int xlist] => int xlist"
|
wneuper@59235
|
16 |
("((Script Sortprog (_ =))//
|
neuper@37954
|
17 |
(_))" 9)
|
neuper@37906
|
18 |
|
wneuper@59229
|
19 |
subsection {* functions *}
|
wneuper@59234
|
20 |
primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
|
wneuper@59229
|
21 |
where
|
wneuper@59234
|
22 |
ins_Nil: "ins i [|| ||] = [||i||]" |
|
wneuper@59234
|
23 |
ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"
|
neuper@37906
|
24 |
|
wneuper@59234
|
25 |
fun sort :: "int xlist \<Rightarrow> int xlist"
|
wneuper@59229
|
26 |
where
|
wneuper@59234
|
27 |
sort_deff: "sort xs = xfoldr ins xs [|| ||]"
|
wneuper@59233
|
28 |
print_theorems
|
wneuper@59233
|
29 |
thm sort_def (* InsSort.sort \<equiv> sort_sumC *)
|
wneuper@59233
|
30 |
thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
|
neuper@37906
|
31 |
|
wneuper@59229
|
32 |
(* access to definitions from ML *)
|
wneuper@59229
|
33 |
ML {*
|
wneuper@59231
|
34 |
@{thm ins.simps(1)};
|
wneuper@59231
|
35 |
@{thm ins.simps(2)};
|
wneuper@59229
|
36 |
*}
|
neuper@37906
|
37 |
|
wneuper@59234
|
38 |
value "sort [||2,3,1||]"
|
wneuper@59234
|
39 |
lemma test: "sort [||2,3,1||] = [||1,2,3||]"
|
wneuper@59229
|
40 |
by simp
|
neuper@37954
|
41 |
|
wneuper@59229
|
42 |
subsection {* eval functions *}
|
wneuper@59229
|
43 |
subsection {* rulesets *}
|
wneuper@59229
|
44 |
ML {*
|
wneuper@59229
|
45 |
val ins_sort =
|
wneuper@59229
|
46 |
Rls {
|
wneuper@59229
|
47 |
id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,
|
wneuper@59229
|
48 |
srls = e_rls, calc = [], rules = [
|
wneuper@59234
|
49 |
Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
|
wneuper@59234
|
50 |
Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
|
wneuper@59232
|
51 |
|
wneuper@59232
|
52 |
Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
|
wneuper@59232
|
53 |
Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
|
wneuper@59233
|
54 |
Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
|
wneuper@59232
|
55 |
|
wneuper@59232
|
56 |
Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
|
wneuper@59232
|
57 |
Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
|
wneuper@59232
|
58 |
Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
|
wneuper@59232
|
59 |
Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
|
wneuper@59229
|
60 |
|
wneuper@59229
|
61 |
Calc ("Orderings.ord_class.less", eval_equ "#less_"),
|
wneuper@59232
|
62 |
Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
|
wneuper@59232
|
63 |
Thm ("if_True", @{thm if_True} (* *)),
|
wneuper@59232
|
64 |
Thm ("if_False", @{thm if_False} (* *))],
|
wneuper@59229
|
65 |
errpatts = [], scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")};
|
s1210629013@55373
|
66 |
*}
|
neuper@52125
|
67 |
setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
|
neuper@37954
|
68 |
|
wneuper@59229
|
69 |
subsection {* problems *}
|
wneuper@59229
|
70 |
setup {* KEStore_Elems.add_pbts
|
wneuper@59229
|
71 |
[(prep_pbt @{theory} "pbl_Programming" [] e_pblID
|
wneuper@59229
|
72 |
(["Programming"], [], e_rls, NONE, [])),
|
wneuper@59229
|
73 |
(prep_pbt @{theory} "pbl_Prog_sort" [] e_pblID
|
wneuper@59229
|
74 |
(["sort","Programming"], [], e_rls, NONE, [])),
|
wneuper@59229
|
75 |
(prep_pbt @{theory} "pbl_Prog_sort_ins" [] e_pblID
|
wneuper@59229
|
76 |
(["insertion","sort","Programming"],
|
wneuper@59229
|
77 |
[("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
|
wneuper@59229
|
78 |
e_rls,
|
wneuper@59229
|
79 |
NONE, [])) ] *}
|
wneuper@59229
|
80 |
|
wneuper@59229
|
81 |
subsection {* CAS-commands *}
|
wneuper@59229
|
82 |
(** CAS-commands **)
|
wneuper@59229
|
83 |
subsection {* methods *}
|
wneuper@59229
|
84 |
(* TODO: implementation needs extra object-level lists ?!?*)
|
wneuper@59229
|
85 |
setup {* KEStore_Elems.add_mets
|
wneuper@59229
|
86 |
[ prep_met @{theory} "met_Programming" [] e_metID
|
wneuper@59229
|
87 |
(["Programming"], [],
|
wneuper@59229
|
88 |
{rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,
|
wneuper@59229
|
89 |
crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"),
|
wneuper@59229
|
90 |
prep_met @{theory} "met_Programming" [] e_metID
|
wneuper@59229
|
91 |
(["Programming","sort"], [],
|
wneuper@59229
|
92 |
{rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,
|
wneuper@59229
|
93 |
crls = e_rls, errpats = [], nrls = e_rls},
|
wneuper@59229
|
94 |
"empty_script"),
|
wneuper@59229
|
95 |
prep_met @{theory} "met_Programming" [] e_metID
|
wneuper@59229
|
96 |
(["Programming","sort"], [],
|
wneuper@59229
|
97 |
{rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
|
wneuper@59229
|
98 |
crls = Atools_crls, errpats = [], nrls = norm_Rational},
|
wneuper@59235
|
99 |
"Script Sortprog (u_u::int xlist) = (Rewrite_Set ins_sort False) u_u")
|
wneuper@59229
|
100 |
]
|
wneuper@59229
|
101 |
*}
|
neuper@37906
|
102 |
end
|