wneuper/isac: src/sml/IsacKnowledge/InsSort.sml@a0c068d1e54e

     3 (*-------------------------from InsSort.thy 8.3.01----------------------*)

     4 (*List.thy:

     5   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b

     6 primrec

     7   foldl_Nil  "foldl f a [] = a"

     8   foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"

    10 above in sml:

    11 fun foldr f [] a = a

    12   | foldr f (x::xs) a = foldr f xs (f a x);

    13 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)

    14 fun ins [] a = [a]

    15   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

    16 fun sort xs = foldr ins xs [];

    17 *)

    18 (*-------------------------from InsSort.thy 8.3.01----------------------*)

    21 (*-------------------------from InsSort.ML 8.3.01----------------------*)

    23 theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];

    25 val ins_sort =

    26   Rls{preconds = [], rew_ord = ("tless_true",tless_true),

    27       rules = [Thm ("foldr_base",(*num_str*) foldr_base),

    28 	       Thm ("foldr_rec",foldr_rec),

    29 	       Thm ("ins_base",ins_base),

    30 	       Thm ("ins_rec",ins_rec),

    31 	       Thm ("sort_def",sort_def),

    33 	       Calc ("op <",eval_equ "#less_"),

    34 	       Thm ("if_True", if_True),

    35 	       Thm ("if_False", if_False)

    36 	       ],

    37       scr = Script ((term_of o the o (parse thy))

    38       "empty_script")

    39       }:rls;

    44 (*

    45 > get_pbt ["Script.thy","squareroot","univariate","equation"];

    46 > get_met ("Script.thy","max_on_interval_by_calculus");

    47 *)

    48 pbltypes:= (!pbltypes) @

    49 [

    50  prep_pbt InsSort.thy

    51  (["InsSort.thy","inssort"]:pblID,

    52   [("#Given" ,"unsorted u_"),

    53    ("#Find"  ,"sorted s_")

    54   ])

    55 ];

    57 methods:= (!methods) @

    58 [

    59 (*, -------17.6.00,

    60  (("InsSort.thy","inssort"):metID,

    61   {ppc = prep_met

    62    [("#Given" ,"unsorted u_"),

    63     ("#Find"  ,"sorted s_")

    64     ],

    65    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    66    scr=Script (((inst_abs (assoc_thm "InsSort.thy"))

    67               o term_of o the o (parse thy))    (*for [#1,#3,#2] only*)

    68       "Script Ins_sort (u_::'a list) =          \

    69        \ (let u_ = Rewrite sort_def   False u_; \

    70        \      u_ = Rewrite foldr_rec  False u_; \

    71        \      u_ = Rewrite ins_base   False u_; \

    72        \      u_ = Rewrite foldr_rec  False u_; \

    73        \      u_ = Rewrite ins_rec    False u_; \

    74        \      u_ = Calculate le u_;             \

    75        \      u_ = Rewrite if_True    False u_; \

    76        \      u_ = Rewrite ins_base   False u_; \

    77        \      u_ = Rewrite foldr_rec  False u_; \

    78        \      u_ = Rewrite ins_rec    False u_; \

    79        \      u_ = Calculate le u_;             \

    80        \      u_ = Rewrite if_True    False u_; \

    81        \      u_ = Rewrite ins_rec    False u_; \

    82        \      u_ = Calculate le u_;             \

    83        \      u_ = Rewrite if_False   False u_; \

    84        \      u_ = Rewrite foldr_base False u_  \

    85        \  in u_)")

    86   } : meth'),

    88  (("InsSort.thy","sort"):metID,

    89   {ppc = prep_met

    90    [("#Given" ,"unsorted u_"),

    91     ("#Find"  ,"sorted s_")

    92     ],

    93    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

    94    scr=Script ((inst_abs o term_of o the o (parse thy))

    95 	       "Script Sort (u_::'a list) =   \

    96 		\ Rewrite_Set ins_sort False u_")

    97   } : meth')

    98 ------- *)

    99 (*,

   101  (("",""):metID,

   102   {ppc = prep_met

   103    [("#Given" ,""),

   104     ("#Find"  ,""),

   105     ("#Relate","")

   106     ],

   107    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],

   108    scr=EmptyScr} : meth'),

   109 *)

   110 ];

   111 (*-------------------------from InsSort.ML 8.3.01----------------------*)

   114 (*------------------------- nipkow ----------------------*)

   115 consts

   116   sort    :: 'a list => 'a list

   117   ins     :: ['a,'a list] => 'a list

   118 (*foldl   :: [['a,'b] => 'a, 'a, 'b list] => 'a

   119 *)

   120 rules

   121   ins_base  "ins e [] = [e]"

   122   ins_rec   "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"

   124 rules

   125   sort_def  "sort ls = (foldl ins ls [])"

   126 end

   129 (** swp: ..L **)

   130 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)

   131 fun foldL f [] e = e

   132   | foldL f (l::ls) e = f(l,foldL f ls e);

   134 (* fn : int * int list -> int list *)

   135 fun insL (e,[]) = [e]

   136   | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);

   138 fun sortL ls = foldL insL ls [];

   140 sortL [2,3,1]; (* [1,2,3] *)

   143 (** swp, curried: ..LC **)

   144 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)

   145 fun foldLC f [] e = e

   146   | foldLC f (x::xs) e = f x (foldLC f xs e);

   148 (* fn : int * int list -> int list *)

   149 fun insLC e [] = [e]

   150   | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);

   152 fun sortLC ls = foldLC insLC ls [];

   154 sortLC [2,3,1]; (* [1,2,3] *)

   157 (** sml110: ..l **)

   158 (* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)

   159 foldl;

   160 (* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a :  ANDERS !!!

   161 fun foldl f e [] = e

   162   | foldl f e (l::ls) = f e (foldl f (e,ls));     0+...+0+0

   164 foldl op+ (0,[100,11,1]);

   165 val it = 0 : int                         ... GEHT NICHT !!! *)

   167 fun insl (e,[]) = [e]

   168   | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);

   170 fun sortl ls = foldl insl [] ls;

   172 sortl [2,3,1]; (* [1,2,3] *)

   175 (** sml110, curried: ..lC **)

   176 (* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)

   177 fun foldlC f e [] = e

   178   | foldlC f e (l::ls) = f e (foldlC f e ls);

   180 (* fn : int -> int list -> int list *)

   181 fun inslC e [] = [e]

   182   | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);

   184 fun sortlC ls = foldlC inslC [] ls;

   186 sortlC [2,3,1];

   188 (*--- 15.6.00 ---*)

   191 fun Foldl f a [] = a

   192   | Foldl f a (x::xs) = Foldl f (f a x) xs;

   193 (*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)

   195 fun add a b = a+b:int;

   197 Foldl add 0 [1,2,3];

   199 fun ins0 a [] = [a]

   200   | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);

   201 (*val ins = fn : int -> int list -> int list*)

   203 fun ins [] a = [a]

   204   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   205 (*val ins = fn : int -> int list -> int list*)

   207 ins 3 [1,2,4];

   209 fun sort xs = Foldl ins0 xs [];

   210 (*operator domain: int -> int list -> int

   211   operand:         int -> int list -> int list

   212   in expression:

   213     Foldl ins

   214                             *)

   215 fun sort xs = Foldl ins xs [];

   219 (*--- 17.6.00 ---*)

   222 fun foldr f [] a = a

   223   | foldr f (x::xs) a = foldr f xs (f a x);

   224 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)

   226 fun add a b = a+b:int;

   228 fold add [1,2,3] 0;

   230 fun ins [] a = [a]

   231   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   232 (*val ins = fn : int list -> int -> int list*)

   234 ins [1,2,4] 3;

   236 fun sort xs = foldr ins xs [];

   238 sort [3,1,4,2];

   242 (*--- 17.6.00 II ---*)

   244 fun foldl f a [] = a

   245   | foldl f a (x::xs) = foldl f (f a x) xs;

   247 fun ins [] a = [a]

   248   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   250 fun sort xs = foldl ins xs [];

   252 sort [3,1,4,2];

   253 (*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)

   255 (*------------------------- nipkow ----------------------*)

   256 consts

   257   sort    :: 'a list => 'a list

   258   ins     :: ['a,'a list] => 'a list

   259 (*foldl   :: [['a,'b] => 'a, 'a, 'b list] => 'a

   260 *)

   261 rules

   262   ins_base  "ins e [] = [e]"

   263   ins_rec   "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))"

   265 rules

   266   sort_def  "sort ls = (foldl ins ls [])"

   267 end

   270 (** swp: ..L **)

   271 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)

   272 fun foldL f [] e = e

   273   | foldL f (l::ls) e = f(l,foldL f ls e);

   275 (* fn : int * int list -> int list *)

   276 fun insL (e,[]) = [e]

   277   | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls);

   279 fun sortL ls = foldL insL ls [];

   281 sortL [2,3,1]; (* [1,2,3] *)

   284 (** swp, curried: ..LC **)

   285 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *)

   286 fun foldLC f [] e = e

   287   | foldLC f (x::xs) e = f x (foldLC f xs e);

   289 (* fn : int * int list -> int list *)

   290 fun insLC e [] = [e]

   291   | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls);

   293 fun sortLC ls = foldLC insLC ls [];

   295 sortLC [2,3,1]; (* [1,2,3] *)

   298 (** sml110: ..l **)

   299 (* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *)

   300 foldl;

   301 (* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a :  ANDERS !!!

   302 fun foldl f e [] = e

   303   | foldl f e (l::ls) = f e (foldl f (e,ls));     0+...+0+0

   305 foldl op+ (0,[100,11,1]);

   306 val it = 0 : int                         ... GEHT NICHT !!! *)

   308 fun insl (e,[]) = [e]

   309   | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls);

   311 fun sortl ls = foldl insl [] ls;

   313 sortl [2,3,1]; (* [1,2,3] *)

   316 (** sml110, curried: ..lC **)

   317 (* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *)

   318 fun foldlC f e [] = e

   319   | foldlC f e (l::ls) = f e (foldlC f e ls);

   321 (* fn : int -> int list -> int list *)

   322 fun inslC e [] = [e]

   323   | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls);

   325 fun sortlC ls = foldlC inslC [] ls;

   327 sortlC [2,3,1];

   329 (*--- 15.6.00 ---*)

   332 fun Foldl f a [] = a

   333   | Foldl f a (x::xs) = Foldl f (f a x) xs;

   334 (*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*)

   336 fun add a b = a+b:int;

   338 Foldl add 0 [1,2,3];

   340 fun ins0 a [] = [a]

   341   | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs);

   342 (*val ins = fn : int -> int list -> int list*)

   344 fun ins [] a = [a]

   345   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   346 (*val ins = fn : int -> int list -> int list*)

   348 ins 3 [1,2,4];

   350 fun sort xs = Foldl ins0 xs [];

   351 (*operator domain: int -> int list -> int

   352   operand:         int -> int list -> int list

   353   in expression:

   354     Foldl ins

   355                             *)

   356 fun sort xs = Foldl ins xs [];

   360 (*--- 17.6.00 ---*)

   363 fun foldr f [] a = a

   364   | foldr f (x::xs) a = foldr f xs (f a x);

   365 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*)

   367 fun add a b = a+b:int;

   369 fold add [1,2,3] 0;

   371 fun ins [] a = [a]

   372   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   373 (*val ins = fn : int list -> int -> int list*)

   375 ins [1,2,4] 3;

   377 fun sort xs = foldr ins xs [];

   379 sort [3,1,4,2];

   383 (*--- 17.6.00 II ---*)

   385 fun foldl f a [] = a

   386   | foldl f a (x::xs) = foldl f (f a x) xs;

   388 fun ins [] a = [a]

   389   | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs);

   391 fun sort xs = foldl ins xs [];

   393 sort [3,1,4,2];

   394 (*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*)

   395 (*------------------------- nipkow ----------------------*)

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 318	a0c068d1e54e
child 701	8c061a9c46ab
permissions	-rw-r--r--