(* Title:  functions on lists for Programs

   Author: Walther Neuper 0108

   (c) due to copyright terms

*)

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

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 Know_Store ..*)

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 prog_expr =

  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 

    erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],

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

       Rule_Def.Thm ("o_apply", ThmC_Def.numerals_to_Free @{thm o_apply}),

       Rule_Def.Thm ("NTH_CONS",ThmC_Def.numerals_to_Free @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)

       Rule_Def.Thm ("NTH_NIL",ThmC_Def.numerals_to_Free @{thm NTH_NIL}),

       Rule_Def.Thm ("append_Cons",ThmC_Def.numerals_to_Free @{thm append_Cons}),

       Rule_Def.Thm ("append_Nil",ThmC_Def.numerals_to_Free @{thm append_Nil}),

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

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

       Rule_Def.Thm ("concat_Cons",ThmC_Def.numerals_to_Free @{thm concat_Cons}),

       Rule_Def.Thm ("concat_Nil",ThmC_Def.numerals_to_Free @{thm concat_Nil}),

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

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

       Rule_Def.Thm ("distinct_Cons",ThmC_Def.numerals_to_Free @{thm distinct_Cons}),

       Rule_Def.Thm ("distinct_Nil",ThmC_Def.numerals_to_Free @{thm distinct_Nil}),

       Rule_Def.Thm ("dropWhile_Cons",ThmC_Def.numerals_to_Free @{thm dropWhile_Cons}),

       Rule_Def.Thm ("dropWhile_Nil",ThmC_Def.numerals_to_Free @{thm dropWhile_Nil}),

       Rule_Def.Thm ("filter_Cons",ThmC_Def.numerals_to_Free @{thm filter_Cons}),

       Rule_Def.Thm ("filter_Nil",ThmC_Def.numerals_to_Free @{thm filter_Nil}),

       Rule_Def.Thm ("foldr_Cons",ThmC_Def.numerals_to_Free @{thm foldr_Cons}),

       Rule_Def.Thm ("foldr_Nil",ThmC_Def.numerals_to_Free @{thm foldr_Nil}),

       Rule_Def.Thm ("hd_thm",ThmC_Def.numerals_to_Free @{thm hd_thm}),

       Rule_Def.Thm ("LAST",ThmC_Def.numerals_to_Free @{thm LAST}),

       Rule_Def.Thm ("LENGTH_CONS",ThmC_Def.numerals_to_Free @{thm LENGTH_CONS}),

       Rule_Def.Thm ("LENGTH_NIL",ThmC_Def.numerals_to_Free @{thm LENGTH_NIL}),

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

       Rule_Def.Thm ("map_Cons",ThmC_Def.numerals_to_Free @{thm map_Cons}),

       Rule_Def.Thm ("map_Nil",ThmC_Def.numerals_to_Free @{thm map_Cons}),

(*       Rule_Def.Thm ("mem_Cons",ThmC_Def.numerals_to_Free @{thm mem_Cons}),

       Rule_Def.Thm ("mem_Nil",ThmC_Def.numerals_to_Free @{thm mem_Nil}), *)

(*       Rule_Def.Thm ("null_Cons",ThmC_Def.numerals_to_Free @{thm null_Cons}),

       Rule_Def.Thm ("null_Nil",ThmC_Def.numerals_to_Free @{thm null_Nil}),*)

       Rule_Def.Thm ("remdups_Cons",ThmC_Def.numerals_to_Free @{thm remdups_Cons}),

       Rule_Def.Thm ("remdups_Nil",ThmC_Def.numerals_to_Free @{thm remdups_Nil}),

       Rule_Def.Thm ("rev_Cons",ThmC_Def.numerals_to_Free @{thm rev_Cons}),

       Rule_Def.Thm ("rev_Nil",ThmC_Def.numerals_to_Free @{thm rev_Nil}),

       Rule_Def.Thm ("take_Nil",ThmC_Def.numerals_to_Free @{thm take_Nil}),

       Rule_Def.Thm ("take_Cons",ThmC_Def.numerals_to_Free @{thm take_Cons}),

       Rule_Def.Thm ("tl_Cons",ThmC_Def.numerals_to_Free @{thm tl_Cons}),

       Rule_Def.Thm ("tl_Nil",ThmC_Def.numerals_to_Free @{thm tl_Nil}),

       Rule_Def.Thm ("zip_Cons",ThmC_Def.numerals_to_Free @{thm zip_Cons}),

       Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})],

    scr = Rule_Def.Empty_Prog}: Rule_Set.T;

\<close>

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

end