1 theory TestMorePerm |
1 theory TestMorePerm |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 "Weirdo" example from Peter Sewell's bestiary. |
6 "Weirdo" example from Peter Sewell's bestiary. |
7 |
7 |
8 In case of deep binders, it is not coverd by our |
8 This example is not covered by our binding |
9 approach of defining alpha-equivalence with a |
9 specification. |
10 single permutation. |
|
11 |
|
12 Check whether it works with shallow binders as |
|
13 defined below. |
|
14 |
10 |
15 *} |
11 *} |
16 ML {* val _ = cheat_equivp := true *} |
12 ML {* val _ = cheat_equivp := true *} |
17 |
13 |
18 atom_decl name |
14 atom_decl name |
19 |
15 |
20 nominal_datatype foo = |
16 nominal_datatype weird = |
21 Foo_var "name" |
17 Foo_var "name" |
22 | Foo_pair "foo" "foo" |
18 | Foo_pair "weird" "weird" |
23 | Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo" |
19 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
24 bind x in p1, bind x in p2, |
20 bind x in p1 p2, |
25 bind y in p2, bind y in p3 |
21 bind y in p2 p3 |
26 |
22 |
27 thm alpha_foo_raw.intros[no_vars] |
23 thm alpha_weird_raw.intros[no_vars] |
28 |
24 |
29 thm permute_weird_raw.simps[no_vars] |
25 thm permute_weird_raw.simps[no_vars] |
30 thm alpha_weird_raw.intros[no_vars] |
26 thm alpha_weird_raw.intros[no_vars] |
31 thm fv_weird_raw.simps[no_vars] |
27 thm fv_weird_raw.simps[no_vars] |
|
28 |
|
29 declare permute_weird_raw.simps[eqvt] |
|
30 declare alpha_gen_eqvt[eqvt] |
|
31 equivariance alpha_weird_raw |
32 |
32 |
33 |
33 |
34 end |
34 end |
35 |
35 |
36 |
36 |