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