2679
|
1 |
theory Minimal
|
2681
|
2 |
imports "Nominal2"
|
2679
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
|
7 |
nominal_datatype lam =
|
|
8 |
Var "name"
|
|
9 |
| App "lam" "lam"
|
|
10 |
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
|
|
11 |
|
2686
|
12 |
|
|
13 |
|
2679
|
14 |
lemma alpha_test:
|
|
15 |
shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
|
|
16 |
by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
|
|
17 |
|
|
18 |
end |