1604
+ − 1 theory ExLetRec
1603
+ − 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