1 (* Title: functions on lists for Programs
2 Author: Walther Neuper 0108
3 (c) due to copyright terms
7 imports Complex_Main "~~/src/Tools/isac/KEStore"
10 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
11 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
12 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
14 text {* 'nat' in List.thy replaced by 'real' *}
16 primrec LENGTH :: "'a list => real"
18 LENGTH_NIL: "LENGTH [] = 0" (*length: 'a list => nat*)
19 | LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
21 primrec del :: "['a list, 'a] => 'a list"
23 del_base: "del [] x = []"
24 | del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))"
27 list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *)
28 ("(_ --/ _)" [66, 66] 65)
29 where "a -- b == foldl del a b"
31 consts NTH :: "[real, 'a list] => 'a"
33 axioms(*axiomatization where*)
34 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
35 NTH_NIL: "NTH 1 (x#xs) = x" (*and*)
36 (* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
38 (*rewriter does not reach base case ...... ;
39 the condition involves another rule set (erls, eval_binop in Atools):*)
40 NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" (*and*)
42 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
44 hd_thm: "hd(x#xs) = x" (*and*)
46 tl_Nil: "tl([]) = []" (*and*)
47 tl_Cons: "tl(x#xs) = xs" (*and*)
49 null_Nil: "null([]) = True" (*and*)
50 null_Cons: "null(x#xs) = False" (*and*)
52 LAST: "last(x#xs) = (if xs=[] then x else last xs)" (*and*)
54 butlast_Nil: "butlast [] = []" (*and*)
55 butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" (*and*)
57 mem_Nil: "x mem [] = False"
58 mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
60 mem_Nil: "x : set [] = False" (*and*)
61 mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" (*and*)
62 (*primrec-------already named---
64 "set (x#xs) = insert x (set xs)"
66 list_all_Nil "list_all P [] = True"
67 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
70 map_Nil: "map f [] = []" (*and*)
71 map_Cons: "map f (x#xs) = f(x)#map f xs" (*and*)
73 append_Nil: "[] @ys = ys" (*and*)
74 append_Cons: "(x#xs)@ys = x#(xs@ys)" (*and*)
76 rev_Nil: "rev([]) = []" (*and*)
77 rev_Cons: "rev(x#xs) = rev(xs) @ [x]" (*and*)
79 filter_Nil: "filter P [] = []" (*and*)
80 filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" (*and*)
81 (*primrec-------already named---
82 foldl_Nil "foldl f a [] = a"
83 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
86 foldr_Nil: "foldr f [] a = a" (*and*)
87 foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" (*and*)
89 concat_Nil: "concat([]) = []" (*and*)
90 concat_Cons: "concat(x#xs) = x @ concat(xs)" (*and*)
91 (*primrec-------already named---
92 drop_Nil "drop n [] = []"
93 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
94 (* Warning: simpset does not contain this definition but separate theorems
97 take_Nil "take n [] = []"
98 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
99 (* Warning: simpset does not contain this definition but separate theorems
102 nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
103 (* Warning: simpset does not contain this definition but separate theorems
107 "(x#xs)[i:=v] = (case i of 0 => v # xs
108 | Suc j => x # xs[j:=v])"
111 takeWhile_Nil: "takeWhile P [] = []" (*and*)
113 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" (*and*)
115 dropWhile_Nil: "dropWhile P [] = []" (*and*)
117 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" (*and*)
119 zip_Nil: "zip xs [] = []" (*and*)
120 zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" (*and*)
121 (* Warning: simpset does not contain this definition but separate theorems
122 for xs=[] / xs=z#zs *)
125 upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
128 distinct_Nil: "distinct [] = True" (*and*)
129 distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" (*and*)
131 remdups_Nil: "remdups [] = []" (*and*)
132 remdups_Cons: "remdups (x#xs) =
133 (if x : set xs then remdups xs else x # remdups xs)"
134 (*primrec-------already named---
135 replicate_0 "replicate 0 x = []"
136 replicate_Suc "replicate (Suc n) x = x # replicate n x"
139 (** Lexicographic orderings on lists ...!!!**)
141 ML{* (*the former ListC.ML*)
142 (** rule set for evaluating listexpr in scripts **)
144 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
145 erls = Erls, srls = Erls, calc = [], errpatts = [],
146 rules = (*8.01: copied from*)
147 [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
148 Thm ("o_apply", num_str @{thm o_apply}),
150 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
151 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
152 Thm ("append_Cons",num_str @{thm append_Cons}),
153 Thm ("append_Nil",num_str @{thm append_Nil}),
154 Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
155 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),
156 Thm ("concat_Cons",num_str @{thm concat_Cons}),
157 Thm ("concat_Nil",num_str @{thm concat_Nil}),
158 Thm ("del_base",num_str @{thm del_base}),
159 Thm ("del_rec",num_str @{thm del_rec}),
161 Thm ("distinct_Cons",num_str @{thm distinct_Cons}),
162 Thm ("distinct_Nil",num_str @{thm distinct_Nil}),
163 Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}),
164 Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}),
165 Thm ("filter_Cons",num_str @{thm filter_Cons}),
166 Thm ("filter_Nil",num_str @{thm filter_Nil}),
167 Thm ("foldr_Cons",num_str @{thm foldr_Cons}),
168 Thm ("foldr_Nil",num_str @{thm foldr_Nil}),
169 Thm ("hd_thm",num_str @{thm hd_thm}),
170 Thm ("LAST",num_str @{thm LAST}),
171 Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
172 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
173 Thm ("list_diff_def",num_str @{thm list_diff_def}),
174 Thm ("map_Cons",num_str @{thm map_Cons}),
175 Thm ("map_Nil",num_str @{thm map_Cons}),
176 Thm ("mem_Cons",num_str @{thm mem_Cons}),
177 Thm ("mem_Nil",num_str @{thm mem_Nil}),
178 Thm ("null_Cons",num_str @{thm null_Cons}),
179 Thm ("null_Nil",num_str @{thm null_Nil}),
180 Thm ("remdups_Cons",num_str @{thm remdups_Cons}),
181 Thm ("remdups_Nil",num_str @{thm remdups_Nil}),
182 Thm ("rev_Cons",num_str @{thm rev_Cons}),
183 Thm ("rev_Nil",num_str @{thm rev_Nil}),
184 Thm ("take_Nil",num_str @{thm take_Nil}),
185 Thm ("take_Cons",num_str @{thm take_Cons}),
186 Thm ("tl_Cons",num_str @{thm tl_Cons}),
187 Thm ("tl_Nil",num_str @{thm tl_Nil}),
188 Thm ("zip_Cons",num_str @{thm zip_Cons}),
189 Thm ("zip_Nil",num_str @{thm zip_Nil})
190 ], scr = EmptyScr}:rls;
194 ruleset' := overwritelthy @{theory} (!ruleset',
195 [("list_rls",list_rls)
198 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
200 ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF Theory_Data*)*}
202 (* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
203 AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
204 HERE IS ME_Isa: 'eval_rls' not in system ...*)
205 assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)