(* Title:  functions on lists for Programs

    Author: Walther Neuper 0108

    (c) due to copyright terms

 *)

 theory ListC imports KEStore

 begin

 ML_file termC.sml

 ML_file contextC.sml

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 subsection \<open>Notes on Isac's programming language\<close>

 text \<open>

   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.

 \<close>

 subsection \<open>General constants\<close>

 consts

   EmptyList :: "bool list" 

   UniversalList :: "bool list" 

 ML \<open>

 \<close> ML \<open>

 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";

 val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";     

 \<close> ML \<open>

 \<close>

 subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close>

 (* 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 \<open>Functions for 'xlist'\<close>

 (* 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"

 subsection \<open>Functions for 'list'\<close>

 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)" 

 consts lastI :: "'a list \<Rightarrow> 'a"

 axiomatization where

 last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"

 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>

 ML \<open>

 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;

 \<close>

 setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>

 end