--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLet.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,236 @@
+theory ExLet
+imports "../Parser" "../../Attic/Prove"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+ML {* val _ = alpha_type := AlphaLst *}
+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
+(*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+
+thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct[no_vars]
+thm trm_lts.inducts[no_vars]
+thm trm_lts.distinct
+(*thm trm_lts.supp*)
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
+
+
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw pi (Lnil_raw) = Lnil_raw"
+| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+  apply simp_all
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma permute_bn_zero:
+  "permute_bn 0 a = a"
+  apply(induct a rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma permute_bn_add:
+  "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+  oops
+
+lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+  apply(induct lts rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
+  done
+
+lemma perm_bn:
+  "p \<bullet> bn l = bn(permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma fv_perm_bn:
+  "fv_bn l = fv_bn (permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+lemma fv_fv_bn:
+  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  by blast
+
+lemma Lt_subst:
+  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  apply (simp only: trm_lts.eq_iff)
+  apply (rule_tac x="q" in exI)
+  apply (simp add: alphas)
+  apply (simp add: permute_bn_alpha_bn)
+  apply (simp add: perm_bn[symmetric])
+  apply (simp add: eqvts[symmetric])
+  apply (simp add: supp_abs)
+  apply (simp add: trm_lts.supp)
+  apply (rule supp_perm_eq[symmetric])
+  apply (subst supp_finite_atom_set)
+  apply (rule finite_Diff)
+  apply (simp add: finite_supp)
+  apply (assumption)
+  done
+
+
+lemma fin_bn:
+  "finite (set (bn l))"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(simp_all add:permute_bn eqvts)
+  done
+
+thm trm_lts.inducts[no_vars]
+
+lemma 
+  fixes t::trm
+  and   l::lts
+  and   c::"'a::fs"
+  assumes a1: "\<And>name c. P1 c (Vr name)"
+  and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
+  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
+  and     a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+  and     a5: "\<And>c. P2 c Lnil"
+  and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
+  shows "P1 c t" and "P2 c l"
+proof -
+  have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
+       b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
+    apply(induct rule: trm_lts.inducts)
+    apply(simp)
+    apply(rule a1)
+    apply(simp)
+    apply(rule a2)
+    apply(simp)
+    apply(simp)
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" 
+               and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+    apply(rule supp_perm_eq)
+    apply(simp)
+    apply(simp)
+    apply(rule a3)
+    apply(simp add: atom_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(rule at_set_avoiding2_atom)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_def)
+    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    apply(subst Lt_subst)
+    apply assumption
+    apply(rule a4)
+    apply(simp add:perm_bn[symmetric])
+    apply(simp add: eqvts)
+    apply (simp add: fresh_star_def fresh_def)
+    apply(rotate_tac 1)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def fresh_def supp_abs)
+    apply(simp add: eqvts permute_bn)
+    apply(rule a5)
+    apply(simp add: permute_bn)
+    apply(rule a6)
+    apply simp
+    apply simp
+    done
+  then have a: "P1 c (0 \<bullet> t)" by blast
+  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+
+
+
+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))"
+  by (simp add: trm_lts.eq_iff)
+
+lemma lets_ok:
+  "(Lt (Lcons x (Vr y) 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)
+  apply (simp add: 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 fresh_star_def eqvts)
+  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
+
+
+