1 theory ExLetRec

     2 imports "../NewParser"

     3 begin

     4 

     5 

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

     7 

     8 atom_decl name

     9 

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

    11 

    12 nominal_datatype trm =

    13   Vr "name"

    14 | Ap "trm" "trm"

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

    16 | Lt a::"lts" t::"trm"   bind "bn a" in a 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 

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

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

    38 by auto

    39 

    40 lemma lets_bla:

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

    42   apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)

    43   done

    44 

    45 lemma lets_ok:

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

    47   apply (simp add: trm_lts.eq_iff)

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

    49   apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)

    50   done

    51 

    52 lemma lets_ok3:

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

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

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

    56   apply (simp add: alphas trm_lts.eq_iff)

    57   done

    58 

    59 

    60 lemma lets_not_ok1:

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

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

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

    64   apply (simp add: alphas trm_lts.eq_iff)

    65   done

    66 

    67 lemma lets_nok:

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

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

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

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

    72   done

    73 

    74 lemma lets_ok4:

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

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

    77   apply (simp add: alphas trm_lts.eq_iff supp_at_base)

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

    79   apply (simp add: atom_eqvt fresh_star_def)

    80   done

    81 

    82 end

    83 

    84 

    85