|
neuper@37871
|
1 |
(* use"Scripts/ListG.ML";
|
|
neuper@37871
|
2 |
W.N. 8.01
|
|
neuper@37871
|
3 |
*)
|
|
neuper@37871
|
4 |
|
|
neuper@37871
|
5 |
"---------";
|
|
neuper@37871
|
6 |
refl;
|
|
neuper@37871
|
7 |
@{thm length_Nil_'};
|
|
neuper@37871
|
8 |
(*
|
|
neuper@37871
|
9 |
nth_Cons_';
|
|
neuper@37871
|
10 |
|
|
neuper@37871
|
11 |
val list_rls =
|
|
neuper@37871
|
12 |
Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
|
neuper@37871
|
13 |
erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
|
|
neuper@37871
|
14 |
rules = (*8.01: copied from*)
|
|
neuper@37871
|
15 |
[Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
|
|
neuper@37871
|
16 |
(*Thm ("o_apply", num_str Fun.o_apply)*)
|
|
neuper@37871
|
17 |
Thm ("nth_Cons_",num_str nth_Cons_),(*erls for cond. in Atools.ML*)
|
|
neuper@37871
|
18 |
Thm ("nth_Nil_",num_str nth_Nil_)
|
|
neuper@37871
|
19 |
|
|
neuper@37871
|
20 |
]};
|
|
neuper@37871
|
21 |
*)
|
|
neuper@37871
|
22 |
|
|
neuper@37871
|
23 |
(** rule set for evaluating listexpr in scripts **)
|
|
neuper@37871
|
24 |
(*
|
|
neuper@37871
|
25 |
val list_rls =
|
|
neuper@37871
|
26 |
Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
|
|
neuper@37871
|
27 |
erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
|
|
neuper@37871
|
28 |
rules = (*8.01: copied from*)
|
|
neuper@37871
|
29 |
[Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
|
|
neuper@37871
|
30 |
Thm ("o_apply", num_str o_apply),
|
|
neuper@37871
|
31 |
|
|
neuper@37871
|
32 |
Thm ("nth_Cons_",num_str nth_Cons_),(*erls for cond. in Atools.ML*)
|
|
neuper@37871
|
33 |
Thm ("nth_Nil_",num_str nth_Nil_),
|
|
neuper@37871
|
34 |
Thm ("append_Cons",num_str append_Cons),
|
|
neuper@37871
|
35 |
Thm ("append_Nil",num_str append_Nil),
|
|
neuper@37871
|
36 |
Thm ("butlast_Cons",num_str butlast_Cons),
|
|
neuper@37871
|
37 |
Thm ("butlast_Nil",num_str butlast_Nil),
|
|
neuper@37871
|
38 |
Thm ("concat_Cons",num_str concat_Cons),
|
|
neuper@37871
|
39 |
Thm ("concat_Nil",num_str concat_Nil),
|
|
neuper@37871
|
40 |
Thm ("del_base",num_str del_base),
|
|
neuper@37871
|
41 |
Thm ("del_rec",num_str del_rec),
|
|
neuper@37871
|
42 |
|
|
neuper@37871
|
43 |
Thm ("distinct_Cons",num_str distinct_Cons),
|
|
neuper@37871
|
44 |
Thm ("distinct_Nil",num_str distinct_Nil),
|
|
neuper@37871
|
45 |
Thm ("dropWhile_Cons",num_str dropWhile_Cons),
|
|
neuper@37871
|
46 |
Thm ("dropWhile_Nil",num_str dropWhile_Nil),
|
|
neuper@37871
|
47 |
Thm ("filter_Cons",num_str filter_Cons),
|
|
neuper@37871
|
48 |
Thm ("filter_Nil",num_str filter_Nil),
|
|
neuper@37871
|
49 |
Thm ("foldr_Cons",num_str foldr_Cons),
|
|
neuper@37871
|
50 |
Thm ("foldr_Nil",num_str foldr_Nil),
|
|
neuper@37871
|
51 |
Thm ("hd_thm",num_str hd_thm),
|
|
neuper@37871
|
52 |
Thm ("last_thm",num_str last_thm),
|
|
neuper@37871
|
53 |
Thm ("length_Cons_",num_str length_Cons_),
|
|
neuper@37871
|
54 |
Thm ("length_Nil_",num_str length_Nil_),
|
|
neuper@37871
|
55 |
Thm ("list_diff_def",num_str list_diff_def),
|
|
neuper@37871
|
56 |
Thm ("map_Cons",num_str map_Cons),
|
|
neuper@37871
|
57 |
Thm ("map_Nil",num_str map_Cons),
|
|
neuper@37871
|
58 |
Thm ("mem_Cons",num_str mem_Cons),
|
|
neuper@37871
|
59 |
Thm ("mem_Nil",num_str mem_Nil),
|
|
neuper@37871
|
60 |
Thm ("null_Cons",num_str null_Cons),
|
|
neuper@37871
|
61 |
Thm ("null_Nil",num_str null_Nil),
|
|
neuper@37871
|
62 |
Thm ("remdups_Cons",num_str remdups_Cons),
|
|
neuper@37871
|
63 |
Thm ("remdups_Nil",num_str remdups_Nil),
|
|
neuper@37871
|
64 |
Thm ("rev_Cons",num_str rev_Cons),
|
|
neuper@37871
|
65 |
Thm ("rev_Nil",num_str rev_Nil),
|
|
neuper@37871
|
66 |
Thm ("take_Nil",num_str take_Nil),
|
|
neuper@37871
|
67 |
Thm ("take_Cons",num_str take_Cons),
|
|
neuper@37871
|
68 |
Thm ("tl_Cons",num_str tl_Cons),
|
|
neuper@37871
|
69 |
Thm ("tl_Nil",num_str tl_Nil),
|
|
neuper@37871
|
70 |
Thm ("zip_Cons",num_str zip_Cons),
|
|
neuper@37871
|
71 |
Thm ("zip_Nil",num_str zip_Nil)
|
|
neuper@37871
|
72 |
], scr = EmptyScr}:rls;
|
|
neuper@37871
|
73 |
|
|
neuper@37871
|
74 |
ruleset' := overwritelthy thy (!ruleset',
|
|
neuper@37871
|
75 |
[("list_rls",list_rls)
|
|
neuper@37871
|
76 |
]);
|
|
neuper@37871
|
77 |
*)
|