# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307013243 -3600
# Node ID ab6c24ae137fb6e1ab687d2bacc7961d0b4aae48
# Parent  13af2c8d732927ec95b180d5473dc48671895dac# Parent  377bea405940f3133cff345d99adca06d05c1c09
merged

diff -r 13af2c8d7329 -r ab6c24ae137f Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 12:09:31 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 12:14:03 2011 +0100
@@ -561,16 +561,9 @@
   apply (rule, perm_simp, rule)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
-  apply (simp add: Abs1_eq_iff)
-  apply (auto)
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
   apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
-  apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
   done
 
 termination
@@ -620,6 +613,7 @@
   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 unfolding eqvt_def Z_graph_def
 apply (rule, perm_simp, rule)
 oops
@@ -633,7 +627,7 @@
   "f [] = 0"
 | "f [e] = e"
 | "f (l @ m) = f l + f m"
-apply(simp_all)
+  apply(simp_all)
 oops
 
 
diff -r 13af2c8d7329 -r ab6c24ae137f Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jun 02 12:09:31 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 02 12:14:03 2011 +0100
@@ -427,15 +427,17 @@
   apply (simp add: fresh_star_Un fresh_star_inter1)
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
+  apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: inter_eqvt)
+  apply blast
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
-oops
-(*
-  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
+  apply (simp add: IntI image_eqI)
   apply (drule subsetD[OF supp_subst])
-  apply auto[1]
   apply (simp add: fresh_star_def fresh_def)
+  apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: )
   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
-  apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt)
+  apply (metis inf1I inter_eqvt mem_def supp_eqvt )
   apply (rotate_tac 6)
   apply (drule sym)
   apply (simp add: subst_eqvt)
@@ -446,7 +448,7 @@
   apply (simp add: fresh_star_def fresh_def)
   apply blast
   done
-*)
+
 
 text {* Some Tests about Alpha-Equality *}