1 theory ExLet

     2 imports "Parser"

     3 begin

     4 

     5 text {* example 3 or example 5 from Terms.thy *}

     6 

     7 atom_decl name

     8 

     9 ML {* val _ = recursive := true *}

    10 nominal_datatype trm =

    11   Vr "name"

    12 | Ap "trm" "trm"

    13 | Lm x::"name" t::"trm"  bind x in t

    14 | Lt a::"lts" t::"trm"   bind "bn a" in t

    15 and lts =

    16   Lnil

    17 | Lcons "name" "trm" "lts"

    18 binder

    19   bn

    20 where

    21   "bn Lnil = {}"

    22 | "bn (Lcons x t l) = {atom x} \<union> (bn l)"

    23 

    24 thm trm_lts.fv

    25 thm trm_lts.eq_iff

    26 thm trm_lts.bn

    27 thm trm_lts.perm

    28 thm trm_lts.induct

    29 thm trm_lts.distinct

    30 thm trm_lts.fv[simplified trm_lts.supp]

    31 

    32 (* why is this not in HOL simpset? *)

    33 lemma set_sub: "{a, b} - {b} = {a} - {b}"

    34 by auto

    35 

    36 lemma lets_bla:

    37   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"

    38   apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub)

    39   done

    40 

    41 lemma lets_ok:

    42   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"

    43   apply (simp add: trm_lts.eq_iff)

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

    45   apply (simp_all add: alpha_gen2 fresh_star_def eqvts)

    46   done

    47 

    48 lemma lets_ok3:

    49   "x \<noteq> y \<Longrightarrow>

    50    (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

    51    (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"

    52   apply (simp add: alphas trm_lts.eq_iff)

    53   done

    54 

    55 

    56 lemma lets_not_ok1:

    57   "x \<noteq> y \<Longrightarrow>

    58    (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

    59    (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"

    60   apply (simp add: alphas trm_lts.eq_iff)

    61   done

    62 

    63 lemma lets_nok:

    64   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>

    65    (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

    66    (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"

    67   apply (simp add: alphas trm_lts.eq_iff fresh_star_def)

    68   done

    69 

    70 

    71 end

    72 

    73 

    74