6 unsorted :: "int xlist => unl" |
6 unsorted :: "int xlist => unl" |
7 sorted :: "int xlist => unl" |
7 sorted :: "int xlist => unl" |
8 |
8 |
9 (* CAS-command *) |
9 (* CAS-command *) |
10 Sort :: "int xlist \<Rightarrow> int xlist" |
10 Sort :: "int xlist \<Rightarrow> int xlist" |
11 |
|
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) |
|
19 |
11 |
20 section \<open>functions\<close> |
12 section \<open>functions\<close> |
21 primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist" |
13 primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist" |
22 where |
14 where |
23 ins_Nil: "ins i {|| ||} = {||i||}" | |
15 ins_Nil: "ins i {|| ||} = {||i||}" | |
115 [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID |
107 [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID |
116 (["Programming","SORT","insertion"], |
108 (["Programming","SORT","insertion"], |
117 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])], |
109 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])], |
118 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
110 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
119 crls = Atools_crls, errpats = [], nrls = norm_Rational}, |
111 crls = Atools_crls, errpats = [], nrls = norm_Rational}, |
120 @{thm sort_program.simps} |
112 @{thm sort_program.simps})] |
121 (*"Script Sortprog (unso :: int xlist) = " ^ |
|
122 " (let uns = Take (sort unso) " ^ |
|
123 " in " ^ |
|
124 " (Rewrite_Set ''ins_sort'' False) uns" ^ |
|
125 " )"*))] |
|
126 \<close> |
113 \<close> |
127 |
114 |
128 partial_function (tailrec) sort_program2 :: "int xlist => int xlist" |
115 partial_function (tailrec) sort_program2 :: "int xlist => int xlist" |
129 where |
116 where |
130 "sort_program2 unso = |
117 "sort_program2 unso = |
147 [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID |
134 [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID |
148 (["Programming","SORT","insertion_steps"], |
135 (["Programming","SORT","insertion_steps"], |
149 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])], |
136 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])], |
150 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
137 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, |
151 crls = Atools_crls, errpats = [], nrls = norm_Rational}, |
138 crls = Atools_crls, errpats = [], nrls = norm_Rational}, |
152 @{thm sort_program2.simps} |
139 @{thm sort_program2.simps})] |
153 (*"Script Sortprog (unso :: int xlist) = " ^ |
|
154 " (let uns = Take (sort unso) " ^ |
|
155 " in " ^ |
|
156 " (Repeat " ^ |
|
157 " ((Repeat (Rewrite ''xfoldr_Nil'' False)) Or " ^ |
|
158 " (Repeat (Rewrite ''xfoldr_Cons'' False)) Or " ^ |
|
159 " (Repeat (Rewrite ''ins_Nil'' False)) Or " ^ |
|
160 " (Repeat (Rewrite ''ins_Cons'' False)) Or " ^ |
|
161 " (Repeat (Rewrite ''sort_deff'' False)) Or " ^ |
|
162 " (Repeat (Rewrite ''o_id'' False)) Or " ^ |
|
163 " (Repeat (Rewrite ''o_assoc'' False)) Or " ^ |
|
164 " (Repeat (Rewrite ''o_apply'' False)) Or " ^ |
|
165 " (Repeat (Rewrite ''id_apply'' False)) Or " ^ |
|
166 " (Repeat (Calculate ''le'' )) Or " ^ |
|
167 " (Repeat (Rewrite ''If_def'' False)) Or " ^ |
|
168 " (Repeat (Rewrite ''if_True'' False)) Or " ^ |
|
169 " (Repeat (Rewrite ''if_False'' False)))) uns" ^ |
|
170 " )"*)) |
|
171 ] |
|
172 \<close> |
140 \<close> |
173 |
141 |
174 subsection \<open>CAS-commands\<close> |
142 subsection \<open>CAS-commands\<close> |
175 ML \<open> |
143 ML \<open> |
176 (* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet; |
144 (* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet; |