1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,395 @@
1.4 +
1.5 +
1.6 +(*-------------------------from InsSort.thy 8.3.01----------------------*)
1.7 +(*List.thy:
1.8 + foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
1.9 +primrec
1.10 + foldl_Nil "foldl f a [] = a"
1.11 + foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
1.12 +
1.13 +above in sml:
1.14 +fun foldr f [] a = a
1.15 + | foldr f (x::xs) a = foldr f xs (f a x);
1.16 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
1.17 +fun ins [] a = [a]
1.18 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.19 +fun sort xs = foldr ins xs [];
1.20 +*)
1.21 +(*-------------------------from InsSort.thy 8.3.01----------------------*)
1.22 +
1.23 +
1.24 +(*-------------------------from InsSort.ML 8.3.01----------------------*)
1.25 +
1.26 +theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
1.27 +
1.28 +val ins_sort =
1.29 + Rls{preconds = [], rew_ord = ("tless_true",tless_true),
1.30 + rules = [Thm ("foldr_base",(*num_str*) foldr_base),
1.31 + Thm ("foldr_rec",foldr_rec),
1.32 + Thm ("ins_base",ins_base),
1.33 + Thm ("ins_rec",ins_rec),
1.34 + Thm ("sort_def",sort_def),
1.35 +
1.36 + Calc ("op <",eval_equ "#less_"),
1.37 + Thm ("if_True", if_True),
1.38 + Thm ("if_False", if_False)
1.39 + ],
1.40 + scr = Script ((term_of o the o (parse thy))
1.41 + "empty_script")
1.42 + }:rls;
1.43 +
1.44 +
1.45 +
1.46 +
1.47 +(*
1.48 +> get_pbt ["Script.thy","squareroot","univariate","equation"];
1.49 +> get_met ("Script.thy","max_on_interval_by_calculus");
1.50 +*)
1.51 +pbltypes:= (!pbltypes) @
1.52 +[
1.53 + prep_pbt InsSort.thy
1.54 + (["InsSort.thy","inssort"]:pblID,
1.55 + [("#Given" ,"unsorted u_"),
1.56 + ("#Find" ,"sorted s_")
1.57 + ])
1.58 +];
1.59 +
1.60 +methods:= (!methods) @
1.61 +[
1.62 +(*, -------17.6.00,
1.63 + (("InsSort.thy","inssort"):metID,
1.64 + {ppc = prep_met
1.65 + [("#Given" ,"unsorted u_"),
1.66 + ("#Find" ,"sorted s_")
1.67 + ],
1.68 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
1.69 + scr=Script (((inst_abs (assoc_thm "InsSort.thy"))
1.70 + o term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
1.71 + "Script Ins_sort (u_::'a list) = \
1.72 + \ (let u_ = Rewrite sort_def False u_; \
1.73 + \ u_ = Rewrite foldr_rec False u_; \
1.74 + \ u_ = Rewrite ins_base False u_; \
1.75 + \ u_ = Rewrite foldr_rec False u_; \
1.76 + \ u_ = Rewrite ins_rec False u_; \
1.77 + \ u_ = Calculate le u_; \
1.78 + \ u_ = Rewrite if_True False u_; \
1.79 + \ u_ = Rewrite ins_base False u_; \
1.80 + \ u_ = Rewrite foldr_rec False u_; \
1.81 + \ u_ = Rewrite ins_rec False u_; \
1.82 + \ u_ = Calculate le u_; \
1.83 + \ u_ = Rewrite if_True False u_; \
1.84 + \ u_ = Rewrite ins_rec False u_; \
1.85 + \ u_ = Calculate le u_; \
1.86 + \ u_ = Rewrite if_False False u_; \
1.87 + \ u_ = Rewrite foldr_base False u_ \
1.88 + \ in u_)")
1.89 + } : met),
1.90 +
1.91 + (("InsSort.thy","sort"):metID,
1.92 + {ppc = prep_met
1.93 + [("#Given" ,"unsorted u_"),
1.94 + ("#Find" ,"sorted s_")
1.95 + ],
1.96 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
1.97 + scr=Script ((inst_abs o term_of o the o (parse thy))
1.98 + "Script Sort (u_::'a list) = \
1.99 + \ Rewrite_Set ins_sort False u_")
1.100 + } : met)
1.101 +------- *)
1.102 +(*,
1.103 +
1.104 + (("",""):metID,
1.105 + {ppc = prep_met
1.106 + [("#Given" ,""),
1.107 + ("#Find" ,""),
1.108 + ("#Relate","")
1.109 + ],
1.110 + rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
1.111 + scr=EmptyScr} : met),
1.112 +*)
1.113 +];
1.114 +(*-------------------------from InsSort.ML 8.3.01----------------------*)
1.115 +
1.116 +
1.117 +(*------------------------- nipkow ----------------------*)
1.118 +consts
1.119 + sort :: 'a list => 'a list
1.120 + ins :: ['a,'a list] => 'a list
1.121 +(*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a
1.122 +*)
1.123 +rules
1.124 + ins_base "ins e [] = [e]"
1.125 + ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"
1.126 +
1.127 +rules
1.128 + sort_def "sort ls = (foldl ins ls [])"
1.129 +end
1.130 +
1.131 +
1.132 +(** swp: ..L **)
1.133 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
1.134 +fun foldL f [] e = e
1.135 + | foldL f (l::ls) e = f(l,foldL f ls e);
1.136 +
1.137 +(* fn : int * int list -> int list *)
1.138 +fun insL (e,[]) = [e]
1.139 + | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);
1.140 +
1.141 +fun sortL ls = foldL insL ls [];
1.142 +
1.143 +sortL [2,3,1]; (* [1,2,3] *)
1.144 +
1.145 +
1.146 +(** swp, curried: ..LC **)
1.147 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
1.148 +fun foldLC f [] e = e
1.149 + | foldLC f (x::xs) e = f x (foldLC f xs e);
1.150 +
1.151 +(* fn : int * int list -> int list *)
1.152 +fun insLC e [] = [e]
1.153 + | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);
1.154 +
1.155 +fun sortLC ls = foldLC insLC ls [];
1.156 +
1.157 +sortLC [2,3,1]; (* [1,2,3] *)
1.158 +
1.159 +
1.160 +(** sml110: ..l **)
1.161 +(* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)
1.162 +foldl;
1.163 +(* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!!
1.164 +fun foldl f e [] = e
1.165 + | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0
1.166 +
1.167 +foldl op+ (0,[100,11,1]);
1.168 +val it = 0 : int ... GEHT NICHT !!! *)
1.169 +
1.170 +fun insl (e,[]) = [e]
1.171 + | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);
1.172 +
1.173 +fun sortl ls = foldl insl [] ls;
1.174 +
1.175 +sortl [2,3,1]; (* [1,2,3] *)
1.176 +
1.177 +
1.178 +(** sml110, curried: ..lC **)
1.179 +(* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)
1.180 +fun foldlC f e [] = e
1.181 + | foldlC f e (l::ls) = f e (foldlC f e ls);
1.182 +
1.183 +(* fn : int -> int list -> int list *)
1.184 +fun inslC e [] = [e]
1.185 + | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);
1.186 +
1.187 +fun sortlC ls = foldlC inslC [] ls;
1.188 +
1.189 +sortlC [2,3,1];
1.190 +
1.191 +(*--- 15.6.00 ---*)
1.192 +
1.193 +
1.194 +fun Foldl f a [] = a
1.195 + | Foldl f a (x::xs) = Foldl f (f a x) xs;
1.196 +(*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)
1.197 +
1.198 +fun add a b = a+b:int;
1.199 +
1.200 +Foldl add 0 [1,2,3];
1.201 +
1.202 +fun ins0 a [] = [a]
1.203 + | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);
1.204 +(*val ins = fn : int -> int list -> int list*)
1.205 +
1.206 +fun ins [] a = [a]
1.207 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.208 +(*val ins = fn : int -> int list -> int list*)
1.209 +
1.210 +ins 3 [1,2,4];
1.211 +
1.212 +fun sort xs = Foldl ins0 xs [];
1.213 +(*operator domain: int -> int list -> int
1.214 + operand: int -> int list -> int list
1.215 + in expression:
1.216 + Foldl ins
1.217 + *)
1.218 +fun sort xs = Foldl ins xs [];
1.219 +
1.220 +
1.221 +
1.222 +(*--- 17.6.00 ---*)
1.223 +
1.224 +
1.225 +fun foldr f [] a = a
1.226 + | foldr f (x::xs) a = foldr f xs (f a x);
1.227 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
1.228 +
1.229 +fun add a b = a+b:int;
1.230 +
1.231 +fold add [1,2,3] 0;
1.232 +
1.233 +fun ins [] a = [a]
1.234 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.235 +(*val ins = fn : int list -> int -> int list*)
1.236 +
1.237 +ins [1,2,4] 3;
1.238 +
1.239 +fun sort xs = foldr ins xs [];
1.240 +
1.241 +sort [3,1,4,2];
1.242 +
1.243 +
1.244 +
1.245 +(*--- 17.6.00 II ---*)
1.246 +
1.247 +fun foldl f a [] = a
1.248 + | foldl f a (x::xs) = foldl f (f a x) xs;
1.249 +
1.250 +fun ins [] a = [a]
1.251 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.252 +
1.253 +fun sort xs = foldl ins xs [];
1.254 +
1.255 +sort [3,1,4,2];
1.256 +(*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)
1.257 +
1.258 +(*------------------------- nipkow ----------------------*)
1.259 +consts
1.260 + sort :: 'a list => 'a list
1.261 + ins :: ['a,'a list] => 'a list
1.262 +(*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a
1.263 +*)
1.264 +rules
1.265 + ins_base "ins e [] = [e]"
1.266 + ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"
1.267 +
1.268 +rules
1.269 + sort_def "sort ls = (foldl ins ls [])"
1.270 +end
1.271 +
1.272 +
1.273 +(** swp: ..L **)
1.274 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
1.275 +fun foldL f [] e = e
1.276 + | foldL f (l::ls) e = f(l,foldL f ls e);
1.277 +
1.278 +(* fn : int * int list -> int list *)
1.279 +fun insL (e,[]) = [e]
1.280 + | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);
1.281 +
1.282 +fun sortL ls = foldL insL ls [];
1.283 +
1.284 +sortL [2,3,1]; (* [1,2,3] *)
1.285 +
1.286 +
1.287 +(** swp, curried: ..LC **)
1.288 +(* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)
1.289 +fun foldLC f [] e = e
1.290 + | foldLC f (x::xs) e = f x (foldLC f xs e);
1.291 +
1.292 +(* fn : int * int list -> int list *)
1.293 +fun insLC e [] = [e]
1.294 + | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);
1.295 +
1.296 +fun sortLC ls = foldLC insLC ls [];
1.297 +
1.298 +sortLC [2,3,1]; (* [1,2,3] *)
1.299 +
1.300 +
1.301 +(** sml110: ..l **)
1.302 +(* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)
1.303 +foldl;
1.304 +(* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!!
1.305 +fun foldl f e [] = e
1.306 + | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0
1.307 +
1.308 +foldl op+ (0,[100,11,1]);
1.309 +val it = 0 : int ... GEHT NICHT !!! *)
1.310 +
1.311 +fun insl (e,[]) = [e]
1.312 + | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);
1.313 +
1.314 +fun sortl ls = foldl insl [] ls;
1.315 +
1.316 +sortl [2,3,1]; (* [1,2,3] *)
1.317 +
1.318 +
1.319 +(** sml110, curried: ..lC **)
1.320 +(* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)
1.321 +fun foldlC f e [] = e
1.322 + | foldlC f e (l::ls) = f e (foldlC f e ls);
1.323 +
1.324 +(* fn : int -> int list -> int list *)
1.325 +fun inslC e [] = [e]
1.326 + | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);
1.327 +
1.328 +fun sortlC ls = foldlC inslC [] ls;
1.329 +
1.330 +sortlC [2,3,1];
1.331 +
1.332 +(*--- 15.6.00 ---*)
1.333 +
1.334 +
1.335 +fun Foldl f a [] = a
1.336 + | Foldl f a (x::xs) = Foldl f (f a x) xs;
1.337 +(*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)
1.338 +
1.339 +fun add a b = a+b:int;
1.340 +
1.341 +Foldl add 0 [1,2,3];
1.342 +
1.343 +fun ins0 a [] = [a]
1.344 + | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);
1.345 +(*val ins = fn : int -> int list -> int list*)
1.346 +
1.347 +fun ins [] a = [a]
1.348 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.349 +(*val ins = fn : int -> int list -> int list*)
1.350 +
1.351 +ins 3 [1,2,4];
1.352 +
1.353 +fun sort xs = Foldl ins0 xs [];
1.354 +(*operator domain: int -> int list -> int
1.355 + operand: int -> int list -> int list
1.356 + in expression:
1.357 + Foldl ins
1.358 + *)
1.359 +fun sort xs = Foldl ins xs [];
1.360 +
1.361 +
1.362 +
1.363 +(*--- 17.6.00 ---*)
1.364 +
1.365 +
1.366 +fun foldr f [] a = a
1.367 + | foldr f (x::xs) a = foldr f xs (f a x);
1.368 +(*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)
1.369 +
1.370 +fun add a b = a+b:int;
1.371 +
1.372 +fold add [1,2,3] 0;
1.373 +
1.374 +fun ins [] a = [a]
1.375 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.376 +(*val ins = fn : int list -> int -> int list*)
1.377 +
1.378 +ins [1,2,4] 3;
1.379 +
1.380 +fun sort xs = foldr ins xs [];
1.381 +
1.382 +sort [3,1,4,2];
1.383 +
1.384 +
1.385 +
1.386 +(*--- 17.6.00 II ---*)
1.387 +
1.388 +fun foldl f a [] = a
1.389 + | foldl f a (x::xs) = foldl f (f a x) xs;
1.390 +
1.391 +fun ins [] a = [a]
1.392 + | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);
1.393 +
1.394 +fun sort xs = foldl ins xs [];
1.395 +
1.396 +sort [3,1,4,2];
1.397 +(*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)
1.398 +(*------------------------- nipkow ----------------------*)