1595
|
1 |
theory TestMorePerm
|
|
2 |
imports "Parser"
|
|
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 |
|
|
33 |
text {* weirdo example from Peter Sewell's bestiary *}
|
|
34 |
|
|
35 |
nominal_datatype weird =
|
|
36 |
WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
|
|
37 |
bind x in p1, bind x in p2, bind y in p2, bind y in p3
|
|
38 |
| WV "name"
|
|
39 |
| WP "weird" "weird"
|
|
40 |
|
|
41 |
thm permute_weird_raw.simps[no_vars]
|
|
42 |
thm alpha_weird_raw.intros[no_vars]
|
|
43 |
thm fv_weird_raw.simps[no_vars]
|
|
44 |
|
|
45 |
|
|
46 |
end
|
|
47 |
|
|
48 |
|
|
49 |
|