1604
+ − 1 theory ExLetRec
1773
+ − 2 imports "../Parser"
1603
+ − 3 begin
+ − 4
1685
+ − 5
1603
+ − 6 text {* example 3 or example 5 from Terms.thy *}
+ − 7
+ − 8 atom_decl name
+ − 9
+ − 10 ML {* val _ = recursive := true *}
1685
+ − 11 ML {* val _ = alpha_type := AlphaLst *}
1603
+ − 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
1685
+ − 23 "bn Lnil = []"
+ − 24 | "bn (Lcons x t l) = (atom x) # (bn l)"
1603
+ − 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
1685
+ − 32 thm trm_lts.supp
1603
+ − 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))"
1674
+ − 41 by (simp add: trm_lts.eq_iff alphas2 set_sub)
1603
+ − 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)
1674
+ − 47 apply (simp_all add: alphas2 fresh_star_def eqvts)
1603
+ − 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
1685
+ − 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
1603
+ − 79
+ − 80 end
+ − 81
+ − 82
+ − 83