fixed the lemma where the new names generated by nominal_induct
authorurbanc
Wed, 30 Nov 2005 15:30:08 +0100
changeset 18301 0c5c3b1a700e
parent 18300 ca1ac9e81bc8
child 18302 577e5d19b33c
fixed the lemma where the new names generated by nominal_induct caused problems.
src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 15:27:30 2005 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 30 15:30:08 2005 +0100
@@ -1372,10 +1372,10 @@
   and   t1:: "lam"
   and   t2:: "lam"
   and   a :: "name"
-  shows "pi\<bullet>(t1[a::=t2]) = (pi\<bullet>t1)[(pi\<bullet>a)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 fresh: a t2 rule: lam_induct)
+  shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
+apply(nominal_induct t1 fresh: b t2 rule: lam_induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm)
-apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>ba)")(*A*)
+apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
 apply(simp) 
 apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) 
 done