133 ML{* (*the former ListC.ML*) |
138 ML{* (*the former ListC.ML*) |
134 (** rule set for evaluating listexpr in scripts **) |
139 (** rule set for evaluating listexpr in scripts **) |
135 val list_rls = |
140 val list_rls = |
136 Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), |
141 Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), |
137 erls = Erls, srls = Erls, calc = [], errpatts = [], |
142 erls = Erls, srls = Erls, calc = [], errpatts = [], |
138 rules = [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
143 rules = [Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
139 Thm ("o_apply", num_str @{thm o_apply}), |
144 Thm ("o_apply", TermC.num_str @{thm o_apply}), |
140 |
145 |
141 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
146 Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
142 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
147 Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
143 Thm ("append_Cons",num_str @{thm append_Cons}), |
148 Thm ("append_Cons",TermC.num_str @{thm append_Cons}), |
144 Thm ("append_Nil",num_str @{thm append_Nil}), |
149 Thm ("append_Nil",TermC.num_str @{thm append_Nil}), |
145 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}), |
150 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}), |
146 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*) |
151 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*) |
147 Thm ("concat_Cons",num_str @{thm concat_Cons}), |
152 Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}), |
148 Thm ("concat_Nil",num_str @{thm concat_Nil}), |
153 Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}), |
149 (* Thm ("del_base",num_str @{thm del_base}), |
154 (* Thm ("del_base",num_str @{thm del_base}), |
150 Thm ("del_rec",num_str @{thm del_rec}), *) |
155 Thm ("del_rec",num_str @{thm del_rec}), *) |
151 |
156 |
152 Thm ("distinct_Cons",num_str @{thm distinct_Cons}), |
157 Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}), |
153 Thm ("distinct_Nil",num_str @{thm distinct_Nil}), |
158 Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}), |
154 Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}), |
159 Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}), |
155 Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}), |
160 Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}), |
156 Thm ("filter_Cons",num_str @{thm filter_Cons}), |
161 Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}), |
157 Thm ("filter_Nil",num_str @{thm filter_Nil}), |
162 Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}), |
158 Thm ("foldr_Cons",num_str @{thm foldr_Cons}), |
163 Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}), |
159 Thm ("foldr_Nil",num_str @{thm foldr_Nil}), |
164 Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}), |
160 Thm ("hd_thm",num_str @{thm hd_thm}), |
165 Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
161 Thm ("LAST",num_str @{thm LAST}), |
166 Thm ("LAST",TermC.num_str @{thm LAST}), |
162 Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
167 Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), |
163 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
168 Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), |
164 (* Thm ("list_diff_def",num_str @{thm list_diff_def}),*) |
169 (* Thm ("list_diff_def",num_str @{thm list_diff_def}),*) |
165 Thm ("map_Cons",num_str @{thm map_Cons}), |
170 Thm ("map_Cons",TermC.num_str @{thm map_Cons}), |
166 Thm ("map_Nil",num_str @{thm map_Cons}), |
171 Thm ("map_Nil",TermC.num_str @{thm map_Cons}), |
167 (* Thm ("mem_Cons",num_str @{thm mem_Cons}), |
172 (* Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}), |
168 Thm ("mem_Nil",num_str @{thm mem_Nil}), *) |
173 Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *) |
169 (* Thm ("null_Cons",num_str @{thm null_Cons}), |
174 (* Thm ("null_Cons",TermC.num_str @{thm null_Cons}), |
170 Thm ("null_Nil",num_str @{thm null_Nil}),*) |
175 Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*) |
171 Thm ("remdups_Cons",num_str @{thm remdups_Cons}), |
176 Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}), |
172 Thm ("remdups_Nil",num_str @{thm remdups_Nil}), |
177 Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}), |
173 Thm ("rev_Cons",num_str @{thm rev_Cons}), |
178 Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}), |
174 Thm ("rev_Nil",num_str @{thm rev_Nil}), |
179 Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}), |
175 Thm ("take_Nil",num_str @{thm take_Nil}), |
180 Thm ("take_Nil",TermC.num_str @{thm take_Nil}), |
176 Thm ("take_Cons",num_str @{thm take_Cons}), |
181 Thm ("take_Cons",TermC.num_str @{thm take_Cons}), |
177 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
182 Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
178 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
183 Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}), |
179 Thm ("zip_Cons",num_str @{thm zip_Cons}), |
184 Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}), |
180 Thm ("zip_Nil",num_str @{thm zip_Nil})], |
185 Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})], |
181 scr = EmptyScr}:rls; |
186 scr = EmptyScr}:rls; |
182 *} |
187 *} |
183 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
188 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
184 |
189 |
185 end |
190 end |