(* use"test-inssort.sml";

   W.N.17.6.00

*)

(* insertion sort, would need lists different from script-lists WN.11.00

WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *)

"--------------- sort [1,4,3,2] by rewrite_set ----------------";

val thy' = "InsSort";

val ct = "sort [1,4,3,2]";

"--- 1 ---";

val rls = "ins_sort";

val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct);

if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK"

else error "sort [1,4,3,2] didn't work";

"---------------- sort [1,3,2] by rewrite stepwise ----------------";

val thy' = "InsSort";

val ct = "sort [1,3,2]";

"--- 1 ---";

val thm = ("sort_def","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*)

"--- 2 ---";

val thm = ("foldr_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#3, #2] (ins [] #1)"*)

"--- 3 ---";

val thm = ("ins_base","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#3, #2] [#1]"*)

"--- 4 ---";

val thm = ("foldr_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#2] (ins [#1] #3)"*)

"--- 5 ---";

val thm = ("ins_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"*)

"--- 6 ---";

val op_ = "le";

val (ct,_) = the (calculate thy' op_ ct);

(*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*)

"--- 7 ---";

val thm = ("if_True","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#2] (#1 # ins [] #3)"*)

"--- 8 ---";

val thm = ("ins_base","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [#2] [#1, #3]"*)

"--- 9 ---";

val thm = ("foldr_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [] (ins [#1, #3] #2)"*)

"--- 10 ---";

val thm = ("ins_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [] (if #1 < #2 then #1 # ins [#3] #2 else [#2, #1, #3])"*)

"--- 11 ---";

val op_ = "le";

val (ct,_) = the (calculate thy' op_ ct);

(*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*)

"--- 12 ---";

val thm = ("if_True","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*"foldr ins [] (#1 # ins [#3] #2)"*)

"--- 13 ---";

val thm = ("ins_rec","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*"foldr ins [] (#1 # (if #3 < #2 then #3 # ins [] #2 else [#2, #3]))"*)

"--- 14 ---";

val op_ = "le";

val (ct,_) = the (calculate thy' op_ ct);

(*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*)

"--- 15 ---";

val thm = ("if_False","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "foldr ins [] [#1, #2, #3]"*)

"--- 16 ---";

val thm = ("foldr_base","");

val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

(*val ct = "[#1, #2, #3]"*)

if ct="[1, 2, 3]" then "sort [1,3,2] OK"

else error "sort [1,3,2] didn't work";

"---------------- sort [1,3,2] from script ----------------";

val fmz = ["unsorted [1,3,2]", "sorted S"];

val (dI',pI',mI') = 

  ("InsSort", ["inssort","functional"], ("InsSort","inssort"));

val p = e_pos'; val c = []; 

(* ------- 17.6.00: mit kleinen problemen aufgegeben

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

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

		\ Rewrite_Set ins_sort False u_");

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

      "Script Ins_sort (u_::real 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_)");

val scr=parse thy

      "Script Ins_sort (u_::real 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_ = u_   \

       \  in u_)";

atomty (term_of (the scr));

------- *)