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

(*List.thy:

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

primrec

  foldl_Nil  "foldl f a [] = a"

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

above in sml:

fun foldr f [] a = a

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

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

fun ins [] a = [a]

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

fun sort xs = foldr ins xs [];

*)

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

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

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

val ins_sort = 

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

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

	       Thm ("foldr_rec",foldr_rec),

	       Thm ("ins_base",ins_base),

	       Thm ("ins_rec",ins_rec),

	       Thm ("sort_def",sort_def),

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

	       Thm ("if_True", if_True),

	       Thm ("if_False", if_False)

	       ],

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

      "empty_script")

      }:rls;      

(* 

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

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

*)

pbltypes:= (!pbltypes) @ 

[

 prep_pbt InsSort.thy

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

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

   ("#Find"  ,"sorted s_")

  ])

];

methods:= (!methods) @

[

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

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

  {ppc = prep_met

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

    ("#Find"  ,"sorted s_")

    ],

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

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

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

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

       \ (let u_ = Rewrite sort_def   False u_; \

       \      u_ = Rewrite foldr_rec  False u_; \

       \      u_ = Rewrite ins_base   False u_; \

       \      u_ = Rewrite foldr_rec  False u_; \

       \      u_ = Rewrite ins_rec    False u_; \

       \      u_ = Calculate le u_;             \

       \      u_ = Rewrite if_True    False u_; \

       \      u_ = Rewrite ins_base   False u_; \

       \      u_ = Rewrite foldr_rec  False u_; \

       \      u_ = Rewrite ins_rec    False u_; \

       \      u_ = Calculate le u_;             \

       \      u_ = Rewrite if_True    False u_; \

       \      u_ = Rewrite ins_rec    False u_; \

       \      u_ = Calculate le u_;             \

       \      u_ = Rewrite if_False   False u_; \

       \      u_ = Rewrite foldr_base False u_  \

       \  in u_)")

  } : met),

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

  {ppc = prep_met

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

    ("#Find"  ,"sorted s_")

    ],

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

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

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

		\ Rewrite_Set ins_sort False u_")

  } : met)

------- *)

(*,

 (("",""):metID,

  {ppc = prep_met

   [("#Given" ,""),

    ("#Find"  ,""),

    ("#Relate","")

    ],

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

   scr=EmptyScr} : met),

*)

];

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

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

consts

  sort    :: 'a list => 'a list

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

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

*)

rules

  ins_base  "ins e [] = [e]"

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

rules

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

end

(** swp: ..L **)

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

fun foldL f [] e = e

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

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

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

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

fun sortL ls = foldL insL ls [];

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

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

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

fun foldLC f [] e = e

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

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

fun insLC e [] = [e]

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

fun sortLC ls = foldLC insLC ls [];

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

(** sml110: ..l **)

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

foldl;

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

fun foldl f e [] = e

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

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

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

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

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

fun sortl ls = foldl insl [] ls;

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

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

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

fun foldlC f e [] = e

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

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

fun inslC e [] = [e]

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

fun sortlC ls = foldlC inslC [] ls;

sortlC [2,3,1];

(*--- 15.6.00 ---*)

fun Foldl f a [] = a

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

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

fun add a b = a+b:int;

Foldl add 0 [1,2,3];

fun ins0 a [] = [a]

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

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

fun ins [] a = [a]

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

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

ins 3 [1,2,4];

fun sort xs = Foldl ins0 xs [];

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

  operand:         int -> int list -> int list

  in expression:

    Foldl ins    

                            *)

fun sort xs = Foldl ins xs [];

(*--- 17.6.00 ---*)

fun foldr f [] a = a

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

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

fun add a b = a+b:int;

fold add [1,2,3] 0;

fun ins [] a = [a]

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

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

ins [1,2,4] 3;

fun sort xs = foldr ins xs [];

sort [3,1,4,2];

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

fun foldl f a [] = a

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

fun ins [] a = [a]

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

fun sort xs = foldl ins xs [];

sort [3,1,4,2];

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

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

consts

  sort    :: 'a list => 'a list

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

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

*)

rules

  ins_base  "ins e [] = [e]"

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

rules

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

end

(** swp: ..L **)

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

fun foldL f [] e = e

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

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

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

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

fun sortL ls = foldL insL ls [];

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

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

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

fun foldLC f [] e = e

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

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

fun insLC e [] = [e]

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

fun sortLC ls = foldLC insLC ls [];

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

(** sml110: ..l **)

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

foldl;

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

fun foldl f e [] = e

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

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

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

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

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

fun sortl ls = foldl insl [] ls;

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

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

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

fun foldlC f e [] = e

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

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

fun inslC e [] = [e]

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

fun sortlC ls = foldlC inslC [] ls;

sortlC [2,3,1];

(*--- 15.6.00 ---*)

fun Foldl f a [] = a

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

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

fun add a b = a+b:int;

Foldl add 0 [1,2,3];

fun ins0 a [] = [a]

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

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

fun ins [] a = [a]

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

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

ins 3 [1,2,4];

fun sort xs = Foldl ins0 xs [];

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

  operand:         int -> int list -> int list

  in expression:

    Foldl ins    

                            *)

fun sort xs = Foldl ins xs [];

(*--- 17.6.00 ---*)

fun foldr f [] a = a

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

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

fun add a b = a+b:int;

fold add [1,2,3] 0;

fun ins [] a = [a]

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

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

ins [1,2,4] 3;

fun sort xs = foldr ins xs [];

sort [3,1,4,2];

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

fun foldl f a [] = a

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

fun ins [] a = [a]

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

fun sort xs = foldl ins xs [];

sort [3,1,4,2];

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

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