1 theory Term5

     2 imports "Parser"

     3 begin

     4 

     5 atom_decl name

     6 

     7 ML {* restricted_nominal := 2 *}

     8 

     9 nominal_datatype trm5 =

    10   Vr5 "name"

    11 | Ap5 "trm5" "trm5"

    12 | Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t

    13 and lts =

    14   Lnil

    15 | Lcons "name" "trm5" "lts"

    16 binder

    17   bv5

    18 where

    19   "bv5 Lnil = {}"

    20 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"

    21 

    22 lemma lets_ok:

    23   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"

    24 apply (simp add: trm5_lts_inject)

    25 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

    26 apply (simp_all add: alpha_gen)

    27 apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)

    28 done

    29 

    30 lemma lets_nok:

    31   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"

    32 apply (simp only: trm5_lts_inject not_ex)

    33 apply (rule allI)

    34 apply (simp add: alpha_gen)

    35 apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)

    36 done

    37 

    38 end