# HG changeset patch
# User urbanc
# Date 1137001112 -3600
# Node ID 2ff0ae57431d47a9b0ae9d874d002ee49bc6e4ba
# Parent  317a6f0ef8b98ede18a06bea1c261a31f689dfef
changes to make use of the new induction principle proved by
Stefan horay (hooraayyy)

diff -r 317a6f0ef8b9 -r 2ff0ae57431d src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Jan 11 18:21:23 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Jan 11 18:38:32 2006 +0100
@@ -10,7 +10,7 @@
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
 using a
-proof (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a t2 rule: lam.induct)
   case (Var b) 
   thus ?case by (simp add: fresh_atm)
 next 
@@ -32,7 +32,7 @@
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
-  by (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+  by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
      (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
@@ -41,7 +41,7 @@
   and     b: "a\<sharp>t2"
   shows "a\<sharp>(t1[b::=t2])"
 using a b
-proof (nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
   case (Var c) 
   thus ?case by simp
 next
@@ -64,7 +64,7 @@
   and     b: "a\<sharp>t2"
   shows "a\<sharp>(t1[b::=t2])"
 using a b
-by (nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+by (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
    (auto simp add: abs_fresh fresh_atm)
 
 
@@ -78,7 +78,7 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-proof (nominal_induct M avoiding: x y N L rule: lam_induct)
+proof (nominal_induct M avoiding: x y N L rule: lam.induct)
   case (Var z) (* case 1: Variables*)
   have "x\<noteq>y" by fact
   have "x\<sharp>L" by fact
@@ -132,14 +132,14 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-by (nominal_induct M avoiding: x y N L rule: lam_induct)
+by (nominal_induct M avoiding: x y N L rule: lam.induct)
    (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
-proof (nominal_induct t1 avoiding: a c t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
   case (Var b)
   thus "(Var b)[a::=t2] = ([(c,a)]\<bullet>(Var b))[c::=t2]" by (simp add: calc_atm fresh_atm)
 next
@@ -166,7 +166,7 @@
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
-apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a c t2 rule: lam.induct)
 apply(auto simp add: calc_atm fresh_atm abs_fresh)
 done
 
@@ -352,7 +352,7 @@
   assumes a: "a\<sharp>t2" 
   shows "a\<sharp>(t1[a::=t2])"
 using a 
-proof (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+proof (nominal_induct t1 avoiding: a t2 rule: lam.induct)
   case (Var b) 
   thus ?case by (simp add: fresh_atm)
 next
@@ -473,7 +473,7 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-proof (nominal_induct M avoiding: x N N' rule: lam_induct)
+proof (nominal_induct M avoiding: x N N' rule: lam.induct)
   case (Var y) 
   show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto)
 next
@@ -488,7 +488,7 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-apply(nominal_induct M avoiding: x N N' rule: lam_induct)
+apply(nominal_induct M avoiding: x N N' rule: lam.induct)
 apply(auto simp add: fresh_prod fresh_atm)
 done
 
diff -r 317a6f0ef8b9 -r 2ff0ae57431d src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Jan 11 18:21:23 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Jan 11 18:38:32 2006 +0100
@@ -14,56 +14,6 @@
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-section {* Strong induction principles for lam *}
-
-lemma lam_induct'[case_names Fin Var App Lam]:
-  fixes P :: "'a \<Rightarrow> lam \<Rightarrow> bool"
-  and   f :: "'a \<Rightarrow> 'a"
-  assumes fs: "\<And>x. finite ((supp (f x))::name set)"
-      and h1: "\<And>a x. P x (Var  a)"  
-      and h2: "\<And>t1 t2 x. (\<And>z. P z t1) \<Longrightarrow> (\<And>z. P z t2) \<Longrightarrow> P x (App t1 t2)" 
-      and h3: "\<And>a t x. a\<sharp>f x \<Longrightarrow> (\<And>z. P z t) \<Longrightarrow> P x (Lam [a].t)"
-  shows "P x t"
-proof -
-  have "\<And>(pi::name prm) x. P x (pi\<bullet>t)"
-  proof (induct rule: lam.induct_weak)
-    case (Lam a t)
-    have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact
-    show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))"
-    proof (simp)
-      fix x::"'a" and pi::"name prm"
-      have "\<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 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 fresh_atm)
-      have "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)
-      moreover
-      from ih have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>t)" by force
-      hence "\<And>x. P x ([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))" by (simp add: pt_name2[symmetric])
-      hence "P x (Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t)))" using h3 f2
-	by (auto simp add: fresh_def at_fin_set_supp[OF at_name_inst, OF fs])
-      ultimately show "P x (Lam [(pi\<bullet>a)].(pi\<bullet>t))" by simp
-    qed
-  qed (auto intro: h1 h2)
-  hence "P x (([]::name prm)\<bullet>t)" by blast
-  thus "P x t" by simp
-qed
-
-lemma lam_induct[case_names Var App Lam]: 
-  fixes P :: "('a::fs_name) \<Rightarrow> lam \<Rightarrow> bool"
-  and   x :: "'a::fs_name"
-  and   t :: "lam"
-  assumes h1: "\<And>a x. P x (Var  a)" 
-  and     h2: "\<And>t1 t2 x. (\<And>z. P z t1)\<Longrightarrow>(\<And>z. P z t2)\<Longrightarrow>P x (App t1 t2)" 
-  and     h3: "\<And>a t x. a\<sharp>x \<Longrightarrow> (\<And>z. P z t)\<Longrightarrow> P x (Lam [a].t)"
-  shows  "P x t"
-apply(rule lam_induct'[of "\<lambda>x. x" "P"])
-apply(simp add: fs_name1)
-apply(auto intro: h1 h2 h3)
-done
-
 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)"
@@ -915,7 +865,8 @@
   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 (rule lam_induct'[of "\<lambda>_. (f1,f2,f3)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"])
+apply (rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"])
+apply(fold fresh_def)
 (* finite support *)
 apply(rule f)
 (* VAR *)
@@ -1029,7 +980,8 @@
   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>_. (f1,f2,f3)" "\<lambda>_ t. 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(fold fresh_def)
 apply(simp add: f)
 apply(unfold rfun_gen'_def)
 apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
@@ -1362,15 +1314,16 @@
   and   t2:: "lam"
   and   a :: "name"
   shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 avoiding: b t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: b t2 rule: lam.induct)
 apply(auto simp add: perm_bij fresh_prod fresh_atm)
-apply(subgoal_tac "(pi\<bullet>a)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
-apply(simp) 
+apply(subgoal_tac "(pi\<bullet>name)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
+apply(simp)
+(*A*) 
 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 avoiding: a t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a t2 rule: lam.induct)
 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
 apply(blast)
 apply(blast)
diff -r 317a6f0ef8b9 -r 2ff0ae57431d src/HOL/Nominal/Examples/Lambda_mu.thy
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Wed Jan 11 18:21:23 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Wed Jan 11 18:38:32 2006 +0100
@@ -14,113 +14,3 @@
                      | Pss  "mvar" "trm"
                      | Act  "\<guillemotleft>mvar\<guillemotright>trm"  ("Act [_]._" [100,100] 100)
 
-section {* strong induction principle *}
-
-(* FIXME: this induction rule needs some slight change to conform *)
-(* with the convention from lam_substs                            *)
-
-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 317a6f0ef8b9 -r 2ff0ae57431d src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 18:21:23 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 18:38:32 2006 +0100
@@ -10,7 +10,7 @@
 
 lemma subst_rename[rule_format]: 
   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
-apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a c t2 rule: lam.induct)
 apply(auto simp add: calc_atm fresh_atm abs_fresh)
 done
 
@@ -18,7 +18,7 @@
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
-apply (nominal_induct t1 avoiding: a t2 rule: lam_induct)
+apply (nominal_induct t1 avoiding: a t2 rule: lam.induct)
 apply(auto simp add: abs_fresh fresh_atm)
 done
 
@@ -28,7 +28,7 @@
   and     b: "a\<sharp>t2"
   shows "a\<sharp>(t1[b::=t2])"
 using a b
-apply(nominal_induct t1 avoiding: a b t2 rule: lam_induct)
+apply(nominal_induct t1 avoiding: a b t2 rule: lam.induct)
 apply(auto simp add: abs_fresh fresh_atm)
 done
 
@@ -37,11 +37,11 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-by (nominal_induct M avoiding: x y N L rule: lam_induct)
+by (nominal_induct M avoiding: x y N L rule: lam.induct)
    (auto simp add: fresh_fact forget)
 
 lemma id_subs: "t[x::=Var x] = t"
-apply(nominal_induct t avoiding: x rule: lam_induct)
+apply(nominal_induct t avoiding: x rule: lam.induct)
 apply(simp_all add: fresh_atm)
 done
 
@@ -407,7 +407,7 @@
   and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
   shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
 using a b
-proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam_induct)
+proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
   case (Var a) 
   have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
@@ -846,13 +846,13 @@
   assumes a: "c\<sharp>\<theta>"
   shows "(t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
 using a
-apply(nominal_induct t avoiding: \<theta> c s rule: lam_induct)
+apply(nominal_induct t avoiding: \<theta> c s rule: lam.induct)
 apply(auto dest: fresh_domain)
 apply(drule fresh_at)
 apply(assumption)
 apply(rule forget)
 apply(assumption)
-apply(subgoal_tac "a\<sharp>((c,s)#\<theta>)")(*A*)
+apply(subgoal_tac "name\<sharp>((c,s)#\<theta>)")(*A*)
 apply(simp)
 (*A*)
 apply(simp add: fresh_list_cons fresh_prod)
@@ -863,7 +863,7 @@
   and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
   shows "t[<\<theta>>]\<in>RED \<tau>"
 using a b
-proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
+proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
   case (Lam a t) --"lambda case"
   have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow> 
                     (\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) 
@@ -904,7 +904,7 @@
 
 lemma id_apply:  
   shows "t[<(id \<Gamma>)>] = t"
-apply(nominal_induct t avoiding: \<Gamma> rule: lam_induct)
+apply(nominal_induct t avoiding: \<Gamma> rule: lam.induct)
 apply(auto)
 apply(simp add: id_var)
 apply(drule id_fresh)+