equal
deleted
inserted
replaced
1 theory TestMorePerm |
1 theory TestMorePerm |
2 imports "../Parser" |
2 imports "../Parser" |
3 begin |
3 begin |
4 |
|
5 (* Since there are more permutations, we do not know how to prove equivalence |
|
6 (it is probably not true with the way alpha is defined now) so *) |
|
7 ML {* val _ = cheat_equivp := true *} |
|
8 |
|
9 |
|
10 atom_decl name |
|
11 |
|
12 (* example from my PHD *) |
|
13 |
|
14 atom_decl coname |
|
15 |
|
16 nominal_datatype phd = |
|
17 Ax "name" "coname" |
|
18 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
19 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
20 | AndL1 n::"name" t::"phd" "name" bind n in t |
|
21 | AndL2 n::"name" t::"phd" "name" bind n in t |
|
22 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
23 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
24 |
|
25 thm phd.fv |
|
26 thm phd.eq_iff |
|
27 thm phd.bn |
|
28 thm phd.perm |
|
29 thm phd.induct |
|
30 thm phd.distinct |
|
31 thm phd.fv[simplified phd.supp] |
|
32 |
4 |
33 text {* weirdo example from Peter Sewell's bestiary *} |
5 text {* weirdo example from Peter Sewell's bestiary *} |
34 |
6 |
35 nominal_datatype weird = |
7 nominal_datatype weird = |
36 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
8 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |