(* Title:  functions on lists for Programs

   Author: Walther Neuper 0108

   (c) due to copyright terms

*)

theory ListC 

imports "~~/src/Tools/isac/KEStore"

begin

ML_file "~~/src/Tools/isac/ProgLang/termC.sml"

ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"

ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"

ML {*

*} ML {*

*} 

subsection {* Notes on Isac's programming language *}

text {*

  Isac's programming language combines tacticals (TRY, etc) and 

  tactics (Rewrite, etc) with list processing.

  In order to distinguish list expressions of the meta (programming)

  language from the object language in Lucas-Interpretation, a 

  new 'type xlist' is introduced.

  TODO: Switch the role of 'xlist' and 'list' (the former only used

  by InsSort.thy)

  Isac's programming language preceeded the function package

  in 2002. For naming "axiomatization" is used for reasons of uniformity

  with the other replacements for "axioms".

  Another reminiscence from Isabelle2002 are Isac-specific numerals,

  introduced in order to have floating point numerals at a time, 

  when Isabelle did not consider that requirement. For the sake of uniformity

  'nat' from List.thy is replaced by 'real' by 'fun parse',

  however, 'fun parseNEW' has started to replace this fix (after finishing

  this fix, there will be a 'rename all parseNEW --> parse).

  Note: *one* "axiomatization" over all equations caused strange "'a list list"

  types.

*}

subsection {* Type 'xlist' for Lucas-Interpretation *}

(* cp fom ~~/src/HOL/List.thy

   TODO: ask for shorter deliminters in xlist *)

datatype  'a xlist =

    XNil  ("{|| ||}")

  | XCons (xhd: 'a)  (xtl: "'a xlist")  (infixr "@#" 65)

syntax

   \<comment> \<open>list Enumeration\<close>

  "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")

translations

  "{||x, xs||}" == "x@#{||xs||}"

  "{||x||}" == "x@#{|| ||}"

term "{|| ||}"

term "{||1,2,3||}"

subsection {* Functions for 'xlist' *}

(* TODO: 

(1) revise, if definition of identifiers like LENGTH_NIL are still required.

(2) switch the role of 'xlist' and 'list' in the functions below, in particular for

  'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.

  For transition phase just outcomment InsSort.thy and inssort.sml.

*)

primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where

xfoldr_Nil:  "xfoldr f {|| ||} = id" |

xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"

primrec LENGTH   :: "'a list => real"

where

LENGTH_NIL:	"LENGTH [] = 0" |

LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"

consts NTH ::  "[real, 'a list] => 'a"

axiomatization where

NTH_NIL: "NTH 1 (x # xs) = x" and

NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"

(* redefine together with identifiers (still) required for KEStore ..*)

axiomatization where

hd_thm:	"hd (x # xs) = x"

axiomatization where

tl_Nil:	"tl []  = []" and

tl_Cons: "tl (x # xs) = xs"

axiomatization where

LAST:	"last (x # xs) = (if xs = [] then x else last xs)"

axiomatization where

butlast_Nil: "butlast []    = []" and

butlast_Cons:	"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"

axiomatization where

map_Nil:"map f [] = []" and

map_Cons:	"map f (x # xs) = f x  #  map f xs"

axiomatization where

rev_Nil: "rev [] = []" and

rev_Cons:	"rev (x # xs) = rev xs @ [x]"

axiomatization where

filter_Nil:	"filter P [] = []" and

filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)" 

axiomatization where

concat_Nil:	"concat [] = []" and

concat_Cons: "concat (x # xs) = x @ concat xs"

axiomatization where

takeWhile_Nil: "takeWhile P []     = []" and

takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"

axiomatization where

dropWhile_Nil: "dropWhile P [] = []" and

dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"

axiomatization where

zip_Nil: "zip xs [] = []" and

zip_Cons:	"zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"

axiomatization where

distinct_Nil:	"distinct []     = True" and

distinct_Cons:	"distinct (x # xs) = (x ~: set xs & distinct xs)"

axiomatization where

remdups_Nil:	"remdups [] = []" and

remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

(** Lexicographic orderings on lists ...!!!**)

ML{* (*the former ListC.ML*)

(** rule set for evaluating listexpr in scripts **)

val list_rls = 

  Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

    erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],

    rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)

       Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),

       Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)

       Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),

       Rule.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),

       Rule.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),

(*       Thm ("butlast_Cons",num_str @{thm butlast_Cons}),

       Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)

       Rule.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),

       Rule.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),

(*       Rule.Thm ("del_base",num_str @{thm del_base}),

       Rule.Thm ("del_rec",num_str @{thm del_rec}), *)

       Rule.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),

       Rule.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),

       Rule.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),

       Rule.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),

       Rule.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),

       Rule.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),

       Rule.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),

       Rule.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),

       Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),

       Rule.Thm ("LAST",TermC.num_str @{thm LAST}),

       Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),

       Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),

(*       Rule.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)

       Rule.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),

       Rule.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),

(*       Rule.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),

       Rule.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)

(*       Rule.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),

       Rule.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)

       Rule.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),

       Rule.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),

       Rule.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),

       Rule.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),

       Rule.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),

       Rule.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),

       Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),

       Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),

       Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),

       Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],

    scr = Rule.EmptyScr}: Rule.rls;

*}

setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}

end