# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269332503 -3600
# Node ID 2b367c80c0d7c9a51463a3959724a151fc4c4ea7
# Parent  a7e60da429e27832c55ecf2f54f3be33d4cc467c
Moved let properties from Term5 to ExLetRec.

diff -r a7e60da429e2 -r 2b367c80c0d7 Nominal/ExLetRec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLetRec.thy	Tue Mar 23 09:21:43 2010 +0100
@@ -0,0 +1,74 @@
+theory ExLet
+imports "Parser"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm"  bind x in t
+| Lt a::"lts" t::"trm"   bind "bn a" in t
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = {}"
+| "bn (Lcons x t l) = {atom x} \<union> (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.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 (simp add: trm_lts.eq_iff alpha_gen2 set_sub)
+  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: alpha_gen2 fresh_star_def eqvts)
+  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
+
+
+end
+
+
+
diff -r a7e60da429e2 -r 2b367c80c0d7 Nominal/Manual/Term5.thy
--- a/Nominal/Manual/Term5.thy	Tue Mar 23 09:13:17 2010 +0100
+++ b/Nominal/Manual/Term5.thy	Tue Mar 23 09:21:43 2010 +0100
@@ -289,56 +289,4 @@
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
 lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
-(* why is this not in Isabelle? *)
-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>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ bv5)
-apply simp
-apply (rule allI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
-apply (rule impI)
-apply (rule impI)
-apply (rule impI)
-apply (simp add: set_sub)
-done
-
-lemma lets_ok:
-  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-thm alpha5_INJ
-apply (simp only: alpha5_INJ)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: eqvts)
-done
-
-lemma lets_ok3:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
-done
-
-
-lemma lets_not_ok1:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: alpha5_INJ alpha_gen)
-apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ)
-done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
-done
-
 end