
neuper@37965: (* Title:  functions on lists for Scripts
neuper@37965:    Author: Walther Neuper 0108
neuper@37965:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37947: theory ListC imports Complex_Main
neuper@41943: uses ("../library.sml")
neuper@41943:      ("../calcelems.sml")
neuper@48761:      ("termC.sml") ("calculate.sml") ("rewrite.sml")
neuper@37906: begin
neuper@48761: use "../library.sml"
neuper@48761: use "../calcelems.sml"
neuper@48761: use "termC.sml"
neuper@48761: use "calculate.sml"
neuper@48761: use "rewrite.sml"
neuper@37906: 
neuper@37906: text {* 'nat' in List.thy replaced by 'real' *}
neuper@37906: 
neuper@37997: primrec LENGTH   :: "'a list => real"
neuper@37906: where
neuper@37997:   LENGTH_NIL:	"LENGTH [] = 0"     (*length: 'a list => nat*)
neuper@37997: | LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
neuper@37906: 
neuper@37906: primrec del :: "['a list, 'a] => 'a list"
neuper@37906: where
neuper@37906:   del_base: "del [] x = []"
neuper@37906: | del_rec:  "del (y#ys) x = (if x = y then ys else y#(del ys x))"
neuper@37906: 
neuper@37906: definition
neuper@37906:   list_diff :: "['a list, 'a list] => 'a list"         (* as -- bs *)
neuper@37906:               ("(_ --/ _)" [66, 66] 65)
neuper@37906:   where "a -- b == foldl del a b"
neuper@37906:   
neuper@37997: consts NTH ::  "[real, 'a list] => 'a"
t@42197: 
t@42211: axioms(*axiomatization where*)
neuper@37906:  (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
t@42211:   NTH_NIL:      "NTH 1 (x#xs) = x" (*and*)
neuper@37997: (*  NTH_CONS:     "NTH n (x#xs) = NTH (n+ -1) xs"  *)
neuper@37906: 
neuper@37906: (*rewriter does not reach base case   ......    ;
neuper@37906:   the condition involves another rule set (erls, eval_binop in Atools):*)
t@42211:   NTH_CONS:     "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" (*and*)
neuper@37906: 
neuper@37906: (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
neuper@37906: (*primrec*)
t@42211:   hd_thm:	"hd(x#xs) = x" (*and*)
neuper@37906: (*primrec*)
t@42211:   tl_Nil:	"tl([])   = []" (*and*)
t@42211:   tl_Cons:		"tl(x#xs) = xs" (*and*)
neuper@37906: (*primrec*)
t@42211:   null_Nil:	"null([])   = True" (*and*)
t@42211:   null_Cons:	"null(x#xs) = False" (*and*)
neuper@37906: (*primrec*)
t@42211:   LAST:	"last(x#xs) = (if xs=[] then x else last xs)" (*and*)
neuper@37906: (*primrec*)
t@42211:   butlast_Nil:	"butlast []    = []" (*and*)
t@42211:   butlast_Cons:	"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" (*and*)
neuper@41899: (*primrec
neuper@37906:   mem_Nil:	"x mem []     = False"
neuper@37906:   mem_Cons:	"x mem (y#ys) = (if y=x then True else x mem ys)"
neuper@41899: *)
t@42211:   mem_Nil:	"x : set []     = False" (*and*)
t@42211:   mem_Cons:	"x : set (y#ys) = (if y=x then True else x : set ys)" (*and*)
neuper@37906: (*primrec-------already named---
neuper@37906:   "set [] = {}"
neuper@37906:   "set (x#xs) = insert x (set xs)"
neuper@37906:   primrec
neuper@37906:   list_all_Nil  "list_all P [] = True"
neuper@37906:   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
neuper@37906: ----------------*)
neuper@37906: (*primrec*)
t@42211:   map_Nil:	"map f []     = []" (*and*)
t@42211:   map_Cons:	"map f (x#xs) = f(x)#map f xs" (*and*)
neuper@37906: (*primrec*)
t@42211:   append_Nil:  "[]    @ys = ys" (*and*)
t@42211:   append_Cons: "(x#xs)@ys = x#(xs@ys)" (*and*)
neuper@37906: (*primrec*)
t@42211:   rev_Nil:	"rev([])   = []" (*and*)
t@42211:   rev_Cons:	"rev(x#xs) = rev(xs) @ [x]" (*and*)
neuper@37906: (*primrec*)
t@42211:   filter_Nil:	"filter P []     = []" (*and*)
t@42211:   filter_Cons:	"filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" (*and*)
neuper@37906: (*primrec-------already named---
neuper@37906:   foldl_Nil  "foldl f a [] = a"
neuper@37906:   foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
neuper@37906: ----------------*)
neuper@37906: (*primrec*)
t@42211:   foldr_Nil:	"foldr f [] a     = a" (*and*)
t@42211:   foldr_Cons:	"foldr f (x#xs) a = f x (foldr f xs a)" (*and*)
neuper@37906: (*primrec*)
t@42211:   concat_Nil:	"concat([])   = []" (*and*)
t@42211:   concat_Cons:	"concat(x#xs) = x @ concat(xs)" (*and*)
neuper@37906: (*primrec-------already named---
neuper@37906:   drop_Nil  "drop n [] = []"
neuper@37906:   drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
neuper@37906:   (* Warning: simpset does not contain this definition but separate theorems 
neuper@37906:      for n=0 / n=Suc k*)
neuper@37906: (*primrec*)
neuper@37906:   take_Nil  "take n [] = []"
neuper@37906:   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
neuper@37906:   (* Warning: simpset does not contain this definition but separate theorems 
neuper@37906:      for n=0 / n=Suc k*)
neuper@37906: (*primrec*) 
neuper@37906:   nth_Cons  "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
neuper@37906:   (* Warning: simpset does not contain this definition but separate theorems 
neuper@37906:      for n=0 / n=Suc k*)
neuper@37906: (*primrec*)
neuper@37906:  "    [][i:=v] = []"
neuper@37906:  "(x#xs)[i:=v] = (case i of 0     => v # xs 
neuper@37906: 			  | Suc j => x # xs[j:=v])"
neuper@37906: ----------------*)
neuper@37906: (*primrec*)
t@42211:   takeWhile_Nil:	"takeWhile P []     = []" (*and*)
neuper@37906:   takeWhile_Cons:
t@42211:   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" (*and*)
neuper@37906: (*primrec*)
t@42211:   dropWhile_Nil:	"dropWhile P []     = []" (*and*)
neuper@37906:   dropWhile_Cons:
t@42211:   "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" (*and*)
neuper@37906: (*primrec*)
t@42211:   zip_Nil:	"zip xs []     = []" (*and*)
t@42211:   zip_Cons:	"zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" (*and*)
neuper@37906:   (* Warning: simpset does not contain this definition but separate theorems 
neuper@37906:      for xs=[] / xs=z#zs *)
neuper@37906: (*primrec
neuper@37906:   upt_0   "[i..0(] = []"
neuper@37906:   upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
neuper@37906: *)
neuper@37906: (*primrec*)
t@42211:   distinct_Nil:	"distinct []     = True" (*and*)
t@42211:   distinct_Cons:	"distinct (x#xs) = (x ~: set xs & distinct xs)" (*and*)
neuper@37906: (*primrec*)
t@42211:   remdups_Nil:	"remdups [] = []" (*and*)
t@42197:   remdups_Cons:	"remdups (x#xs) = 
t@42197: 		 (if x : set xs then remdups xs else x # remdups xs)" 
neuper@37906: (*primrec-------already named---
neuper@37906:   replicate_0   "replicate  0      x = []"
neuper@37906:   replicate_Suc "replicate (Suc n) x = x # replicate n x"
neuper@37906: ----------------*)
neuper@37906: 
neuper@37906: (** Lexicographic orderings on lists ...!!!**)
neuper@37906: 
neuper@37947: ML{* (*the former ListC.ML*)
neuper@37906: (** rule set for evaluating listexpr in scripts **)
neuper@37906: val list_rls = 
neuper@37906:   Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
neuper@42458:       erls = Erls, srls = Erls, calc = [], errpatts = [],
neuper@37906:       rules = (*8.01: copied from*)
neuper@37966:       [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
neuper@37906:        Thm ("o_apply", num_str @{thm o_apply}),
neuper@37906: 
neuper@37906:        Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
neuper@37906:        Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
neuper@37906:        Thm ("append_Cons",num_str @{thm append_Cons}),
neuper@37906:        Thm ("append_Nil",num_str @{thm append_Nil}),
neuper@37906:        Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
neuper@37906:        Thm ("butlast_Nil",num_str @{thm butlast_Nil}),
neuper@37906:        Thm ("concat_Cons",num_str @{thm concat_Cons}),
neuper@37906:        Thm ("concat_Nil",num_str @{thm concat_Nil}),
neuper@37906:        Thm ("del_base",num_str @{thm del_base}),
neuper@37906:        Thm ("del_rec",num_str @{thm del_rec}),
neuper@37906: 
neuper@37906:        Thm ("distinct_Cons",num_str @{thm distinct_Cons}),
neuper@37906:        Thm ("distinct_Nil",num_str @{thm distinct_Nil}),
neuper@37906:        Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}),
neuper@37906:        Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}),
neuper@37906:        Thm ("filter_Cons",num_str @{thm filter_Cons}),
neuper@37906:        Thm ("filter_Nil",num_str @{thm filter_Nil}),
neuper@37906:        Thm ("foldr_Cons",num_str @{thm foldr_Cons}),
neuper@37906:        Thm ("foldr_Nil",num_str @{thm foldr_Nil}),
neuper@37906:        Thm ("hd_thm",num_str @{thm hd_thm}),
neuper@37906:        Thm ("LAST",num_str @{thm LAST}),
neuper@37906:        Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
neuper@37906:        Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
neuper@37906:        Thm ("list_diff_def",num_str @{thm list_diff_def}),
neuper@37906:        Thm ("map_Cons",num_str @{thm map_Cons}),
neuper@37906:        Thm ("map_Nil",num_str @{thm map_Cons}),
neuper@37906:        Thm ("mem_Cons",num_str @{thm mem_Cons}),
neuper@37906:        Thm ("mem_Nil",num_str @{thm mem_Nil}),
neuper@37906:        Thm ("null_Cons",num_str @{thm null_Cons}),
neuper@37906:        Thm ("null_Nil",num_str @{thm null_Nil}),
neuper@37906:        Thm ("remdups_Cons",num_str @{thm remdups_Cons}),
neuper@37906:        Thm ("remdups_Nil",num_str @{thm remdups_Nil}),
neuper@37906:        Thm ("rev_Cons",num_str @{thm rev_Cons}),
neuper@37906:        Thm ("rev_Nil",num_str @{thm rev_Nil}),
neuper@37906:        Thm ("take_Nil",num_str @{thm take_Nil}),
neuper@37906:        Thm ("take_Cons",num_str @{thm take_Cons}),
neuper@37906:        Thm ("tl_Cons",num_str @{thm tl_Cons}),
neuper@37906:        Thm ("tl_Nil",num_str @{thm tl_Nil}),
neuper@37906:        Thm ("zip_Cons",num_str @{thm zip_Cons}),
neuper@37906:        Thm ("zip_Nil",num_str @{thm zip_Nil})
neuper@37906:        ], scr = EmptyScr}:rls;
neuper@37906: *}
neuper@37906: 
neuper@37906: ML{*
neuper@37906: ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37906:   [("list_rls",list_rls)
neuper@37906:    ]);
neuper@37906: *}
neuper@37906: end




