1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Fri Aug 26 12:02:43 2016 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Fri Aug 26 12:25:03 2016 +0200
     1.3 @@ -7,24 +7,24 @@
     1.4    sorted     :: "'a list => unl"
     1.5  
     1.6  (* subproblem and script-name *)
     1.7 -  Ins'_sort  :: "['a list,  
     1.8 -		    'a list] => 'a list"
     1.9 +  Ins'_sort  :: "['a xlist,  
    1.10 +		    'a xlist] => 'a xlist"
    1.11                 ("((Script Ins'_sort (_ =))//  
    1.12  		    (_))" 9)
    1.13 -  Sort       :: "['a list,  
    1.14 -		    'a list] => 'a list"
    1.15 +  Sort       :: "['a xlist,  
    1.16 +		    'a xlist] => 'a xlist"
    1.17                 ("((Script Sort (_ =))//  
    1.18  		    (_))" 9)
    1.19  
    1.20  subsection {* functions *}
    1.21 -primrec ins :: "int \<Rightarrow> int list \<Rightarrow> int list"
    1.22 +primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
    1.23  where
    1.24 -ins_Nil:  "ins i [] = [i]" |
    1.25 -ins_Cons: "ins i (x # xs) = (if i < x then (i # x # xs) else x # (ins i xs))"
    1.26 +ins_Nil:  "ins i [|| ||] = [||i||]" |
    1.27 +ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"
    1.28  
    1.29 -fun sort :: "int list \<Rightarrow> int list"
    1.30 +fun sort :: "int xlist \<Rightarrow> int xlist"
    1.31  where
    1.32 -sort_deff: "sort xs = foldr ins xs []"
    1.33 +sort_deff: "sort xs = xfoldr ins xs [|| ||]"
    1.34  print_theorems
    1.35  thm sort_def  (* InsSort.sort \<equiv> sort_sumC *)
    1.36  thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
    1.37 @@ -35,8 +35,8 @@
    1.38  @{thm ins.simps(2)};
    1.39  *}
    1.40  
    1.41 -value "sort [2,3,1]"
    1.42 -lemma test: "sort [2,3,1] = [1,2,3]"
    1.43 +value "sort [||2,3,1||]"
    1.44 +lemma test: "sort [||2,3,1||] = [||1,2,3||]"
    1.45  by simp
    1.46  
    1.47  subsection {* eval functions *}
    1.48 @@ -46,8 +46,8 @@
    1.49    Rls {
    1.50      id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = e_rls,
    1.51      srls = e_rls, calc = [], rules = [
    1.52 -      Thm ("foldr_Nil",(*num_str*) @{thm foldr_Nil} (* foldr ?f [] = id *)),
    1.53 -	    Thm ("foldr_Cons", @{thm foldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
    1.54 +      Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
    1.55 +	    Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
    1.56  
    1.57  	    Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
    1.58  	    Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
    1.59 @@ -96,7 +96,7 @@
    1.60        (["Programming","sort"], [],
    1.61          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
    1.62            crls = Atools_crls, errpats = [], nrls = norm_Rational},
    1.63 -        "Script Sort (u_u::'a list) = (Rewrite_Set ins_sort False) u_u")
    1.64 +        "Script Sort (u_u::'a xlist) = (Rewrite_Set ins_sort False) u_u")
    1.65    ]
    1.66  *}
    1.67  end