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