--- a/Nominal/Ex/Let.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Ex/Let.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -30,278 +30,7 @@
 thm trm_assn.exhaust
 thm trm_assn.strong_exhaust
 
-lemma 
-  fixes t::trm
-  and   as::assn
-  and   c::"'a::fs"
-  assumes a1: "\<And>x c. P1 c (Var x)"
-  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
-  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
-  and     a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
-  and     a5: "\<And>c. P2 c ANil"
-  and     a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
-  shows "P1 c t" "P2 c as"
-using assms
-apply(induction_schema)
-apply(rule_tac y="t" in trm_assn.strong_exhaust(1))
-apply(blast)
-apply(blast)
-apply(blast)
-apply(blast)
-apply(rule_tac ya="as" in trm_assn.strong_exhaust(2))
-apply(blast)
-apply(blast)
-apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
-apply(simp_all add: trm_assn.size)
-done
-
-text {* *}
-
-
 (*
-proof -
-  have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" 
-   and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"
-    apply(induct rule: trm_assn.inducts)
-    apply(simp)
-    apply(rule a1)
-    apply(simp)
-    apply(rule a2)
-    apply(assumption)
-    apply(assumption)
-    -- "lam case"
-    apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
-    apply(erule exE)
-    apply(erule conjE)
-    apply(drule supp_perm_eq[symmetric])
-    apply(simp)
-    apply(thin_tac "?X = ?Y")
-    apply(rule a3)
-    apply(simp add: atom_eqvt permute_set_eq)
-    apply(simp only: permute_plus[symmetric])
-    apply(rule at_set_avoiding2)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: freshs fresh_star_def)
-    --"let case"
-    apply(simp)
-    thm trm_assn.eq_iff
-    thm eq_iffs
-    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")
-    apply(erule exE)
-    apply(erule conjE)
-    prefer 2
-    apply(rule at_set_avoiding2)
-    apply(rule fin_bn)
-    apply(simp add: finite_supp)
-    apply(simp add: finite_supp)
-    apply(simp add: abs_fresh)
-    apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
-    prefer 2
-    apply(rule a4)
-    prefer 4
-    apply(simp add: eq_iffs)
-    apply(rule conjI)
-    prefer 2
-    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    prefer 2
-    apply(simp add: eq_iffs)
-    thm eq_iffs
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    apply(simp add: supps)
-    apply(simp add: fresh_star_def freshs)
-    apply(drule supp_perm_eq[symmetric])
-    apply(simp)
-    apply(simp add: eq_iffs)
-    apply(simp)
-    apply(thin_tac "?X = ?Y")
-    apply(rule a4) 
-    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    apply(subst permute_plus[symmetric])
-    apply(blast)
-    apply(simp add: supps)
-    thm at_set_avoiding2
-    --"HERE"
-    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 freshs)
-    apply(rule ballI)
-    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
-*)
-
-text {* *}
-
-(*
-
-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 (rule TrueI)+
-  apply simp_all
-  apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp_all
-  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)
-  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 Lt_subst:
-  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
-  apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
-  apply (rule_tac x="q" in exI)
-  apply (simp add: alphas)
-  apply (simp add: perm_bn[symmetric])
-  apply(rule conjI)
-  apply(drule supp_perm_eq)
-  apply(simp add: abs_eq_iff)
-  apply(simp add: alphas_abs alphas)
-  apply(drule conjunct1)
-  apply (simp add: trm_lts.supp)
-  apply(simp add: supp_abs)
-  apply (simp add: trm_lts.supp)
-  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)
-    thm Lt_subst
-    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)