|
1 structure List = |
|
2 struct |
|
3 |
|
4 local |
|
5 val parse_ast_translation = [] |
|
6 val parse_preproc = None |
|
7 val parse_postproc = None |
|
8 val parse_translation = [] |
|
9 val print_translation = [] |
|
10 val print_preproc = None |
|
11 val print_postproc = None |
|
12 val print_ast_translation = [] |
|
13 in |
|
14 |
|
15 (**** begin of user section ****) |
|
16 |
|
17 (**** end of user section ****) |
|
18 |
|
19 val thy = extend_theory (Nat2.thy) |
|
20 "List" |
|
21 ([], |
|
22 [], |
|
23 [(["list"], 1)], |
|
24 [(["list"], ([["term"]], "term"))], |
|
25 [(["hd"], "'a list => 'a"), |
|
26 (["tl"], "'a list => 'a list"), |
|
27 (["forall"], "['a list, 'a => o] => o"), |
|
28 (["len"], "'a list => nat"), |
|
29 (["at"], "['a list, nat] => 'a")], |
|
30 Some (NewSext { |
|
31 mixfix = |
|
32 [Delimfix("[]", "'a list", "[]"), |
|
33 Infixr(".", "['a, 'a list] => 'a list", 80), |
|
34 Infixr("++", "['a list, 'a list] => 'a list", 70)], |
|
35 xrules = |
|
36 [], |
|
37 parse_ast_translation = parse_ast_translation, |
|
38 parse_preproc = parse_preproc, |
|
39 parse_postproc = parse_postproc, |
|
40 parse_translation = parse_translation, |
|
41 print_translation = print_translation, |
|
42 print_preproc = print_preproc, |
|
43 print_postproc = print_postproc, |
|
44 print_ast_translation = print_ast_translation})) |
|
45 [("list_ind", "[| P([]); ALL x l. P(l)-->P(x.l) |] ==> All(P)"), |
|
46 ("forall_cong", "[| l = l'; !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"), |
|
47 ("list_distinct1", "~[] = x.l"), |
|
48 ("list_distinct2", "~x.l = []"), |
|
49 ("list_free", "x.l = x'.l' <-> x=x' & l=l'"), |
|
50 ("app_nil", "[]++l = l"), |
|
51 ("app_cons", "(x.l)++l' = x.(l++l')"), |
|
52 ("tl_eq", "tl(m.q) = q"), |
|
53 ("hd_eq", "hd(m.q) = m"), |
|
54 ("forall_nil", "forall([],P)"), |
|
55 ("forall_cons", "forall(x.l,P) <-> P(x) & forall(l,P)"), |
|
56 ("len_nil", "len([]) = 0"), |
|
57 ("len_cons", "len(m.q) = succ(len(q))"), |
|
58 ("at_0", "at(m.q,0) = m"), |
|
59 ("at_succ", "at(m.q,succ(n)) = at(q,n)")] |
|
60 |
|
61 val ax = get_axiom thy |
|
62 |
|
63 val list_ind = ax "list_ind" |
|
64 val forall_cong = ax "forall_cong" |
|
65 val list_distinct1 = ax "list_distinct1" |
|
66 val list_distinct2 = ax "list_distinct2" |
|
67 val list_free = ax "list_free" |
|
68 val app_nil = ax "app_nil" |
|
69 val app_cons = ax "app_cons" |
|
70 val tl_eq = ax "tl_eq" |
|
71 val hd_eq = ax "hd_eq" |
|
72 val forall_nil = ax "forall_nil" |
|
73 val forall_cons = ax "forall_cons" |
|
74 val len_nil = ax "len_nil" |
|
75 val len_cons = ax "len_cons" |
|
76 val at_0 = ax "at_0" |
|
77 val at_succ = ax "at_succ" |
|
78 |
|
79 |
|
80 end |
|
81 end |