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/contextC.sml"
12 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
13 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
18 subsection \<open>Notes on Isac's programming language\<close>
20 Isac's programming language combines tacticals (TRY, etc) and
21 tactics (Rewrite, etc) with list processing.
23 In order to distinguish list expressions of the meta (programming)
24 language from the object language in Lucas-Interpretation, a
25 new 'type xlist' is introduced.
26 TODO: Switch the role of 'xlist' and 'list' (the former only used
29 Isac's programming language preceeded the function package
30 in 2002. For naming "axiomatization" is used for reasons of uniformity
31 with the other replacements for "axioms".
32 Another reminiscence from Isabelle2002 are Isac-specific numerals,
33 introduced in order to have floating point numerals at a time,
34 when Isabelle did not consider that requirement. For the sake of uniformity
35 'nat' from List.thy is replaced by 'real' by 'fun parse',
36 however, 'fun parseNEW' has started to replace this fix (after finishing
37 this fix, there will be a 'rename all parseNEW --> parse).
39 Note: *one* "axiomatization" over all equations caused strange "'a list list"
43 subsection \<open>Type 'xlist' for Lucas-Interpretation\<close>
44 (* cp fom ~~/src/HOL/List.thy
45 TODO: ask for shorter deliminters in xlist *)
48 | XCons (xhd: 'a) (xtl: "'a xlist") (infixr "@#" 65)
51 \<comment> \<open>list Enumeration\<close>
52 "_xlist" :: "args => 'a xlist" ("{|| (_) ||}")
55 "{||x, xs||}" == "x@#{||xs||}"
56 "{||x||}" == "x@#{|| ||}"
61 subsection \<open>Functions for 'xlist'\<close>
63 (1) revise, if definition of identifiers like LENGTH_NIL are still required.
64 (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
65 'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
66 For transition phase just outcomment InsSort.thy and inssort.sml.
69 primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
70 xfoldr_Nil: "xfoldr f {|| ||} = id" |
71 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
73 primrec LENGTH :: "'a list => real"
75 LENGTH_NIL: "LENGTH [] = 0" |
76 LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
78 consts NTH :: "[real, 'a list] => 'a"
80 NTH_NIL: "NTH 1 (x # xs) = x" and
81 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
83 (* redefine together with identifiers (still) required for KEStore ..*)
85 hd_thm: "hd (x # xs) = x"
88 tl_Nil: "tl [] = []" and
89 tl_Cons: "tl (x # xs) = xs"
92 LAST: "last (x # xs) = (if xs = [] then x else last xs)"
95 butlast_Nil: "butlast [] = []" and
96 butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
99 map_Nil:"map f [] = []" and
100 map_Cons: "map f (x # xs) = f x # map f xs"
103 rev_Nil: "rev [] = []" and
104 rev_Cons: "rev (x # xs) = rev xs @ [x]"
107 filter_Nil: "filter P [] = []" and
108 filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
111 concat_Nil: "concat [] = []" and
112 concat_Cons: "concat (x # xs) = x @ concat xs"
115 takeWhile_Nil: "takeWhile P [] = []" and
116 takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
119 dropWhile_Nil: "dropWhile P [] = []" and
120 dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
123 zip_Nil: "zip xs [] = []" and
124 zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
127 distinct_Nil: "distinct [] = True" and
128 distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
131 remdups_Nil: "remdups [] = []" and
132 remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
135 (** rule set for evaluating listexpr in scripts, will be extended in several thys **)
137 Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
138 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
139 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
140 Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),
142 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
143 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
144 Rule.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
145 Rule.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
146 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
147 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
148 Rule.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
149 Rule.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
150 (* Rule.Thm ("del_base",num_str @{thm del_base}),
151 Rule.Thm ("del_rec",num_str @{thm del_rec}), *)
153 Rule.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
154 Rule.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
155 Rule.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
156 Rule.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
157 Rule.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
158 Rule.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
159 Rule.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
160 Rule.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
161 Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
162 Rule.Thm ("LAST",TermC.num_str @{thm LAST}),
163 Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
164 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
165 (* Rule.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
166 Rule.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
167 Rule.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
168 (* Rule.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
169 Rule.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
170 (* Rule.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
171 Rule.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
172 Rule.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
173 Rule.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
174 Rule.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
175 Rule.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
176 Rule.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
177 Rule.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
178 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
179 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
180 Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
181 Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
182 scr = Rule.EmptyScr}: Rule.rls;
184 setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>