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 |
|
wenzelm@60192
|
6 |
theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
wneuper@59586
|
7 |
|
neuper@37906
|
8 |
begin
|
neuper@52122
|
9 |
|
walther@59630
|
10 |
text \<open>Abstract:
|
walther@59630
|
11 |
There are examples in the Knowledge, which demonstrate list processing, e.g. InsSort.thy.
|
neuper@37906
|
12 |
|
walther@59630
|
13 |
Lists in example calculations must have a different type for list processing in Isac programs.
|
walther@59630
|
14 |
Presently the lists in examples have a new type xlist with the unfamiliar list
|
walther@59630
|
15 |
notation "{||a, b, c||}". One could expect math-authors to use such unfamiliar notation
|
walther@59630
|
16 |
and expose students to familiar notation in calculations, and not vice versa as done presently.
|
wneuper@59234
|
17 |
|
walther@59630
|
18 |
Thus this theory resides in ProgLang so far.
|
wneuper@59472
|
19 |
\<close>
|
neuper@37906
|
20 |
|
walther@59620
|
21 |
subsection \<open>General constants\<close>
|
walther@59620
|
22 |
consts
|
walther@59620
|
23 |
EmptyList :: "bool list"
|
walther@59620
|
24 |
UniversalList :: "bool list"
|
walther@59620
|
25 |
|
walther@59620
|
26 |
ML \<open>
|
walther@59620
|
27 |
\<close> ML \<open>
|
walther@60339
|
28 |
val UniversalList = TermC.parseNEW'' @{theory} "UniversalList";
|
walther@60339
|
29 |
val EmptyList = TermC.parseNEW'' @{theory} "[]::bool list";
|
walther@59620
|
30 |
\<close> ML \<open>
|
walther@59620
|
31 |
\<close>
|
walther@59620
|
32 |
|
walther@59620
|
33 |
subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close>
|
wneuper@59457
|
34 |
(* cp fom ~~/src/HOL/List.thy
|
wneuper@59457
|
35 |
TODO: ask for shorter deliminters in xlist *)
|
wneuper@59457
|
36 |
datatype 'a xlist =
|
wneuper@59457
|
37 |
XNil ("{|| ||}")
|
wneuper@59457
|
38 |
| XCons (xhd: 'a) (xtl: "'a xlist") (infixr "@#" 65)
|
wneuper@59234
|
39 |
|
wneuper@59234
|
40 |
syntax
|
wneuper@59457
|
41 |
\<comment> \<open>list Enumeration\<close>
|
wneuper@59244
|
42 |
"_xlist" :: "args => 'a xlist" ("{|| (_) ||}")
|
wneuper@59234
|
43 |
|
wneuper@59234
|
44 |
translations
|
wneuper@59244
|
45 |
"{||x, xs||}" == "x@#{||xs||}"
|
wneuper@59244
|
46 |
"{||x||}" == "x@#{|| ||}"
|
wneuper@59234
|
47 |
|
wneuper@59244
|
48 |
term "{|| ||}"
|
wneuper@59244
|
49 |
term "{||1,2,3||}"
|
wneuper@59234
|
50 |
|
wneuper@59472
|
51 |
subsection \<open>Functions for 'xlist'\<close>
|
wneuper@59234
|
52 |
(* TODO:
|
wneuper@59234
|
53 |
(1) revise, if definition of identifiers like LENGTH_NIL are still required.
|
wneuper@59234
|
54 |
(2) switch the role of 'xlist' and 'list' in the functions below, in particular for
|
wneuper@59234
|
55 |
'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
|
wneuper@59234
|
56 |
For transition phase just outcomment InsSort.thy and inssort.sml.
|
wneuper@59234
|
57 |
*)
|
wneuper@59234
|
58 |
|
wneuper@59234
|
59 |
primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
|
wneuper@59244
|
60 |
xfoldr_Nil: "xfoldr f {|| ||} = id" |
|
wneuper@59234
|
61 |
xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
|
wneuper@59234
|
62 |
|
walther@60121
|
63 |
primrec Length :: "'a list => real"
|
neuper@37906
|
64 |
where
|
walther@60121
|
65 |
LENGTH_NIL: "Length [] = 0" |
|
walther@60121
|
66 |
LENGTH_CONS: "Length (x#xs) = 1 + Length xs"
|
neuper@37906
|
67 |
|
walther@59620
|
68 |
subsection \<open>Functions for 'list'\<close>
|
walther@59620
|
69 |
|
neuper@52148
|
70 |
consts NTH :: "[real, 'a list] => 'a"
|
neuper@52148
|
71 |
axiomatization where
|
neuper@52148
|
72 |
NTH_NIL: "NTH 1 (x # xs) = x" and
|
neuper@52148
|
73 |
NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
|
neuper@37906
|
74 |
|
walther@59887
|
75 |
(* redefine together with identifiers (still) required for Know_Store ..*)
|
neuper@52148
|
76 |
axiomatization where
|
neuper@52148
|
77 |
hd_thm: "hd (x # xs) = x"
|
t@42197
|
78 |
|
neuper@52148
|
79 |
axiomatization where
|
neuper@52148
|
80 |
tl_Nil: "tl [] = []" and
|
neuper@52148
|
81 |
tl_Cons: "tl (x # xs) = xs"
|
neuper@37906
|
82 |
|
neuper@52148
|
83 |
axiomatization where
|
neuper@52148
|
84 |
LAST: "last (x # xs) = (if xs = [] then x else last xs)"
|
neuper@37906
|
85 |
|
neuper@52148
|
86 |
axiomatization where
|
neuper@52148
|
87 |
butlast_Nil: "butlast [] = []" and
|
neuper@52148
|
88 |
butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
|
neuper@52148
|
89 |
|
neuper@52148
|
90 |
axiomatization where
|
neuper@52148
|
91 |
map_Nil:"map f [] = []" and
|
neuper@52148
|
92 |
map_Cons: "map f (x # xs) = f x # map f xs"
|
neuper@52148
|
93 |
|
neuper@52148
|
94 |
axiomatization where
|
neuper@52148
|
95 |
rev_Nil: "rev [] = []" and
|
neuper@52148
|
96 |
rev_Cons: "rev (x # xs) = rev xs @ [x]"
|
neuper@52148
|
97 |
|
neuper@52148
|
98 |
axiomatization where
|
neuper@52148
|
99 |
filter_Nil: "filter P [] = []" and
|
neuper@52148
|
100 |
filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
|
neuper@52148
|
101 |
|
neuper@52148
|
102 |
axiomatization where
|
neuper@52148
|
103 |
concat_Nil: "concat [] = []" and
|
neuper@52148
|
104 |
concat_Cons: "concat (x # xs) = x @ concat xs"
|
neuper@52148
|
105 |
|
neuper@52148
|
106 |
axiomatization where
|
neuper@52148
|
107 |
takeWhile_Nil: "takeWhile P [] = []" and
|
neuper@52148
|
108 |
takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
|
neuper@52148
|
109 |
|
neuper@52148
|
110 |
axiomatization where
|
neuper@52148
|
111 |
dropWhile_Nil: "dropWhile P [] = []" and
|
neuper@52148
|
112 |
dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
|
neuper@52148
|
113 |
|
neuper@52148
|
114 |
axiomatization where
|
neuper@52148
|
115 |
zip_Nil: "zip xs [] = []" and
|
neuper@52148
|
116 |
zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
|
neuper@52148
|
117 |
|
neuper@52148
|
118 |
axiomatization where
|
neuper@52148
|
119 |
distinct_Nil: "distinct [] = True" and
|
neuper@52148
|
120 |
distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
|
neuper@52148
|
121 |
|
neuper@52148
|
122 |
axiomatization where
|
neuper@52148
|
123 |
remdups_Nil: "remdups [] = []" and
|
neuper@52148
|
124 |
remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
|
neuper@37906
|
125 |
|
wneuper@59602
|
126 |
consts lastI :: "'a list \<Rightarrow> 'a"
|
wneuper@59602
|
127 |
axiomatization where
|
wneuper@59602
|
128 |
last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
|
wneuper@59602
|
129 |
|
walther@59620
|
130 |
subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
|
walther@59620
|
131 |
ML \<open>
|
walther@59630
|
132 |
\<close> ML \<open>
|
walther@59850
|
133 |
val prog_expr =
|
walther@59857
|
134 |
Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@59851
|
135 |
erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
|
walther@60337
|
136 |
rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
|
walther@60337
|
137 |
Rule_Def.Thm ("o_apply", @{thm o_apply}),
|
neuper@37906
|
138 |
|
walther@60337
|
139 |
Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
|
walther@60337
|
140 |
Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}),
|
walther@60337
|
141 |
Rule_Def.Thm ("append_Cons", @{thm append_Cons}),
|
walther@60337
|
142 |
Rule_Def.Thm ("append_Nil", @{thm append_Nil}),
|
neuper@52148
|
143 |
(* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
|
neuper@52148
|
144 |
Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
|
walther@60337
|
145 |
Rule_Def.Thm ("concat_Cons", @{thm concat_Cons}),
|
walther@60337
|
146 |
Rule_Def.Thm ("concat_Nil", @{thm concat_Nil}),
|
walther@59850
|
147 |
(* Rule_Def.Thm ("del_base",num_str @{thm del_base}),
|
walther@59850
|
148 |
Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *)
|
neuper@37906
|
149 |
|
walther@60337
|
150 |
Rule_Def.Thm ("distinct_Cons", @{thm distinct_Cons}),
|
walther@60337
|
151 |
Rule_Def.Thm ("distinct_Nil", @{thm distinct_Nil}),
|
walther@60337
|
152 |
Rule_Def.Thm ("dropWhile_Cons", @{thm dropWhile_Cons}),
|
walther@60337
|
153 |
Rule_Def.Thm ("dropWhile_Nil", @{thm dropWhile_Nil}),
|
walther@60337
|
154 |
Rule_Def.Thm ("filter_Cons", @{thm filter_Cons}),
|
walther@60337
|
155 |
Rule_Def.Thm ("filter_Nil", @{thm filter_Nil}),
|
walther@60337
|
156 |
Rule_Def.Thm ("foldr_Cons", @{thm foldr_Cons}),
|
walther@60337
|
157 |
Rule_Def.Thm ("foldr_Nil", @{thm foldr_Nil}),
|
walther@60337
|
158 |
Rule_Def.Thm ("hd_thm", @{thm hd_thm}),
|
walther@60337
|
159 |
Rule_Def.Thm ("LAST", @{thm LAST}),
|
walther@60337
|
160 |
Rule_Def.Thm ("LENGTH_CONS", @{thm LENGTH_CONS}),
|
walther@60337
|
161 |
Rule_Def.Thm ("LENGTH_NIL", @{thm LENGTH_NIL}),
|
walther@59850
|
162 |
(* Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
|
walther@60337
|
163 |
Rule_Def.Thm ("map_Cons", @{thm map_Cons}),
|
walther@60337
|
164 |
Rule_Def.Thm ("map_Nil", @{thm map_Cons}),
|
walther@60337
|
165 |
(* Rule_Def.Thm ("mem_Cons", @{thm mem_Cons}),
|
walther@60337
|
166 |
Rule_Def.Thm ("mem_Nil", @{thm mem_Nil}), *)
|
walther@60337
|
167 |
(* Rule_Def.Thm ("null_Cons", @{thm null_Cons}),
|
walther@60337
|
168 |
Rule_Def.Thm ("null_Nil", @{thm null_Nil}),*)
|
walther@60337
|
169 |
Rule_Def.Thm ("remdups_Cons", @{thm remdups_Cons}),
|
walther@60337
|
170 |
Rule_Def.Thm ("remdups_Nil", @{thm remdups_Nil}),
|
walther@60337
|
171 |
Rule_Def.Thm ("rev_Cons", @{thm rev_Cons}),
|
walther@60337
|
172 |
Rule_Def.Thm ("rev_Nil", @{thm rev_Nil}),
|
walther@60337
|
173 |
Rule_Def.Thm ("take_Nil", @{thm take_Nil}),
|
walther@60337
|
174 |
Rule_Def.Thm ("take_Cons", @{thm take_Cons}),
|
walther@60337
|
175 |
Rule_Def.Thm ("tl_Cons", @{thm tl_Cons}),
|
walther@60337
|
176 |
Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}),
|
walther@60337
|
177 |
Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}),
|
walther@60337
|
178 |
Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})],
|
walther@59878
|
179 |
scr = Rule_Def.Empty_Prog}: Rule_Set.T;
|
wneuper@59472
|
180 |
\<close>
|
wenzelm@60289
|
181 |
rule_set_knowledge prog_expr = prog_expr
|
neuper@52122
|
182 |
|
walther@60278
|
183 |
ML \<open>
|
walther@60278
|
184 |
\<close> ML \<open>
|
walther@60278
|
185 |
\<close> ML \<open>
|
walther@60278
|
186 |
\<close>
|
neuper@37906
|
187 |
end
|