1 theory InsSort imports "../Interpret/Interpret" Rational(*for norm_Rational?!?*)
4 subsection {* consts *}
6 unsorted :: "int xlist => unl"
7 sorted :: "int xlist => unl"
10 Sort :: "int xlist \<Rightarrow> int xlist"
12 (* subproblem and script-name *)
13 Ins'_sort :: "[int xlist,
14 int xlist] => int xlist"
15 ("((Script Ins'_sort (_ =))// (_))" 9)
16 Sortprog :: "[int xlist,
17 int xlist] => int xlist"
18 ("((Script Sortprog (_ =))// (_))" 9)
20 subsection {* functions *}
21 primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
23 ins_Nil: "ins i {|| ||} = {||i||}" |
24 ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"
26 fun sort :: "int xlist \<Rightarrow> int xlist"
28 sort_deff: "sort xs = xfoldr ins xs {|| ||}"
30 (* thm sort_def InsSort.sort \<equiv> sort_sumC *)
31 thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
33 (* access to definitions from ML *)
39 value "sort {||2,3,1||}"
40 lemma test: "sort {||2,3,1||} = {||1,2,3||}"
43 subsection {* eval functions *}
44 subsection {* rulesets *}
48 id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Celem.e_rls,
49 srls = Celem.e_rls, calc = [], rules = [
50 Celem.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
51 Celem.Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
53 Celem.Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
54 Celem.Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
55 Celem.Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
57 Celem.Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
58 Celem.Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
59 Celem.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
60 Celem.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
62 Celem.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
63 Celem.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) *)),
64 Celem.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
65 Celem.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
66 errpatts = [], scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")};
68 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
70 subsection {* problems *}
71 setup {* KEStore_Elems.add_pbts
72 [(Specify.prep_pbt @{theory} "pbl_Programming" [] Celem.e_pblID
73 (["Programming"], [], Celem.e_rls, NONE, [])),
74 (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Celem.e_pblID
75 (["SORT","Programming"], [], Celem.e_rls, NONE, [])),
76 (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Celem.e_pblID
77 (["insertion","SORT","Programming"],
78 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
80 SOME "Sort u_u", [["Programming","SORT","insertion_steps"]]))] *}
82 subsection {* methods *}
83 (* TODO: implementation needs extra object-level lists ?!?*)
84 setup {* KEStore_Elems.add_mets
85 [ Specify.prep_met @{theory} "met_Programming" [] Celem.e_metID
87 {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
88 crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls}, "empty_script"),
89 Specify.prep_met @{theory} "met_Prog_sort" [] Celem.e_metID
90 (["Programming","SORT"], [],
91 {rew_ord'="tless_true",rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
92 crls = Celem.e_rls, errpats = [], nrls = Celem.e_rls},
94 Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
95 (["Programming","SORT","insertion"],
96 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
97 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
98 crls = Atools_crls, errpats = [], nrls = norm_Rational},
99 "Script Sortprog (unso :: int xlist) = " ^
100 " (let uns = Take (sort unso) " ^
102 " (Rewrite_Set ins_sort False) uns" ^
104 Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
105 (["Programming","SORT","insertion_steps"],
106 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
107 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Celem.e_rls, prls = Celem.e_rls,
108 crls = Atools_crls, errpats = [], nrls = norm_Rational},
109 "Script Sortprog (unso :: int xlist) = " ^
110 " (let uns = Take (sort unso) " ^
113 " ((Repeat (Rewrite xfoldr_Nil False)) Or " ^
114 " (Repeat (Rewrite xfoldr_Cons False)) Or " ^
115 " (Repeat (Rewrite ins_Nil False)) Or " ^
116 " (Repeat (Rewrite ins_Cons False)) Or " ^
117 " (Repeat (Rewrite sort_deff False)) Or " ^
118 " (Repeat (Rewrite o_id False)) Or " ^
119 " (Repeat (Rewrite o_assoc False)) Or " ^
120 " (Repeat (Rewrite o_apply False)) Or " ^
121 " (Repeat (Rewrite id_apply False)) Or " ^
122 " (Repeat (Calculate le )) Or " ^
123 " (Repeat (Rewrite If_def False)) Or " ^
124 " (Repeat (Rewrite if_True False)) Or " ^
125 " (Repeat (Rewrite if_False False)))) uns" ^
130 subsection {* CAS-commands *}
132 (* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet;
133 associate above input with dataformat of pbt (without "#Given", etc):
136 [(@{term "unsorted"}, [t]),
137 (@{term "sorted"}, [@{term "DUMMY::int xlist"}])
139 | argl2dtss _ = error "InsSort.thy: wrong argument for argl2dtss"
141 (* associate input with other data required for formal specification *)
142 setup {* KEStore_Elems.add_cas
144 (("InsSort", ["insertion","SORT","Programming"], ["no_met"]), argl2dtss)