theory InsSort imports "../Interpret/Interpret" Rational(*for norm_Rational?!?*)

begin

subsection {* consts *}

consts

  unsorted   :: "'a list => unl"

  sorted     :: "'a list => unl"

(* subproblem and script-name *)

  Ins'_sort  :: "['a xlist,  

		    'a xlist] => 'a xlist"

               ("((Script Ins'_sort (_ =))//  

		    (_))" 9)

  Sort       :: "['a xlist,  

		    'a xlist] => 'a xlist"

               ("((Script Sort (_ =))//  

		    (_))" 9)

subsection {* functions *}

primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"

where

ins_Nil:  "ins i [|| ||] = [||i||]" |

ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"

fun sort :: "int xlist \<Rightarrow> int xlist"

where

sort_deff: "sort xs = xfoldr ins xs [|| ||]"

print_theorems

thm sort_def  (* InsSort.sort \<equiv> sort_sumC *)

thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)

(* access to definitions from ML *)

ML {*

@{thm ins.simps(1)};

@{thm ins.simps(2)};

*}

value "sort [||2,3,1||]"

lemma test: "sort [||2,3,1||] = [||1,2,3||]"

by simp

subsection {* eval functions *}

subsection {* rulesets *}

ML {*

val ins_sort = 

  Rls {

    id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,

    srls = e_rls, calc = [], rules = [

      Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),

	    Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),

	    Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),

	    Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),

	    Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),

	    Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),

	    Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),

	    Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),

	    Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),

	    Calc ("Orderings.ord_class.less", eval_equ "#less_"),

	    Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),

	    Thm ("if_True", @{thm if_True} (*  *)),

	    Thm ("if_False", @{thm if_False} (*  *))],

	  errpatts = [], scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")};      

*}

setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}

subsection {* problems *}

setup {* KEStore_Elems.add_pbts

  [(prep_pbt @{theory} "pbl_Programming" [] e_pblID 

     (["Programming"], [], e_rls, NONE, [])),

   (prep_pbt @{theory} "pbl_Prog_sort" [] e_pblID 

     (["sort","Programming"], [], e_rls, NONE, [])),

   (prep_pbt @{theory} "pbl_Prog_sort_ins" [] e_pblID

     (["insertion","sort","Programming"], 

     [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])], 

     e_rls, 

     NONE, [])) ] *}

subsection {* CAS-commands *}

(** CAS-commands **)

subsection {* methods *}

(* TODO: implementation needs extra object-level lists ?!?*)

setup {* KEStore_Elems.add_mets

  [ prep_met @{theory} "met_Programming" [] e_metID

      (["Programming"], [],

        {rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,

          crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"),

    prep_met @{theory} "met_Programming" [] e_metID

      (["Programming","sort"], [],

        {rew_ord'="tless_true",rls' = e_rls, calc = [], srls = e_rls, prls = e_rls,

          crls = e_rls, errpats = [], nrls = e_rls},

        "empty_script"),

    prep_met @{theory} "met_Programming" [] e_metID

      (["Programming","sort"], [],

        {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,

          crls = Atools_crls, errpats = [], nrls = norm_Rational},

        "Script Sort (u_u::'a xlist) = (Rewrite_Set ins_sort False) u_u")

  ]

*}

end