1 (* Title: functions on lists for Programs
2 Author: Walther Neuper 0108
3 (c) due to copyright terms
6 theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
11 There are examples in the Knowledge, which demonstrate list processing, e.g. InsSort.thy.
13 Lists in example calculations must have a different type for list processing in Isac programs.
14 Presently the lists in examples have a new type xlist with the unfamiliar list
15 notation "{||a, b, c||}". One could expect math-authors to use such unfamiliar notation
16 and expose students to familiar notation in calculations, and not vice versa as done presently.
18 Thus this theory resides in ProgLang so far.
21 subsection \<open>General constants\<close>
23 EmptyList :: "bool list"
24 UniversalList :: "bool list"
28 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
29 val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
33 subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close>
34 (* cp fom ~~/src/HOL/List.thy
35 TODO: ask for shorter deliminters in xlist *)
38 | XCons (xhd: 'a) (xtl: "'a xlist") (infixr "@#" 65)
41 \<comment> \<open>list Enumeration\<close>
42 "_xlist" :: "args => 'a xlist" ("{|| (_) ||}")
45 "{||x, xs||}" == "x@#{||xs||}"
46 "{||x||}" == "x@#{|| ||}"
51 subsection \<open>Functions for 'xlist'\<close>
53 (1) revise, if definition of identifiers like LENGTH_NIL are still required.
54 (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
55 'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
56 For transition phase just outcomment InsSort.thy and inssort.sml.
59 primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
60 xfoldr_Nil: "xfoldr f {|| ||} = id" |
61 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
63 primrec LENGTH :: "'a list => real"
65 LENGTH_NIL: "LENGTH [] = 0" |
66 LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
68 subsection \<open>Functions for 'list'\<close>
70 consts NTH :: "[real, 'a list] => 'a"
72 NTH_NIL: "NTH 1 (x # xs) = x" and
73 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
75 (* redefine together with identifiers (still) required for KEStore ..*)
77 hd_thm: "hd (x # xs) = x"
80 tl_Nil: "tl [] = []" and
81 tl_Cons: "tl (x # xs) = xs"
84 LAST: "last (x # xs) = (if xs = [] then x else last xs)"
87 butlast_Nil: "butlast [] = []" and
88 butlast_Cons: "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
91 map_Nil:"map f [] = []" and
92 map_Cons: "map f (x # xs) = f x # map f xs"
95 rev_Nil: "rev [] = []" and
96 rev_Cons: "rev (x # xs) = rev xs @ [x]"
99 filter_Nil: "filter P [] = []" and
100 filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
103 concat_Nil: "concat [] = []" and
104 concat_Cons: "concat (x # xs) = x @ concat xs"
107 takeWhile_Nil: "takeWhile P [] = []" and
108 takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
111 dropWhile_Nil: "dropWhile P [] = []" and
112 dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
115 zip_Nil: "zip xs [] = []" and
116 zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
119 distinct_Nil: "distinct [] = True" and
120 distinct_Cons: "distinct (x # xs) = (x ~: set xs & distinct xs)"
123 remdups_Nil: "remdups [] = []" and
124 remdups_Cons: "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
126 consts lastI :: "'a list \<Rightarrow> 'a"
128 last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
130 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
134 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
135 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
136 rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
137 Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),
139 Rule_Def.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
140 Rule_Def.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
141 Rule_Def.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
142 Rule_Def.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
143 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
144 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
145 Rule_Def.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
146 Rule_Def.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
147 (* Rule_Def.Thm ("del_base",num_str @{thm del_base}),
148 Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *)
150 Rule_Def.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
151 Rule_Def.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
152 Rule_Def.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
153 Rule_Def.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
154 Rule_Def.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
155 Rule_Def.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
156 Rule_Def.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
157 Rule_Def.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
158 Rule_Def.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
159 Rule_Def.Thm ("LAST",TermC.num_str @{thm LAST}),
160 Rule_Def.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
161 Rule_Def.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
162 (* Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
163 Rule_Def.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
164 Rule_Def.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
165 (* Rule_Def.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
166 Rule_Def.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
167 (* Rule_Def.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
168 Rule_Def.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
169 Rule_Def.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
170 Rule_Def.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
171 Rule_Def.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
172 Rule_Def.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
173 Rule_Def.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
174 Rule_Def.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
175 Rule_Def.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
176 Rule_Def.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
177 Rule_Def.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
178 Rule_Def.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
179 scr = Rule_Def.EmptyScr}: Rule_Set.T;
181 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>