1 (* Title: functions on lists for Programs
2 Author: Walther Neuper 0108
3 (c) due to copyright terms
7 imports "~~/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"
22 subsection {* Notes on Isac's programming language *}
24 Isac's programming language combines tacticals (TRY, etc) and
25 tactics (Rewrite, etc) with list processing.
27 In order to distinguish list expressions of the meta (programming)
28 language from the object language in Lucas-Interpretation, a
29 new 'type xlist' is introduced.
30 TODO: Switch the role of 'xlist' and 'list' (the former only used
33 Isac's programming language preceeded the function package
34 in 2002. For naming "axiomatization" is used for reasons of uniformity
35 with the other replacements for "axioms".
36 Another reminiscence from Isabelle2002 are Isac-specific numerals,
37 introduced in order to have floating point numerals at a time,
38 when Isabelle did not consider that requirement. For the sake of uniformity
39 'nat' from List.thy is replaced by 'real' by 'fun parse',
40 however, 'fun parseNEW' has started to replace this fix (after finishing
41 this fix, there will be a 'rename all parseNEW --> parse).
43 Note: *one* "axiomatization" over all equations caused strange "'a list list"
47 subsection {* Type 'xlist' for Lucas-Interpretation *}
48 (*TODO: ask for shorter deliminters in xlist *)
51 | XCons 'a "'a xlist" (infixr "@#" 65)
54 -- {* list Enumeration *}
55 "_xlist" :: "args => 'a xlist" ("{|| (_) ||}")
58 "{||x, xs||}" == "x@#{||xs||}"
59 "{||x||}" == "x@#{|| ||}"
64 subsection {* Functions for 'xlist' *}
66 (1) revise, if definition of identifiers like LENGTH_NIL are still required.
67 (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
68 'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
69 For transition phase just outcomment InsSort.thy and inssort.sml.
72 primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
73 xfoldr_Nil: "xfoldr f {|| ||} = id" |
74 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
76 primrec LENGTH :: "'a list => real"
78 LENGTH_NIL: "LENGTH [] = 0" |
79 LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
81 consts NTH :: "[real, 'a list] => 'a"
83 NTH_NIL: "NTH 1 (x # xs) = x" and
84 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
87 hd_thm: "hd (x # xs) = x"
90 tl_Nil: "tl [] = []" and
91 tl_Cons: "tl (x # xs) = xs"
94 LAST: "last (x # xs) = (if xs = [] then x else last xs)"
97 butlast_Nil: "butlast [] = []" and
98 butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
101 map_Nil:"map f [] = []" and
102 map_Cons: "map f (x # xs) = f x # map f xs"
105 rev_Nil: "rev [] = []" and
106 rev_Cons: "rev (x # xs) = rev xs @ [x]"
109 filter_Nil: "filter P [] = []" and
110 filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
113 concat_Nil: "concat [] = []" and
114 concat_Cons: "concat (x # xs) = x @ concat xs"
117 takeWhile_Nil: "takeWhile P [] = []" and
118 takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
121 dropWhile_Nil: "dropWhile P [] = []" and
122 dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
125 zip_Nil: "zip xs [] = []" and
126 zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
129 distinct_Nil: "distinct [] = True" and
130 distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
133 remdups_Nil: "remdups [] = []" and
134 remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
136 (** Lexicographic orderings on lists ...!!!**)
138 ML{* (*the former ListC.ML*)
139 (** rule set for evaluating listexpr in scripts **)
141 Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
142 erls = Erls, srls = Erls, calc = [], errpatts = [],
143 rules = [Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
144 Thm ("o_apply", TermC.num_str @{thm o_apply}),
146 Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
147 Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
148 Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
149 Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
150 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
151 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
152 Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
153 Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
154 (* Thm ("del_base",num_str @{thm del_base}),
155 Thm ("del_rec",num_str @{thm del_rec}), *)
157 Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
158 Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
159 Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
160 Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
161 Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
162 Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
163 Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
164 Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
165 Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
166 Thm ("LAST",TermC.num_str @{thm LAST}),
167 Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
168 Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
169 (* Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
170 Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
171 Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
172 (* Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
173 Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
174 (* Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
175 Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
176 Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
177 Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
178 Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
179 Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
180 Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
181 Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
182 Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
183 Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
184 Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
185 Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
188 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}