(* Title:  functions on lists for Programs

    Author: Walther Neuper 0108

    (c) due to copyright terms

 *)

 theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"

 begin

 text \<open>Abstract:

   There are examples in the Knowledge, which demonstrate list processing, e.g. InsSort.thy.

   Lists in example calculations must have a different type for list processing in Isac programs.

   Presently the lists in examples have a new type xlist with the unfamiliar list

   notation "{||a, b, c||}". One could expect math-authors to use such unfamiliar notation 

   and expose students to familiar notation in calculations, and not vice versa as done presently.

   Thus this theory resides in ProgLang so far.

 \<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>

 \<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