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