diff -r 324b148fc6b5 -r da0fccee125c Nominal/Ex/Beta.thy
--- a/Nominal/Ex/Beta.thy	Sat Nov 26 09:48:14 2011 +0000
+++ b/Nominal/Ex/Beta.thy	Sat Nov 26 09:53:52 2011 +0000
@@ -161,6 +161,32 @@
 
 end
 
+quotient_definition subst_qlam ("_[_ ::q= _]")
+ where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst  
+
+lemma
+  "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))"
+apply(descending)
+apply(simp)
+apply(auto intro: equ_refl)
+done
+
+lemma
+  "(QApp t1 t2)[y ::q= s] = QApp (t1[y ::q= s]) (t2[y ::q= s])"
+apply(descending)
+apply(simp)
+apply(rule equ_refl)
+done
+
+lemma
+  "(QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])"
+apply(descending)
+apply(subst subst.simps)
+prefer 3
+apply(rule equ_refl)
+oops
+
+
 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)"
  apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])
  apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified])
@@ -194,22 +220,6 @@
 apply(simp add: QVar_def)
 done
 
- lemma supports_qapp:
-  "supp (t, s) supports (QApp t s)"
-apply(subgoal_tac "supp (t, s) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))")
-apply(simp add: QApp_def)
-apply(subgoal_tac "supp (App (rep_qlam t) (rep_qlam s)) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))")
-prefer 2
-apply(rule supports_abs_qlam)
-apply(simp add: lam.supp)
-oops
-
-lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)"
- apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified])
- apply (rule rep_abs_rsp[OF Quotient_qlam])
- apply (rule equ_refl)
- done
-
 section {* Supp *}
 
 definition
@@ -229,6 +239,37 @@
 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" 
   is "Supp::lam \<Rightarrow> atom set"
 
+lemma s:
+  assumes "s \<approx> t"
+  shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)"
+using assms
+by (metis Quotient_qlam Quotient_rel_abs)
+
+lemma ss:
+  "Supp t supports (abs_qlam t)"
+apply(simp only: supports_def)
+apply(rule allI)+
+apply(rule impI)
+apply(rule swap_fresh_fresh)
+apply(drule conjunct1)
+apply(auto)[1]
+apply(simp add: Supp_def)
+apply(auto)[1]
+apply(simp add: s[symmetric])
+apply(rule supports_fresh)
+apply(rule supports_abs_qlam)
+apply(simp add: finite_supp)
+apply(simp)
+apply(drule conjunct2)
+apply(auto)[1]
+apply(simp add: Supp_def)
+apply(auto)[1]
+apply(simp add: s[symmetric])
+apply(rule supports_fresh)
+apply(rule supports_abs_qlam)
+apply(simp add: finite_supp)
+apply(simp)
+done
 
 lemma
   fixes t::"qlam"