equal
deleted
inserted
replaced
1 theory LF |
1 theory LF |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 declare [[STEPS = 100]] |
|
6 |
|
7 atom_decl name |
5 atom_decl name |
8 atom_decl ident |
6 atom_decl ident |
9 |
7 |
10 nominal_datatype kind = |
8 nominal_datatype lf: |
11 Type |
9 kind = |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
10 Type |
|
11 | KPi "ty" n::"name" k::"kind" bind n in k |
13 and ty = |
12 and ty = |
14 TConst "ident" |
13 TConst "ident" |
15 | TApp "ty" "trm" |
14 | TApp "ty" "trm" |
16 | TPi "ty" n::"name" ty::"ty" bind n in ty |
15 | TPi "ty" n::"name" ty::"ty" bind n in ty |
17 and trm = |
16 and trm = |
18 Const "ident" |
17 Const "ident" |
19 | Var "name" |
18 | Var "name" |
20 | App "trm" "trm" |
19 | App "trm" "trm" |
21 | Lam "ty" n::"name" t::"trm" bind n in t |
20 | Lam "ty" n::"name" t::"trm" bind n in t |
22 |
21 |
23 (*thm kind_ty_trm.supp*) |
22 thm lf.distinct |
|
23 thm lf.induct |
|
24 thm lf.inducts |
|
25 thm lf.exhaust |
|
26 thm lf.strong_exhaust |
|
27 thm lf.fv_defs |
|
28 thm lf.bn_defs |
|
29 thm lf.perm_simps |
|
30 thm lf.eq_iff |
|
31 thm lf.fv_bn_eqvt |
|
32 thm lf.size_eqvt |
|
33 thm lf.supports |
|
34 thm lf.fsupp |
|
35 thm lf.supp |
|
36 thm lf.fresh |
|
37 thm lf.fresh[simplified] |
|
38 |
24 |
39 |
25 |
40 |
26 end |
41 end |
27 |
42 |
28 |
43 |