--- a/Nominal/Ex/Lambda.thy	Mon Apr 26 13:08:14 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 26 20:17:41 2010 +0200
@@ -156,10 +156,11 @@
       apply -
       apply(perm_strict_simp)
       apply(rule a1)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(drule_tac p="p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(rotate_tac 1)
+      apply(drule_tac p="p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
       done
@@ -168,12 +169,13 @@
     then show ?case
       apply -
       apply(perm_strict_simp)
-      apply(rule_tac ?T1.0="p \<bullet> T1" in a2)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(rule a2)
+      apply(drule_tac p="p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
       apply(assumption)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(rotate_tac 2)
+      apply(drule_tac p="p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
       apply(assumption)
@@ -185,31 +187,33 @@
       apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 
         supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
       apply(erule exE)
-      apply(rule_tac t="p \<bullet> \<Gamma>" and  s="q \<bullet> p \<bullet> \<Gamma>" in subst)
+      apply(rule_tac t="p \<bullet> \<Gamma>" and  s="(q + p) \<bullet> \<Gamma>" in subst)
+      apply(simp only: permute_plus)
       apply(rule supp_perm_eq)
       apply(simp add: supp_Pair fresh_star_union)
-      apply(rule_tac t="p \<bullet> Lam x t" and  s="q \<bullet> p \<bullet> Lam x t" in subst)
-      apply(rule supp_perm_eq)
-      apply(simp add: supp_Pair fresh_star_union)
-      apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst)
+      apply(rule_tac t="p \<bullet> Lam x t" and  s="(q + p) \<bullet> Lam x t" in subst)
+      apply(simp only: permute_plus)
       apply(rule supp_perm_eq)
       apply(simp add: supp_Pair fresh_star_union)
-      apply(simp add: eqvts)
+      apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)
+      apply(simp only: permute_plus)
+      apply(rule supp_perm_eq)
+      apply(simp add: supp_Pair fresh_star_union)
+      apply(simp (no_asm) only: eqvts)
       apply(rule a3)
+      apply(simp only: eqvts permute_plus)
       apply(simp add: fresh_star_def)
-      apply(rule_tac p="-q" in permute_boolE)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(drule_tac p="q + p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
-      apply(rule_tac p="-q" in permute_boolE)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(rule_tac p="-p" in permute_boolE)
+      apply(rotate_tac 1)
+      apply(drule_tac p="q + p" in permute_boolI)
       apply(perm_strict_simp add: permute_minus_cancel)
       apply(assumption)
       apply(drule_tac x="d" in meta_spec)
       apply(drule_tac x="q + p" in meta_spec)
-      apply(simp)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
       apply(rule at_set_avoiding2)
       apply(simp add: finite_supp)
       apply(simp add: finite_supp)
@@ -219,10 +223,11 @@
 	(* supplied by the user *)
       apply(simp add: fresh_star_prod)
       apply(simp add: fresh_star_def)
-
-
-      done
-(* HERE *)      
+      sorry
+  qed
+  then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .
+  then show "P c \<Gamma> t T" by simp
+qed
 
 
 
@@ -414,6 +419,38 @@
 done
 *)
 
+ML {*
+fun mk_avoids ctxt params name set =
+  let
+    val (_, ctxt') = ProofContext.add_fixes
+      (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
+    fun mk s =
+      let
+        val t = Syntax.read_term ctxt' s;
+        val t' = list_abs_free (params, t) |>
+          funpow (length params) (fn Abs (_, _, t) => t)
+      in (t', HOLogic.dest_setT (fastype_of t)) end
+      handle TERM _ =>
+        error ("Expression " ^ quote s ^ " to be avoided in case " ^
+          quote name ^ " is not a set type");
+    fun add_set p [] = [p]
+      | add_set (t, T) ((u, U) :: ps) =
+          if T = U then
+            let val S = HOLogic.mk_setT T
+            in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps
+            end
+          else (u, U) :: add_set (t, T) ps
+  in
+    (mk #> add_set) set 
+  end;
+*}
+
+
+ML {* 
+  writeln (commas (map (Syntax.string_of_term @{context} o fst) 
+    (mk_avoids @{context} [] "t_Var" "{x}" []))) 
+*}
+
 
 ML {*