1 (* use_thy_only"../Scripts/ListG"; |
|
2 use_thy_only"Scripts/ListG"; |
|
3 use_thy"Scripts/ListG"; |
|
4 |
|
5 use_thy_only"ListG"; |
|
6 W.N. 8.01 |
|
7 attaches identifiers to definition of listfuns, |
|
8 for storing them in list_rls |
|
9 |
|
10 WN.29.4.03: |
|
11 *) |
|
12 |
|
13 theory ListG imports Complex_Main |
|
14 uses ("library.sml")("calcelems.sml") |
|
15 ("Scripts/term_G.sml")("Scripts/calculate.sml") |
|
16 ("Scripts/rewrite.sml") |
|
17 begin |
|
18 use "library.sml" (*indent,...*) |
|
19 use "calcelems.sml" (*str_of_type, Thm,...*) |
|
20 use "Scripts/term_G.sml" (*num_str,...*) |
|
21 use "Scripts/calculate.sml" (*???*) |
|
22 use "Scripts/rewrite.sml" (*?*** At command "end" (line 205../ListG.thy*) |
|
23 |
|
24 text {* 'nat' in List.thy replaced by 'real' *} |
|
25 |
|
26 primrec length_' :: "'a list => real" |
|
27 where |
|
28 LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*) |
|
29 | LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs" |
|
30 |
|
31 primrec del :: "['a list, 'a] => 'a list" |
|
32 where |
|
33 del_base: "del [] x = []" |
|
34 | del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))" |
|
35 |
|
36 definition |
|
37 list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *) |
|
38 ("(_ --/ _)" [66, 66] 65) |
|
39 where "a -- b == foldl del a b" |
|
40 |
|
41 consts nth_' :: "[real, 'a list] => 'a" |
|
42 axioms |
|
43 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*) |
|
44 NTH_NIL: "nth_' 1 (x#xs) = x" |
|
45 (* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *) |
|
46 |
|
47 (*rewriter does not reach base case ...... ; |
|
48 the condition involves another rule set (erls, eval_binop in Atools):*) |
|
49 NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs" |
|
50 |
|
51 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*) |
|
52 (*primrec*) |
|
53 hd_thm: "hd(x#xs) = x" |
|
54 (*primrec*) |
|
55 tl_Nil: "tl([]) = []" |
|
56 tl_Cons: "tl(x#xs) = xs" |
|
57 (*primrec*) |
|
58 null_Nil: "null([]) = True" |
|
59 null_Cons: "null(x#xs) = False" |
|
60 (*primrec*) |
|
61 LAST: "last(x#xs) = (if xs=[] then x else last xs)" |
|
62 (*primrec*) |
|
63 butlast_Nil: "butlast [] = []" |
|
64 butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" |
|
65 (*primrec*) |
|
66 mem_Nil: "x mem [] = False" |
|
67 mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)" |
|
68 (*primrec-------already named--- |
|
69 "set [] = {}" |
|
70 "set (x#xs) = insert x (set xs)" |
|
71 primrec |
|
72 list_all_Nil "list_all P [] = True" |
|
73 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
|
74 ----------------*) |
|
75 (*primrec*) |
|
76 map_Nil: "map f [] = []" |
|
77 map_Cons: "map f (x#xs) = f(x)#map f xs" |
|
78 (*primrec*) |
|
79 append_Nil: "[] @ys = ys" |
|
80 append_Cons: "(x#xs)@ys = x#(xs@ys)" |
|
81 (*primrec*) |
|
82 rev_Nil: "rev([]) = []" |
|
83 rev_Cons: "rev(x#xs) = rev(xs) @ [x]" |
|
84 (*primrec*) |
|
85 filter_Nil: "filter P [] = []" |
|
86 filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" |
|
87 (*primrec-------already named--- |
|
88 foldl_Nil "foldl f a [] = a" |
|
89 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
|
90 ----------------*) |
|
91 (*primrec*) |
|
92 foldr_Nil: "foldr f [] a = a" |
|
93 foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" |
|
94 (*primrec*) |
|
95 concat_Nil: "concat([]) = []" |
|
96 concat_Cons: "concat(x#xs) = x @ concat(xs)" |
|
97 (*primrec-------already named--- |
|
98 drop_Nil "drop n [] = []" |
|
99 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
|
100 (* Warning: simpset does not contain this definition but separate theorems |
|
101 for n=0 / n=Suc k*) |
|
102 (*primrec*) |
|
103 take_Nil "take n [] = []" |
|
104 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
|
105 (* Warning: simpset does not contain this definition but separate theorems |
|
106 for n=0 / n=Suc k*) |
|
107 (*primrec*) |
|
108 nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)" |
|
109 (* Warning: simpset does not contain this definition but separate theorems |
|
110 for n=0 / n=Suc k*) |
|
111 (*primrec*) |
|
112 " [][i:=v] = []" |
|
113 "(x#xs)[i:=v] = (case i of 0 => v # xs |
|
114 | Suc j => x # xs[j:=v])" |
|
115 ----------------*) |
|
116 (*primrec*) |
|
117 takeWhile_Nil: "takeWhile P [] = []" |
|
118 takeWhile_Cons: |
|
119 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
|
120 (*primrec*) |
|
121 dropWhile_Nil: "dropWhile P [] = []" |
|
122 dropWhile_Cons: |
|
123 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
|
124 (*primrec*) |
|
125 zip_Nil: "zip xs [] = []" |
|
126 zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" |
|
127 (* Warning: simpset does not contain this definition but separate theorems |
|
128 for xs=[] / xs=z#zs *) |
|
129 (*primrec |
|
130 upt_0 "[i..0(] = []" |
|
131 upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" |
|
132 *) |
|
133 (*primrec*) |
|
134 distinct_Nil: "distinct [] = True" |
|
135 distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" |
|
136 (*primrec*) |
|
137 remdups_Nil: "remdups [] = []" |
|
138 remdups_Cons: "remdups (x#xs) = |
|
139 (if x : set xs then remdups xs else x # remdups xs)" |
|
140 (*primrec-------already named--- |
|
141 replicate_0 "replicate 0 x = []" |
|
142 replicate_Suc "replicate (Suc n) x = x # replicate n x" |
|
143 ----------------*) |
|
144 |
|
145 (** Lexicographic orderings on lists ...!!!**) |
|
146 |
|
147 ML{* (*the former ListG.ML*) |
|
148 (** rule set for evaluating listexpr in scripts **) |
|
149 val list_rls = |
|
150 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
|
151 erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*) |
|
152 rules = (*8.01: copied from*) |
|
153 [Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*) |
|
154 Thm ("o_apply", num_str @{thm o_apply}), |
|
155 |
|
156 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
|
157 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
|
158 Thm ("append_Cons",num_str @{thm append_Cons}), |
|
159 Thm ("append_Nil",num_str @{thm append_Nil}), |
|
160 Thm ("butlast_Cons",num_str @{thm butlast_Cons}), |
|
161 Thm ("butlast_Nil",num_str @{thm butlast_Nil}), |
|
162 Thm ("concat_Cons",num_str @{thm concat_Cons}), |
|
163 Thm ("concat_Nil",num_str @{thm concat_Nil}), |
|
164 Thm ("del_base",num_str @{thm del_base}), |
|
165 Thm ("del_rec",num_str @{thm del_rec}), |
|
166 |
|
167 Thm ("distinct_Cons",num_str @{thm distinct_Cons}), |
|
168 Thm ("distinct_Nil",num_str @{thm distinct_Nil}), |
|
169 Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}), |
|
170 Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}), |
|
171 Thm ("filter_Cons",num_str @{thm filter_Cons}), |
|
172 Thm ("filter_Nil",num_str @{thm filter_Nil}), |
|
173 Thm ("foldr_Cons",num_str @{thm foldr_Cons}), |
|
174 Thm ("foldr_Nil",num_str @{thm foldr_Nil}), |
|
175 Thm ("hd_thm",num_str @{thm hd_thm}), |
|
176 Thm ("LAST",num_str @{thm LAST}), |
|
177 Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
|
178 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
|
179 Thm ("list_diff_def",num_str @{thm list_diff_def}), |
|
180 Thm ("map_Cons",num_str @{thm map_Cons}), |
|
181 Thm ("map_Nil",num_str @{thm map_Cons}), |
|
182 Thm ("mem_Cons",num_str @{thm mem_Cons}), |
|
183 Thm ("mem_Nil",num_str @{thm mem_Nil}), |
|
184 Thm ("null_Cons",num_str @{thm null_Cons}), |
|
185 Thm ("null_Nil",num_str @{thm null_Nil}), |
|
186 Thm ("remdups_Cons",num_str @{thm remdups_Cons}), |
|
187 Thm ("remdups_Nil",num_str @{thm remdups_Nil}), |
|
188 Thm ("rev_Cons",num_str @{thm rev_Cons}), |
|
189 Thm ("rev_Nil",num_str @{thm rev_Nil}), |
|
190 Thm ("take_Nil",num_str @{thm take_Nil}), |
|
191 Thm ("take_Cons",num_str @{thm take_Cons}), |
|
192 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
|
193 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
|
194 Thm ("zip_Cons",num_str @{thm zip_Cons}), |
|
195 Thm ("zip_Nil",num_str @{thm zip_Nil}) |
|
196 ], scr = EmptyScr}:rls; |
|
197 *} |
|
198 |
|
199 ML{* |
|
200 ruleset' := overwritelthy @{theory} (!ruleset', |
|
201 [("list_rls",list_rls) |
|
202 ]); |
|
203 *} |
|
204 end |
|