--- a/src/HOL/Nominal/Examples/CR.thy Wed Nov 30 16:59:19 2005 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy Wed Nov 30 17:56:08 2005 +0100
@@ -8,21 +8,22 @@
lemma forget[rule_format]:
shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
-proof (nominal_induct t1 rule: lam_induct)
+proof (nominal_induct t1 fresh: a t2 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)
+ case (Lam c t a t2)
+ have i: "\<And>c t2. c\<sharp>t \<longrightarrow> t[c::=t2] = t" by fact
+ have a: "c\<sharp>t2" by fact
+ have "c\<sharp>a" by fact
+ hence b: "a\<noteq>c" by (simp add: fresh_atm)
show ?case
proof
assume "a\<sharp>Lam [c].t"
- hence "a\<sharp>t" using a by (force simp add: abs_fresh)
+ hence "a\<sharp>t" using b by (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
@@ -30,8 +31,8 @@
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)
+apply (nominal_induct t1 fresh: a t2 rule: lam_induct)
+apply(auto simp add: abs_fresh fresh_atm)
done
lemma fresh_fact[rule_format]:
@@ -40,24 +41,23 @@
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)
+proof (nominal_induct t1 fresh: a b t2 rule: lam_induct)
+ case (Var c a b t2)
+ show ?case by simp
next
- case App
- thus ?case by (simp add: fresh_prod)
+ case App thus ?case by simp
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)
+ case (Lam c t a b t2)
+ have i: "\<And>(a::name) b t2. a\<sharp>t\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t[b::=t2])" by fact
+ have fr: "c\<sharp>a" "c\<sharp>b" "c\<sharp>t2" by fact+
+ hence fr': "c\<noteq>a" by (simp add: 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" using fr' by (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)
+ thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr by (simp add: abs_fresh)
qed
qed
@@ -67,7 +67,7 @@
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(nominal_induct t1 fresh: a b t2 rule: lam_induct)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)
done
@@ -77,101 +77,57 @@
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
+ assumes a: "x\<noteq>y"
+ 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 fresh: 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
+ show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
+ proof -
+ { (*Case 1.1*)
+ assume "z=x"
+ have "(1)": "?LHS = N[y::=L]" using `z=x` by simp
+ have "(2)": "?RHS = N[y::=L]" using `z=x` `x\<noteq>y` by simp
+ from "(1)" "(2)" have "?LHS = ?RHS" by simp
+ }
+ moreover
+ { (*Case 1.2*)
+ assume "z\<noteq>x" and "z=y"
+ have "(1)": "?LHS = L" using `z\<noteq>x` `z=y` by force
+ have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by force
+ have "(3)": "L[x::=N[y::=L]] = L" using `x\<sharp>L` by (simp add: forget)
+ from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp
+ }
+ moreover
+ { (*Case 1.3*)
+ assume "z\<noteq>x" and "z\<noteq>y"
+ have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
+ have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
+ from "(1)" "(2)" have "?LHS = ?RHS" by simp
+ }
+ ultimately show "?LHS = ?RHS" by blast
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
+ case (Lam z M1) (* case 2: lambdas *)
+ have ih: "\<And>x y N L. x\<noteq>y \<Longrightarrow> x\<sharp>L \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
+ have "x\<noteq>y" by fact
+ have "x\<sharp>L" by fact
+ have "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
+ hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
+ 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 `z\<sharp>x` `z\<sharp>y` `z\<sharp>N` `z\<sharp>L` by simp
+ also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using `x\<noteq>y` `x\<sharp>L` by simp
+ also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using `z\<sharp>x` `z\<sharp>N[y::=L]` by simp
+ also have "\<dots> = ?RHS" using `z\<sharp>y` `z\<sharp>L` by simp
+ finally show "?LHS = ?RHS" .
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
+ case (App M1 M2) (* case 3: applications *)
+ thus ?case by simp
qed
lemma subs_lemma:
@@ -180,10 +136,12 @@
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
+ assumes "x\<noteq>y"
+ and "x\<sharp>L"
+ shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
+using prems
+by (nominal_induct M fresh: x y N L rule: lam_induct)
+ (auto simp add: fresh_fact forget)
lemma subst_rename[rule_format]:
fixes c :: "name"
@@ -191,25 +149,25 @@
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)
+proof (nominal_induct t1 fresh: a c t2 rule: lam_induct)
+ case (Var 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)
+ case App thus ?case by force
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)+
+ case (Lam b s)
+ have i: "\<And>a c t2. c\<sharp>s \<longrightarrow> (s[a::=t2] = ([(c,a)]\<bullet>s)[c::=t2])" by fact
+ have f: "b\<sharp>a" "b\<sharp>c" "b\<sharp>t2" by fact
+ from f have a:"b\<noteq>c" and b: "b\<noteq>a" and c: "b\<sharp>t2" by (simp add: 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 "c\<sharp>s" using a by (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)
+ also have "\<dots> = ?RHS" using a b by (simp add: calc_atm)
finally show "?LHS = ?RHS" by simp
qed
qed
@@ -220,8 +178,8 @@
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)
+apply(nominal_induct t1 fresh: a c t2 rule: lam_induct)
+apply(auto simp add: calc_atm fresh_atm abs_fresh)
done
section {* Beta Reduction *}
@@ -245,89 +203,69 @@
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
+ assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
+ shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
+ using a by (induct, auto)
-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"
+lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
+ fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<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])
+ and a1: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
+ and a2: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
+ and a3: "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
+ and a4: "\<And>a t1 s1 x. a\<sharp>(s1,x) \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
+ shows "P x t s"
+proof -
+ from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
+ 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)
+ have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
+ have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
+ show ?case
+ proof (simp)
+ 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 x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
+ 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 x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
+ using x alpha1 alpha2 by (simp only: pt_name2)
+ qed
+ next
+ case (b4 a s1 s2)
+ show ?case
+ proof (simp add: subst_eqvt)
+ 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 x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])"
+ 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 x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
+ using x alpha1 alpha2 by (simp only: pt_name2)
+ qed
+ qed
+ hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast
+ thus ?thesis by simp
+qed
section {* One-Reduction *}
@@ -350,109 +288,93 @@
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
+ assumes a: "t\<longrightarrow>\<^isub>1s"
+ shows "(pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)"
+ using a by (induct, auto)
-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"
+lemma one_induct[consumes 1, case_names o1 o2 o3 o4]:
+ fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<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])
+ and a1: "\<And>t x. P x t t"
+ and a2: "\<And>t1 t2 s1 s2 x. t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P z t1 t2) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow>
+ P x (App t1 s1) (App t2 s2)"
+ and a3: "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
+ and a4: "\<And>a t1 t2 s1 s2 x.
+ a\<sharp>(s1,s2,x) \<Longrightarrow> t1\<longrightarrow>\<^isub>1t2 \<Longrightarrow> (\<And>z. P z t1 t2) \<Longrightarrow> s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (\<And>z. P z s1 s2)
+ \<Longrightarrow> P x (App (Lam [a].t1) s1) (t2[a::=s2])"
+ shows "P x t s"
+proof -
+ from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
+ 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)
+ have j1: "t1 \<longrightarrow>\<^isub>1 t2" by fact
+ have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact
+ show ?case
+ proof (simp)
+ 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 x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t2))"
+ 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 x (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (Lam [(pi\<bullet>a)].(pi\<bullet>t2))"
+ using x alpha1 alpha2 by (simp only: pt_name2)
+ qed
+ next
+ case (o4 a s1 s2 t1 t2)
+ have j0: "t1 \<longrightarrow>\<^isub>1 t2" by fact
+ have j1: "s1 \<longrightarrow>\<^isub>1 s2" by fact
+ have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact
+ have j3: "\<And>(pi::name prm) x. P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
+ show ?case
+ proof (simp)
+ 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 x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (pi\<bullet>s1)) ((([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)])"
+ 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 x (App (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (pi\<bullet>s1)) ((pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
+ using x alpha1 alpha2 by (simp only: pt_name2)
+ qed
+ qed
+ hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast
+ thus ?thesis by simp
+qed
-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])+
+lemma fresh_fact':
+ assumes a: "a\<sharp>t2"
+ shows "a\<sharp>(t1[a::=t2])"
+using a
+proof (nominal_induct t1 fresh: a t2 rule: lam_induct)
+ case (Var b)
+ thus ?case by (simp add: fresh_atm)
next
- case App
- thus ?case by (simp add: fresh_prod)
+ case App thus ?case by simp
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)
+ case (Lam c t)
+ have "a\<sharp>t2" "c\<sharp>a" "c\<sharp>t2" by fact
+ moreover
+ have ih: "\<And>a t2. a\<sharp>t2 \<Longrightarrow> a\<sharp>(t[a::=t2])" by fact
+ ultimately show ?case by (simp add: abs_fresh)
qed
lemma one_fresh_preserv[rule_format]:
@@ -561,33 +483,36 @@
apply(force intro: eqvt_one)
done
-(* first case in Lemma 3.2.4*)
+text {* first case in Lemma 3.2.4*}
-lemma one_subst_aux[rule_format]:
+lemma one_subst_aux:
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)
+ assumes a: "N\<longrightarrow>\<^isub>1N'"
+ shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+using a
+proof (nominal_induct M fresh: 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
- 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
+ case (App P Q) (* application case - third line *)
+ thus "(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)
+ case (Lam y P) (* abstraction case - fourth line *)
+ thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp
qed
-lemma one_subst_aux[rule_format]:
+lemma one_subst_aux:
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)
+ assumes a: "N\<longrightarrow>\<^isub>1N'"
+ shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+using a
+apply(nominal_induct M fresh: x N N' rule: lam_induct)
apply(auto simp add: fresh_prod fresh_atm)
done
@@ -597,40 +522,40 @@
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)
+ assumes a: "M\<longrightarrow>\<^isub>1M'"
+ and b: "N\<longrightarrow>\<^isub>1N'"
+ shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']"
+using prems
+proof (nominal_induct M M' fresh: N N' x rule: one_induct)
+ case (o1 M)
+ thus ?case by (simp add: one_subst_aux)
next
- case (o2 x N N' M1 M2 N1 N2)
+ case (o2 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)
+ case (o3 a M1 M2)
+ thus ?case by simp
next
- case (o4 N N' x a M1 M2 N1 N2)
- assume e3: "a\<sharp>(N1,N2,N,N',x)"
+ case (o4 a M1 M2 N1 N2)
+ have e3: "a\<sharp>N1" "a\<sharp>N2" "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" by fact
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)
+ proof -
+ have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using e3 by simp
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
+ using o4 b 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)
+ using e3 by (simp add: subs_lemma 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)
+ and b: "N\<longrightarrow>\<^isub>1N'"
+ shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']"
+using a b
+apply(nominal_induct M M' fresh: N N' x rule: one_induct)
+apply(auto simp add: one_subst_aux subs_lemma fresh_atm)
done
lemma diamond[rule_format]: