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@52148
|
14 |
text {*
|
neuper@52148
|
15 |
This file gives names to equations of function definitions,
|
neuper@52148
|
16 |
which are required for Lucas-Interpretation (by Isac's rewriter) of
|
neuper@52148
|
17 |
Isac's programming language. This language preceeded the function package
|
neuper@52148
|
18 |
in 2002. For naming "axiomatization" is used for reasons of uniformity
|
neuper@52148
|
19 |
with the other replacements for "axioms".
|
neuper@52148
|
20 |
Another reminiscence from Isabelle2002 are Isac-specific numerals,
|
neuper@52148
|
21 |
introduced in order to have floating point numerals at a time,
|
neuper@52148
|
22 |
when Isabelle did not consider that requirement. For the sake of uniformity
|
neuper@52148
|
23 |
'nat' from List.thy is replaced by 'real'.
|
neuper@52148
|
24 |
|
neuper@52148
|
25 |
TODO: shift name-declarations to HOL/List.thy, adopt new names from there
|
neuper@52148
|
26 |
and remove this ListC.thy.
|
neuper@52148
|
27 |
Note: *one* "axiomatization" over all equations caused strange "'a list list"
|
neuper@52148
|
28 |
types.
|
neuper@52148
|
29 |
*}
|
neuper@37906
|
30 |
|
neuper@37997
|
31 |
primrec LENGTH :: "'a list => real"
|
neuper@37906
|
32 |
where
|
neuper@52148
|
33 |
LENGTH_NIL: "LENGTH [] = 0" |
|
neuper@52148
|
34 |
LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
|
neuper@37906
|
35 |
|
neuper@52148
|
36 |
consts NTH :: "[real, 'a list] => 'a"
|
neuper@52148
|
37 |
axiomatization where
|
neuper@52148
|
38 |
NTH_NIL: "NTH 1 (x # xs) = x" and
|
neuper@52148
|
39 |
NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
|
neuper@37906
|
40 |
|
neuper@52148
|
41 |
axiomatization where
|
neuper@52148
|
42 |
hd_thm: "hd (x # xs) = x"
|
t@42197
|
43 |
|
neuper@52148
|
44 |
axiomatization where
|
neuper@52148
|
45 |
tl_Nil: "tl [] = []" and
|
neuper@52148
|
46 |
tl_Cons: "tl (x # xs) = xs"
|
neuper@37906
|
47 |
|
neuper@52148
|
48 |
axiomatization where
|
neuper@52148
|
49 |
LAST: "last (x # xs) = (if xs = [] then x else last xs)"
|
neuper@37906
|
50 |
|
neuper@52148
|
51 |
axiomatization where
|
neuper@52148
|
52 |
butlast_Nil: "butlast [] = []" and
|
neuper@52148
|
53 |
butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
|
neuper@52148
|
54 |
|
neuper@52148
|
55 |
axiomatization where
|
neuper@52148
|
56 |
map_Nil:"map f [] = []" and
|
neuper@52148
|
57 |
map_Cons: "map f (x # xs) = f x # map f xs"
|
neuper@52148
|
58 |
|
neuper@52148
|
59 |
axiomatization where
|
neuper@52148
|
60 |
rev_Nil: "rev [] = []" and
|
neuper@52148
|
61 |
rev_Cons: "rev (x # xs) = rev xs @ [x]"
|
neuper@52148
|
62 |
|
neuper@52148
|
63 |
axiomatization where
|
neuper@52148
|
64 |
filter_Nil: "filter P [] = []" and
|
neuper@52148
|
65 |
filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
|
neuper@52148
|
66 |
|
neuper@52148
|
67 |
axiomatization where
|
neuper@52148
|
68 |
concat_Nil: "concat [] = []" and
|
neuper@52148
|
69 |
concat_Cons: "concat (x # xs) = x @ concat xs"
|
neuper@52148
|
70 |
|
neuper@52148
|
71 |
axiomatization where
|
neuper@52148
|
72 |
takeWhile_Nil: "takeWhile P [] = []" and
|
neuper@52148
|
73 |
takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
|
neuper@52148
|
74 |
|
neuper@52148
|
75 |
axiomatization where
|
neuper@52148
|
76 |
dropWhile_Nil: "dropWhile P [] = []" and
|
neuper@52148
|
77 |
dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
|
neuper@52148
|
78 |
|
neuper@52148
|
79 |
axiomatization where
|
neuper@52148
|
80 |
zip_Nil: "zip xs [] = []" and
|
neuper@52148
|
81 |
zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
|
neuper@52148
|
82 |
|
neuper@52148
|
83 |
axiomatization where
|
neuper@52148
|
84 |
distinct_Nil: "distinct [] = True" and
|
neuper@52148
|
85 |
distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
|
neuper@52148
|
86 |
|
neuper@52148
|
87 |
axiomatization where
|
neuper@52148
|
88 |
remdups_Nil: "remdups [] = []" and
|
neuper@52148
|
89 |
remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
|
neuper@37906
|
90 |
|
neuper@37906
|
91 |
(** Lexicographic orderings on lists ...!!!**)
|
neuper@37906
|
92 |
|
neuper@37947
|
93 |
ML{* (*the former ListC.ML*)
|
neuper@37906
|
94 |
(** rule set for evaluating listexpr in scripts **)
|
neuper@37906
|
95 |
val list_rls =
|
neuper@52139
|
96 |
Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
|
neuper@52139
|
97 |
erls = Erls, srls = Erls, calc = [], errpatts = [],
|
neuper@52139
|
98 |
rules = [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
|
neuper@37906
|
99 |
Thm ("o_apply", num_str @{thm o_apply}),
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
|
neuper@37906
|
102 |
Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
|
neuper@37906
|
103 |
Thm ("append_Cons",num_str @{thm append_Cons}),
|
neuper@37906
|
104 |
Thm ("append_Nil",num_str @{thm append_Nil}),
|
neuper@52148
|
105 |
(* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
|
neuper@52148
|
106 |
Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
|
neuper@37906
|
107 |
Thm ("concat_Cons",num_str @{thm concat_Cons}),
|
neuper@37906
|
108 |
Thm ("concat_Nil",num_str @{thm concat_Nil}),
|
neuper@52148
|
109 |
(* Thm ("del_base",num_str @{thm del_base}),
|
neuper@52148
|
110 |
Thm ("del_rec",num_str @{thm del_rec}), *)
|
neuper@37906
|
111 |
|
neuper@37906
|
112 |
Thm ("distinct_Cons",num_str @{thm distinct_Cons}),
|
neuper@37906
|
113 |
Thm ("distinct_Nil",num_str @{thm distinct_Nil}),
|
neuper@37906
|
114 |
Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}),
|
neuper@37906
|
115 |
Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}),
|
neuper@37906
|
116 |
Thm ("filter_Cons",num_str @{thm filter_Cons}),
|
neuper@37906
|
117 |
Thm ("filter_Nil",num_str @{thm filter_Nil}),
|
neuper@37906
|
118 |
Thm ("foldr_Cons",num_str @{thm foldr_Cons}),
|
neuper@37906
|
119 |
Thm ("foldr_Nil",num_str @{thm foldr_Nil}),
|
neuper@37906
|
120 |
Thm ("hd_thm",num_str @{thm hd_thm}),
|
neuper@37906
|
121 |
Thm ("LAST",num_str @{thm LAST}),
|
neuper@37906
|
122 |
Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
|
neuper@37906
|
123 |
Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
|
neuper@52148
|
124 |
(* Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
|
neuper@37906
|
125 |
Thm ("map_Cons",num_str @{thm map_Cons}),
|
neuper@37906
|
126 |
Thm ("map_Nil",num_str @{thm map_Cons}),
|
neuper@52148
|
127 |
(* Thm ("mem_Cons",num_str @{thm mem_Cons}),
|
neuper@52148
|
128 |
Thm ("mem_Nil",num_str @{thm mem_Nil}), *)
|
neuper@52148
|
129 |
(* Thm ("null_Cons",num_str @{thm null_Cons}),
|
neuper@52148
|
130 |
Thm ("null_Nil",num_str @{thm null_Nil}),*)
|
neuper@37906
|
131 |
Thm ("remdups_Cons",num_str @{thm remdups_Cons}),
|
neuper@37906
|
132 |
Thm ("remdups_Nil",num_str @{thm remdups_Nil}),
|
neuper@37906
|
133 |
Thm ("rev_Cons",num_str @{thm rev_Cons}),
|
neuper@37906
|
134 |
Thm ("rev_Nil",num_str @{thm rev_Nil}),
|
neuper@37906
|
135 |
Thm ("take_Nil",num_str @{thm take_Nil}),
|
neuper@37906
|
136 |
Thm ("take_Cons",num_str @{thm take_Cons}),
|
neuper@37906
|
137 |
Thm ("tl_Cons",num_str @{thm tl_Cons}),
|
neuper@37906
|
138 |
Thm ("tl_Nil",num_str @{thm tl_Nil}),
|
neuper@37906
|
139 |
Thm ("zip_Cons",num_str @{thm zip_Cons}),
|
neuper@52139
|
140 |
Thm ("zip_Nil",num_str @{thm zip_Nil})],
|
neuper@52139
|
141 |
scr = EmptyScr}:rls;
|
neuper@37906
|
142 |
*}
|
neuper@52122
|
143 |
setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
|
neuper@52122
|
144 |
|
neuper@37906
|
145 |
end
|