7 nominal_datatype lam =

     7 nominal_datatype lam =

     8   Var "name"

     8   Var "name"

     9 | App "lam" "lam"

     9 | App "lam" "lam"

    10 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)

    10 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)

    11 

    11 

    12 lemma alpha_test:

    14 lemma alpha_test:

    13   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"

    15   shows "Lam [x]. (Var x) = Lam [y]. (Var y)"

    14   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)

    16   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)

    15 

    17 

    16 end

    18 end