1.1 --- a/src/Tools/isac/IsacKnowledge/InsSort.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,63 +0,0 @@
     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