diff -r fc4b3e367c86 -r 83744806b660 Nominal/Ex/Beta.thy
--- a/Nominal/Ex/Beta.thy	Wed Nov 09 11:44:01 2011 +0000
+++ b/Nominal/Ex/Beta.thy	Thu Nov 10 01:15:19 2011 +0000
@@ -175,6 +175,35 @@
 apply(simp add: swap_fresh_fresh)
 done
 
+lemma rep_qlam_inverse:
+  "abs_qlam (rep_qlam t) = t"
+by (metis Quotient_abs_rep Quotient_qlam)
+
+lemma supports_rep_qlam:
+  "supp (rep_qlam t) supports t"
+apply(subst (2) rep_qlam_inverse[symmetric])
+apply(rule supports_abs_qlam)
+done
+
+ lemma supports_qvar:
+  "{atom x} supports (QVar x)"
+apply(subgoal_tac "supp (Var x) supports (abs_qlam (Var x))")
+apply(simp add: lam.supp supp_at_base)
+defer
+apply(rule supports_abs_qlam)
+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])
@@ -203,24 +232,15 @@
 
 lemma
   fixes t::"qlam"
-  shows "supp t = supp_qlam t"
+  shows "(supp x) supports (QVar x)"
+apply(rule_tac x="QVar x" in Abs_qlam_cases)
+apply(auto)
+thm QVar_def
 apply(descending)
 oops
 
 
  
-
-lemma [quot_respect]:
-  shows "(equ ===> op=) Size Size"
-unfolding fun_rel_def
-unfolding Size_def
-apply(auto)
-apply(rule_tac f="Least" in arg_cong)
-apply(auto)
-apply (metis equ_trans)
-by (metis equivp_def qlam_equivp)
-
-
 section {* Size *}
 
 definition
@@ -265,7 +285,6 @@
   "size (QLam [x].t) = Suc (size t)"
 apply(descending)
 apply(simp add: Size_def)
-apply(auto)
 apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2)
 apply(simp add: Collect_def)
 apply(rule_tac x="Lam [x].t" in exI)
@@ -274,7 +293,6 @@
 apply(rule_tac x="t" in exI)
 apply(auto intro: equ_refl)[1]
 apply(simp add: Collect_def)
-apply(auto)[1]
 defer
 apply(simp add: Collect_def)
 apply(auto)[1]