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

begin

section \<open>consts\<close>

consts

  unsorted   :: "int xlist => unl"

  sorted     :: "int xlist => unl"

  (* CAS-command *)

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

section \<open>functions\<close>

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))"

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

axiomatization where

sort_deff [code]: "sort xs = xfoldr ins xs {|| ||}"

(* this broke with 406681ebe781 ERROR "partial_function: shift respective thys to ProgLang" with

   ERROR Tactic failed

   The error(s) above occurred for the goal statement\<^here>:

   sort xs = xfoldr ins 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 \<open>

@{thm ins.simps(1)};

@{thm ins.simps(2)};

\<close>

value "sort {||2,3,1||}"

(* this broke with 406681ebe781 ERROR "Failed to apply initial proof method\<^here>:" with

lemma test: "sort {||2,3,1||} = {||1,2,3||}"

by auto

*)

section \<open>eval functions\<close>

section \<open>term order\<close>

section \<open>rulesets\<close>

ML \<open>

val ins_sort = 

  Rule_Def.Repeat {

    id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Rule_Set.empty,

    srls = Rule_Set.empty, calc = [], rules = [

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

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

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

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

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

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

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

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

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

	    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

	    Rule.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) *)),

	    Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),

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

	  errpatts = [], scr = Rule.Empty_Prog};      

\<close>

setup \<open>KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))]\<close>

section \<open>problems\<close>

setup \<open>KEStore_Elems.add_pbts

  [ Problem.prep_input @{theory} "pbl_Programming" [] Problem.id_empty 

     (["Programming"], [], Rule_Set.empty, NONE, []),

    Problem.prep_input @{theory} "pbl_Prog_sort" [] Problem.id_empty 

     (["SORT", "Programming"], [], Rule_Set.empty, NONE, []),

    Problem.prep_input @{theory} "pbl_Prog_sort_ins" [] Problem.id_empty

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

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

     Rule_Set.empty, 

     SOME "Sort u_u", [["Programming", "SORT", "insertion_steps"]])]\<close>

section \<open>methods\<close>

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

setup \<open>KEStore_Elems.add_mets

  [ MethodC.prep_input @{theory} "met_Programming" [] MethodC.id_empty

      (["Programming"], [],

        {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,

          crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),

    MethodC.prep_input @{theory} "met_Prog_sort" [] MethodC.id_empty

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

        {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,

          crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},

        @{thm refl})]

\<close>

partial_function (tailrec) sort_program :: "int xlist => int xlist"

  where

"sort_program unso = (

  let

    uns = Take (sort unso)

  in

    (Rewrite_Set ''ins_sort'') uns)"

setup \<open>KEStore_Elems.add_mets

   [MethodC.prep_input @{theory} "met_Prog_sort_ins" [] MethodC.id_empty

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

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

        {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,

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

        @{thm sort_program.simps})]

\<close>

partial_function (tailrec) sort_program2 :: "int xlist => int xlist"

  where 

"sort_program2 unso = (

  let

    uns = Take (sort unso) 

  in (

    Repeat (

      (Repeat (Rewrite ''xfoldr_Nil'')) Or

      (Repeat (Rewrite ''xfoldr_Cons'')) Or

      (Repeat (Rewrite ''ins_Nil'')) Or

      (Repeat (Rewrite ''ins_Cons'')) Or

      (Repeat (Rewrite ''sort_deff'')) Or

      (Repeat (Rewrite ''o_id'')) Or

      (Repeat (Rewrite ''o_assoc'')) Or

      (Repeat (Rewrite ''o_apply'')) Or

      (Repeat (Rewrite ''id_apply'')) Or

      (Repeat (Calculate ''le'')) Or

      (Repeat (Rewrite ''If_def'')) Or

      (Repeat (Rewrite ''if_True'')) Or

      (Repeat (Rewrite ''if_False'')))

    ) uns)"

setup \<open>KEStore_Elems.add_mets

   [MethodC.prep_input @{theory} "met_Prog_sort_ins_steps" [] MethodC.id_empty

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

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

        {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,

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

        @{thm sort_program2.simps})]

\<close>

subsection \<open>CAS-commands\<close>

ML \<open>

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

   combine this input with dataformat of pbt (without "#Given", etc):

*)

fun argl2dtss [t] =

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

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

     ]

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

\<close>

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

setup \<open>KEStore_Elems.add_cas

  [ ( @{term "Sort"},  

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

    )

  ]

\<close> ML \<open>

\<close> ML \<open>

\<close>

end