1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/IsacKnowledge/InsSort.thy Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,63 @@
1.4 +(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
1.5 +
1.6 +Proving equations for primrec function(s) "InsSort.foldr" ...
1.7 +GC #1.17.30.54.345.21479: (10 ms)
1.8 +*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
1.9 +*** imposes additional sort constraints on the declared type of the constant
1.10 +*** The error(s) above occurred in definition "InsSort.ins.ins_list_def (@@@)"
1.11 +*)
1.12 +
1.13 +(* insertion sort, would need lists different from script-lists WN.11.00
1.14 +WN.7.5.03: -"- started with someList :: 'a list => unl, fun dest_list
1.15 +WN.8.5.03: error (@@@) remained with outcommenting foldr ?!?
1.16 +
1.17 + use_thy_only"IsacKnowledge/InsSort";
1.18 +
1.19 +*)
1.20 +
1.21 +InsSort = Script +
1.22 +
1.23 +consts
1.24 +
1.25 +(*foldr :: [['a,'b] => 'a, 'b list, 'a] => 'a
1.26 +WN.8.5.03: already defined in Isabelle2002 (instantiated by Typefix):
1.27 + "[[real, real] => real, real list, real] => real") : term
1.28 +
1.29 + val t = str2term "foldr";
1.30 +val t =
1.31 + Const
1.32 + ("List.foldr",
1.33 + "[[RealDef.real, RealDef.real] => RealDef.real, RealDef.real List.list,
1.34 + RealDef.real] => RealDef.real") : term
1.35 + *)
1.36 + ins :: ['a list,'a] => 'a list
1.37 + sort :: 'a list => 'a list
1.38 +
1.39 +(*descriptions, script-id*)
1.40 + unsorted :: 'a list => unl
1.41 + sorted :: 'a list => unl
1.42 +
1.43 +(*subproblem and script-name*)
1.44 + Ins'_sort :: "['a list, \
1.45 + \ 'a list] => 'a list"
1.46 + ("((Script Ins'_sort (_ =))// \
1.47 + \ (_))" 9)
1.48 + Sort :: "['a list, \
1.49 + \ 'a list] => 'a list"
1.50 + ("((Script Sort (_ =))// \
1.51 + \ (_))" 9)
1.52 +
1.53 +(*primrec
1.54 + foldr_base "foldr f [] a = a"
1.55 + foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)"
1.56 +*)
1.57 +
1.58 +rules
1.59 +
1.60 +(*primrec .. outcommented analoguous to ListG.thy*)
1.61 + ins_base "ins [] a = [a]"
1.62 + ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"
1.63 +
1.64 + sort_def "sort ls = foldr ins ls []"
1.65 +
1.66 +end