1.1 --- a/src/Tools/isac/IsacKnowledge/InsSort.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,395 +0,0 @@
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 ----------------------*)