equal
deleted
inserted
replaced
1 theory TypeVarsTest |
1 theory TypeVarsTest |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
|
4 |
|
5 (* a nominal datatype with type variables and sorts *) |
|
6 |
|
7 |
|
8 (* the sort constraints need to be attached to the *) |
|
9 (* first occurence of the type variables on the *) |
|
10 (* left-hand side *) |
4 |
11 |
5 atom_decl name |
12 atom_decl name |
6 |
13 |
7 class s1 |
14 class s1 |
8 class s2 |
15 class s2 |
9 |
16 |
10 instance nat :: s1 .. |
17 instance nat :: s1 .. |
11 instance int :: s2 .. |
18 instance int :: s2 .. |
12 |
19 |
13 nominal_datatype ('a, 'b) lam = |
20 nominal_datatype ('a, 'b, 'c) lam = |
14 Var "name" |
21 Var "name" |
15 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" |
22 | App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam" |
16 | Lam x::"name" l::"('a, 'b) lam" bind x in l |
23 | Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l |
|
24 | Foo "'a" "'b" |
|
25 | Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l |
|
26 |
|
27 term Foo |
|
28 term Bar |
17 |
29 |
18 thm lam.distinct |
30 thm lam.distinct |
19 thm lam.induct |
31 thm lam.induct |
20 thm lam.exhaust |
32 thm lam.exhaust |
|
33 thm lam.strong_exhaust |
21 thm lam.fv_defs |
34 thm lam.fv_defs |
22 thm lam.bn_defs |
35 thm lam.bn_defs |
23 thm lam.perm_simps |
36 thm lam.perm_simps |
24 thm lam.eq_iff |
37 thm lam.eq_iff |
25 thm lam.fv_bn_eqvt |
38 thm lam.fv_bn_eqvt |