1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Fri Aug 26 12:02:43 2016 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Aug 26 12:25:03 2016 +0200
     1.3 @@ -11,23 +11,60 @@
     1.4  ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
     1.5  ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
     1.6  
     1.7 -text {* 
     1.8 -  This file gives names to equations of function definitions,
     1.9 -  which are required for Lucas-Interpretation (by Isac's rewriter) of 
    1.10 -  Isac's programming language. This language preceeded the function package
    1.11 +subsection {* Notes on Isac's programming language *}
    1.12 +text {*
    1.13 +  Isac's programming language combines tacticals (TRY, etc) and 
    1.14 +  tactics (Rewrite, etc) with list processing.
    1.15 +
    1.16 +  In order to distinguish list expressions of the meta (programming)
    1.17 +  language from the object language in Lucas-Interpretation, a 
    1.18 +  new 'type xlist' is introduced.
    1.19 +  TODO: Switch the role of 'xlist' and 'list' (the former only used
    1.20 +  by InsSort.thy)
    1.21 +
    1.22 +  Isac's programming language preceeded the function package
    1.23    in 2002. For naming "axiomatization" is used for reasons of uniformity
    1.24    with the other replacements for "axioms".
    1.25    Another reminiscence from Isabelle2002 are Isac-specific numerals,
    1.26    introduced in order to have floating point numerals at a time, 
    1.27    when Isabelle did not consider that requirement. For the sake of uniformity
    1.28 -  'nat' from List.thy is replaced by 'real'.
    1.29 +  'nat' from List.thy is replaced by 'real' by 'fun parse',
    1.30 +  however, 'fun parseNEW' has started to replace this fix (after finishing
    1.31 +  this fix, there will be a 'rename all parseNEW --> parse).
    1.32  
    1.33 -  TODO: shift name-declarations to HOL/List.thy, adopt new names from there
    1.34 -  and remove this ListC.thy.
    1.35    Note: *one* "axiomatization" over all equations caused strange "'a list list"
    1.36    types.
    1.37  *}
    1.38  
    1.39 +subsection {* Type 'xlist' for Lucas-Interpretation *}
    1.40 +(*TODO: ask for shorter deliminters in xlist *)
    1.41 +datatype 'a xlist =
    1.42 +    XNil    ("[|| ||]")
    1.43 +  | XCons 'a  "'a xlist"    (infixr "@#" 65)
    1.44 +
    1.45 +syntax
    1.46 +  -- {* list Enumeration *}
    1.47 +  "_xlist" :: "args => 'a xlist"    ("[||(_)||]")
    1.48 +
    1.49 +translations
    1.50 +  "[||x, xs||]" == "x@#[||xs||]"
    1.51 +  "[||x||]" == "x@#[|| ||]"
    1.52 +
    1.53 +term "[|| ||]"
    1.54 +term "[||1,2,3||]"
    1.55 +
    1.56 +subsection {* Functions for 'xlist' *}
    1.57 +(* TODO: 
    1.58 +(1) revise, if definition of identifiers like LENGTH_NIL are still required.
    1.59 +(2) switch the role of 'xlist' and 'list' in the functions below, in particular for
    1.60 +  'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
    1.61 +  For transition phase just outcomment InsSort.thy and inssort.sml.
    1.62 +*)
    1.63 +
    1.64 +primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.65 +xfoldr_Nil:  "xfoldr f [|| ||] = id" |
    1.66 +xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
    1.67 +
    1.68  primrec LENGTH   :: "'a list => real"
    1.69  where
    1.70  LENGTH_NIL:	"LENGTH [] = 0" |