--- a/Nominal/Ex/BetaCR.thy	Tue Dec 20 11:40:04 2011 +0900
+++ b/Nominal/Ex/BetaCR.thy	Tue Dec 20 16:12:32 2011 +0900
@@ -153,6 +153,13 @@
 lemma Lam_beta: "A \<longrightarrow>b* B \<Longrightarrow> Lam [x]. A \<longrightarrow>b* Lam [x]. B"
   by (erule beta_star.induct) auto
 
+lemma Lam_rsp: "A \<approx> B \<Longrightarrow> Lam [x]. A \<approx> Lam [x]. B"
+  unfolding equ_def
+  apply auto
+  apply (rule_tac x="Lam [x]. r" in exI)
+  apply (auto simp add: Lam_beta)
+  done
+
 lemma [quot_respect]:
   shows "(op = ===> equ) Var Var"
   and   "(equ ===> equ ===> equ) App App"
@@ -221,13 +228,17 @@
 lemma beta_subst: "A \<longrightarrow>b* B \<Longrightarrow> C \<longrightarrow>b* D \<Longrightarrow> A [x ::= C] \<longrightarrow>b* B [x ::= D]"
   using beta_subst1 beta_subst2 beta_star_trans by metis
 
+lemma subst_rsp_pre:
+  "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]"
+  unfolding equ_def
+  apply auto
+  apply (rule_tac x="r [xa ::= ra]" in exI)
+  apply (simp add: beta_subst)
+  done
+
 lemma [quot_respect]:
   shows "(equ ===> op = ===> equ ===> equ) subst subst"
-unfolding fun_rel_def equ_def
-apply auto
-apply (rule_tac x="r [xa ::= ra]" in exI)
-apply (simp add: beta_subst)
-done
+unfolding fun_rel_def by (auto simp add: subst_rsp_pre)
 
 lemma [quot_respect]:
   shows "(op = ===> equ ===> equ) permute permute"
@@ -307,20 +318,21 @@
 quotient_definition subst_qlam ("_[_ ::q= _]")
   where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  
 
-lemmas qsubst = subst.simps(1-2)[quot_lifted]
-
 definition
   "Supp t = \<Inter>{supp s | s. s \<approx> t}"
 
-lemma [quot_respect]:
-  shows "(equ ===> op=) Supp Supp"
-  unfolding fun_rel_def Supp_def
-  apply(intro allI impI)
+lemma Supp_rsp:
+  "a \<approx> b \<Longrightarrow> Supp a = Supp b"
+  unfolding Supp_def
   apply(rule_tac f="Inter" in arg_cong)
   apply(auto)
   apply (metis equ_trans)
   by (metis equivp_def qlam_equivp)
 
+lemma [quot_respect]:
+  shows "(equ ===> op=) Supp Supp"
+  unfolding fun_rel_def by (auto simp add: Supp_rsp)
+
 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 
   is "Supp::lam \<Rightarrow> atom set"
 
@@ -332,6 +344,99 @@
 apply(auto simp add: equ_refl)
 done
 
