--- 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"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/QuotientSet.thy	Sat Nov 26 09:53:52 2011 +0000
@@ -0,0 +1,91 @@
+theory QuotientSet
+imports 
+  "../Nominal2"
+begin
+
+lemma supp_quot:
+  "(supp (R, x)) supports (R `` {x})"
+unfolding supports_def
+unfolding fresh_def[symmetric]
+apply(perm_simp)
+apply(simp add: swap_fresh_fresh)
+done
+
+lemma
+  assumes "equiv UNIV R"
+  and "(x, y) \<in> R"
+  shows "R `` {x} = R `` {y}"
+using assms
+by (rule equiv_class_eq)
+
+lemma s1:
+  assumes "equiv UNIV R"
+  and "(x, y) \<in> R"
+  shows "a \<sharp> (R `` {x}) \<longleftrightarrow> a \<sharp> (R `` {y})"
+using assms
+apply(subst equiv_class_eq)
+apply(auto)
+done
+
+lemma s2:
+  fixes x::"'a::fs"
+  assumes "equiv UNIV R"
+  and     "supp R = {}"
+  shows "\<Inter>{supp y | y. (x, y) \<in> R} supports (R `` {x})"
+unfolding supports_def
+apply(rule allI)+
+apply(rule impI)
+apply(rule swap_fresh_fresh)
+apply(drule conjunct1)
+apply(auto)[1]
+apply(subst s1)
+apply(rule assms)
+apply(assumption)
+apply(rule supports_fresh)
+apply(rule supp_quot)
+apply(simp add: supp_Pair finite_supp assms)
+apply(simp add: supp_Pair assms)
+apply(drule conjunct2)
+apply(auto)[1]
+apply(subst s1)
+apply(rule assms)
+apply(assumption)
+apply(rule supports_fresh)
+apply(rule supp_quot)
+apply(simp add: supp_Pair finite_supp assms)
+apply(simp add: supp_Pair assms)
+done
+
+lemma s3:
+  fixes S::"'a::fs set"
+  assumes "finite S"
+  and "S \<noteq> {}"
+  and "a \<sharp> S"
+  shows "\<exists>x \<in> S. a \<sharp> x"
+using assms
+apply(auto simp add: fresh_def)
+apply(subst (asm) supp_of_finite_sets)
+apply(auto)
+done
+
+(*
+lemma supp_inter:
+  fixes x::"'a::fs"
+  assumes "equiv UNIV R"
+  and     "supp R = {}"
+  shows "supp (R `` {x}) = \<Inter>{supp y | y. (x, y) \<in> R}"
+apply(rule finite_supp_unique)
+apply(rule s2)
+apply(rule assms)
+apply(rule assms)
+apply(metis (lam_lifting, no_types) at_base_infinite finite_UNIV)
+*)
+
+  
+
+
+
+end
+
+
+