1 theory ExLetRec

     2 imports "../Parser"

     3 begin

     4 

     5 

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

     7 

     8 atom_decl name

     9 

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

    11 ML {* val _ = alpha_type := AlphaLst *}

    12 nominal_datatype trm =

    13   Vr "name"

    14 | Ap "trm" "trm"

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

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

    17 and lts =

    18   Lnil

    19 | Lcons "name" "trm" "lts"

    20 binder

    21   bn

    22 where

    23   "bn Lnil = []"

    24 | "bn (Lcons x t l) = (atom x) # (bn l)"

    25 

    26 thm trm_lts.fv

    27 thm trm_lts.eq_iff

    28 thm trm_lts.bn

    29 thm trm_lts.perm

    30 thm trm_lts.induct

    31 thm trm_lts.distinct

    32 thm trm_lts.supp

    33 thm trm_lts.fv[simplified trm_lts.supp]

    34 

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

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

    37 by auto

    38 

    39 lemma lets_bla:

    40   "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))"

    41   by (simp add: trm_lts.eq_iff alphas2 set_sub)

    42 

    43 lemma lets_ok:

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

    45   apply (simp add: trm_lts.eq_iff)

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

    47   apply (simp_all add: alphas2 fresh_star_def eqvts)

    48   done

    49 

    50 lemma lets_ok3:

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

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

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

    54   apply (simp add: alphas trm_lts.eq_iff)

    55   done

    56 

    57 

    58 lemma lets_not_ok1:

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

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

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

    62   apply (simp add: alphas trm_lts.eq_iff)

    63   done

    64 

    65 lemma lets_nok:

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

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

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

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

    70   done

    71 

    72 lemma lets_ok4:

    73   "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =

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

    75   apply (simp add: alphas trm_lts.eq_iff)

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

    77   apply (simp add: atom_eqvt fresh_star_def)

    78   done

    79 

    80 end

    81 

    82 

    83