# HG changeset patch
# User urbanc
# Date 1131373143 -3600
# Node ID 836135c8acb27efc0af3cb0a8a42538532e40a57
# Parent  4c9c081a416b8adbc2f8380c0092e2ca66e66155
Initial commit.

diff -r 4c9c081a416b -r 836135c8acb2 src/HOL/Nominal/Examples/CR.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/CR.thy	Mon Nov 07 15:19:03 2005 +0100
@@ -0,0 +1,952 @@
+
+theory cr
+imports lam_substs
+begin
+
+lemma forget[rule_format]: 
+  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
+proof (nominal_induct t1 rule: lam_induct)
+  case (Var a t2 b) 
+  show ?case by (simp, simp add: fresh_atm)
+next 
+  case App
+  thus ?case by (simp add: fresh_prod)
+next
+  case (Lam a t2 c t)
+  have i: "\<forall>a b. a\<sharp>t \<longrightarrow>  t[a::=b] = t" by fact
+  have "c\<sharp>(a,t2)" by fact
+  hence a: "a\<noteq>c" and b: "c\<sharp>t2" by (auto simp add: fresh_prod fresh_atm)
+  show ?case
+  proof 
+    assume "a\<sharp>Lam [c].t" 
+    hence "a\<sharp>t" using a by (force simp add: abs_fresh)
+    hence "t[a::=t2] = t" using i by simp
+    thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by (simp add: alpha)
+  qed
+qed
+
+lemma forget[rule_format]: 
+  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
+apply (nominal_induct t1 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_atm fresh_prod)
+done
+
+lemma fresh_fact[rule_format]: 
+  fixes   b :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam" 
+  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
+proof (nominal_induct t1 rule: lam_induct)
+  case (Var a b t2 c) 
+  show ?case by (simp)
+next
+  case App 
+  thus ?case by (simp add: fresh_prod)
+next
+  case (Lam a b t2 c t)
+  have  i: "\<forall>(a::name) b t2. a\<sharp>t\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t[b::=t2])" by fact
+  have "c\<sharp>(a,b,t2)" by fact
+  hence b: "c\<noteq>a \<and> c\<noteq>b \<and> c\<sharp>t2" by (simp add: fresh_prod fresh_atm) 
+  show ?case 
+  proof (intro strip)
+    assume a1: "a\<sharp>t2"
+    assume a2: "a\<sharp>Lam [c].t"
+    hence "a\<sharp>t" using b by (force simp add: abs_fresh)
+    hence "a\<sharp>t[b::=t2]" using a1 i by simp
+    thus "a\<sharp>(Lam [c].t)[b::=t2]" using b by (simp add: abs_fresh)
+  qed
+qed
+
+lemma fresh_fact[rule_format]: 
+  fixes   b :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam" 
+  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
+apply(nominal_induct t1 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_prod fresh_atm)
+done
+
+lemma subs_lemma:  
+  fixes x::"name"
+  and   y::"name"
+  and   L::"lam"
+  and   M::"lam"
+  and   N::"lam"
+  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+proof (nominal_induct M rule: lam_induct)
+  case (Var L N x y z) (* case 1: Variables*)
+  show ?case
+  proof (intro strip)
+    assume a1: "x\<noteq>y"
+    and    a2: "x\<sharp>L"
+    show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
+    proof -
+      have "z=x \<or> (z\<noteq>x \<and> z=y) \<or> (z\<noteq>x \<and> z\<noteq>y)" by force 
+      moreover (*Case 1.1*)
+      { assume c1: "z=x"
+	have c1l: "?LHS = N[y::=L]"    using c1    by simp
+	have c1r: "?RHS = N[y::=L]"    using c1 a1 by simp
+	from c1l and c1r have "?LHS = ?RHS"  by simp
+      }
+      moreover (*Case 1.2*)
+      { assume c2: "z\<noteq>x \<and> z=y"
+	have c2l: "?LHS = L"               using c2 by force
+	have c2r: "?RHS = L[x::=N[y::=L]]" using c2 by force
+	have c2x: "L[x::=N[y::=L]] = L"    using a2 by (simp add: forget)
+	from c2l and c2r and c2x have "?LHS = ?RHS" by simp
+      }
+      moreover (*Case 1.3*)
+      { assume c3: "z\<noteq>x \<and> z\<noteq>y"
+	have c3l: "?LHS = Var z" using c3 by force
+	have c3r: "?RHS = Var z" using c3 by force
+	from c3l and c3r have "?LHS = ?RHS" by simp
+      }
+      ultimately show "?LHS = ?RHS" by blast
+    qed
+  qed
+next
+  case (Lam L N x y z M1) (* case 2: lambdas *)
+  assume f1: "z\<sharp>(L,N,x,y)"
+  from f1 have f2: "z \<sharp> N[y::=L]" by (simp add: fresh_fact fresh_prod)
+  show ?case
+  proof (intro strip)
+    assume  a1: "x\<noteq>y"
+    and     a2: "x\<sharp>L"
+    show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
+    proof -
+      have "?LHS = Lam [z].(M1[x::=N][y::=L])"             using f1 
+	by (simp add: fresh_prod fresh_atm)
+      also have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])"   using a1 a2 Lam(2)  by simp
+      also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using f1 f2 
+	by (simp add: fresh_prod fresh_atm)
+      also have "\<dots> = ?RHS" using f1 by (simp add: fresh_prod fresh_atm)
+      finally show "?LHS = ?RHS" .
+    qed
+  qed
+next
+  case (App L N x y M1 M2) (* case 3: applications *)
+  show ?case
+  proof (intro strip)
+    assume a1: "x\<noteq>y"
+    and    a2: "x\<sharp>L"
+    from a1 a2 App show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
+  qed
+qed
+
+lemma subs_lemma: 
+  fixes x::"name"
+  and   y::"name"
+  and   L::"lam"
+  and   M::"lam"
+  and   N::"lam"
+  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+proof (nominal_induct M rule: lam_induct)
+  case (Var L N x y z) (* case 1: Variables*)
+  show ?case
+  proof -
+    have "z=x \<or> (z\<noteq>x \<and> z=y) \<or> (z\<noteq>x \<and> z\<noteq>y)" by force
+    thus "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" 
+    using forget by force
+  qed
+next
+  case (Lam L N x y z M1) (* case 2: lambdas *)
+  assume f1: "z\<sharp>(L,N,x,y)" 
+  hence f2: "z\<sharp>N[y::=L]" by (simp add: fresh_fact fresh_prod)
+  show ?case
+  proof (intro strip)
+    assume a1: "x\<noteq>y"
+    and    a2: "x\<sharp>L"
+    show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
+    proof -
+      have "?LHS = Lam [z].(M1[x::=N][y::=L])" using f1 by (simp add: fresh_prod fresh_atm)
+      also have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])"   using a1 a2 Lam(2)  by simp
+      also have "\<dots> = ?RHS" using f1 f2 by (simp add: fresh_prod fresh_atm)
+      finally show "?LHS = ?RHS" .
+    qed
+  qed
+next
+  case (App L N x y M1 M2) (* case 3: applications *)
+  thus "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
+qed
+
+lemma subs_lemma:  
+  fixes x::"name"
+  and   y::"name"
+  and   L::"lam"
+  and   M::"lam"
+  and   N::"lam"
+  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+apply(nominal_induct M rule: lam_induct)
+apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)
+done
+
+lemma subst_rename[rule_format]: 
+  fixes  c  :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam"
+  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
+proof (nominal_induct t1 rule: lam_induct)
+  case (Var a c t2 b)
+  show "c\<sharp>(Var b) \<longrightarrow> (Var b)[a::=t2] = ([(c,a)]\<bullet>(Var b))[c::=t2]" by (simp add: calc_atm fresh_atm)
+next
+  case App thus ?case by (force simp add: fresh_prod)
+next
+  case (Lam a c t2 b s)
+  have i: "\<forall>a c t2. c\<sharp>s \<longrightarrow> (s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2])" by fact
+  have f: "b\<sharp>(a,c,t2)" by fact
+  from f have a:"b\<noteq>c" and b: "b\<noteq>a" and c: "b\<sharp>t2" by (simp add: fresh_prod fresh_atm)+
+  show "c\<sharp>Lam [b].s \<longrightarrow> (Lam [b].s)[a::=t2] = ([(c,a)]\<bullet>(Lam [b].s))[c::=t2]" (is "_ \<longrightarrow> ?LHS = ?RHS")
+  proof
+    assume "c\<sharp>Lam [b].s"
+    hence "c\<sharp>s" using a by (force simp add: abs_fresh)
+    hence d: "s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2]" using i by simp
+    have    "?LHS = Lam [b].(s[a::=t2])" using b c by simp
+    also have "\<dots> = Lam [b].(([(c,a)]\<bullet>s)[c::=t2])" using d by simp
+    also have "\<dots> = (Lam [b].([(c,a)]\<bullet>s))[c::=t2]" using a c by simp
+    also have "\<dots> = ?RHS" using a b by (force simp add: calc_atm)
+    finally show "?LHS = ?RHS" by simp
+  qed
+qed
+
+lemma subst_rename[rule_format]: 
+  fixes  c  :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam"
+  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
+apply(nominal_induct t1 rule: lam_induct)
+apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)
+done
+
+section {* Beta Reduction *}
+
+consts
+  Beta :: "(lam\<times>lam) set"
+syntax 
+  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+translations 
+  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
+  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
+inductive Beta
+  intros
+  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
+  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
+  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+
+lemma eqvt_beta: 
+  fixes pi :: "name prm"
+  and   t  :: "lam"
+  and   s  :: "lam"
+  shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
+  apply(erule Beta.induct)
+  apply(auto)
+  done
+
+lemma beta_induct_aux[rule_format]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+  and a1:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
+  and a2:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
+  and a3:    "\<And>x (a::name) s1 s2. 
+              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
+  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
+using a
+proof (induct)
+  case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
+next
+  case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
+next
+  case (b3 a s1 s2)
+  assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"
+  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
+  show ?case 
+  proof (simp, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name"
+     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+      by (force simp add: fresh_prod fresh_atm)
+    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"
+      using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
+      by (simp add: lam.inject alpha)
+    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+next
+  case (b4 a s1 s2)
+  show ?case
+  proof (simp add: subst_eqvt, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name" 
+    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+      by (force simp add: fresh_prod fresh_atm)
+    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"
+      using a4 f2 by (blast intro!: eqvt_beta)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
+      using f3 by (simp only: subst_rename[symmetric] pt_name2)
+    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+qed
+
+
+lemma beta_induct[case_names b1 b2 b3 b4]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  and    x :: "'a::fs_name"
+  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+  and a1:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
+  and a2:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
+  and a3:    "\<And>x (a::name) s1 s2. 
+              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<And>x (a::name) t1 s1. 
+              a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
+  shows "P t s x"
+using a a1 a2 a3 a4
+by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])
+
+section {* One-Reduction *}
+
+consts
+  One :: "(lam\<times>lam) set"
+syntax 
+  "_One"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
+  "_One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
+translations 
+  "t1 \<longrightarrow>\<^isub>1 t2" \<rightleftharpoons> "(t1,t2) \<in> One"
+  "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> One\<^sup>*"
+inductive One
+  intros
+  o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
+  o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)"
+  o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [(a::name)].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
+  o4[simp,intro!]: "\<lbrakk>s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [(a::name)].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
+
+lemma eqvt_one: 
+  fixes pi :: "name prm"
+  and   t  :: "lam"
+  and   s  :: "lam"
+  shows "t\<longrightarrow>\<^isub>1s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)"
+  apply(erule One.induct)
+  apply(auto)
+  done
+
+lemma one_induct_aux[rule_format]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  and a1:    "\<forall>x t. P t t x"
+  and a2:    "\<forall>x t1 t2 s1 s2. 
+              (t1\<longrightarrow>\<^isub>1t2 \<and> (\<forall>z. P t1 t2 z) \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
+              \<longrightarrow> P (App t1 s1) (App t2 s2) x"
+  and a3:    "\<forall>x (a::name) s1 s2. (a\<sharp>x \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
+             \<longrightarrow>  P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<forall>x (a::name) t1 t2 s1 s2. 
+              (a\<sharp>(s1,s2,x) \<and> t1\<longrightarrow>\<^isub>1t2 \<and> (\<forall>z. P t1 t2 z) \<and> s1\<longrightarrow>\<^isub>1s2 \<and> (\<forall>z. P s1 s2 z)) 
+              \<longrightarrow> P (App (Lam [a].t1) s1) (t2[a::=s2]) x"
+  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
+using a
+proof (induct)
+  case o1 show ?case using a1 by force
+next
+  case (o2 s1 s2 t1 t2) 
+  thus ?case using a2 by (simp, blast intro: eqvt_one)
+next
+  case (o3 a t1 t2)
+  assume j1: "t1 \<longrightarrow>\<^isub>1 t2"
+  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>t1) (pi\<bullet>t2) x"
+  show ?case 
+  proof (simp, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name"
+     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
+      by (force simp add: fresh_prod fresh_atm)
+    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t2)) x"
+      using a3 f2 j1 j2 by (simp, blast intro: eqvt_one)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t2))" using f1 f3
+      by (simp add: lam.inject alpha)
+    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (Lam [(pi\<bullet>a)].(pi\<bullet>t2)) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+next
+case (o4 a s1 s2 t1 t2)
+  assume j0: "t1 \<longrightarrow>\<^isub>1 t2"
+  assume j1: "s1 \<longrightarrow>\<^isub>1 s2"
+  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>t1) (pi\<bullet>t2) x"
+  assume j3: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
+  show ?case
+  proof (simp, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name" 
+    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s1,pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
+      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
+    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (pi\<bullet>s1)) ((([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)]) x"
+      using a4 f2 j0 j1 j2 j3 by (simp, blast intro!: eqvt_one)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)] = (pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
+      using f4 by (simp only: subst_rename[symmetric] pt_name2)
+    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (pi\<bullet>s1)) ((pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+qed
+
+lemma one_induct[rule_format, case_names o1 o2 o3 o4]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  and    x :: "'a::fs_name"
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  and a1:    "\<And>x t. P t t x"
+  and a2:    "\<And>x t1 t2 s1 s2. 
+              t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P t1 t2 z) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) \<Longrightarrow> 
+              P (App t1 s1) (App t2 s2) x"
+  and a3:    "\<And>x (a::name) s1 s2. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) 
+              \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<And>x (a::name) t1 t2 s1 s2. 
+              a\<sharp>(s1,s2,x) \<Longrightarrow> t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P t1 t2 z) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P s1 s2 z) 
+              \<Longrightarrow> P (App (Lam [a].t1) s1) (t2[a::=s2]) x"
+  shows "P t s x"
+using a a1 a2 a3 a4
+by (auto intro!: one_induct_aux[of "t" "s" "P" "[]" "x", simplified])
+
+lemma fresh_fact'[rule_format]:  
+  shows "a\<sharp>t2 \<longrightarrow> a\<sharp>(t1[a::=t2])" 
+proof (nominal_induct t1 rule: lam_induct)
+  case (Var a t2 b) 
+  show ?case by (cases "b=a") (force simp add: at_fresh[OF at_name_inst])+ 
+next
+  case App
+  thus ?case by (simp add: fresh_prod)
+next
+  case (Lam a t2 c t) 
+  from Lam(1) have "c\<noteq>a \<and> c\<sharp>t2" by (simp add: fresh_prod fresh_atm) 
+  thus ?case using Lam(2) by (force simp add: abs_fresh)
+qed
+
+lemma one_fresh_preserv[rule_format]:
+  fixes    t :: "lam"
+  and      s :: "lam"
+  and      a :: "name"
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  shows "a\<sharp>t \<longrightarrow> a\<sharp>s"
+using a
+proof (induct)
+  case o1 show ?case by simp
+next
+  case o2 thus ?case by (simp add: fresh_prod)
+next
+  case (o3 c s1 s2)
+  assume i: "a\<sharp>s1 \<longrightarrow>  a\<sharp>s2"
+  show ?case
+  proof (intro strip, cases "a=c")
+    assume "a=c" 
+    thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh)
+  next
+    assume b: "a\<noteq>c" and "a\<sharp>Lam [c].s1"
+    hence "a\<sharp>s1" by (simp add: abs_fresh)
+    hence "a\<sharp>s2" using i by simp
+    thus "a\<sharp>Lam [c].s2" using b by (simp add: abs_fresh) 
+  qed
+next 
+  case (o4 c t1 t2 s1 s2)
+  assume i1: "a\<sharp>t1 \<longrightarrow> a\<sharp>t2"
+     and i2: "a\<sharp>s1 \<longrightarrow> a\<sharp>s2"
+  show "a\<sharp>App (Lam [c].s1) t1 \<longrightarrow> a\<sharp>s2[c::=t2]"
+  proof
+    assume "a\<sharp>App (Lam [c].s1) t1"
+    hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+
+    from c2 i1 have c3: "a\<sharp>t2" by simp
+    show "a\<sharp>s2[c::=t2]"
+    proof (cases "a=c")
+      assume "a=c"
+      thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact')
+    next
+      assume d1: "a\<noteq>c"
+      from c1 d1 have "a\<sharp>s1" by (simp add: abs_fresh)
+      hence "a\<sharp>s2" using i2 by simp
+      thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact)
+    qed
+  qed
+qed
+
+lemma one_abs: 
+  fixes    t :: "lam"
+  and      t':: "lam"
+  and      a :: "name"
+  shows "(Lam [a].t)\<longrightarrow>\<^isub>1t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
+  apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+  apply(auto simp add: lam.distinct lam.inject alpha)
+  apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
+  apply(rule conjI)
+  apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric])
+  apply(simp)
+  apply(rule pt_name3)
+  apply(rule at_ds5[OF at_name_inst])
+  apply(frule_tac a="a" in one_fresh_preserv)
+  apply(assumption)
+  apply(rule conjI)
+  apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
+  apply(simp add: calc_atm)
+  apply(force intro!: eqvt_one)
+  done
+
+lemma one_app: 
+  "App t1 t2 \<longrightarrow>\<^isub>1 t' \<Longrightarrow> 
+  (\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
+  (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
+  apply(ind_cases "App t1 s1 \<longrightarrow>\<^isub>1 t'")
+  apply(auto simp add: lam.distinct lam.inject)
+  done
+
+lemma one_red: 
+  "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M \<Longrightarrow>
+  (\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
+  (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
+  apply(ind_cases "App (Lam [a].t1) s1 \<longrightarrow>\<^isub>1 M")
+  apply(simp_all add: lam.inject)
+  apply(force)
+  apply(erule conjE)
+  apply(drule sym[of "Lam [a].t1"])
+  apply(simp)
+  apply(drule one_abs)
+  apply(erule exE)
+  apply(simp)
+  apply(force simp add: alpha)
+  apply(erule conjE)
+  apply(simp add: lam.inject alpha)
+  apply(erule disjE)
+  apply(simp)
+  apply(force)
+  apply(simp)
+  apply(rule disjI2)
+  apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI)
+  apply(rule_tac x="s2" in exI)
+  apply(auto)
+  apply(subgoal_tac "a\<sharp>t2a")(*A*)
+  apply(simp add: subst_rename)
+  (*A*)
+  apply(force intro: one_fresh_preserv)
+  apply(force intro: eqvt_one)
+  done
+
+(* first case in Lemma 3.2.4*)
+
+lemma one_subst_aux[rule_format]:
+  fixes    M :: "lam"
+  and      N :: "lam"
+  and      N':: "lam"
+  and      x :: "name"
+  shows "N\<longrightarrow>\<^isub>1N'\<longrightarrow>M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+proof (nominal_induct M rule: lam_induct)
+  case (Var N N' x y) 
+  show "N\<longrightarrow>\<^isub>1N' \<longrightarrow> Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
+next
+  case (App N N' x P Q) (* application case - third line *)
+  thus "N\<longrightarrow>\<^isub>1N' \<longrightarrow> (App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp
+next 
+  case (Lam N N' x y P) (* abstraction case - fourth line *)
+  thus "N\<longrightarrow>\<^isub>1N' \<longrightarrow> (Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 
+    by (simp add: fresh_prod fresh_atm)
+qed
+
+lemma one_subst_aux[rule_format]:
+  fixes    M :: "lam"
+  and      N :: "lam"
+  and      N':: "lam"
+  and      x :: "name"
+  shows "N\<longrightarrow>\<^isub>1N'\<longrightarrow>M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+apply(nominal_induct M rule: lam_induct)
+apply(auto simp add: fresh_prod fresh_atm)
+done
+
+lemma one_subst[rule_format]: 
+  fixes    M :: "lam"
+  and      M':: "lam"
+  and      N :: "lam"
+  and      N':: "lam"
+  and      x :: "name"
+  assumes a: "M\<longrightarrow>\<^isub>1M'" 
+  shows "N\<longrightarrow>\<^isub>1N' \<longrightarrow> M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+using a
+proof (nominal_induct M M' rule: one_induct)
+  case (o1 x N N' M)
+  show ?case by (simp add: one_subst_aux)
+next
+  case (o2 x N N' M1 M2 N1 N2)
+  thus ?case by simp
+next
+  case (o3 x N N' a M1 M2)
+  thus ?case by (simp add: fresh_prod fresh_atm)
+next
+  case (o4 N N' x a M1 M2 N1 N2)
+  assume e3: "a\<sharp>(N1,N2,N,N',x)"
+  show ?case
+  proof  
+    assume a1: "N\<longrightarrow>\<^isub>1N'"
+    have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" 
+      using e3 by (simp add: fresh_prod fresh_atm)
+    also have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" 
+      using  o4 a1 by force
+    also have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" 
+      using e3 by (simp add: subs_lemma fresh_prod fresh_atm)
+    ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp
+  qed
+qed
+
+lemma one_subst[rule_format]: 
+  assumes a: "M\<longrightarrow>\<^isub>1M'" 
+  shows "N\<longrightarrow>\<^isub>1N' \<longrightarrow> M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+using a
+apply(nominal_induct M M' rule: one_induct)
+apply(auto simp add: one_subst_aux subs_lemma fresh_prod fresh_atm)
+done
+
+lemma diamond[rule_format]:
+  fixes    M :: "lam"
+  and      M1:: "lam"
+  assumes a: "M\<longrightarrow>\<^isub>1M1" 
+  shows "\<forall>M2. (M\<longrightarrow>\<^isub>1M2) \<longrightarrow> (\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  using a
+proof (induct)
+  case (o1 M) (* case 1 --- M1 = M *)
+  show "\<forall>M2. M\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3)" by force
+next
+  case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
+  assume i1: "\<forall>M2. Q \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  show "\<forall>M2. App (Lam [x].P) Q\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  proof (intro strip)
+    fix M2
+    assume "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2"
+    hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> 
+           (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" by (simp add: one_red)
+    moreover (* subcase 2.1 *)
+    { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+      then obtain P'' and Q'' where 
+	b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by force
+      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain P''' where
+	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
+      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain Q''' where
+	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+      from c1 c2 d1 d2 
+      have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" 
+	by (force simp add: one_subst)
+      hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
+    }
+    moreover (* subcase 2.2 *)
+    { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+      then obtain P'' Q'' where
+	b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by force
+      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain P''' where
+	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
+      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain Q''' where
+	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+      from c1 c2 d1 d2 
+      have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" 
+	by (force simp add: one_subst)
+      hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
+    }
+    ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
+  qed
+next
+  case (o2 Q Q' P P') (* case 3 *)
+  assume i0: "P\<longrightarrow>\<^isub>1P'"
+  assume i1: "\<forall>M2. Q \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  show "\<forall>M2. App P Q\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  proof (intro strip)
+    fix M2
+    assume "App P Q \<longrightarrow>\<^isub>1 M2"
+    hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> 
+           (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')" 
+      by (simp add: one_app[simplified])
+    moreover (* subcase 3.1 *)
+    { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+      then obtain P'' and Q'' where 
+	b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by force
+      from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain P''' where
+	c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
+      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain Q''' where
+	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+      from c1 c2 d1 d2 
+      have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by force
+      hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
+    }
+    moreover (* subcase 3.2 *)
+    { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+      then obtain x P1 P1'' Q'' where
+	b0: "P=Lam [x].P1" and b1: "M2=P1''[x::=Q'']" and 
+        b2: "P1\<longrightarrow>\<^isub>1P1''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by force
+      from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
+      then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by force 
+      from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain P1''' where
+	c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by force
+      from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
+      then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by force
+      from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
+      then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by force
+      from r1 r3 have r5: "R1=R2" 
+	by (simp add: lam.inject alpha)
+      from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      then obtain Q''' where
+	d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+      from g1 r2 d1 r4 r5 d2 
+      have "App P' Q'\<longrightarrow>\<^isub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^isub>1R1[x::=Q''']" by (simp add: one_subst)
+      hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by force
+    }
+    ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
+  qed
+next
+  case (o3 x P P') (* case 4 *)
+  assume i1: "P\<longrightarrow>\<^isub>1P'"
+  assume i2: "\<forall>M2. P \<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  show "\<forall>M2. (Lam [x].P)\<longrightarrow>\<^isub>1M2 \<longrightarrow> (\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)"
+  proof (intro strip)
+    fix M2
+    assume "(Lam [x].P)\<longrightarrow>\<^isub>1 M2"
+    hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^isub>1P''" by (simp add: one_abs)
+    then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^isub>1P''" by force
+    from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by force
+    then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by force
+    from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
+    then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by force
+    from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
+    then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by force
+    from r1 r3 have r5: "R1=R2" 
+      by (simp add: lam.inject alpha)
+    from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" 
+      by (simp add: one_subst)
+    thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by force
+  qed
+qed
+
+lemma one_abs_cong: 
+  fixes a :: "name"
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
+  shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
+  using a
+proof induct
+  case 1 thus ?case by force
+next
+  case (2 y z) 
+  thus ?case by (force dest: b3 intro: rtrancl_trans)
+qed
+
+lemma one_pr_congL: 
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
+  shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
+  using a
+proof induct
+  case 1 thus ?case by (force)
+next
+  case 2 thus ?case by (force dest: b1 intro: rtrancl_trans)
+qed
+  
+lemma one_pr_congR: 
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
+  shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
+using a
+proof induct
+  case 1 thus ?case by (force)
+next 
+  case 2 thus ?case by (force dest: b2 intro: rtrancl_trans)
+qed
+
+lemma one_pr_cong: 
+  assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
+  and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
+  shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
+proof -
+  have b1: "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_pr_congL)
+  have b2: "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_pr_congR)
+  show ?thesis using b1 and b2 by (force intro: rtrancl_trans)
+qed
+
+lemma one_beta_star: 
+  assumes a: "(t1\<longrightarrow>\<^isub>1t2)" 
+  shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
+  using a
+proof induct
+  case o1 thus ?case by (force)
+next
+  case o2 thus ?case by (force intro!: one_pr_cong)
+next
+  case o3 thus ?case by (force intro!: one_abs_cong)
+next 
+  case (o4 a s1 s2 t1 t2)
+  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" .
+  have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" by (rule b4)
+  from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
+    by (force intro!: one_pr_cong one_abs_cong)
+  show ?case using c1 c2 by (force intro: rtrancl_trans)
+qed
+ 
+lemma one_star_abs_cong: 
+  fixes a :: "name"
+  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
+  shows "(Lam  [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)"
+  using a
+proof induct
+  case 1 thus ?case by (force)
+next
+  case 2 thus ?case by (force intro: rtrancl_trans)
+qed
+
+lemma one_star_pr_congL: 
+  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
+  shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+  using a
+proof induct
+  case 1 thus ?case by (force)
+next
+  case 2 thus ?case by (force intro: rtrancl_trans)
+qed
+
+lemma one_star_pr_congR: 
+  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
+  shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
+  using a
+proof induct
+  case 1 thus ?case by (force)
+next
+  case 2 thus ?case by (force intro: rtrancl_trans)
+qed
+
+lemma beta_one_star: 
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" 
+  shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
+  using a
+proof induct
+  case b1 thus ?case by (force intro!: one_star_pr_congL)
+next
+  case b2 thus ?case by (force intro!: one_star_pr_congR)
+next
+  case b3 thus ?case by (force intro!: one_star_abs_cong)
+next
+  case b4 thus ?case by (force)
+qed
+
+lemma trans_closure: 
+  shows "(t1\<longrightarrow>\<^isub>1\<^sup>*t2) = (t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
+proof
+  assume "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
+  thus "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
+  proof induct
+    case 1 thus ?case by (force)
+  next
+    case 2 thus ?case by (force intro: rtrancl_trans simp add: one_beta_star)
+  qed
+next
+  assume "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
+  thus "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
+  proof induct
+    case 1 thus ?case by (force)
+  next
+    case 2 thus ?case by (force intro: rtrancl_trans simp add: beta_one_star)
+  qed
+qed
+
+lemma cr_one:
+  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" 
+  and b: "t\<longrightarrow>\<^isub>1t2"
+  shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
+proof -
+  have stronger: "\<forall>t2. t\<longrightarrow>\<^isub>1t2\<longrightarrow>(\<exists>t3. t1\<longrightarrow>\<^isub>1t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3)"
+    using a 
+  proof induct
+    case 1 show ?case by (force)
+  next
+    case (2 s1 s2)
+    assume b: "s1 \<longrightarrow>\<^isub>1 s2"
+    assume h: "\<forall>t2. t \<longrightarrow>\<^isub>1 t2 \<longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)"
+    show ?case
+    proof (rule allI, rule impI)
+      fix t2
+      assume  c: "t \<longrightarrow>\<^isub>1 t2"
+      show "(\<exists>t3.  s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" 
+      proof -
+	from c h have "(\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by force
+	then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3"
+                         and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (force)
+	have "(\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4)" using b c1 by (force intro: diamond)
+	thus ?thesis using c2 by (force intro: rtrancl_trans)
+      qed
+    qed
+  qed
+  from a b stronger show ?thesis by force
+qed
+
+
+lemma cr_one_star: 
+  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
+      and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"
+    shows "(\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3)"
+using a
+proof induct
+  case 1
+  show ?case using b by force
+next 
+  case (2 s1 s2)
+  assume d: "s1 \<longrightarrow>\<^isub>1 s2"
+  assume "\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and>  s1 \<longrightarrow>\<^isub>1\<^sup>* t3"
+  then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
+                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" by force
+  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
+  then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4"
+                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by force
+  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (force intro: rtrancl_trans)
+  thus ?case using g2 by (force)
+qed
+  
+lemma cr_beta_star: 
+  assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" 
+  and a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
+  shows "(\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3)"
+proof -
+  from a1 have b1: "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp add: trans_closure[symmetric])
+  from a2 have b2: "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp add: trans_closure[symmetric])
+  from b1 and b2 have c: "\<exists>t3. (t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3)" by (force intro!: cr_one_star) 
+  from c obtain t3 where d1: "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and d2: "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by force
+  from d1 have e1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
+  from d2 have e2: "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp add: trans_closure)
+  show ?thesis using e1 and e2 by (force)
+qed
+
+end
+
diff -r 4c9c081a416b -r 836135c8acb2 src/HOL/Nominal/Examples/Lam_substs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Mon Nov 07 15:19:03 2005 +0100
@@ -0,0 +1,1561 @@
+
+theory lam_substs
+imports "../nominal" 
+begin
+
+atom_decl name 
+
+nominal_datatype lam = Var "name"
+                     | App "lam" "lam"
+                     | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+
+section {* strong induction principles for lam *}
+
+lemma lam_induct_aux:
+  fixes P :: "lam \<Rightarrow> 'a \<Rightarrow> bool"
+  and   f :: "'a \<Rightarrow> name set"
+  assumes fs: "\<And>x. finite (f x)"
+      and h1: "\<And>x a. P (Var  a) x"  
+      and h2: "\<And>x t1 t2. (\<forall>z. P t1 z) \<Longrightarrow> (\<forall>z. P t2 z) \<Longrightarrow> P (App t1 t2) x" 
+      and h3: "\<And>x a t. a\<notin>f x \<Longrightarrow> (\<forall>z. P t z) \<Longrightarrow> P (Lam [a].t) x"
+  shows "\<forall>(pi::name prm) x. P (pi\<bullet>t) x"
+proof (induct rule: lam.induct_weak)
+  case (Lam a t)
+  assume i1: "\<forall>(pi::name prm) x. P (pi\<bullet>t) x" 
+  show ?case
+  proof (intro strip, simp add: abs_perm)
+    fix x::"'a" and pi::"name prm"
+    have f: "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 
+          at_fin_set_supp[OF at_name_inst, OF fs] fs)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" 
+      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
+    have g: "Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" using f1 f3
+      by (simp add: lam.inject alpha)
+    from i1 have "\<forall>x. P (([(c,pi\<bullet>a)]@pi)\<bullet>t) x" by force
+    hence i1b: "\<forall>x. P ([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)) x" by (simp add: pt_name2[symmetric])
+    with h3 f2 have "P (Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) x" 
+      by (auto simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs])
+    with g show "P (Lam [(pi\<bullet>a)].(pi\<bullet>t)) x" by simp
+  qed
+qed (auto intro: h1 h2)
+
+lemma lam_induct'[case_names Fin Var App Lam]: 
+  fixes P :: "lam \<Rightarrow> 'a \<Rightarrow> bool"
+  and   x :: "'a"
+  and   t :: "lam"
+  and   f :: "'a \<Rightarrow> name set"
+  assumes fs: "\<And>x. finite (f x)"
+  and     h1: "\<And>x a. P (Var  a) x" 
+  and     h2: "\<And>x t1 t2. (\<forall>z. P t1 z)\<Longrightarrow>(\<forall>z. P t2 z)\<Longrightarrow>P (App t1 t2) x" 
+  and     h3: "\<And>x a t. a\<notin>f x \<Longrightarrow> (\<forall>z. P t z)\<Longrightarrow> P (Lam [a].t) x"
+  shows  "P t x"
+proof - 
+  from fs h1 h2 h3 have "\<forall>(pi::name prm) x. P (pi\<bullet>t) x" by (rule lam_induct_aux, auto)
+  hence "P (([]::name prm)\<bullet>t) x" by blast
+  thus "P t x" by simp
+qed
+
+lemma lam_induct[case_names Var App Lam]: 
+  fixes P :: "lam \<Rightarrow> ('a::fs_name) \<Rightarrow> bool"
+  and   x :: "'a::fs_name"
+  and   t :: "lam"
+  assumes h1: "\<And>x a. P (Var  a) x" 
+  and     h2: "\<And>x t1 t2. (\<forall>z. P t1 z)\<Longrightarrow>(\<forall>z. P t2 z)\<Longrightarrow>P (App t1 t2) x" 
+  and     h3: "\<And>x a t. a\<sharp>x \<Longrightarrow> (\<forall>z. P t z)\<Longrightarrow> P (Lam [a].t) x"
+  shows  "P t x"
+by (rule lam_induct'[of "\<lambda>x. ((supp x)::name set)" "P"], 
+    simp_all add: fs_name1 fresh_def[symmetric], auto intro: h1 h2 h3)
+
+types 'a f1_ty  = "name\<Rightarrow>('a::pt_name)"
+      'a f2_ty  = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
+      'a f3_ty  = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
+
+lemma f3_freshness_conditions:
+  fixes f3::"('a::pt_name) f3_ty"
+  and   y ::"name prm \<Rightarrow> 'a::pt_name"
+  and   a ::"name"
+  and   pi1::"name prm"
+  and   pi2::"name prm"
+  assumes a: "finite ((supp f3)::name set)"
+  and     b: "finite ((supp y)::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) \<and> 
+                       a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) 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,pi2\<bullet>a'')]))"
+  proof -
+    have d5: "[(a'',a')]\<bullet>f3 = f3" 
+      by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) 
+    from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))"
+      by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+    hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 
+      by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
+    hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi1@[(a,pi2\<bullet>a'')])))))" by force
+    thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
+  qed
+  have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')])))"
+  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,pi2\<bullet>a')])))" 
+      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"
+  and   a ::"name"
+  and   pi::"name prm"
+  assumes a: "finite ((supp f3)::name set)"
+  and     b: "finite ((supp y)::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) 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',pi,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,pi,y)" 
+    by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
+  have d3c: "a''\<notin>((supp (f3,a,pi,y))::name set)" using d3b by (simp add: fresh_def)
+  have d4: "a''\<sharp>f3 a'' (y (pi@[(a,a'')]))"
+  proof -
+    have d5: "[(a'',a')]\<bullet>f3 = f3" 
+      by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) 
+    from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))"
+      by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+    hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 
+      by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
+    hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi@[(a,a'')])))))" by force
+    thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
+  qed
+  have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')])))"
+  proof -
+    from a b have d7: "finite ((supp (f3,a,pi,y))::name set)" by (simp add: supp_prod fs_name1)
+    have "((supp (f3,a,pi,y))::name set) supports (\<lambda>a'. f3 a' (y (pi@[(a,a')])))" 
+      by (supports_simp add: perm_append)
+    with d7 d3c show ?thesis by (simp add: supports_fresh)
+  qed
+  from d6 d4 show ?thesis by force
+qed
+
+lemma f3_fresh_fun_supports:
+  fixes f3::"('a::pt_name) f3_ty"
+  and   a ::"name"
+  and   pi1::"name prm"
+  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::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  shows "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))"
+proof (auto simp add: "op supports_def" perm_fun_def expand_fun_eq fresh_def[symmetric])
+  fix b::"name" and c::"name" and pi::"name prm"
+  assume b1: "b\<sharp>(f3,a,y)"
+  and    b2: "c\<sharp>(f3,a,y)"
+  from b1 b2 have b3: "[(b,c)]\<bullet>f3=f3" and t4: "[(b,c)]\<bullet>a=a" and t5: "[(b,c)]\<bullet>y=y"
+    by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod)
+  let ?g = "\<lambda>a'. f3 a' (y (([(b,c)]\<bullet>pi)@[(a,a')]))"
+  and ?h = "\<lambda>a'. f3 a' (y (pi@[(a,a')]))"
+  have a0: "finite ((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set)" using a b 
+    by (simp add: supp_prod fs_name1)
+  have a1: "((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set) supports ?g" by (supports_simp add: perm_append)
+  hence a2: "finite ((supp ?g)::name set)" using a0 by (rule supports_finite)
+  have a3: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
+    by (rule f3_freshness_conditions_simple[OF a, OF b, OF c])
+  have "((supp (f3,a,y))::name set) \<subseteq> (supp (f3,a,[(b,c)]\<bullet>pi,y))" by (force simp add: supp_prod)
+  have a4: "[(b,c)]\<bullet>?g = ?h" using b1 b2
+    by (simp add: fresh_prod, perm_simp add: perm_append)
+  have "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ([(b,c)]\<bullet>?g)" 
+    by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF a2, OF a3])
+  also have "\<dots> = fresh_fun ?h" using a4 by simp
+  finally show "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ?h" .
+qed
+
+lemma f3_fresh_fun_supp_finite:
+  fixes f3::"('a::pt_name) f3_ty"
+  and   a ::"name"
+  and   pi1::"name prm"
+  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::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
+  shows "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)"
+proof -
+  have "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))"
+    using a b c by (rule f3_fresh_fun_supports)
+  moreover
+  have "finite ((supp (f3,a,y))::name set)" using a b by (simp add: supp_prod fs_name1) 
+  ultimately show ?thesis by (rule supports_finite)
+qed
+
+(*
+types 'a recT  = "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> ((lam\<times>name prm\<times>('a::pt_name)) set)"
+
+consts
+  rec :: "('a::pt_name) recT"
+
+inductive "rec f1 f2 f3"
+intros
+r1: "(Var a,pi,f1 (pi\<bullet>a))\<in>rec f1 f2 f3" 
+r2: "\<lbrakk>finite ((supp y1)::name set);(t1,pi,y1)\<in>rec f1 f2 f3; 
+      finite ((supp y2)::name set);(t2,pi,y2)\<in>rec f1 f2 f3\<rbrakk> 
+      \<Longrightarrow> (App t1 t2,pi,f2 y1 y2)\<in>rec f1 f2 f3"
+r3: "\<lbrakk>finite ((supp y)::name set);\<forall>a'. ((t,pi@[(a,a')],y)\<in>rec f1 f2 f3)\<rbrakk> 
+      \<Longrightarrow> (Lam [a].t,pi,fresh_fun (\<lambda>a'. f3 a' y))\<in>rec f1 f2 f3"
+
+*)
+
+(*
+types 'a recT  = "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam\<times>(name prm \<Rightarrow> ('a::pt_name))) set"
+
+consts
+  rec :: "('a::pt_name) recT"
+
+inductive "rec f1 f2 f3"
+intros
+r1: "(Var a,\<lambda>pi. f1 (pi\<bullet>a))\<in>rec f1 f2 f3" 
+r2: "\<lbrakk>finite ((supp y1)::name set);(t1,y1)\<in>rec f1 f2 f3; 
+      finite ((supp y2)::name set);(t2,y2)\<in>rec f1 f2 f3\<rbrakk> 
+      \<Longrightarrow> (App t1 t2,\<lambda>pi. f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3"
+r3: "\<lbrakk>finite ((supp y)::name set);(t,y)\<in>rec f1 f2 f3\<rbrakk> 
+      \<Longrightarrow> (Lam [a].t,fresh_fun (\<lambda>a' pi. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3"
+*)
+
+term lam_Rep.Var
+term lam_Rep.Lam
+
+consts nthe :: "'a nOption \<Rightarrow> 'a"
+primrec
+ "nthe (nSome x) = x"
+
+types 'a recT  = "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam\<times>(name prm \<Rightarrow> ('a::pt_name))) set"
+
+(*
+consts fn :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam_Rep \<Rightarrow> ('a::pt_name)"
+
+primrec
+"fn f1 f2 f3 (lam_Rep.Var a)     = f1 a"
+"fn f1 f2 f3 (lam_Rep.App t1 t2) = f2 (fn f1 f2 f3 t1) (fn f1 f2 f3 t2)"
+"fn f1 f2 f3 (lam_Rep.Lam f)     = fresh_fun (\<lambda>a'. f3 a' (fn f1 f2 f3 (fn' (f a'))))"
+*)
+
+consts
+  rec :: "('a::pt_name) recT"
+
+inductive "rec f1 f2 f3"
+intros
+r1: "(Var a,\<lambda>pi. f1 (pi\<bullet>a))\<in>rec f1 f2 f3" 
+r2: "\<lbrakk>finite ((supp y1)::name set);(t1,y1)\<in>rec f1 f2 f3; 
+      finite ((supp y2)::name set);(t2,y2)\<in>rec f1 f2 f3\<rbrakk> 
+      \<Longrightarrow> (App t1 t2,\<lambda>pi. f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3"
+r3: "\<lbrakk>finite ((supp y)::name set);(t,y)\<in>rec f1 f2 f3\<rbrakk> 
+      \<Longrightarrow> (Lam [a].t,\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3"
+
+constdefs
+  rfun' :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> name prm \<Rightarrow> ('a::pt_name)" 
+  "rfun' f1 f2 f3 t \<equiv> (THE y. (t,y)\<in>rec f1 f2 f3)"
+
+  rfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" 
+  "rfun f1 f2 f3 t \<equiv> rfun' f1 f2 f3 t ([]::name prm)"
+
+lemma rec_prm_eq[rule_format]:
+  fixes f1 ::"('a::pt_name) f1_ty"
+  and   f2 ::"('a::pt_name) f2_ty"
+  and   f3 ::"('a::pt_name) f3_ty"
+  and   t  ::"lam"
+  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
+  shows "(t,y)\<in>rec f1 f2 f3 \<Longrightarrow> (\<forall>(pi1::name prm) (pi2::name prm). pi1 \<sim> pi2 \<longrightarrow> (y pi1 = y pi2))"
+apply(erule rec.induct)
+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 spec)
+apply(drule_tac x="pi2@[(a,x)]" in spec)
+apply(force simp add: prm_eq_def pt2[OF pt_name_inst])
+done
+
+(* silly helper lemma *)
+lemma rec_trans: 
+  fixes f1 ::"('a::pt_name) f1_ty"
+  and   f2 ::"('a::pt_name) f2_ty"
+  and   f3 ::"('a::pt_name) f3_ty"
+  and   t  ::"lam"
+  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
+  assumes a: "(t,y)\<in>rec f1 f2 f3"
+  and     b: "y=y'"
+  shows   "(t,y')\<in>rec f1 f2 f3"
+using a b by simp
+
+
+lemma rec_prm_equiv:
+  fixes f1 ::"('a::pt_name) f1_ty"
+  and   f2 ::"('a::pt_name) f2_ty"
+  and   f3 ::"('a::pt_name) f3_ty"
+  and   t  ::"lam"
+  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
+  and   pi ::"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)"
+  and     a: "(t,y)\<in>rec f1 f2 f3"
+  shows "(pi\<bullet>t,pi\<bullet>y)\<in>rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+using a
+proof (induct)
+  case (r1 c)
+  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f1 (pi'\<bullet>c))"
+  and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f1) (pi'\<bullet>(pi\<bullet>c))"
+  have "?g'=?g" 
+  proof (auto simp only: expand_fun_eq perm_fun_def)
+    fix pi'::"name prm"
+    let ?h = "((rev pi)\<bullet>(pi'\<bullet>(pi\<bullet>c)))"
+    and ?h'= "(((rev pi)\<bullet>pi')\<bullet>c)"
+    have "?h' = ((rev pi)\<bullet>pi')\<bullet>((rev pi)\<bullet>(pi\<bullet>c))" 
+      by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+    also have "\<dots> = ?h"
+      by (simp add: pt_perm_compose[OF pt_name_inst, OF at_name_inst,symmetric])
+    finally show "pi\<bullet>(f1 ?h) = pi\<bullet>(f1 ?h')" by simp
+  qed
+  thus ?case by (force intro: rec_trans rec.r1)
+next
+  case (r2 t1 t2 y1 y2)
+  assume a1: "finite ((supp y1)::name set)"
+  and    a2: "finite ((supp y2)::name set)"
+  and    a3: "(pi\<bullet>t1,pi\<bullet>y1) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+  and    a4: "(pi\<bullet>t2,pi\<bullet>y2) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+  from a1 a2 have a1': "finite ((supp (pi\<bullet>y1))::name set)" and a2': "finite ((supp (pi\<bullet>y2))::name set)"
+    by (simp_all add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
+  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f2 (y1 pi') (y2 pi'))"
+  and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f2) ((pi\<bullet>y1) pi') ((pi\<bullet>y2) pi')"
+  have "?g'=?g" by  (simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+  thus ?case using a1' a2' a3 a4 by (force intro: rec.r2 rec_trans)
+next
+  case (r3 a t y)
+  assume a1: "finite ((supp y)::name set)"
+  and    a2: "(pi\<bullet>t,pi\<bullet>y) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
+  from a1 have a1': "finite ((supp (pi\<bullet>y))::name set)" 
+    by (simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
+  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi'@[(a,a')]))))"
+  and ?g'="(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. (pi\<bullet>f3) a' ((pi\<bullet>y) (pi'@[((pi\<bullet>a),a')]))))"
+  have "?g'=?g" 
+  proof (auto simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst] 
+                        perm_append)
+    fix pi'::"name prm"
+    let ?h  = "\<lambda>a'. pi\<bullet>(f3 ((rev pi)\<bullet>a') (y (((rev pi)\<bullet>pi')@[(a,(rev pi)\<bullet>a')])))"
+    and ?h' = "\<lambda>a'. f3 a' (y (((rev pi)\<bullet>pi')@[(a,a')]))"
+    have fs_f3: "finite ((supp f3)::name set)" using f by (simp add: supp_prod)
+    have fs_h': "finite ((supp ?h')::name set)"
+    proof -
+      have "((supp (f3,a,(rev pi)\<bullet>pi',y))::name set) supports ?h'" 
+	by (supports_simp add: perm_append)
+      moreover
+      have "finite ((supp (f3,a,(rev pi)\<bullet>pi',y))::name set)" using a1 fs_f3 
+	by (simp add: supp_prod fs_name1)
+      ultimately show ?thesis by (rule supports_finite)
+    qed
+    have fcond: "\<exists>(a''::name). a''\<sharp>?h' \<and> a''\<sharp>(?h' a'')"
+      by (rule f3_freshness_conditions_simple[OF fs_f3, OF a1, OF c])
+    have "fresh_fun ?h = fresh_fun (pi\<bullet>?h')"
+      by (simp add: perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+    also have "\<dots> = pi\<bullet>(fresh_fun ?h')"
+      by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF fs_h', OF fcond])
+    finally show "fresh_fun ?h = pi\<bullet>(fresh_fun ?h')" .
+  qed
+  thus ?case using a1' a2 by (force intro: rec.r3 rec_trans)
+qed
+
+lemma rec_perm:
+  fixes f1 ::"('a::pt_name) f1_ty"
+  and   f2 ::"('a::pt_name) f2_ty"
+  and   f3 ::"('a::pt_name) f3_ty"
+  and   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)"
+  and     a: "(t,y)\<in>rec f1 f2 f3"
+  shows "(pi1\<bullet>t, \<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3"
+proof -
+  have lem: "\<forall>(y::name prm\<Rightarrow>('a::pt_name))(pi::name prm). 
+             finite ((supp y)::name set) \<longrightarrow> finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)"
+  proof (intro strip)
+    fix y::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm"
+    assume  "finite ((supp y)::name set)"
+    hence "finite ((supp (y,pi))::name set)" by (simp add: supp_prod fs_name1)      
+    moreover
+    have  "((supp (y,pi))::name set) supports (\<lambda>pi'. y (pi'@pi))" 
+      by (supports_simp add: perm_append)
+    ultimately show "finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)" by (simp add: supports_finite)
+  qed
+from a
+show ?thesis
+proof (induct)
+  case (r1 c)
+  show ?case
+    by (auto simp add: pt2[OF pt_name_inst], rule rec.r1)
+next
+  case (r2 t1 t2 y1 y2)
+  thus ?case using lem by (auto intro!: rec.r2) 
+next
+  case (r3 c t y)
+  assume a0: "(t,y)\<in>rec f1 f2 f3"
+  and    a1: "finite ((supp y)::name set)"
+  and    a2: "(pi1\<bullet>t,\<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3"
+  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
+  show ?case
+  proof(simp)
+    have a3: "finite ((supp (\<lambda>pi2. y (pi2@pi1)))::name set)" using lem a1 by force
+    let ?g' = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' ((\<lambda>pi2. y (pi2@pi1)) (pi@[(pi1\<bullet>c,a')])))"
+    and ?g  = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(pi1\<bullet>c,a')]@pi1)))"
+    and ?h  = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@pi1@[(c,a')])))"
+    have eq1: "?g = ?g'" by simp
+    have eq2: "?g'= ?h" 
+    proof (auto simp only: expand_fun_eq)
+      fix pi::"name prm"
+      let ?q  = "\<lambda>a'. f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1))"
+      and ?q' = "\<lambda>a'. f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))"
+      and ?r  = "\<lambda>a'. f3 a' (y ((pi@pi1)@[(c,a')]))"
+      and ?r' = "\<lambda>a'. f3 a' (y (pi@(pi1@[(c,a')])))"
+      have eq3a: "?r = ?r'" by simp
+      have eq3: "?q = ?q'"
+      proof (auto simp only: expand_fun_eq)
+	fix a'::"name"
+	have "(y ((pi@[(pi1\<bullet>c,a')])@pi1)) =  (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" 
+	  proof -
+	    have "((pi@[(pi1\<bullet>c,a')])@pi1) \<sim> ((pi@pi1)@[(c,(rev pi1)\<bullet>a')])"
+	    by (force simp add: prm_eq_def at_append[OF at_name_inst] 
+                   at_calc[OF at_name_inst] at_bij[OF at_name_inst] 
+                   at_pi_rev[OF at_name_inst] at_rev_pi[OF at_name_inst])
+	    with a0 show ?thesis by (rule rec_prm_eq)
+	  qed
+	thus "f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1)) = f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" by simp
+      qed
+      have fs_a: "finite ((supp ?q')::name set)"
+      proof -
+	have "((supp (f3,c,(pi@pi1),(rev pi1),y))::name set) supports ?q'" 
+	  by (supports_simp add: perm_append fresh_list_append fresh_list_rev)
+	moreover
+	have "finite ((supp (f3,c,(pi@pi1),(rev pi1),y))::name set)" using f' a1
+	  by (simp add: supp_prod fs_name1)
+	ultimately show ?thesis by (rule supports_finite)
+      qed
+      have fs_b: "finite ((supp ?r)::name set)"
+      proof -
+	have "((supp (f3,c,(pi@pi1),y))::name set) supports ?r" 
+	  by (supports_simp add: perm_append fresh_list_append)
+	moreover
+	have "finite ((supp (f3,c,(pi@pi1),y))::name set)" using f' a1
+	  by (simp add: supp_prod fs_name1)
+	ultimately show ?thesis by (rule supports_finite)
+      qed
+      have c1: "\<exists>(a''::name). a''\<sharp>?q' \<and> a''\<sharp>(?q' a'')"
+	by (rule f3_freshness_conditions[OF f', OF a1, OF c])
+      have c2: "\<exists>(a''::name). a''\<sharp>?r \<and> a''\<sharp>(?r a'')"
+	by (rule f3_freshness_conditions_simple[OF f', OF a1, OF c])
+      have c3: "\<exists>(d::name). d\<sharp>(?q',?r,(rev pi1))" 
+	by (rule at_exists_fresh[OF at_name_inst], 
+            simp only: finite_Un supp_prod fs_a fs_b fs_name1, simp)
+      then obtain d::"name" where d1: "d\<sharp>?q'" and d2: "d\<sharp>?r" and d3: "d\<sharp>(rev pi1)" 
+	by (auto simp only: fresh_prod)
+      have eq4: "(rev pi1)\<bullet>d = d" using d3 by (simp add: at_prm_fresh[OF at_name_inst])
+      have "fresh_fun ?q = fresh_fun ?q'" using eq3 by simp
+      also have "\<dots> = ?q' d" using fs_a c1 d1 
+	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
+      also have "\<dots> = ?r d" using fs_b c2 d2 eq4
+	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
+      also have "\<dots> = fresh_fun ?r" using fs_b c2 d2 
+	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
+      finally show "fresh_fun ?q = fresh_fun ?r'" by simp
+    qed
+    from a3 a2 have "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?g')\<in>rec f1 f2 f3" by (rule rec.r3)
+    thus "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?h)\<in>rec f1 f2 f3" using eq2 by simp
+  qed
+qed
+qed    
+
+lemma rec_perm_rev:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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>rec f1 f2 f3"
+  shows "(t, \<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3"
+proof - 
+  from a have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3"
+    by (rule rec_perm[OF f, OF c])
+  thus ?thesis by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+qed
+
+
+lemma rec_unique:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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>rec f1 f2 f3"
+  shows "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm).
+         (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi"
+using a
+proof (induct)
+  case (r1 c)
+  show ?case 
+   apply(auto)
+   apply(ind_cases "(Var c, y') \<in> rec f1 f2 f3")
+   apply(simp_all add: lam.distinct lam.inject)
+   done
+next
+  case (r2 t1 t2 y1 y2)
+  thus ?case 
+    apply(clarify)
+    apply(ind_cases "(App t1 t2, y') \<in> rec f1 f2 f3") 
+    apply(simp_all (no_asm_use) only: lam.distinct lam.inject) 
+    apply(clarify)
+    apply(drule_tac x="y1" in spec)
+    apply(drule_tac x="y2" in spec)
+    apply(auto)
+    done
+next
+  case (r3 c t y)
+  assume i1: "finite ((supp y)::name set)"
+  and    i2: "(t,y)\<in>rec f1 f2 f3"
+  and    i3: "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm).
+              (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi"
+  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
+  show ?case 
+  proof (auto)
+    fix y'::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm"
+    assume i4: "(Lam [c].t, y') \<in> rec f1 f2 f3"
+    from i4 show "fresh_fun (\<lambda>a'. f3 a' (y (pi@[(c,a')]))) = y' pi"
+    proof (cases, simp_all add: lam.distinct lam.inject, auto)
+      fix a::"name" and t'::"lam" and y''::"name prm\<Rightarrow>('a::pt_name)"
+      assume i5: "[c].t = [a].t'"
+      and    i6: "(t',y'')\<in>rec f1 f2 f3"
+      and    i6':"finite ((supp y'')::name set)"
+      let ?g = "\<lambda>a'. f3 a' (y  (pi@[(c,a')]))"
+      and ?h = "\<lambda>a'. f3 a' (y'' (pi@[(a,a')]))"
+      show "fresh_fun ?g = fresh_fun ?h" using i5
+      proof (cases "a=c")
+	case True
+	assume i7: "a=c"
+	with i5 have i8: "t=t'" by (simp add: alpha)
+	show "fresh_fun ?g = fresh_fun ?h" using i3 i6 i7 i8 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 r1: "finite ((supp ?g)::name set)" 
+	proof -
+	  have "((supp (f3,c,pi,y))::name set) supports ?g" 
+	    by (supports_simp add: perm_append)
+	  moreover
+	  have "finite ((supp (f3,c,pi,y))::name set)" using f' i1
+	    by (simp add: supp_prod fs_name1)
+	  ultimately show ?thesis by (rule supports_finite)
+	qed
+	have r2: "finite ((supp ?h)::name set)" 
+	proof -
+	  have "((supp (f3,a,pi,y''))::name set) supports ?h" 
+	    by (supports_simp add: perm_append)
+	  moreover
+	  have "finite ((supp (f3,a,pi,y''))::name set)" using f' i6'
+	    by (simp add: supp_prod fs_name1)
+	  ultimately show ?thesis by (rule supports_finite)
+	qed
+	have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
+	  by (rule f3_freshness_conditions_simple[OF f', OF i1, OF c])
+	have c2: "\<exists>(a''::name). a''\<sharp>?h \<and> a''\<sharp>(?h a'')"
+	  by (rule f3_freshness_conditions_simple[OF f', OF i6', OF c])
+	have "\<exists>(d::name). d\<sharp>(?g,?h,t,a,c)" 
+	  by (rule at_exists_fresh[OF at_name_inst], 
+              simp only: finite_Un supp_prod r1 r2 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 at_fresh[OF at_name_inst] at_fresh[OF at_name_inst])
+	have g1: "[(a,d)]\<bullet>t = t" 
+	  by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF i11, OF f3]) 
+	from i6 have "(([(a,c)]@[(a,d)])\<bullet>t,y'')\<in>rec f1 f2 f3" using g1 i10 by (simp only: pt_name2)
+	hence "(t, \<lambda>pi2. y'' (pi2@(rev ([(a,c)]@[(a,d)]))))\<in>rec f1 f2 f3"
+	  by (simp only: rec_perm_rev[OF f, OF c])
+	hence g2: "(t, \<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)])))\<in>rec 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)]) \<sim> (pi@[(a,d)])"
+	  by (force simp add: prm_eq_def at_calc[OF at_name_inst] at_append[OF at_name_inst])
+	have "fresh_fun ?g = ?g d" using r1 c1 f1
+	  by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
+	also have "\<dots> = f3 d ((\<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)]))) (pi@[(c,d)]))" using i3 g2 by simp 
+	also have "\<dots> = f3 d (y'' (pi@[(c,d)]@[(a,d)]@[(a,c)]))" by simp
+	also have "\<dots> = f3 d (y'' (pi@[(a,d)]))" using i6 g3 by (simp add: rec_prm_eq)
+	also have "\<dots> = fresh_fun ?h" using r2 c2 f2
+	  by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
+	finally show "fresh_fun ?g = fresh_fun ?h" .
+      qed
+    qed
+  qed
+qed
+
+lemma rec_total_aux:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))"
+proof (induct t rule: lam.induct_weak)
+  case (Var c)
+  have a1: "(Var c,\<lambda>(pi::name prm). f1 (pi\<bullet>c))\<in>rec f1 f2 f3" by (rule rec.r1)
+  have a2: "finite ((supp (\<lambda>(pi::name prm). f1 (pi\<bullet>c)))::name set)"
+  proof -
+    have "((supp (f1,c))::name set) supports (\<lambda>(pi::name prm). f1 (pi\<bullet>c))" by (supports_simp)
+    moreover have "finite ((supp (f1,c))::name set)" using f by (simp add: supp_prod fs_name1)
+    ultimately show ?thesis by (rule supports_finite)
+  qed
+  from a1 a2 show ?case by force
+next
+  case (App t1 t2)
+  assume "\<exists>y1. (t1,y1)\<in>rec f1 f2 f3 \<and> finite ((supp y1)::name set)"
+  then obtain y1::"name prm \<Rightarrow> ('a::pt_name)"
+    where a11: "(t1,y1)\<in>rec f1 f2 f3" and a12: "finite ((supp y1)::name set)" by force
+  assume "\<exists>y2. (t2,y2)\<in>rec f1 f2 f3 \<and> finite ((supp y2)::name set)"
+  then obtain y2::"name prm \<Rightarrow> ('a::pt_name)"
+    where a21: "(t2,y2)\<in>rec f1 f2 f3" and a22: "finite ((supp y2)::name set)" by force
+  
+  have a1: "(App t1 t2,\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3"
+    using a12 a11 a22 a21 by (rule rec.r2)
+  have a2: "finite ((supp (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi)))::name set)"
+  proof -
+    have "((supp (f2,y1,y2))::name set) supports (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))" 
+      by (supports_simp)
+    moreover have "finite ((supp (f2,y1,y2))::name set)" using f a21 a22 
+      by (simp add: supp_prod fs_name1)
+    ultimately show ?thesis by (rule supports_finite)
+  qed
+  from a1 a2 show ?case by force
+next
+  case (Lam a t)
+  assume "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)"
+  then obtain y::"name prm \<Rightarrow> ('a::pt_name)"
+    where a11: "(t,y)\<in>rec f1 f2 f3" and a12: "finite ((supp y)::name set)" by force
+  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
+  have a1: "(Lam [a].t,\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3"
+    using a12 a11 by (rule rec.r3)
+  have a2: "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)" 
+    using f' a12 c by (rule f3_fresh_fun_supp_finite)
+  from a1 a2 show ?case by force
+qed
+
+lemma rec_total:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3)"
+proof -
+  have "\<exists>y. ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))"
+    by (rule rec_total_aux[OF f, OF c])
+  thus ?thesis by force
+qed
+
+lemma rec_function:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "\<exists>!y. (t,y)\<in>rec f1 f2 f3"
+proof 
+  case goal1
+  show ?case by (rule rec_total[OF f, OF c])
+next
+  case (goal2 y1 y2)
+  assume a1: "(t,y1)\<in>rec f1 f2 f3" and a2: "(t,y2)\<in>rec f1 f2 f3"
+  hence "\<forall>pi. y1 pi = y2 pi" using rec_unique[OF f, OF c] by force
+  thus ?case by (force simp add: expand_fun_eq) 
+qed
+  
+lemma theI2':
+  assumes a1: "P a" 
+  and     a2: "\<exists>!x. P x" 
+  and     a3: "P a \<Longrightarrow> Q a"
+  shows "Q (THE x. P x)"
+apply(rule theI2)
+apply(rule a1)
+apply(subgoal_tac "\<exists>!x. P x")
+apply(auto intro: a1 simp add: Ex1_def)
+apply(fold Ex1_def)
+apply(rule a2)
+apply(subgoal_tac "x=a")
+apply(simp)
+apply(rule a3)
+apply(assumption)
+apply(subgoal_tac "\<exists>!x. P x")
+apply(auto intro: a1 simp add: Ex1_def)
+apply(fold Ex1_def)
+apply(rule a2)
+done
+
+lemma rfun'_equiv:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  and   pi::"name prm"
+  and   t ::"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)"
+  shows "pi\<bullet>(rfun' f1 f2 f3 t) = rfun' (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
+apply(auto simp add: rfun'_def)
+apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)")
+apply(auto)
+apply(rule sym)
+apply(rule_tac a="y" in theI2')
+apply(assumption)
+apply(rule rec_function[OF f, OF c])
+apply(rule the1_equality)
+apply(rule rec_function)
+apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
+apply(simp add: supp_prod)
+apply(simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
+apply(rule f)
+apply(subgoal_tac "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)")
+apply(auto)
+apply(rule_tac x="pi\<bullet>a" in exI)
+apply(auto)
+apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac x="(rev pi)\<bullet>x" in spec)
+apply(subgoal_tac "(pi\<bullet>f3) (pi\<bullet>a) x  = pi\<bullet>(f3 a ((rev pi)\<bullet>x))")
+apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+apply(subgoal_tac "pi\<bullet>(f3 a ((rev pi)\<bullet>x)) = (pi\<bullet>f3) (pi\<bullet>a) (pi\<bullet>((rev pi)\<bullet>x))")
+apply(simp)
+apply(simp add: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
+apply(simp add: pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
+apply(rule c)
+apply(rule rec_prm_equiv)
+apply(rule f, rule c, assumption)
+apply(rule rec_total_aux)
+apply(rule f)
+apply(rule c)
+done
+
+lemma rfun'_supports:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)"
+proof (auto simp add: "op supports_def" fresh_def[symmetric])
+  fix a::"name" and b::"name"
+  assume a1: "a\<sharp>(f1,f2,f3,t)"
+  and    a2: "b\<sharp>(f1,f2,f3,t)"
+  from a1 a2 have "[(a,b)]\<bullet>f1=f1" and "[(a,b)]\<bullet>f2=f2" and "[(a,b)]\<bullet>f3=f3" and "[(a,b)]\<bullet>t=t"
+    by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod)
+  thus "[(a,b)]\<bullet>(rfun' f1 f2 f3 t) = rfun' f1 f2 f3 t"
+    by (simp add: rfun'_equiv[OF f, OF c])
+qed
+
+lemma rfun'_finite_supp:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "finite ((supp (rfun' f1 f2 f3 t))::name set)"
+apply(rule supports_finite)
+apply(rule rfun'_supports[OF f, OF c])
+apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
+apply(simp add: supp_prod fs_name1)
+apply(rule f)
+done
+
+lemma rfun'_prm:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  and   pi1::"name prm"
+  and   pi2::"name prm"
+  and   t ::"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)"
+  shows "rfun' f1 f2 f3 (pi1\<bullet>t) pi2 = rfun' f1 f2 f3 t (pi2@pi1)"
+apply(auto simp add: rfun'_def)
+apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)")
+apply(auto)
+apply(rule_tac a="y" in theI2')
+apply(assumption)
+apply(rule rec_function[OF f, OF c])
+apply(rule_tac a="\<lambda>pi2. y (pi2@pi1)" in theI2')
+apply(rule rec_perm)
+apply(rule f, rule c)
+apply(assumption)
+apply(rule rec_function)
+apply(rule f)
+apply(rule c)
+apply(simp)
+apply(rule rec_total_aux)
+apply(rule f)
+apply(rule c)
+done
+
+lemma rfun_Var:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "rfun f1 f2 f3 (Var c) = (f1 c)"
+apply(auto simp add: rfun_def rfun'_def)
+apply(subgoal_tac "(THE y. (Var c, y) \<in> rec f1 f2 f3) = (\<lambda>(pi::name prm). f1 (pi\<bullet>c))")(*A*)
+apply(simp)
+apply(rule the1_equality)
+apply(rule rec_function)
+apply(rule f)
+apply(rule c)
+apply(rule rec.r1)
+done
+
+lemma rfun_App:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "rfun f1 f2 f3 (App t1 t2) = (f2 (rfun f1 f2 f3 t1) (rfun f1 f2 f3 t2))"
+apply(auto simp add: rfun_def rfun'_def)
+apply(subgoal_tac "(THE y. (App t1 t2, y)\<in>rec f1 f2 f3) = 
+      (\<lambda>(pi::name prm). f2 ((rfun' f1 f2 f3 t1) pi) ((rfun' f1 f2 f3 t2) pi))")(*A*)
+apply(simp add: rfun'_def)
+apply(rule the1_equality)
+apply(rule rec_function[OF f, OF c])
+apply(rule rec.r2)
+apply(rule rfun'_finite_supp[OF f, OF c])
+apply(subgoal_tac "\<exists>y. (t1,y)\<in>rec f1 f2 f3")
+apply(erule exE, simp add: rfun'_def)
+apply(rule_tac a="y" in theI2')
+apply(assumption)
+apply(rule rec_function[OF f, OF c])
+apply(assumption)
+apply(rule rec_total[OF f, OF c])
+apply(rule rfun'_finite_supp[OF f, OF c])
+apply(subgoal_tac "\<exists>y. (t2,y)\<in>rec f1 f2 f3")
+apply(auto simp add: rfun'_def)
+apply(rule_tac a="y" in theI2')
+apply(assumption)
+apply(rule rec_function[OF f, OF c])
+apply(assumption)
+apply(rule rec_total[OF f, OF c])
+done 
+
+lemma rfun_Lam_aux1:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "rfun f1 f2 f3 (Lam [a].t) = fresh_fun (\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))"
+apply(simp add: rfun_def rfun'_def)
+apply(subgoal_tac "(THE y. (Lam [a].t, y)\<in>rec f1 f2 f3) = 
+        (\<lambda>(pi::name prm). fresh_fun(\<lambda>a'. f3 a' ((rfun' f1 f2 f3 t) (pi@[(a,a')]))))")(*A*)
+apply(simp add: rfun'_def[symmetric])
+apply(rule the1_equality)
+apply(rule rec_function[OF f, OF c])
+apply(rule rec.r3)
+apply(rule rfun'_finite_supp[OF f, OF c])
+apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3")
+apply(erule exE, simp add: rfun'_def)
+apply(rule_tac a="y" in theI2')
+apply(assumption)
+apply(rule rec_function[OF f, OF c])
+apply(assumption)
+apply(rule rec_total[OF f, OF c])
+done
+
+lemma rfun_Lam_aux2:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))"
+proof -
+  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
+  have eq1: "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)"
+  proof -
+    have "Lam [a].t = Lam [b].([(a,b)]\<bullet>t)" using a
+      by (force simp add: lam.inject alpha fresh_prod at_fresh[OF at_name_inst]
+             pt_swap_bij[OF pt_name_inst, OF at_name_inst] 
+             pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst])
+    thus ?thesis by simp
+  qed
+  let ?g = "(\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))"
+  have a0: "((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set) supports ?g"
+    by (supports_simp add: perm_append)
+  have a1: "finite ((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set)"
+    using f' by (simp add: supp_prod fs_name1 rfun'_finite_supp[OF f, OF c])
+  from a0 a1 have a2: "finite ((supp ?g)::name set)"
+    by (rule supports_finite)
+  have c0: "finite ((supp (rfun' f1 f2 f3 t))::name set)"
+    by (rule rfun'_finite_supp[OF f, OF c])
+  have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
+    by (rule f3_freshness_conditions_simple[OF f', OF c0, OF c])
+  have c2: "b\<sharp>?g"
+  proof -
+    have fs_g: "finite ((supp (f1,f2,f3,t))::name set)" using f
+      by (simp add: supp_prod fs_name1)
+    have "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)"
+      by (simp add: rfun'_supports[OF f, OF c])
+    hence c3: "b\<sharp>(rfun' f1 f2 f3 t)" using fs_g 
+    proof(rule supports_fresh, simp add: fresh_def[symmetric])
+      show "b\<sharp>(f1,f2,f3,t)" using a by (simp add: fresh_prod)
+    qed
+    show ?thesis 
+    proof(rule supports_fresh[OF a0, OF a1], simp add: fresh_def[symmetric])
+      show "b\<sharp>(f3,a,([]::name prm),rfun' f1 f2 f3 t)" using a c3
+	by (simp add: fresh_prod fresh_list_nil)
+    qed
+  qed
+  (* main proof *)
+  have "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1)
+  also have "\<dots> = fresh_fun ?g" by (rule rfun_Lam_aux1[OF f, OF c])
+  also have "\<dots> = ?g b" using c2
+    by (rule fresh_fun_app[OF pt_name_inst, OF at_name_inst, OF a2, OF c1])
+  also have "\<dots> = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))"
+    by (simp add: rfun_def rfun'_prm[OF f, OF c])
+  finally show "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))" .
+qed
+
+
+lemma rfun_Lam:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "rfun f1 f2 f3 (Lam [b].t) = f3 b (rfun 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 "rfun f1 f2 f3 (Lam [b].t) = rfun f1 f2 f3 (Lam [b].(([(a,b)])\<bullet>([(a,b)]\<bullet>t)))"
+    by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst])
+  also have "\<dots> = f3 b (rfun f1 f2 f3 (([(a,b)])\<bullet>([(a,b)]\<bullet>t)))" 
+  proof(rule rfun_Lam_aux2[OF f, OF c])
+    have "b\<sharp>([(a,b)]\<bullet>t)" using a1 a2
+      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst] 
+        at_fresh[OF at_name_inst])
+    thus "b\<sharp>(a,[(a,b)]\<bullet>t,f1,f2,f3)" using a a1 by (force simp add: fresh_prod at_fresh[OF at_name_inst])
+  qed
+  also have "\<dots> = f3 b (rfun f1 f2 f3 t)" by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst])
+  finally show ?thesis .
+qed
+  
+lemma rec_unique:
+  fixes fun::"lam \<Rightarrow> ('a::pt_name)"
+  and   f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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     a1: "\<forall>c. fun (Var c) = f1 c" 
+  and     a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" 
+  and     a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)"
+  shows "fun t = rfun f1 f2 f3 t"
+(*apply(nominal_induct t rule: lam_induct')*)
+apply (rule lam_induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>t _. fun t = rfun f1 f2 f3 t"])
+(* finite support *)
+apply(rule f)
+(* VAR *)
+apply(simp add: a1 rfun_Var[OF f, OF c, symmetric])
+(* APP *)
+apply(simp add: a2 rfun_App[OF f, OF c, symmetric])
+(* LAM *)
+apply(fold fresh_def)
+apply(simp add: a3 rfun_Lam[OF f, OF c, symmetric])
+done
+
+lemma rec_function:
+  fixes f1::"('a::pt_name) f1_ty"
+  and   f2::"('a::pt_name) f2_ty"
+  and   f3::"('a::pt_name) f3_ty"
+  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 "(\<exists>!(fun::lam \<Rightarrow> ('a::pt_name)).
+              (\<forall>c.     fun (Var c)     = f1 c) \<and> 
+              (\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)) \<and> 
+              (\<forall>a t.   a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)))"
+apply(rule_tac a="\<lambda>t. rfun f1 f2 f3 t" in ex1I)
+(* existence *)
+apply(simp add: rfun_Var[OF f, OF c])
+apply(simp add: rfun_App[OF f, OF c])
+apply(simp add: rfun_Lam[OF f, OF c])
+(* uniqueness *)
+apply(auto simp add: expand_fun_eq)
+apply(rule rec_unique[OF f, OF c])
+apply(force)+
+done
+
+(* "real" recursion *)
+
+types 'a f1_ty' = "name\<Rightarrow>('a::pt_name)"
+      'a f2_ty' = "lam\<Rightarrow>lam\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
+      'a f3_ty' = "lam\<Rightarrow>name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
+
+constdefs
+  rfun_gen' :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> (lam\<times>'a::pt_name)" 
+  "rfun_gen' f1 f2 f3 t \<equiv> (rfun 
+                             (\<lambda>(a::name). (Var a,f1 a)) 
+                             (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2))) 
+                             (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r)))
+                           t)"
+
+  rfun_gen :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> 'a::pt_name" 
+  "rfun_gen f1 f2 f3 t \<equiv> snd(rfun_gen' f1 f2 f3 t)"
+
+
+
+lemma f1'_supports:
+  fixes f1::"('a::pt_name) f1_ty'"
+  shows "((supp f1)::name set) supports (\<lambda>(a::name). (Var a,f1 a))"
+  by (supports_simp)
+
+lemma f2'_supports:
+  fixes f2::"('a::pt_name) f2_ty'"
+  shows "((supp f2)::name set) supports 
+                         (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2)))"
+  by (supports_simp add: perm_fst perm_snd)  
+
+lemma f3'_supports:
+  fixes f3::"('a::pt_name) f3_ty'"
+  shows "((supp f3)::name set) supports (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r)))"
+by (supports_simp add: perm_fst perm_snd)
+
+lemma fcb': 
+  fixes f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  shows  "\<exists>a.  a \<sharp> (\<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))) \<and>
+                (\<forall>y.  a \<sharp> (Lam [a].fst y, f3 (fst y) a (snd y)))"
+using c f
+apply(auto)
+apply(rule_tac x="a" in exI)
+apply(auto simp add: abs_fresh fresh_prod)
+apply(rule supports_fresh)
+apply(rule f3'_supports)
+apply(simp add: supp_prod)
+apply(simp add: fresh_def)
+done
+
+lemma fsupp':
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  shows "finite((supp
+          (\<lambda>a. (Var a, f1 a),
+           \<lambda>r1 r2.
+              (App (fst r1) (fst r2),
+               f2 (fst r1) (fst r2) (snd r1) (snd r2)),
+           \<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))))::name set)"
+using f
+apply(auto simp add: supp_prod)
+apply(rule supports_finite)
+apply(rule f1'_supports)
+apply(assumption)
+apply(rule supports_finite)
+apply(rule f2'_supports)
+apply(assumption)
+apply(rule supports_finite)
+apply(rule f3'_supports)
+apply(assumption)
+done
+
+lemma rfun_gen'_fst:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)" 
+  and     c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))"
+  shows "fst (rfun_gen' f1 f2 f3 t) = t"
+apply (rule lam_induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>t _. fst (rfun_gen' f1 f2 f3 t) = t"])
+apply(simp add: f)
+apply(unfold rfun_gen'_def)
+apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+apply(simp)
+apply(simp only: rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+apply(simp)
+apply(fold fresh_def)
+apply(auto)
+apply(rule trans)
+apply(rule_tac f="fst" in arg_cong)
+apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+apply(auto simp add: fresh_prod)
+apply(rule supports_fresh)
+apply(rule f1'_supports)
+apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
+apply(simp add: supp_prod)
+apply(rule f)
+apply(simp add: fresh_def)
+apply(rule supports_fresh)
+apply(rule f2'_supports)
+apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
+apply(simp add: supp_prod)
+apply(rule f)
+apply(simp add: fresh_def)
+apply(rule supports_fresh)
+apply(rule f3'_supports)
+apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
+apply(simp add: supp_prod)
+apply(rule f)
+apply(simp add: fresh_def)
+done
+
+lemma rfun_gen'_Var:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  shows "rfun_gen' f1 f2 f3 (Var c) = (Var c, f1 c)"
+apply(simp add: rfun_gen'_def)
+apply(simp add: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+done
+
+lemma rfun_gen'_App:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  shows "rfun_gen' f1 f2 f3 (App t1 t2) = 
+                (App t1 t2, f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2))"
+apply(simp add: rfun_gen'_def)
+apply(rule trans)
+apply(rule rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+apply(fold rfun_gen'_def)
+apply(simp_all add: rfun_gen'_fst[OF f, OF c])
+apply(simp_all add: rfun_gen_def)
+done
+
+lemma rfun_gen'_Lam:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  and     a: "b\<sharp>(f1,f2,f3)"
+  shows "rfun_gen' f1 f2 f3 (Lam [b].t) = (Lam [b].t, f3 t b (rfun_gen f1 f2 f3 t))"
+using a f
+apply(simp add: rfun_gen'_def)
+apply(rule trans)
+apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
+apply(auto simp add: fresh_prod)
+apply(rule supports_fresh)
+apply(rule f1'_supports)
+apply(simp add: supp_prod)
+apply(simp add: fresh_def)
+apply(rule supports_fresh)
+apply(rule f2'_supports)
+apply(simp add: supp_prod)
+apply(simp add: fresh_def)
+apply(rule supports_fresh)
+apply(rule f3'_supports)
+apply(simp add: supp_prod)
+apply(simp add: fresh_def)
+apply(fold rfun_gen'_def)
+apply(simp_all add: rfun_gen'_fst[OF f, OF c])
+apply(simp_all add: rfun_gen_def)
+done
+
+lemma rfun_gen_Var:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  shows "rfun_gen f1 f2 f3 (Var c) = f1 c"
+apply(unfold rfun_gen_def)
+apply(simp add: rfun_gen'_Var[OF f, OF c])
+done
+
+lemma rfun_gen_App:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  shows "rfun_gen f1 f2 f3 (App t1 t2) = f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2)"
+apply(unfold rfun_gen_def)
+apply(simp add: rfun_gen'_App[OF f, OF c])
+apply(simp add: rfun_gen_def)
+done
+
+lemma rfun_gen_Lam:
+  fixes f1::"('a::pt_name) f1_ty'"
+  and   f2::"('a::pt_name) f2_ty'"
+  and   f3::"('a::pt_name) f3_ty'"
+  assumes f: "finite ((supp (f1,f2,f3))::name set)"
+  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
+  and     a: "b\<sharp>(f1,f2,f3)"
+  shows "rfun_gen f1 f2 f3 (Lam [b].t) = f3 t b (rfun_gen f1 f2 f3 t)"
+using a
+apply(unfold rfun_gen_def)
+apply(simp add: rfun_gen'_Lam[OF f, OF c])
+apply(simp add: rfun_gen_def)
+done
+
+instance nat :: pt_name
+apply(intro_classes)
+apply(simp_all add: perm_nat_def)
+done
+
+constdefs 
+  depth_Var :: "name \<Rightarrow> nat"
+  "depth_Var \<equiv> \<lambda>(a::name). 1"
+  
+  depth_App :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  "depth_App \<equiv> \<lambda>n1 n2. (max n1 n2)+1"
+
+  depth_Lam :: "name \<Rightarrow> nat \<Rightarrow> nat"
+  "depth_Lam \<equiv> \<lambda>(a::name) n. n+1"
+
+  depth_lam :: "lam \<Rightarrow> nat"
+  "depth_lam \<equiv> rfun depth_Var depth_App depth_Lam"
+
+lemma supp_depth_Var:
+  shows "((supp depth_Var)::name set)={}"
+  apply(simp add: depth_Var_def)
+  apply(simp add: supp_def)
+  apply(simp add: perm_fun_def)
+  apply(simp add: perm_nat_def)
+  done
+
+lemma supp_depth_App:
+  shows "((supp depth_App)::name set)={}"
+  apply(simp add: depth_App_def)
+  apply(simp add: supp_def)
+  apply(simp add: perm_fun_def)
+  apply(simp add: perm_nat_def)
+  done
+
+lemma supp_depth_Lam:
+  shows "((supp depth_Lam)::name set)={}"
+  apply(simp add: depth_Lam_def)
+  apply(simp add: supp_def)
+  apply(simp add: perm_fun_def)
+  apply(simp add: perm_nat_def)
+  done
+ 
+
+lemma fin_supp_depth:
+  shows "finite ((supp (depth_Var,depth_App,depth_Lam))::name set)"
+  using supp_depth_Var supp_depth_Lam supp_depth_App
+by (simp add: supp_prod)
+
+lemma fresh_depth_Lam:
+  shows "\<exists>(a::name). a\<sharp>depth_Lam \<and> (\<forall>n. a\<sharp>depth_Lam a n)"
+apply(rule exI)
+apply(rule conjI)
+apply(simp add: fresh_def supp_depth_Lam)
+apply(auto simp add: depth_Lam_def)
+apply(unfold fresh_def)
+apply(simp add: supp_def)
+apply(simp add: perm_nat_def)
+done
+
+lemma depth_Var:
+  shows "depth_lam (Var c) = 1"
+apply(simp add: depth_lam_def)
+apply(simp add: rfun_Var[OF fin_supp_depth, OF fresh_depth_Lam])
+apply(simp add: depth_Var_def)
+done
+
+lemma depth_App:
+  shows "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1"
+apply(simp add: depth_lam_def)
+apply(simp add: rfun_App[OF fin_supp_depth, OF fresh_depth_Lam])
+apply(simp add: depth_App_def)
+done
+
+lemma depth_Lam:
+  shows "depth_lam (Lam [a].t) = (depth_lam t)+1"
+apply(simp add: depth_lam_def)
+apply(rule trans)
+apply(rule rfun_Lam[OF fin_supp_depth, OF fresh_depth_Lam])
+apply(simp add: fresh_def supp_prod supp_depth_Var supp_depth_App supp_depth_Lam)
+apply(simp add: depth_Lam_def)
+done
+
+
+(* substitution *)
+
+constdefs 
+  subst_Var :: "name \<Rightarrow>lam \<Rightarrow> name \<Rightarrow> lam"
+  "subst_Var b t \<equiv> \<lambda>a. (if a=b then t else (Var a))"
+  
+  subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
+  "subst_App b t \<equiv> \<lambda>r1 r2. App r1 r2"
+
+  subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
+  "subst_Lam b t \<equiv> \<lambda>a r. Lam [a].r"
+
+  subst_lam :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
+  "subst_lam b t \<equiv> rfun (subst_Var b t) (subst_App b t) (subst_Lam b t)"
+
+
+lemma supports_subst_Var:
+  shows "((supp (b,t))::name set) supports (subst_Var b t)"
+apply(supports_simp add: subst_Var_def)
+apply(rule impI)
+apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
+apply(simp add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
+done
+
+lemma supports_subst_App:
+  shows "((supp (b,t))::name set) supports subst_App b t"
+by (supports_simp add: subst_App_def)
+
+lemma supports_subst_Lam:
+  shows "((supp (b,t))::name set) supports subst_Lam b t"
+  by (supports_simp add: subst_Lam_def)
+
+
+lemma fin_supp_subst:
+  shows "finite ((supp (subst_Var b t,subst_App b t,subst_Lam b t))::name set)"
+apply(auto simp add: supp_prod)
+apply(rule supports_finite)
+apply(rule supports_subst_Var)
+apply(simp add: fs_name1)
+apply(rule supports_finite)
+apply(rule supports_subst_App)
+apply(simp add: fs_name1)
+apply(rule supports_finite)
+apply(rule supports_subst_Lam)
+apply(simp add: fs_name1)
+done
+
+lemma fresh_subst_Lam:
+  shows "\<exists>(a::name). a\<sharp>(subst_Lam b t)\<and> (\<forall>y. a\<sharp>(subst_Lam b t) a y)"
+apply(subgoal_tac "\<exists>(c::name). c\<sharp>(b,t)")
+apply(auto)
+apply(rule_tac x="c" in exI)
+apply(auto)
+apply(rule supports_fresh)
+apply(rule supports_subst_Lam)
+apply(simp_all add: fresh_def[symmetric] fs_name1)
+apply(simp add: subst_Lam_def)
+apply(simp add: abs_fresh)
+apply(rule at_exists_fresh[OF at_name_inst])
+apply(simp add: fs_name1)
+done
+
+lemma subst_Var:
+  shows "subst_lam b t (Var a) = (if a=b then t else (Var a))"
+apply(simp add: subst_lam_def)
+apply(auto simp add: rfun_Var[OF fin_supp_subst, OF fresh_subst_Lam])
+apply(auto simp add: subst_Var_def)
+done
+
+lemma subst_App:
+  shows "subst_lam b t (App t1 t2) = App (subst_lam b t t1) (subst_lam b t t2)"
+apply(simp add: subst_lam_def)
+apply(auto simp add: rfun_App[OF fin_supp_subst, OF fresh_subst_Lam])
+apply(auto simp add: subst_App_def)
+done
+
+lemma subst_Lam:
+  assumes a: "a\<sharp>(b,t)"
+  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
+using a
+apply(simp add: subst_lam_def)
+apply(subgoal_tac "a\<sharp>(subst_Var b t,subst_App b t,subst_Lam b t)")
+apply(auto simp add: rfun_Lam[OF fin_supp_subst, OF fresh_subst_Lam])
+apply(simp (no_asm) add: subst_Lam_def)
+apply(auto simp add: fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_subst_Var)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_subst_App)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_subst_Lam)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+done
+
+lemma subst_Lam':
+  assumes a: "a\<noteq>b"
+  and     b: "a\<sharp>t"
+  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
+apply(rule subst_Lam)
+apply(simp add: fresh_prod a b fresh_atm)
+done
+
+consts
+  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900)
+translations 
+  "t1[a::=t2]" \<rightleftharpoons> "subst_lam a t2 t1"
+
+declare subst_Var[simp]
+declare subst_App[simp]
+declare subst_Lam[simp]
+declare subst_Lam'[simp]
+
+lemma subst_eqvt[simp]:
+  fixes pi:: "name prm"
+  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 rule: lam_induct)
+apply(auto)
+apply(auto simp add: perm_bij fresh_prod fresh_atm)
+apply(subgoal_tac "(aa\<bullet>ab)\<sharp>(aa\<bullet>a,aa\<bullet>b)")(*A*)
+apply(simp) 
+apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) 
+done
+
+lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)"
+apply(nominal_induct t1 rule: lam_induct)
+apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
+apply(blast)
+apply(blast)
+done
+
+(* parallel substitution *)
+
+
+consts
+  "dom_sss" :: "(name\<times>lam) list \<Rightarrow> (name list)"
+primrec
+  "dom_sss []    = []"
+  "dom_sss (x#\<theta>) = (fst x)#(dom_sss \<theta>)" 
+
+consts
+  "apply_sss"  :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" (" _ < _ >" [80,80] 80)
+primrec  
+"(x#\<theta>)<a>  = (if (a = fst x) then (snd x) else \<theta><a>)" 
+
+
+lemma apply_sss_eqvt[rule_format]:
+  fixes pi::"name prm"
+  shows "a\<in>set (dom_sss \<theta>) \<longrightarrow> pi\<bullet>(\<theta><a>) = (pi\<bullet>\<theta>)<pi\<bullet>a>"
+apply(induct_tac \<theta>)
+apply(auto)
+apply(simp add: pt_bij[OF pt_name_inst, OF at_name_inst])
+done
+
+lemma dom_sss_eqvt[rule_format]:
+  fixes pi::"name prm"
+  shows "((pi\<bullet>a)\<in>set (dom_sss \<theta>)) =  (a\<in>set (dom_sss ((rev pi)\<bullet>\<theta>)))"
+apply(induct_tac \<theta>)
+apply(auto)
+apply(simp_all add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+apply(simp_all add: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
+done
+
+constdefs 
+  psubst_Var :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"
+  "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (dom_sss \<theta>) then \<theta><a> else (Var a))"
+  
+  psubst_App :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
+  "psubst_App \<theta> \<equiv> \<lambda>r1 r2. App r1 r2"
+
+  psubst_Lam :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
+  "psubst_Lam \<theta> \<equiv> \<lambda>a r. Lam [a].r"
+
+  psubst_lam :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"
+  "psubst_lam \<theta> \<equiv> rfun (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)"
+
+lemma supports_psubst_Var:
+  shows "((supp \<theta>)::name set) supports (psubst_Var \<theta>)"
+  by (supports_simp add: psubst_Var_def apply_sss_eqvt dom_sss_eqvt)
+
+lemma supports_psubst_App:
+  shows "((supp \<theta>)::name set) supports psubst_App \<theta>"
+  by (supports_simp add: psubst_App_def)
+
+lemma supports_psubst_Lam:
+  shows "((supp \<theta>)::name set) supports psubst_Lam \<theta>"
+  by (supports_simp add: psubst_Lam_def)
+
+lemma fin_supp_psubst:
+  shows "finite ((supp (psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>))::name set)"
+apply(auto simp add: supp_prod)
+apply(rule supports_finite)
+apply(rule supports_psubst_Var)
+apply(simp add: fs_name1)
+apply(rule supports_finite)
+apply(rule supports_psubst_App)
+apply(simp add: fs_name1)
+apply(rule supports_finite)
+apply(rule supports_psubst_Lam)
+apply(simp add: fs_name1)
+done
+
+lemma fresh_psubst_Lam:
+  shows "\<exists>(a::name). a\<sharp>(psubst_Lam \<theta>)\<and> (\<forall>y. a\<sharp>(psubst_Lam \<theta>) a y)"
+apply(subgoal_tac "\<exists>(c::name). c\<sharp>\<theta>")
+apply(auto)
+apply(rule_tac x="c" in exI)
+apply(auto)
+apply(rule supports_fresh)
+apply(rule supports_psubst_Lam)
+apply(simp_all add: fresh_def[symmetric] fs_name1)
+apply(simp add: psubst_Lam_def)
+apply(simp add: abs_fresh)
+apply(rule at_exists_fresh[OF at_name_inst])
+apply(simp add: fs_name1)
+done
+
+lemma psubst_Var:
+  shows "psubst_lam \<theta> (Var a) = (if a\<in>set (dom_sss \<theta>) then \<theta><a> else (Var a))"
+apply(simp add: psubst_lam_def)
+apply(auto simp add: rfun_Var[OF fin_supp_psubst, OF fresh_psubst_Lam])
+apply(auto simp add: psubst_Var_def)
+done
+
+lemma psubst_App:
+  shows "psubst_lam \<theta> (App t1 t2) = App (psubst_lam \<theta> t1) (psubst_lam \<theta> t2)"
+apply(simp add: psubst_lam_def)
+apply(auto simp add: rfun_App[OF fin_supp_psubst, OF fresh_psubst_Lam])
+apply(auto simp add: psubst_App_def)
+done
+
+lemma psubst_Lam:
+  assumes a: "a\<sharp>\<theta>"
+  shows "psubst_lam \<theta> (Lam [a].t1) = Lam [a].(psubst_lam \<theta> t1)"
+using a
+apply(simp add: psubst_lam_def)
+apply(subgoal_tac "a\<sharp>(psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>)")
+apply(auto simp add: rfun_Lam[OF fin_supp_psubst, OF fresh_psubst_Lam])
+apply(simp (no_asm) add: psubst_Lam_def)
+apply(auto simp add: fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_psubst_Var)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_psubst_App)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+apply(rule supports_fresh)
+apply(rule supports_psubst_Lam)
+apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
+done
+
+declare psubst_Var[simp]
+declare psubst_App[simp]
+declare psubst_Lam[simp]
+
+consts
+  psubst_syn  :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900)
+translations 
+  "t[<\<theta>>]" \<rightleftharpoons> "psubst_lam \<theta> t"
+
+end
\ No newline at end of file
diff -r 4c9c081a416b -r 836135c8acb2 src/HOL/Nominal/Examples/Lambda_mu.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Mon Nov 07 15:19:03 2005 +0100
@@ -0,0 +1,122 @@
+
+theory lambda_mu 
+imports "../nominal" 
+begin
+
+section {* Mu-Calculus from Gavin's cilmu-Paper*}
+
+atom_decl var mvar
+
+nominal_datatype trm = Var   "var" 
+                     | Lam  "\<guillemotleft>var\<guillemotright>trm"   ("Lam [_]._" [100,100] 100)
+                     | App  "trm" "trm" 
+                     | Pss  "mvar" "trm"
+                     | Act  "\<guillemotleft>mvar\<guillemotright>trm"  ("Act [_]._" [100,100] 100)
+
+section {* strong induction principle *}
+
+lemma trm_induct_aux:
+  fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
+  and   f1 :: "'a \<Rightarrow> var set"
+  and   f2 :: "'a \<Rightarrow> mvar set"
+  assumes fs1: "\<And>x. finite (f1 x)"
+      and fs2: "\<And>x. finite (f2 x)"
+      and h1: "\<And>k x. P (Var x) k"  
+      and h2: "\<And>k x t. x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (Lam [x].t) k" 
+      and h3: "\<And>k t1 t2. (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l) \<Longrightarrow> P (App t1 t2) k" 
+      and h4: "\<And>k a t1. (\<forall>l. P t1 l) \<Longrightarrow> P (Pss a t1) k" 
+      and h5: "\<And>k a t1. a\<notin>f2 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> P (Act [a].t1) k"
+  shows "\<forall>(pi1::var prm) (pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
+proof (induct rule: trm.induct_weak)
+  case (goal1 a)
+  show ?case using h1 by simp
+next
+  case (goal2 x t)
+  assume i1: "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k" 
+  show ?case
+  proof (intro strip, simp add: abs_perm)
+    fix pi1::"var prm" and pi2::"mvar prm" and k::"'a"
+    have f: "\<exists>c::var. c\<sharp>(f1 k,pi1\<bullet>(pi2\<bullet>x),pi1\<bullet>(pi2\<bullet>t))"
+      by (rule at_exists_fresh[OF at_var_inst], simp add: supp_prod fs_var1 
+          at_fin_set_supp[OF at_var_inst, OF fs1] fs1)
+    then obtain c::"var" 
+      where f1: "c\<noteq>(pi1\<bullet>(pi2\<bullet>x))" and f2: "c\<sharp>(f1 k)" and f3: "c\<sharp>(pi1\<bullet>(pi2\<bullet>t))" 
+      by (force simp add: fresh_prod at_fresh[OF at_var_inst])
+    have g: "Lam [c].([(c,pi1\<bullet>(pi2\<bullet>x))]\<bullet>(pi1\<bullet>(pi2\<bullet>t))) = Lam [(pi1\<bullet>(pi2\<bullet>x))].(pi1\<bullet>(pi2\<bullet>t))" using f1 f3
+      by (simp add: trm.inject alpha)
+    from i1 have "\<forall>k. P (([(c,pi1\<bullet>(pi2\<bullet>x))]@pi1)\<bullet>(pi2\<bullet>t)) k" by force
+    hence i1b: "\<forall>k. P ([(c,pi1\<bullet>(pi2\<bullet>x))]\<bullet>(pi1\<bullet>(pi2\<bullet>t))) k" by (simp add: pt_var2[symmetric])
+    with h3 f2 have "P (Lam [c].([(c,pi1\<bullet>(pi2\<bullet>x))]\<bullet>(pi1\<bullet>(pi2\<bullet>t)))) k" 
+      by (auto simp add: fresh_def at_fin_set_supp[OF at_var_inst, OF fs1])
+    with g show "P (Lam [(pi1\<bullet>(pi2\<bullet>x))].(pi1\<bullet>(pi2\<bullet>t))) k" by simp 
+  qed
+next 
+  case (goal3 t1 t2)
+  assume i1: "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t1)) k" 
+  assume i2: "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t2)) k"
+  show ?case 
+  proof (intro strip)
+    fix pi1::"var prm" and pi2::"mvar prm" and k::"'a"
+    from h3 i1 i2 have "P (App (pi1\<bullet>(pi2\<bullet>t1)) (pi1\<bullet>(pi2\<bullet>t2))) k" by force
+    thus "P (pi1\<bullet>(pi2\<bullet>(App t1 t2))) k" by simp
+  qed
+next
+  case (goal4 b t)
+  assume i1: "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k" 
+  show ?case 
+  proof (intro strip)
+    fix pi1::"var prm" and pi2::"mvar prm" and k::"'a"
+    from h4 i1 have "P (Pss (pi1\<bullet>(pi2\<bullet>b)) (pi1\<bullet>(pi2\<bullet>t))) k" by force
+    thus "P (pi1\<bullet>(pi2\<bullet>(Pss b t))) k" by simp
+  qed
+next
+  case (goal5 b t)
+  assume i1: "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k" 
+  show ?case
+  proof (intro strip, simp add: abs_perm)
+    fix pi1::"var prm" and pi2::"mvar prm" and k::"'a"
+    have f: "\<exists>c::mvar. c\<sharp>(f2 k,pi1\<bullet>(pi2\<bullet>b),pi1\<bullet>(pi2\<bullet>t))"
+      by (rule at_exists_fresh[OF at_mvar_inst], simp add: supp_prod fs_mvar1 
+          at_fin_set_supp[OF at_mvar_inst, OF fs2] fs2)
+    then obtain c::"mvar" 
+      where f1: "c\<noteq>(pi1\<bullet>(pi2\<bullet>b))" and f2: "c\<sharp>(f2 k)" and f3: "c\<sharp>(pi1\<bullet>(pi2\<bullet>t))" 
+      by (force simp add: fresh_prod at_fresh[OF at_mvar_inst])
+    have g: "Act [c].(pi1\<bullet>([(c,pi1\<bullet>(pi2\<bullet>b))]\<bullet>(pi2\<bullet>t))) = Act [(pi1\<bullet>(pi2\<bullet>b))].(pi1\<bullet>(pi2\<bullet>t))" using f1 f3
+      by (simp add: trm.inject alpha, simp add: dj_cp[OF cp_mvar_var_inst, OF dj_var_mvar])
+    from i1 have "\<forall>k. P (pi1\<bullet>(([(c,pi1\<bullet>(pi2\<bullet>b))]@pi2)\<bullet>t)) k" by force
+    hence i1b: "\<forall>k. P (pi1\<bullet>([(c,pi1\<bullet>(pi2\<bullet>b))]\<bullet>(pi2\<bullet>t))) k" by (simp add: pt_mvar2[symmetric])
+    with h5 f2 have "P (Act [c].(pi1\<bullet>([(c,pi1\<bullet>(pi2\<bullet>b))]\<bullet>(pi2\<bullet>t)))) k" 
+      by (auto simp add: fresh_def at_fin_set_supp[OF at_mvar_inst, OF fs2])
+    with g show "P (Act [(pi1\<bullet>(pi2\<bullet>b))].(pi1\<bullet>(pi2\<bullet>t))) k" by simp 
+  qed
+qed
+
+lemma trm_induct'[case_names Var Lam App Pss Act]:
+  fixes P :: "trm \<Rightarrow> 'a \<Rightarrow> bool"
+  and   f1 :: "'a \<Rightarrow> var set"
+  and   f2 :: "'a \<Rightarrow> mvar set"
+  assumes fs1: "\<And>x. finite (f1 x)"
+      and fs2: "\<And>x. finite (f2 x)"
+      and h1: "\<And>k x. P (Var x) k"  
+      and h2: "\<And>k x t. x\<notin>f1 k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (Lam [x].t) k" 
+      and h3: "\<And>k t1 t2. (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l) \<Longrightarrow> P (App t1 t2) k" 
+      and h4: "\<And>k a t1. (\<forall>l. P t1 l) \<Longrightarrow> P (Pss a t1) k" 
+      and h5: "\<And>k a t1. a\<notin>f2 k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> P (Act [a].t1) k"
+  shows "P t k"
+proof -
+  have "\<forall>(pi1::var prm)(pi2::mvar prm) k. P (pi1\<bullet>(pi2\<bullet>t)) k"
+  using fs1 fs2 h1 h2 h3 h4 h5 by (rule trm_induct_aux, auto)
+  hence "P (([]::var prm)\<bullet>(([]::mvar prm)\<bullet>t)) k" by blast
+  thus "P t k" by simp
+qed
+
+lemma trm_induct[case_names Var Lam App Pss Act]: 
+  fixes P :: "trm \<Rightarrow> ('a::{fs_var,fs_mvar}) \<Rightarrow> bool"
+  assumes h1: "\<And>k x. P (Var x) k"  
+      and h2: "\<And>k x t. x\<sharp>k \<Longrightarrow> (\<forall>l. P t l) \<Longrightarrow> P (Lam [x].t) k" 
+      and h3: "\<And>k t1 t2. (\<forall>l. P t1 l) \<Longrightarrow> (\<forall>l. P t2 l) \<Longrightarrow> P (App t1 t2) k" 
+      and h4: "\<And>k a t1. (\<forall>l. P t1 l) \<Longrightarrow> P (Pss a t1) k" 
+      and h5: "\<And>k a t1. a\<sharp>k \<Longrightarrow> (\<forall>l. P t1 l) \<Longrightarrow> P (Act [a].t1) k"
+  shows  "P t k"
+by (rule trm_induct'[of "\<lambda>x. ((supp x)::var set)" "\<lambda>x. ((supp x)::mvar set)" "P"], 
+    simp_all add: fs_var1 fs_mvar1 fresh_def[symmetric], auto intro: h1 h2 h3 h4 h5)
diff -r 4c9c081a416b -r 836135c8acb2 src/HOL/Nominal/Examples/SN.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/SN.thy	Mon Nov 07 15:19:03 2005 +0100
@@ -0,0 +1,902 @@
+
+theory sn
+imports lam_substs  Accessible_Part
+begin
+
+(* Strong normalisation according to the P&T book by Girard et al *)
+
+section {* Beta Reduction *}
+
+lemma subst_rename[rule_format]: 
+  fixes  c  :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam"
+  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
+apply(nominal_induct t1 rule: lam_induct)
+apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)
+done
+
+lemma forget[rule_format]: 
+  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
+apply (nominal_induct t1 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_atm fresh_prod)
+done
+
+lemma fresh_fact[rule_format]: 
+  fixes   b :: "name"
+  and    a  :: "name"
+  and    t1 :: "lam"
+  and    t2 :: "lam" 
+  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
+apply(nominal_induct t1 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_prod fresh_atm)
+done
+
+lemma subs_lemma:  
+  fixes x::"name"
+  and   y::"name"
+  and   L::"lam"
+  and   M::"lam"
+  and   N::"lam"
+  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+apply(nominal_induct M rule: lam_induct)
+apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)
+done
+
+lemma id_subs: "t[x::=Var x] = t"
+apply(nominal_induct t rule: lam_induct)
+apply(simp_all add: fresh_atm)
+done
+
+consts
+  Beta :: "(lam\<times>lam) set"
+syntax 
+  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+translations 
+  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
+  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
+inductive Beta
+  intros
+  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
+  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
+  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+
+lemma eqvt_beta: 
+  fixes pi :: "name prm"
+  and   t  :: "lam"
+  and   s  :: "lam"
+  shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
+  apply(erule Beta.induct)
+  apply(auto)
+  done
+
+lemma beta_induct_aux[rule_format]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+  and a1:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
+  and a2:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
+  and a3:    "\<And>x (a::name) s1 s2. 
+              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
+  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
+using a
+proof (induct)
+  case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
+next
+  case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
+next
+  case (b3 a s1 s2)
+  assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"
+  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
+  show ?case 
+  proof (simp, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name"
+     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+      by (force simp add: fresh_prod fresh_atm)
+    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"
+      using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
+      by (simp add: lam.inject alpha)
+    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+next
+  case (b4 a s1 s2)
+  show ?case
+  proof (simp add: subst_eqvt, intro strip)
+    fix pi::"name prm" and x::"'a::fs_name" 
+    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+      by (force simp add: fresh_prod fresh_atm)
+    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"
+      using a4 f2 by (blast intro!: eqvt_beta)
+    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
+      by (simp add: lam.inject alpha)
+    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
+      using f3 by (simp only: subst_rename[symmetric] pt_name2)
+    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
+      using x alpha1 alpha2 by (simp only: pt_name2)
+  qed
+qed
+
+lemma beta_induct[case_names b1 b2 b3 b4]:
+  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    t :: "lam"
+  and    s :: "lam"
+  and    x :: "'a::fs_name"
+  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+  and a1:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
+  and a2:    "\<And>x t s1 s2. 
+              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
+  and a3:    "\<And>x (a::name) s1 s2. 
+              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
+  and a4:    "\<And>x (a::name) t1 s1. 
+              a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
+  shows "P t s x"
+using a a1 a2 a3 a4
+by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])
+
+lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
+apply(erule Beta.induct)
+apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
+done
+lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
+apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
+apply(auto simp add: lam.distinct lam.inject)
+apply(auto simp add: alpha)
+apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
+apply(rule conjI)
+apply(rule sym)
+apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
+apply(simp)
+apply(rule pt_name3)
+apply(simp add: at_ds5[OF at_name_inst])
+apply(rule conjI)
+apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
+apply(force dest!: supp_beta simp add: fresh_def)
+apply(force intro!: eqvt_beta)
+done
+
+lemma beta_subst[rule_format]: 
+  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
+  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
+using a
+apply(nominal_induct M M' rule: beta_induct)
+apply(auto simp add: fresh_prod fresh_atm subs_lemma)
+done
+
+instance nat :: fs_name
+apply(intro_classes)   
+apply(simp_all add: supp_def perm_nat_def)
+done
+
+datatype ty =
+    TVar "string"
+  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
+
+primrec
+ "pi\<bullet>(TVar s) = TVar s"
+ "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
+
+lemma perm_ty[simp]:
+  fixes pi ::"name prm"
+  and   \<tau>  ::"ty"
+  shows "pi\<bullet>\<tau> = \<tau>"
+  by (cases \<tau>, simp_all)
+
+lemma fresh_ty:
+  fixes a ::"name"
+  and   \<tau>  ::"ty"
+  shows "a\<sharp>\<tau>"
+  by (simp add: fresh_def supp_def)
+
+instance ty :: pt_name
+apply(intro_classes)   
+apply(simp_all)
+done
+
+instance ty :: fs_name
+apply(intro_classes)
+apply(simp add: supp_def)
+done
+
+(* valid contexts *)
+
+consts
+  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
+primrec
+  "dom_ty []    = []"
+  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
+
+consts
+  ctxts :: "((name\<times>ty) list) set" 
+  valid :: "(name\<times>ty) list \<Rightarrow> bool"
+translations
+  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
+inductive ctxts
+intros
+v1[intro]: "valid []"
+v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+
+lemma valid_eqvt:
+  fixes   pi:: "name prm"
+  assumes a: "valid \<Gamma>"
+  shows   "valid (pi\<bullet>\<Gamma>)"
+using a
+apply(induct)
+apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+done
+
+(* typing judgements *)
+
+lemma fresh_context[rule_format]: 
+  fixes  \<Gamma> :: "(name\<times>ty)list"
+  and    a :: "name"
+  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
+apply(induct_tac \<Gamma>)
+apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
+done
+
+lemma valid_elim: 
+  fixes  \<Gamma> :: "(name\<times>ty)list"
+  and    pi:: "name prm"
+  and    a :: "name"
+  and    \<tau> :: "ty"
+  shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
+apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
+done
+
+lemma valid_unicity[rule_format]: 
+  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
+apply(induct_tac \<Gamma>)
+apply(auto dest!: valid_elim fresh_context)
+done
+
+consts
+  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
+syntax
+  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
+translations
+  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
+
+inductive typing
+intros
+t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+
+lemma typing_eqvt: 
+  fixes  \<Gamma> :: "(name\<times>ty) list"
+  and    t :: "lam"
+  and    \<tau> :: "ty"
+  and    pi:: "name prm"
+  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
+  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
+using a
+proof (induct)
+  case (t1 \<Gamma> \<tau> a)
+  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
+  moreover
+  have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>"
+    using typing.intros by (auto simp add: pt_list_set_pi[OF pt_name_inst])
+next 
+  case (t3 \<Gamma> \<sigma> \<tau> a t)
+  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
+  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) : \<tau>\<rightarrow>\<sigma>" 
+    using typing.intros by (force)
+qed (auto)
+
+lemma typing_induct_aux[rule_format]:
+  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    \<Gamma> :: "(name\<times>ty) list"
+  and    t :: "lam"
+  and    \<tau> :: "ty"
+  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
+  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
+  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
+              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P \<Gamma> t2 \<tau> z)
+              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
+  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
+              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
+              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
+  shows "\<forall>(pi::name prm) (x::'a::fs_name). P (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau> x"
+using a
+proof (induct)
+  case (t1 \<Gamma> \<tau> a)
+  assume j1: "valid \<Gamma>"
+  assume j2: "(a,\<tau>)\<in>set \<Gamma>"
+  show ?case
+  proof (intro strip, simp)
+    fix pi::"name prm" and x::"'a::fs_name"
+    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
+    from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
+    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
+    show "P (pi\<bullet>\<Gamma>) (Var (pi\<bullet>a)) \<tau> x" using a1 j3 j4 by force
+  qed
+next
+  case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
+  thus ?case using a2 by (simp, blast intro: typing_eqvt)
+next
+  case (t3 \<Gamma> \<sigma> \<tau> a t)
+  have k1: "a\<sharp>\<Gamma>" by fact
+  have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
+  have k3: "\<forall>(pi::name prm) (x::'a::fs_name). P (pi \<bullet> ((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma> x" by fact
+  show ?case
+  proof (intro strip, simp)
+    fix pi::"name prm" and x::"'a::fs_name"
+    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
+      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+    then obtain c::"name" 
+      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
+      by (force simp add: fresh_prod fresh_atm)
+    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
+      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
+                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
+    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
+      by (simp only: pt_name2, rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
+    have "\<forall>x. P (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using k3 by force
+    hence l2: "\<forall>x. P ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using f1 l1
+      by (force simp add: pt_name2  calc_atm split: if_splits)
+    have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule typing_eqvt)
+    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
+      by (force simp add: pt_name2 calc_atm split: if_splits)
+    have l4: "P (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using f2 f4 l2 l3 a3 by auto
+    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
+      by (simp add: lam.inject alpha)
+    show "P (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>a)].(pi\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using l4 alpha 
+      by (simp only: pt_name2)
+  qed
+qed
+
+lemma typing_induct[case_names t1 t2 t3]:
+  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
+  and    \<Gamma> :: "(name\<times>ty) list"
+  and    t :: "lam"
+  and    \<tau> :: "ty"
+  and    x :: "'a::fs_name"
+  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
+  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
+  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
+              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<forall>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<forall>z. P \<Gamma> t2 \<tau> z)
+              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
+  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
+              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
+              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
+  shows "P \<Gamma> t \<tau> x"
+using a a1 a2 a3 typing_induct_aux[of "\<Gamma>" "t" "\<tau>" "P" "[]" "x", simplified] by force
+
+constdefs
+  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
+  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
+
+lemma weakening[rule_format]: 
+  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>"
+  shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"
+using a
+apply(nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)
+apply(auto simp add: sub_def)
+done
+
+lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
+apply(induct_tac \<Gamma>)
+apply(auto)
+done
+
+lemma free_vars: 
+  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
+  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
+using a
+apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)
+apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)
+done
+
+lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
+apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
+apply(auto simp add: lam.inject lam.distinct)
+done
+
+lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
+apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
+apply(auto simp add: lam.inject lam.distinct)
+done
+
+lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
+apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
+apply(auto simp add: lam.distinct lam.inject alpha) 
+apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt)
+apply(simp)
+apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
+apply(force simp add: calc_atm)
+(*A*)
+apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
+done
+
+lemma typing_valid: 
+  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
+  shows "valid \<Gamma>"
+using a by (induct, auto dest!: valid_elim)
+
+lemma ty_subs[rule_format]:
+  fixes \<Gamma> ::"(name\<times>ty) list"
+  and   t1 ::"lam"
+  and   t2 ::"lam"
+  and   \<tau>  ::"ty"
+  and   \<sigma>  ::"ty" 
+  and   c  ::"name"
+  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
+proof(nominal_induct t1 rule: lam_induct)
+  case (Var \<Gamma> \<sigma> \<tau> c t2 a)
+  show ?case
+  proof(intro strip)
+    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
+    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
+    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
+    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
+    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
+    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
+    proof (cases "a=c", simp_all)
+      assume case1: "a=c"
+      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
+      proof (cases "\<sigma>=\<tau>")
+	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
+      next
+	assume a3: "\<sigma>\<noteq>\<tau>"
+	show ?thesis
+	proof (rule ccontr)
+	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
+	  with case1 a25 show False by force 
+	qed
+      qed
+    next
+      assume case2: "a\<noteq>c"
+      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
+      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
+    qed
+  qed
+next
+  case (App \<Gamma> \<sigma> \<tau> c t2 s1 s2)
+  show ?case
+  proof (intro strip, simp)
+    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
+    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
+    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
+    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
+    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
+      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
+  qed
+next
+  case (Lam \<Gamma> \<sigma> \<tau> c t2 a s)
+  assume "a\<sharp>(\<Gamma>,\<sigma>,\<tau>,c,t2)" 
+  hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
+    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
+  show ?case using f2 f3
+  proof(intro strip, simp)
+    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
+    hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
+    then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
+    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
+    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
+      by (auto dest: valid_elim simp add: fresh_list_cons) 
+    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
+    proof -
+      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
+      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
+	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
+      from c12 c2 c3 show ?thesis by (force intro: weakening)
+    qed
+    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
+    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
+    proof -
+      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
+      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
+      with c8 c82 c83 show ?thesis by (force intro: weakening)
+    qed
+    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
+      using c11 Lam c14 c81 f1 by force
+  qed
+qed
+
+lemma subject[rule_format]: 
+  fixes \<Gamma>  ::"(name\<times>ty) list"
+  and   t1 ::"lam"
+  and   t2 ::"lam"
+  and   \<tau>  ::"ty"
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
+  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
+using a
+proof (nominal_induct t1 t2 rule: beta_induct, auto)
+  case (b1 \<Gamma> \<tau> t s1 s2)
+  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
+  assume "\<Gamma> \<turnstile> App s1 t : \<tau>"
+  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
+  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
+next
+  case (b2 \<Gamma> \<tau> t s1 s2)
+  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
+  assume "\<Gamma> \<turnstile> App t s1 : \<tau>"
+  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
+  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
+next
+  case (b3 \<Gamma> \<tau> a s1 s2)
+  assume "a\<sharp>(\<Gamma>,\<tau>)"
+  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
+  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
+  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
+  with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (force dest: t3_elim)
+  then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by force
+  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
+next
+  case (b4 \<Gamma> \<tau> a s1 s2)
+  have "a\<sharp>(s2,\<Gamma>,\<tau>)" by fact
+  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
+  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
+  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
+  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
+  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
+  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
+qed
+
+
+lemma subject[rule_format]: 
+  fixes \<Gamma>  ::"(name\<times>ty) list"
+  and   t1 ::"lam"
+  and   t2 ::"lam"
+  and   \<tau>  ::"ty"
+  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
+  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
+using a
+apply(nominal_induct t1 t2 rule: beta_induct)
+apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: fresh_prod)
+done
+
+
+
+subsection {* some facts about beta *}
+
+constdefs
+  "NORMAL" :: "lam \<Rightarrow> bool"
+  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
+
+constdefs
+  "SN" :: "lam \<Rightarrow> bool"
+  "SN t \<equiv> t\<in>termi Beta"
+
+lemma qq1: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
+apply(simp add: SN_def)
+apply(drule_tac a="t2" in acc_downward)
+apply(auto)
+done
+
+lemma qq2: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
+apply(simp add: SN_def)
+apply(rule accI)
+apply(auto)
+done
+
+
+section {* Candidates *}
+
+consts
+  RED :: "ty \<Rightarrow> lam set"
+primrec
+ "RED (TVar X) = {t. SN(t)}"
+ "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
+
+constdefs
+  NEUT :: "lam \<Rightarrow> bool"
+  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
+
+(* a slight hack to get the first element of applications *)
+consts
+  FST :: "(lam\<times>lam) set"
+syntax 
+  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
+translations 
+  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
+inductive FST
+intros
+fst[intro!]:  "(App t s) \<guillemotright> t"
+
+lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
+apply(ind_cases "App t s \<guillemotright> t'")
+apply(simp add: lam.inject)
+done
+
+lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
+apply(simp add: SN_def)
+apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
+apply(force)
+(*A*)
+apply(erule acc_induct)
+apply(clarify)
+apply(ind_cases "x \<guillemotright> z")
+apply(clarify)
+apply(rule accI)
+apply(auto intro: b1)
+done
+
+constdefs
+   "CR1" :: "ty \<Rightarrow> bool"
+   "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
+
+   "CR2" :: "ty \<Rightarrow> bool"
+   "CR2 \<tau> \<equiv> \<forall>t t'. ((t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>)"
+
+   "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
+   "CR3_RED t \<tau> \<equiv> \<forall>t'. (t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>)" 
+
+   "CR3" :: "ty \<Rightarrow> bool"
+   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
+   
+   "CR4" :: "ty \<Rightarrow> bool"
+   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
+
+lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
+apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
+apply(blast)
+done
+
+lemma sub_ind: 
+  "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
+apply(simp add: SN_def)
+apply(erule acc_induct)
+apply(auto)
+apply(simp add: CR3_def)
+apply(rotate_tac 5)
+apply(drule_tac x="App t x" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(force simp only: NEUT_def)
+apply(simp (no_asm) add: CR3_RED_def)
+apply(clarify)
+apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
+apply(simp_all add: lam.inject)
+apply(simp only:  CR3_RED_def)
+apply(drule_tac x="s2" in spec)
+apply(simp)
+apply(drule_tac x="s2" in spec)
+apply(simp)
+apply(drule mp)
+apply(simp (no_asm_use) add: CR2_def)
+apply(blast)
+apply(drule_tac x="ta" in spec)
+apply(force)
+apply(auto simp only: NEUT_def lam.inject lam.distinct)
+done
+
+lemma RED_props: "CR1 \<tau> \<and> CR2 \<tau> \<and> CR3 \<tau>"
+apply(induct_tac \<tau>)
+apply(auto)
+(* atom types *)
+(* C1 *)
+apply(simp add: CR1_def)
+(* C2 *)
+apply(simp add: CR2_def)
+apply(clarify)
+apply(drule_tac ?t2.0="t'" in  qq1)
+apply(assumption)+
+(* C3 *)
+apply(simp add: CR3_def CR3_RED_def)
+apply(clarify)
+apply(rule qq2)
+apply(assumption)
+(* arrow types *)
+(* C1 *)
+apply(simp (no_asm) add: CR1_def)
+apply(clarify)
+apply(subgoal_tac "NEUT (Var a)")(*A*)
+apply(subgoal_tac "(Var a)\<in>RED ty1")(*C*)
+apply(drule_tac x="Var a" in spec)
+apply(simp)
+apply(simp add: CR1_def)
+apply(rotate_tac 1)
+apply(drule_tac x="App t (Var a)" in spec)
+apply(simp)
+apply(drule qq3) 
+apply(assumption)
+(*C*)
+apply(simp (no_asm_use) add: CR3_def CR3_RED_def)
+apply(drule_tac x="Var a" in spec)
+apply(drule mp)
+apply(clarify)
+apply(ind_cases " Var a \<longrightarrow>\<^isub>\<beta> t'")
+apply(simp (no_asm_use) add: lam.distinct)+ 
+(*A*)
+apply(simp (no_asm) only: NEUT_def)
+apply(rule disjCI)
+apply(rule_tac x="a" in exI)
+apply(simp (no_asm))
+(* C2 *)
+apply(simp (no_asm) add: CR2_def)
+apply(clarify)
+apply(drule_tac x="u" in spec)
+apply(simp)
+apply(subgoal_tac "App t u \<longrightarrow>\<^isub>\<beta> App t' u")(*X*)
+apply(simp (no_asm_use) only: CR2_def)
+apply(blast)
+(*X*)
+apply(force intro!: b1)
+(* C3 *)
+apply(unfold CR3_def)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(simp (no_asm))
+apply(rule allI)
+apply(rule impI)
+apply(subgoal_tac "SN(u)")(*Z*)
+apply(fold CR3_def)
+apply(drule_tac \<tau>="ty1" and \<sigma>="ty2" in sub_ind)
+apply(simp)
+(*Z*)
+apply(simp add: CR1_def)
+done
+
+lemma double_acc_aux:
+  assumes a_acc: "a \<in> acc r"
+  and b_acc: "b \<in> acc r"
+  and hyp: "\<And>x z.
+    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
+    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
+    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
+    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
+  shows "P a b"
+proof -
+  from a_acc
+  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
+  proof (induct a rule: acc.induct)
+    case (accI x)
+    note accI' = accI
+    have "b \<in> acc r" .
+    thus ?case
+    proof (induct b rule: acc.induct)
+      case (accI y)
+      show ?case
+	apply (rule hyp)
+	apply (erule accI')
+	apply (erule accI')
+	apply (rule acc.accI)
+	apply (erule accI)
+	apply (erule accI)
+	apply (erule accI)
+	done
+    qed
+  qed
+  from b_acc show ?thesis by (rule r)
+qed
+
+lemma double_acc:
+  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
+apply(rule_tac r="r" in double_acc_aux)
+apply(assumption)+
+apply(blast)
+done
+
+lemma abs_RED[rule_format]: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
+apply(simp)
+apply(clarify)
+apply(subgoal_tac "t\<in>termi Beta")(*1*)
+apply(erule rev_mp)
+apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
+apply(erule rev_mp)
+apply(rule_tac a="t" and b="u" in double_acc)
+apply(assumption)
+apply(subgoal_tac "CR1 \<tau>")(*A*)
+apply(simp add: CR1_def SN_def)
+(*A*)
+apply(force simp add: RED_props)
+apply(simp)
+apply(clarify)
+apply(subgoal_tac "CR3 \<sigma>")(*B*)
+apply(simp add: CR3_def)
+apply(rotate_tac 6)
+apply(drule_tac x="App(Lam[x].xa ) z" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(force simp add: NEUT_def)
+apply(simp add: CR3_RED_def)
+apply(clarify)
+apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
+apply(auto simp add: lam.inject lam.distinct)
+apply(drule beta_abs)
+apply(auto)
+apply(drule_tac x="t''" in spec)
+apply(simp)
+apply(drule mp)
+apply(clarify)
+apply(drule_tac x="s" in bspec)
+apply(assumption)
+apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta>  t'' [ x ::= s ]")(*B*)
+apply(subgoal_tac "CR2 \<sigma>")(*C*)
+apply(simp (no_asm_use) add: CR2_def)
+apply(blast)
+(*C*)
+apply(force simp add: RED_props)
+(*B*)
+apply(force intro!: beta_subst)
+apply(assumption)
+apply(rotate_tac 3)
+apply(drule_tac x="s2" in spec)
+apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
+apply(simp)
+(*D*)
+apply(subgoal_tac "CR2 \<tau>")(*E*)
+apply(simp (no_asm_use) add: CR2_def)
+apply(blast)
+(*E*)
+apply(force simp add: RED_props)
+apply(simp add: alpha)
+apply(erule disjE)
+apply(force)
+apply(auto)
+apply(simp add: subst_rename)
+apply(drule_tac x="z" in bspec)
+apply(assumption)
+(*B*)
+apply(force simp add: RED_props)
+(*1*)
+apply(drule_tac x="Var x" in bspec)
+apply(subgoal_tac "CR3 \<tau>")(*2*) 
+apply(drule CR3_CR4)
+apply(simp add: CR4_def)
+apply(drule_tac x="Var x" in spec)
+apply(drule mp)
+apply(rule conjI)
+apply(force simp add: NEUT_def)
+apply(simp add: NORMAL_def)
+apply(clarify)
+apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
+apply(auto simp add: lam.inject lam.distinct)
+apply(force simp add: RED_props)
+apply(simp add: id_subs)
+apply(subgoal_tac "CR1 \<sigma>")(*3*)
+apply(simp add: CR1_def SN_def)
+(*3*)
+apply(force simp add: RED_props)
+done
+
+lemma all_RED: 
+ "((\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(dom_sss \<theta>)\<and>\<theta><a>\<in>RED \<sigma>))\<and>\<Gamma>\<turnstile>t:\<tau>) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
+apply(nominal_induct t rule: lam_induct)
+(* Variables *)
+apply(force dest: t1_elim)
+(* Applications *)
+apply(auto dest!: t2_elim)
+apply(drule_tac x="a" in spec)
+apply(drule_tac x="a" in spec)
+apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
+apply(drule_tac x="\<tau>" in spec)
+apply(drule_tac x="b" in spec)
+apply(drule_tac x="b" in spec)
+apply(force)
+(* Abstractions *)
+apply(drule t3_elim)
+apply(simp add: fresh_prod)
+apply(auto)
+apply(drule_tac x="((ab,\<tau>)#a)" in spec)
+apply(drule_tac x="\<tau>'" in spec)
+apply(drule_tac x="b" in spec)
+apply(simp)
+(* HERE *)
+
+
+done
+