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