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

begin

subsection {* consts *}

consts

  unsorted   :: "int xlist => unl"

  sorted     :: "int xlist => unl"

  (* CAS-command *)

  Sort       :: "int xlist \<Rightarrow> int xlist"

  (* subproblem and script-name *)

  Ins'_sort  :: "[int xlist,  

		    int xlist] => int xlist"

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

		    (_))" 9)

  Sortprog   :: "[int xlist,  

		    int xlist] => int xlist"

               ("((Script Sortprog (_ =))//  

		    (_))" 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} (* "(if True then x else y) = x" *)),

	    Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],

	  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

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

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

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

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

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

     (["insertion","SORT","Programming"], 

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

     e_rls, 

     SOME "Sort u_u", [["Programming","SORT","insertion_steps"]]))] *}

subsection {* methods *}

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

setup {* KEStore_Elems.add_mets

  [ Specify.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"),

    Specify.prep_met @{theory} "met_Prog_sort" [] 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"),

    Specify.prep_met @{theory} "met_Prog_sort_ins" [] e_metID

      (["Programming","SORT","insertion"], 

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

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

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

        "Script Sortprog (unso :: int xlist) = " ^

        "  (let uns = Take (sort unso) " ^

        "  in " ^

        "    (Rewrite_Set ins_sort False) uns" ^

        "  )"),

    Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] e_metID

      (["Programming","SORT","insertion_steps"], 

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

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

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

        "Script Sortprog (unso :: int xlist) =           " ^

        "  (let uns = Take (sort unso)                   " ^

        "  in                                            " ^

          " (Repeat                                      " ^

          "   ((Repeat (Rewrite xfoldr_Nil  False)) Or   " ^

          "    (Repeat (Rewrite xfoldr_Cons False)) Or   " ^

          "    (Repeat (Rewrite ins_Nil     False)) Or   " ^

          "    (Repeat (Rewrite ins_Cons    False)) Or   " ^

          "    (Repeat (Rewrite sort_deff   False)) Or   " ^

          "    (Repeat (Rewrite o_id        False)) Or   " ^

          "    (Repeat (Rewrite o_assoc     False)) Or   " ^

          "    (Repeat (Rewrite o_apply     False)) Or   " ^

          "    (Repeat (Rewrite id_apply    False)) Or   " ^

          "    (Repeat (Calculate le             )) Or   " ^

          "    (Repeat (Rewrite If_def      False)) Or   " ^

          "    (Repeat (Rewrite if_True     False)) Or   " ^

          "    (Repeat (Rewrite if_False    False)))) uns" ^

        "  )")

  ]

*}

subsection {* CAS-commands *}

ML {*

(* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet;

   associate above input with dataformat of pbt (without "#Given", etc):

*)

fun argl2dtss [t] =

    [(@{term "unsorted"}, [t]),

     (@{term "sorted"},   [@{term "DUMMY::int xlist"}])

     ]

  | argl2dtss _ = error "InsSort.thy: wrong argument for argl2dtss"

*}

(* associate input with other data required for formal specification *)

setup {* KEStore_Elems.add_cas

  [ ( @{term "Sort"},  

      (("InsSort", ["insertion","SORT","Programming"], ["no_met"]), argl2dtss)

    )

  ]

*}

end