changes to make use of the new induction principle proved by
Stefan horay (hooraayyy)
--- 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
--- 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)
--- 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)
--- 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)+