+lemma supp_subst:
+  shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"
+  by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)
+
+lemma supp_beta: "x \<longrightarrow>b r \<Longrightarrow> supp r \<subseteq> supp x"
+  apply (induct rule: beta.induct)
+  apply (simp_all add: lam.supp)
+  apply blast+
+  using supp_subst by blast
+
+lemma supp_beta_star: "x \<longrightarrow>b* r \<Longrightarrow> supp r \<subseteq> supp x"
+  apply (erule beta_star.induct)
+  apply auto
+  using supp_beta by blast
+
+lemma supp_equ: "x \<approx> y \<Longrightarrow> \<exists>z. z \<approx> x \<and> supp z \<subseteq> supp x \<inter> supp y"
+  unfolding equ_def
+  apply (simp (no_asm) only: equ_def[symmetric])
+  apply (elim exE)
+  apply (rule_tac x=r in exI)
+  apply rule
+  apply (metis bs1 equ_def)
+  using supp_beta_star by blast
+
+lemma supp_psubset: "Supp x \<subset> supp x \<Longrightarrow> \<exists>t. t \<approx> x \<and> supp t \<subset> supp x"
+proof -
+  assume "Supp x \<subset> supp x"
+  then obtain a where "a \<in> supp x" "a \<notin> Supp x" by blast
+  then obtain y where nin: "y \<approx> x" "a \<notin> supp y" unfolding Supp_def by blast
+  then obtain t where eq: "t \<approx> x" "supp t \<subseteq> supp x \<inter> supp y"
+    using supp_equ equ_sym by blast
+  then have "supp t \<subset> supp x" using nin
+    by (metis `(a\<Colon>atom) \<in> supp (x\<Colon>lam)` le_infE psubset_eq set_rev_mp)
+  then show "\<exists>t. t \<approx> x \<and> supp t \<subset> supp x" using eq by blast
+qed
+
+lemma Supp_exists: "\<exists>t. supp t = Supp t \<and> t \<approx> x"
+proof -
+  have "\<And>fs x. supp x = fs \<Longrightarrow> \<exists>t. supp t = Supp t \<and> t \<approx> x"
+  proof -
+    fix fs
+    show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
+    proof (cases "finite fs")
+      case True
+      assume fs: "finite fs"
+      then show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
+      proof (induct fs rule: finite_psubset_induct, clarify)
+        fix A :: "atom set" fix x :: lam
+        assume IH: "\<And>B xa. \<lbrakk>B \<subset> supp x; supp xa = B\<rbrakk> \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> xa"
+        show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
+        proof (cases "supp x = Supp x")
+          assume "supp x = Supp x"
+          then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
+            by (rule_tac x="x" in exI) (simp add: equ_refl)
+        next
+          assume "supp x \<noteq> Supp x"
+          then have "Supp x \<subset> supp x" using Supp_supp by blast
+          then obtain y where a1: "supp y \<subset> supp x" "y \<approx> x"
+            using supp_psubset by blast
+          then obtain t where "supp t = Supp t \<and> t \<approx> y"
+            using IH[of "supp y" y] by blast
+          then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" using a1 equ_trans
+            by blast
+        qed
+      qed
+    next
+      case False
+      fix x :: lam
+      assume "supp x = fs" "infinite fs"
+      then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"
+        by (auto simp add: finite_supp)
+    qed simp
+  qed
+  then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by blast
+qed
+
+lemma subst3: "x \<noteq> y \<and> atom x \<notin> Supp s \<Longrightarrow> Lam [x]. t [y ::= s] \<approx> Lam [x]. (t [y ::= s])"
+proof -
+  assume as: "x \<noteq> y \<and> atom x \<notin> Supp s"
+  obtain s' where s: "supp s' = Supp s'" "s' \<approx> s" using Supp_exists[of s] by blast
+  then have lhs: "Lam [x]. t [y ::= s] \<approx> Lam [x]. t [y ::= s']" using subst_rsp_pre equ_refl equ_sym by blast
+  have supp: "Supp s' = Supp s" using Supp_rsp s(2) by blast
+  have lhs_rhs: "Lam [x]. t [y ::= s'] = Lam [x]. (t [y ::= s'])"
+    by (simp add: fresh_def supp_Pair s supp as supp_at_base)
+  have "t [y ::= s'] \<approx> t [y ::= s]"
+    using subst_rsp_pre[OF equ_refl s(2)] .
+  with Lam_rsp have rhs: "Lam [x]. (t [y ::= s']) \<approx> Lam [x]. (t [y ::= s])" .
+  show ?thesis 
+    using lhs[unfolded lhs_rhs] rhs equ_trans by blast
+qed
+
+thm subst3[quot_lifted]
+
 lemma Supp_Lam:
   "atom a \<notin> Supp (Lam [a].t)"
 proof -