diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-theory ExLetRec
-imports "../NewParser"
-begin
-
-
-text {* example 3 or example 5 from Terms.thy *}
-
-atom_decl name
-
-ML {* val _ = cheat_equivp := true *}
-
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind_set x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in a t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
-binder
-  bn
-where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
-
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp]
-
-
-(* why is this not in HOL simpset? *)
-lemma set_sub: "{a, b} - {b} = {a} - {b}"
-by auto
-
-lemma lets_bla:
-  "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))"
-  apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
-  done
-
-lemma lets_ok:
-  "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
-  apply (simp add: trm_lts.eq_iff)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
-  done
-
-lemma lets_ok3:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  done
-
-
-lemma lets_not_ok1:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
-   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
-  done
-
-lemma lets_ok4:
-  "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
-   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
-  apply (simp add: alphas trm_lts.eq_iff supp_at_base)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp add: atom_eqvt fresh_star_def)
-  done
-
-end
-
-
-