# HG changeset patch
# User urbanc
# Date 1147781499 -7200
# Node ID 247ca17caddd1a449d4afdb3497c54b3751f3fda
# Parent  33a94c5fc7bb212acf2f8c26359cbefea8a045de
added a much simpler proof for the iteration and
recursion combinator - this also fixes a bug which
prevented the nightly build from being build (sorry)

diff -r 33a94c5fc7bb -r 247ca17caddd src/HOL/Nominal/Examples/Iteration.thy
--- a/src/HOL/Nominal/Examples/Iteration.thy	Tue May 16 13:05:37 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy	Tue May 16 14:11:39 2006 +0200
@@ -4,6 +4,7 @@
 imports "../Nominal"
 begin
 
+
 atom_decl name
 
 nominal_datatype lam = Var "name"
@@ -15,402 +16,189 @@
       'a f3_ty  = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
 
 consts
-  it :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam \<times> (name prm \<Rightarrow> 'a::pt_name)) set"
+  it :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam \<times> 'a::pt_name) set"
 
 inductive "it f1 f2 f3"
 intros
-it1: "(Var a,\<lambda>pi. f1(pi\<bullet>a)) \<in> it f1 f2 f3"
-it2: "\<lbrakk>(t1,r1) \<in> it f1 f2 f3; (t2,r2) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> 
-      (App t1 t2,\<lambda>pi. f2 (r1 pi) (r2 pi)) \<in> it f1 f2 f3"
-it3: "(t,r) \<in> it f1 f2 f3 \<Longrightarrow> (Lam [a].t,\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (r (pi@[(a,a')])))) \<in> it f1 f2 f3"
+it1: "(Var a, f1 a) \<in> it f1 f2 f3"
+it2: "\<lbrakk>(t1,r1) \<in> it f1 f2 f3; (t2,r2) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (App t1 t2, f2 r1 r2) \<in> it f1 f2 f3"
+it3: "\<lbrakk>a\<sharp>(f1,f2,f3); (t,r) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (Lam [a].t,f3 a r) \<in> it f1 f2 f3"
 
-constdefs
-  itfun' :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> name prm \<Rightarrow> ('a::pt_name)" 
-  "itfun' f1 f2 f3 t \<equiv> (THE y. (t,y) \<in> it f1 f2 f3)"
+lemma it_equiv:
+  fixes pi::"name prm"
+  assumes a: "(t,r) \<in> it f1 f2 f3"
+  shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+  using a
+  apply(induct)
+  apply(perm_simp | auto intro!: it.intros simp add: fresh_right)+
+  done
 
-  itfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" 
-  "itfun f1 f2 f3 t \<equiv> itfun' f1 f2 f3 t ([]::name prm)"
+lemma it_fin_supp:
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     a: "(t,r) \<in> it f1 f2 f3"
+  shows "finite ((supp r)::name set)" 
+  using a f
+  apply(induct)
+  apply(finite_guess, simp add: supp_prod fs_name1)+
+  done
 
 lemma it_total:
-  shows "\<exists>r. (t,r) \<in> it f1 f2 f3"
-  by (induct t rule: lam.induct_weak, auto intro: it.intros)
-
-lemma it_prm_eq:
-  assumes a: "(t,y) \<in> it f1 f2 f3" and b: "pi1 \<triangleq> pi2"
-  shows "y pi1 = y pi2"
-using a b
-apply(induct fixing: pi1 pi2)
-apply(auto simp add: pt3[OF pt_name_inst])
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(auto simp add: expand_fun_eq)
-apply(drule_tac x="pi1@[(a,x)]" in meta_spec)
-apply(drule_tac x="pi2@[(a,x)]" in meta_spec)
-apply(force simp add: prm_eq_def pt2[OF pt_name_inst])
+  assumes a: "finite ((supp (f1,f2,f3))::name set)"
+  and     b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  shows "\<exists>r. (t,r)\<in>it f1 f2 f3"
+apply(rule_tac lam.induct'[of "\<lambda>_. (supp (f1,f2,f3))::name set" 
+                              "\<lambda>z. \<lambda>t. \<exists>r. (t,r)\<in>it f1 f2 f3", simplified])
+apply(fold fresh_def)
+apply(auto intro: it.intros a)
 done
 
