branch | Nominal2-Isabelle2011-1 |
changeset 3070 | 4b4742aa43f2 |
parent 3069 | 78d828f43cdf |
child 3071 | 11f6a561eb4b |
3069:78d828f43cdf | 3070:4b4742aa43f2 |
---|---|
1 theory Minimal |
|
2 imports "Nominal2" |
|
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 |
|
12 |
|
13 |
|
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 |