-lemma f3_freshness_conditions:
-  fixes f3::"('a::pt_name) f3_ty"
-  and   y ::"name prm \<Rightarrow> 'a::pt_name"
-  assumes a: "finite ((supp f3)::name set)"
-  and     b: "finite ((supp y)::name set)"
-  and     c: "\<exists>a. a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "\<exists>a''. a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2))) a''" 
-proof -
-  from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force
-  have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi1,pi2,y)" 
-    by (rule at_exists_fresh[OF at_name_inst],  simp add: supp_prod fs_name1 a b)
-  then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi1,pi2,y)" 
-    by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
-  have d3c: "a''\<notin>((supp (f3,a,pi1,pi2,y))::name set)" using d3b by (simp add: fresh_def)
-  have d4: "a''\<sharp>f3 a'' (y (pi1@[(a,a'')]@pi2))"
-  proof -
-    have d5: "[(a'',a')]\<bullet>f3 = f3" using d2 d0 by perm_simp 
-    from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))" by (simp add: fresh_eqvt)
-    hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 by (perm_simp add: calc_atm)
-    hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi1@[(a,a'')]@pi2)))))" by force
-    thus ?thesis by perm_simp
-  qed
-  have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2)))"
-  proof -
-    from a b have d7: "finite ((supp (f3,a,pi1,pi2,y))::name set)" by (simp add: supp_prod fs_name1)
-    have e: "((supp (f3,a,pi1,pi2,y))::name set) supports (\<lambda>a'. f3 a' (y (pi1@[(a,a')]@pi2)))" 
-      by (supports_simp add: perm_append)
-    from e d7 d3c show ?thesis by (rule supports_fresh)
-  qed
-  from d6 d4 show ?thesis by force
-qed
-
-lemma f3_freshness_conditions_simple:
-  fixes f3::"('a::pt_name) f3_ty"
-  and   y ::"name prm \<Rightarrow> 'a::pt_name"
-  assumes a: "finite ((supp f3)::name set)"
-  and     b: "finite ((supp y)::name set)"
-  and     c: "\<exists>a. a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "\<exists>a''. a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) a''"
-using a b c by (simp add: f3_freshness_conditions[of _ _ _ _ "[]",simplified])
-
-lemma it_fin_supp: 
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  and     a: "(t,r) \<in> it f1 f2 f3"
-  shows "finite ((supp r)::name set)"
-using a 
-proof (induct)
-  case it1 thus ?case using f by (finite_guess add: supp_prod fs_name1)
-next
-  case it2 thus ?case using f by (finite_guess add: supp_prod fs_name1)
-next
-  case (it3 c r t)
-  have ih: "finite ((supp r)::name set)" by fact
-  let ?g' = "\<lambda>pi a'. f3 a' (r (pi@[(c,a')]))"     --"helper function"
-  have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using f ih
-    by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
-  have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" 
-  proof 
-    fix pi::"name prm"
-    show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c ih
-      by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
-  qed
-  show ?case using fact1 fact2 ih f by (finite_guess add: fresh_fun_eqvt perm_append supp_prod fs_name1)
-qed 
-
-lemma it_trans: "\<lbrakk>(t,r)\<in>rec f1 f2 f3; r=r'\<rbrakk> \<Longrightarrow> (t,r')\<in>rec f1 f2 f3" by simp
-
-lemma it_perm_aux:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     a: "(t,y) \<in> it f1 f2 f3"
-  shows "(pi1\<bullet>t, \<lambda>pi2. y (pi2@pi1)) \<in> it f1 f2 f3"
-using a
-proof (induct)
-  case (it1 c) show ?case by (auto simp add: pt_name2, rule it.intros)
-next
-  case (it2 t1 t2 r1 r2) thus ?case by (auto intro: it.intros) 
-next
-  case (it3 c r t)
-  let ?g  = "\<lambda>pi' a'. f3 a' (r (pi'@[(pi1\<bullet>c,a')]@pi1))"
-  and ?h  = "\<lambda>pi' a'. f3 a' (r ((pi'@pi1)@[(c,a')]))" 
-  have ih': "(t,r) \<in> it f1 f2 f3" by fact
-  hence fin_r: "finite ((supp r)::name set)" using f c by (auto intro: it_fin_supp)
-  have ih: "(pi1\<bullet>t,\<lambda>pi2. r (pi2@pi1)) \<in> it f1 f2 f3" by fact
-  hence "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t),\<lambda>pi'. fresh_fun (?g pi')) \<in> it f1 f2 f3"
-    by (auto intro: it_trans it.intros) 
-  moreover
-  have "\<forall>pi'. (fresh_fun (?g pi')) = (fresh_fun (?h pi'))" 
-  proof 
-    fix pi'::"name prm"
-    have fin_g: "finite ((supp (?g pi'))::name set)"
-      using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
-    have fr_g: "\<exists>(a::name). (a\<sharp>(?g pi')\<and> a\<sharp>(?g pi' a))" 
-      using f c fin_r by (rule_tac f3_freshness_conditions, simp_all add: supp_prod)
-    have fin_h: "finite ((supp (?h pi'))::name set)"
-      using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
-    have fr_h: "\<exists>(a::name). (a\<sharp>(?h pi')\<and> a\<sharp>(?h pi' a))" 
-      using f c fin_r by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
-    show "fresh_fun (?g pi') = fresh_fun (?h pi')" 
-    proof -
-      have "\<exists>(d::name). d\<sharp>(?g pi', ?h pi', pi1)" using fin_g fin_h
-	by (rule_tac at_exists_fresh[OF at_name_inst], simp only: supp_prod finite_Un fs_name1, simp)
-      then obtain d::"name" where f1: "d\<sharp>?g pi'" and f2: "d\<sharp>?h pi'" and f3: "d\<sharp>(rev pi1)"
-	by (auto simp only: fresh_prod fresh_list_rev)
-      have "?g pi' d = ?h pi' d" 
-      proof -
-	have "r (pi'@[(pi1\<bullet>c,d)]@pi1) = r ((pi'@pi1)@[(c,d)])" using f3 ih'
-	  by (auto intro!: it_prm_eq at_prm_eq_append[OF at_name_inst]
-              simp only: append_assoc at_ds10[OF at_name_inst])
-	then show ?thesis by simp
-      qed
-      then show "fresh_fun (?g pi') = fresh_fun (?h pi')"
-	using f1 fin_g fr_g f2 fin_h fr_h by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
-    qed
-  qed
-  hence "(\<lambda>pi'. (fresh_fun (?g pi'))) = (\<lambda>pi'. (fresh_fun (?h pi')))" by (simp add: expand_fun_eq)
-  ultimately show ?case by simp
-qed
-
-lemma it_perm:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     a: "(pi\<bullet>t,y) \<in> it f1 f2 f3"
-  shows "(t, \<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3"
-proof - 
-  from a f c have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi))) \<in> it f1 f2 f3" by (simp add: it_perm_aux)
-  thus ?thesis by perm_simp
-qed
-
-lemma it_unique:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     a: "(t,y) \<in> it f1 f2 f3"
-  and     b: "(t,y') \<in> it f1 f2 f3"
-  shows "y pi = y' pi"
-using a b
-proof (induct fixing: y' pi)
-  case (it1 c) thus ?case by (cases, simp_all add: lam.inject)
+lemma it_unique: 
+  assumes a: "finite ((supp (f1,f2,f3))::name set)"
+  and     b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  and     c1: "(t,r)\<in>it f1 f2 f3"
+  and     c2: "(t,r')\<in>it f1 f2 f3"
+  shows   "r=r'"
+using c1 c2
+proof (induct fixing: r')
+  case it1
+  then show ?case by cases (simp_all add: lam.inject)
 next
   case (it2 r1 r2 t1 t2)
-  with `(App t1 t2, y') \<in> it f1 f2 f3` show ?case 
-    by (cases, simp_all (no_asm_use) add: lam.inject, force)
+  have ih1: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
+  have ih2: "\<And>r'. (t2,r') \<in> it f1 f2 f3 \<Longrightarrow> r2 = r'" by fact
+  have "(App t1 t2, r') \<in>it f1 f2 f3" by fact
+  then show ?case
+  proof cases
+    case it2
+    then show ?thesis using ih1 ih2 by (simp add: lam.inject) 
+  qed (simp_all (no_asm_use))
 next
-  case (it3 c r t r')
-  have "(t,r) \<in> it f1 f2 f3" by fact
-  hence fin_r: "finite ((supp r)::name set)" using f c by (simp only: it_fin_supp)
-  have ih: "\<And>r' pi. (t,r') \<in> it f1 f2 f3 \<Longrightarrow> r pi = r' pi" by fact
-  have "(Lam [c].t, r') \<in> it f1 f2 f3" by fact
-  then show "fresh_fun (\<lambda>a'. f3 a' (r (pi@[(c,a')]))) = r' pi"
-  proof (cases, auto simp add: lam.inject)
-    fix a::"name" and t'::"lam" and r''::"name prm\<Rightarrow>'a::pt_name"
-    assume i5: "[c].t = [a].t'"
-    and    i6: "(t',r'') \<in> it f1 f2 f3"
-    hence fin_r'': "finite ((supp r'')::name set)" using f c by (auto intro: it_fin_supp)
-    let ?g = "\<lambda>a'. f3 a' (r (pi@[(c,a')]))" and ?h = "\<lambda>a'. f3 a' (r'' (pi@[(a,a')]))"
-    show "fresh_fun ?g = fresh_fun ?h" using i5
-    proof (cases "a=c")
-      case True
-      have i7: "a=c" by fact
-      with i5 have i8: "t=t'" by (simp add: alpha)
-      show "fresh_fun ?g = fresh_fun ?h" using i6 i7 i8 ih by simp
-    next
-      case False
-      assume i9: "a\<noteq>c"
-      with i5[symmetric] have i10: "t'=[(a,c)]\<bullet>t" and i11: "a\<sharp>t" by (simp_all add: alpha)
-      have fin_g: "finite ((supp ?g)::name set)"
-	using f fin_r by (finite_guess add: perm_append supp_prod fs_name1)
-      have fin_h: "finite ((supp ?h)::name set)" 
-	using f fin_r'' by (finite_guess add: perm_append supp_prod fs_name1)
-      have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
-	using f c fin_r by (simp add:  f3_freshness_conditions_simple supp_prod)
-      have fr_h: "\<exists>(a''::name). a''\<sharp>?h \<and> a''\<sharp>(?h a'')"
-	using f c fin_r'' by (simp add: f3_freshness_conditions_simple supp_prod)
-      have "\<exists>(d::name). d\<sharp>(?g,?h,t,a,c)" using fin_g fin_h
-	by (rule_tac at_exists_fresh[OF at_name_inst], simp only: finite_Un supp_prod fs_name1, simp)
-      then obtain d::"name" 
-	where f1: "d\<sharp>?g" and f2: "d\<sharp>?h" and f3: "d\<sharp>t" and f4: "d\<noteq>a" and f5: "d\<noteq>c" 
-	by (force simp add: fresh_prod fresh_atm)
-      have g1: "[(a,d)]\<bullet>t = t" using i11 f3 by perm_simp
-      from i6 have "(([(a,c)]@[(a,d)])\<bullet>t,r'') \<in> it f1 f2 f3" using g1 i10 by (simp only: pt_name2)
-      hence "(t, \<lambda>pi2. r'' (pi2@(rev ([(a,c)]@[(a,d)])))) \<in> it f1 f2 f3" 
-	by (simp only: it_perm[OF f, OF c])
-      hence g2: "(t, \<lambda>pi2. r'' (pi2@([(a,d)]@[(a,c)]))) \<in> it f1 f2 f3" by simp
-      have "distinct [a,c,d]" using i9 f4 f5 by force
-      hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<triangleq> (pi@[(a,d)])"
-	by (rule_tac at_prm_eq_append[OF at_name_inst], force simp add: prm_eq_def calc_atm)
-      have "fresh_fun ?g = ?g d" using fin_g fr_g f1
-	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
-      also have "\<dots> = f3 d ((\<lambda>pi2. r'' (pi2@([(a,d)]@[(a,c)]))) (pi@[(c,d)]))" using ih g2 by simp 
-      also have "\<dots> = f3 d (r'' (pi@[(c,d)]@[(a,d)]@[(a,c)]))" by simp
-      also have "\<dots> = f3 d (r'' (pi@[(a,d)]))" using i6 g3 by (simp add: it_prm_eq)
-      also have "\<dots> = fresh_fun ?h" using fin_h fr_h f2
-	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
-      finally show "fresh_fun ?g = fresh_fun ?h" by simp
-    qed
-  qed
+  case (it3 a1 r1 t1)
+  have f1: "a1\<sharp>(f1,f2,f3)" by fact
+  have ih: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
+  have it1: "(t1,r1) \<in> it f1 f2 f3" by fact
+  have "(Lam [a1].t1, r') \<in> it f1 f2 f3" by fact
+  then show ?case
+  proof cases
+    case (it3 a2 r2 t2)
+    then have f2: "a2\<sharp>(f1,f2,f3)" 
+         and  it2: "(t2,r2) \<in> it f1 f2 f3"
+         and  eq1: "[a1].t1 = [a2].t2" and eq2: "r' = f3 a2 r2" by (simp_all add: lam.inject) 
+    have "\<exists>(c::name). c\<sharp>(f1,f2,f3,a1,a2,t1,t2,r1,r2)" using a it1 it2
+      by (auto intro!: at_exists_fresh[OF at_name_inst] simp add: supp_prod fs_name1 it_fin_supp[OF a])
+    then obtain c where fresh: "c\<sharp>f1" "c\<sharp>f2" "c\<sharp>f3" "c\<noteq>a1" "c\<noteq>a2" "c\<sharp>t1" "c\<sharp>t2" "c\<sharp>r1" "c\<sharp>r2"
+      by (force simp add: fresh_prod fresh_atm)
+    have eq3: "[(a1,c)]\<bullet>t1 = [(a2,c)]\<bullet>t2" using eq1 fresh
+      apply(auto simp add: alpha)
+      apply(rule trans)
+      apply(rule perm_compose)
+      apply(simp add: calc_atm perm_fresh_fresh)
+      apply(rule pt_name3, rule at_ds5[OF at_name_inst])
+      done
+    have eq4: "[(a1,c)]\<bullet>r1 = [(a2,c)]\<bullet>r2" using eq3 it2 f1 f2 fresh
+      apply(drule_tac sym)
+      apply(rule_tac pt_bij2[OF pt_name_inst, OF at_name_inst])
+      apply(rule ih)
+      apply(drule_tac pi="[(a2,c)]" in it_equiv)
+      apply(perm_simp only: fresh_prod)
+      apply(drule_tac pi="[(a1,c)]" in it_equiv)
+      apply(perm_simp)
+      done
+    have fs1: "a1\<sharp>f3 a1 r1" using b f1
+      apply(auto)
+      apply(case_tac "a=a1")
+      apply(simp)
+      apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
+      apply(perm_simp add: calc_atm fresh_prod)
+      done      
+    have fs2: "a2\<sharp>f3 a2 r2" using b f2
+      apply(auto)
+      apply(case_tac "a=a2")
+      apply(simp)
+      apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
+      apply(perm_simp add: calc_atm fresh_prod)
+      done      
+    have fs3: "c\<sharp>f3 a1 r1" using fresh it1 a
+      apply(rule_tac S="supp (f3,a1,r1)" in supports_fresh)
+      apply(supports_simp)
+      apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
+      apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
+      done
+    have fs4: "c\<sharp>f3 a2 r2" using fresh it2 a
+      apply(rule_tac S="supp (f3,a2,r2)" in supports_fresh)
+      apply(supports_simp)
+      apply(simp add: supp_prod fs_name1 it_fin_supp[OF a])
+      apply(simp add: fresh_def[symmetric] fresh_prod fresh_atm)
+      done
+    have "f3 a1 r1 = [(a1,c)]\<bullet>(f3 a1 r1)" using fs1 fs3 by perm_simp
+    also have "\<dots> = f3 c ([(a1,c)]\<bullet>r1)" using f1 fresh by (perm_simp add: calc_atm fresh_prod)
+    also have "\<dots> = f3 c ([(a2,c)]\<bullet>r2)" using eq4 by simp
+    also have "\<dots> = [(a2,c)]\<bullet>(f3 a2 r2)" using f2 fresh by (perm_simp add: calc_atm fresh_prod)
+    also have "\<dots> = f3 a2 r2" using fs2 fs4 by perm_simp
+    finally have eq4: "f3 a1 r1 = f3 a2 r2" by simp
+    then show ?thesis using eq2 by simp
+  qed (simp_all (no_asm_use))
 qed
 
 lemma it_function:
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
   shows "\<exists>!r. (t,r) \<in> it f1 f2 f3"
-proof (rule ex_ex1I, rule it_total)
+proof (rule ex_ex1I, rule it_total[OF f, OF c])
   case (goal1 r1 r2)
   have a1: "(t,r1) \<in> it f1 f2 f3" and a2: "(t,r2) \<in> it f1 f2 f3" by fact
-  hence "\<forall>pi. r1 pi = r2 pi" using it_unique[OF f, OF c] by simp
-  thus "r1=r2" by (simp add: expand_fun_eq) 
+  thus "r1 = r2" using it_unique[OF f, OF c] by simp
 qed
-  
-lemma it_eqvt:
+
+constdefs
+  itfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" 
+  "itfun f1 f2 f3 t \<equiv> (THE r. (t,r) \<in> it f1 f2 f3)"
+
+lemma itfun_eqvt:
   fixes pi::"name prm"
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  and     a: "(t,r) \<in> it f1 f2 f3"
-  shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
-using a proof(induct)
-  case it1 show ?case by (perm_simp add: it.intros perm_compose')
-next
-  case it2 thus ?case by (perm_simp add: it.intros)
-next
-  case (it3 c r t) (* lam case *)
-  let ?g = "pi\<bullet>(\<lambda>pi'. fresh_fun (\<lambda>a'. f3 a' (r (pi'@[(c,a')]))))"
-  and ?h = "\<lambda>pi'. fresh_fun (\<lambda>a'. (pi\<bullet>f3) a' ((pi\<bullet>r) (pi'@[((pi\<bullet>c),a')])))"
-  have "(t,r) \<in> it f1 f2 f3" by fact
-  hence fin_r: "finite ((supp r)::name set)" using f c by (auto intro: it_fin_supp)
-  have ih: "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by fact
-  hence "(Lam [(pi\<bullet>c)].(pi\<bullet>t),?h) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by (simp add: it.intros)
-  moreover 
-  have "?g = ?h"
+  shows "pi\<bullet>(itfun f1 f2 f3 t) = itfun (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
+proof -
+  have f_pi: "finite ((supp (pi\<bullet>f1,pi\<bullet>f2,pi\<bullet>f3))::name set)" using f
+    by (simp add: supp_prod pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
+  have fs_pi: "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" 
   proof -
-    let ?g' = "\<lambda>pi a'. f3 a' (r (pi@[(c,a')]))"
-    have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using fin_r f
-      by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
-    have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" 
-    proof 
-      fix pi::"name prm"
-      show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c fin_r
-	by (simp add: f3_freshness_conditions_simple supp_prod)
-    qed
-    from fact1 fact2 show "?g = ?h" by (perm_simp add: fresh_fun_eqvt perm_append)
-  qed
-  ultimately show "(pi\<bullet>Lam [c].t,?g) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)" by simp
-qed
-
-lemma the1_equality': 
-  assumes a: "\<exists>!r. P r" and b: "P b" and c: "b y = a"
-  shows "(THE r. P r) y = a"
-  by (simp add: c[symmetric], rule fun_cong[OF the1_equality, OF a, OF b])
-
-lemma itfun'_prm:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "itfun' f1 f2 f3 (pi1\<bullet>t) pi2 = itfun' f1 f2 f3 t (pi2@pi1)"
-apply(auto simp add: itfun_def itfun'_def)
-apply(rule the1_equality'[OF it_function, OF f, OF c])
-apply(rule it_perm_aux[OF f, OF c])
-apply(rule theI'[OF it_function,OF f, OF c], simp)
-done
-
-lemma itfun'_eqvt:
-  fixes pi1::"name prm"
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "pi1\<bullet>(itfun' f1 f2 f3 t pi2) = itfun' (pi1\<bullet>f1) (pi1\<bullet>f2) (pi1\<bullet>f3) (pi1\<bullet>t) (pi1\<bullet>pi2)"
-proof -
-  have f_pi: "finite ((supp (pi1\<bullet>f1,pi1\<bullet>f2,pi1\<bullet>f3))::name set)" using f
-    by (simp add: supp_prod pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
-  have fs_pi: "\<exists>(a::name). a\<sharp>(pi1\<bullet>f3) \<and> (\<forall>(y::'a::pt_name). a\<sharp>(pi1\<bullet>f3) a y)" 
-  proof -
-    from c obtain a where fs1: "a\<sharp>f3" and fs2: "(\<forall>(y::'a::pt_name). a\<sharp>f3 a y)" by force
-    have "(pi1\<bullet>a)\<sharp>(pi1\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
+    from c obtain a where fs1: "a\<sharp>f3" and fs2: "\<forall>(r::'a::pt_name). a\<sharp>f3 a r" by force
+    have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
     moreover
-    have "\<forall>(y::'a::pt_name). (pi1\<bullet>a)\<sharp>((pi1\<bullet>f3) (pi1\<bullet>a) y)" 
-    proof
-      fix y::"'a::pt_name"
-      from fs2 have "a\<sharp>f3 a ((rev pi1)\<bullet>y)" by simp
-      then show "(pi1\<bullet>a)\<sharp>((pi1\<bullet>f3) (pi1\<bullet>a) y)"
-	by (perm_simp add: pt_fresh_right[OF pt_name_inst, OF at_name_inst])
-    qed
-    ultimately show "\<exists>(a::name). a\<sharp>(pi1\<bullet>f3) \<and> (\<forall>(y::'a::pt_name). a\<sharp>(pi1\<bullet>f3) a y)" by blast
+    have "\<forall>(r::'a::pt_name). (pi\<bullet>a)\<sharp>((pi\<bullet>f3) (pi\<bullet>a) r)" using fs2 by (perm_simp add: fresh_right)
+    ultimately show "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" by blast
   qed
   show ?thesis
     apply(rule sym)
-    apply(auto simp add: itfun_def itfun'_def)
-    apply(rule the1_equality'[OF it_function, OF f_pi, OF fs_pi])
-    apply(rule it_eqvt[OF f, OF c])
+    apply(auto simp add: itfun_def)
+    apply(rule the1_equality[OF it_function, OF f_pi, OF fs_pi])
+    apply(rule it_equiv)
     apply(rule theI'[OF it_function,OF f, OF c])
-    apply(rule sym)
-    apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst], perm_simp)
     done
 qed
 
 lemma itfun_Var:
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
   shows "itfun f1 f2 f3 (Var c) = (f1 c)"
-using f c by (auto intro!: the1_equality' it_function it.intros simp add: itfun_def itfun'_def)
+using f c by (auto intro!: the1_equality it_function it.intros simp add: itfun_def)
 
 lemma itfun_App:
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
   shows "itfun f1 f2 f3 (App t1 t2) = (f2 (itfun f1 f2 f3 t1) (itfun f1 f2 f3 t2))"
-by (auto intro!: the1_equality' it_function[OF f, OF c] it.intros 
-         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def itfun'_def)
-
-lemma itfun_Lam_aux1:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "itfun f1 f2 f3 (Lam [a].t) = fresh_fun (\<lambda>a'. f3 a' (itfun' f1 f2 f3 t ([]@[(a,a')])))"
-by (auto intro!: the1_equality' it_function[OF f, OF c] it.intros 
-         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def itfun'_def)
-
-lemma itfun_Lam_aux2:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     a: "b\<sharp>(a,t,f1,f2,f3)"
-  shows "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))"
-proof -
-  have eq1: "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)"
-  proof -
-    have "Lam [b].([(b,a)]\<bullet>t) = Lam [a].t" using a by (simp add: lam.inject alpha fresh_prod fresh_atm)
-    thus ?thesis by simp
-  qed
-  let ?g = "(\<lambda>a'. f3 a' (itfun' f1 f2 f3 t ([]@[(a,a')])))"
-  have fin_g: "finite ((supp ?g)::name set)" 
-    using f by (finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
-  have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" using f c 
-    apply (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod, 
-           finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
-    done
-  have fresh_b: "b\<sharp>?g" 
-  proof -
-    have "finite ((supp (a,t,f1,f2,f3))::name set)" using f by (simp add: supp_prod fs_name1)
-    moreover 
-    have "((supp (a,t,f1,f2,f3))::name set) supports ?g"
-      by (supports_simp add: itfun'_eqvt[OF f, OF c] perm_append)
-    ultimately show ?thesis using a by (auto intro!: supports_fresh, simp add: fresh_def)
-  qed
-  have "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = itfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1)
-  also have "\<dots> = fresh_fun ?g" by (rule itfun_Lam_aux1[OF f, OF c])
-  also have "\<dots> = ?g b" using fresh_b fin_g fr_g 
-    by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
-  also have "\<dots> = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))" by (simp add: itfun_def itfun'_prm[OF f, OF c]) 
-  finally show "itfun f1 f2 f3 (Lam [b].([(b,a)]\<bullet>t)) = f3 b (itfun f1 f2 f3 ([(a,b)]\<bullet>t))" by simp 
-qed
+by (auto intro!: the1_equality it_function[OF f, OF c] it.intros 
+         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
 
 lemma itfun_Lam:
   assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     a: "b\<sharp>(f1,f2,f3)"
-  shows "itfun f1 f2 f3 (Lam [b].t) = f3 b (itfun f1 f2 f3 t)"
-proof -
-  have "\<exists>(a::name). a\<sharp>(b,t)"
-    by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1)
-  then obtain a::"name" where a1: "a\<sharp>b" and a2: "a\<sharp>t" by (force simp add: fresh_prod)
-  have fresh_b: "b\<sharp>(a,[(b,a)]\<bullet>t,f1,f2,f3)" using a a1 a2
-    by (simp add: fresh_prod fresh_atm fresh_left calc_atm)
-  have "itfun f1 f2 f3 (Lam [b].t) = itfun f1 f2 f3 (Lam [b].(([(b,a)])\<bullet>([(b,a)]\<bullet>t)))" by (perm_simp)
-  also have "\<dots> = f3 b (itfun f1 f2 f3 (([(a,b)])\<bullet>([(b,a)]\<bullet>t)))" 
-    using fresh_b f c by (simp add: itfun_Lam_aux2)
-  also have "\<dots> = f3 b (itfun f1 f2 f3 t)" by (simp add: pt_swap_bij'[OF pt_name_inst, OF at_name_inst])
-  finally show ?thesis by simp
-qed
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
+  and     a: "a\<sharp>(f1,f2,f3)"
+  shows "itfun f1 f2 f3 (Lam [a].t) = f3 a (itfun f1 f2 f3 t)"
+using a
+by (auto intro!: the1_equality it_function[OF f, OF c] it.intros 
+         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
 
 end
diff -r 33a94c5fc7bb -r 247ca17caddd src/HOL/Nominal/Examples/Recursion.thy
--- a/src/HOL/Nominal/Examples/Recursion.thy	Tue May 16 13:05:37 2006 +0200
+++ b/src/HOL/Nominal/Examples/Recursion.thy	Tue May 16 14:11:39 2006 +0200
@@ -181,4 +181,5 @@
 apply(simp add: rfun_def)
 done
 
+
 end
\ No newline at end of file