--- a/src/HOL/Nominal/Examples/Class1.thy Thu Mar 03 22:06:15 2011 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy Fri Mar 04 00:09:47 2011 +0100
@@ -6532,7 +6532,7 @@
by (auto simp add: abs_fresh fresh_atm forget trm.inject)
next
case (Cut d M u M' x' y' c P)
- from prems show ?case
+ with assms show ?case
apply(simp)
apply(auto)
apply(rule trans)
@@ -6840,7 +6840,7 @@
by (auto simp add: abs_fresh fresh_atm forget trm.inject)
next
case (Cut d M u M' x' y' c P)
- from prems show ?case
+ with assms show ?case
apply(simp)
apply(auto simp add: trm.inject)
apply(rule trans)
@@ -7163,15 +7163,15 @@
case (Cut c M z N)
{ assume asm: "M = Ax x c \<and> N = Ax z b"
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
- using asm prems by simp
- also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using asm prems by (simp add: fresh_atm)
- also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using asm prems by (auto simp add: fresh_prod fresh_atm)
+ using Cut asm by simp
+ also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
+ also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using Cut asm by (auto simp add: fresh_prod fresh_atm)
finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.(P{b:=(y).Q}) (y).Q)" by simp
have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = (Cut <c>.M (y).Q){x:=<a>.(P{b:=(y).Q})}"
- using prems asm by (simp add: fresh_atm)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using asm prems
+ using Cut asm by (simp add: fresh_atm)
+ also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using Cut asm
by (auto simp add: fresh_prod fresh_atm subst_fresh)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using asm prems by (simp add: forget)
+ also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using Cut asm by (simp add: forget)
finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = Cut <a>.(P{b:=(y).Q}) (y).Q"
by simp
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
@@ -7186,18 +7186,18 @@
case False then show ?thesis by (simp add: not_Ax1)
qed
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.(M{x:=<a>.P}) (z).(N{x:=<a>.P})){b:=(y).Q}"
- using asm prems by simp
- also have "\<dots> = (Cut <c>.(M{x:=<a>.P}) (z).N){b:=(y).Q}" using asm prems by (simp add: fresh_atm)
- also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (y).Q" using asm prems by (simp add: abs_fresh)
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" using asm prems by simp
+ using Cut asm by simp
+ also have "\<dots> = (Cut <c>.(M{x:=<a>.P}) (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
+ also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (y).Q" using Cut asm by (simp add: abs_fresh)
+ also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" using Cut asm by simp
finally
have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q"
by simp
have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
- (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using asm prems by simp
+ (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using Cut asm by simp
also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})"
- using asm prems neq by (auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using asm prems by (simp add: forget)
+ using Cut asm neq by (auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
+ also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using Cut asm by (simp add: forget)
finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
= Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" by simp
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
@@ -7212,19 +7212,19 @@
case False then show ?thesis by (simp add: not_Ax2)
qed
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
- using asm prems by simp
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using asm prems neq
+ using Cut asm by simp
+ also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq
by (simp add: abs_fresh)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" using asm prems by simp
+ also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" using Cut asm by simp
finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
= Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
= (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
- using asm prems by auto
+ using Cut asm by auto
also have "\<dots> = (Cut <c>.M (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
- using asm prems by (auto simp add: fresh_atm)
+ using Cut asm by (auto simp add: fresh_atm)
also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using asm prems by (simp add: fresh_prod fresh_atm subst_fresh)
+ using Cut asm by (simp add: fresh_prod fresh_atm subst_fresh)
finally
have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
= Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
@@ -7246,17 +7246,17 @@
case False then show ?thesis by (simp add: not_Ax1)
qed
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.(M{x:=<a>.P}) (z).(N{x:=<a>.P})){b:=(y).Q}"
- using asm prems by simp
- also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using asm prems neq1
+ using Cut asm by simp
+ also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq1
by (simp add: abs_fresh)
also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using asm prems by simp
+ using Cut asm by simp
finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
= Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
- (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}" using asm neq1 prems by simp
+ (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}" using Cut asm neq1 by simp
also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using asm neq2 prems by (simp add: fresh_prod fresh_atm subst_fresh)
+ using Cut asm neq2 by (simp add: fresh_prod fresh_atm subst_fresh)
finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
--- a/src/HOL/Nominal/Examples/Class2.thy Thu Mar 03 22:06:15 2011 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Fri Mar 04 00:09:47 2011 +0100
@@ -300,32 +300,32 @@
proof -
{ assume asm: "N\<noteq>Ax y b"
have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} =
- (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using prems
+ (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
by (simp add: subst_fresh abs_fresh fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using prems
+ also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using LNot
by (auto intro: l_redu.intros simp add: subst_fresh)
- also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using LNot asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally have ?thesis by auto
}
moreover
{ assume asm: "N=Ax y b"
have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} =
- (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using prems
+ (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
by (simp add: subst_fresh abs_fresh fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using prems
+ also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using LNot
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <b>.(Cut <c>.P (y).Ax y b) (u).(M{y:=<c>.P}))" using prems
+ also have "\<dots> = (Cut <b>.(Cut <c>.P (y).Ax y b) (u).(M{y:=<c>.P}))" using LNot asm
by simp
also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(P[c\<turnstile>c>b]) (u).(M{y:=<c>.P}))"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LNot
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -347,7 +347,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using LNot asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -368,15 +368,15 @@
{ assume asm: "M1\<noteq>Ax y a1"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.P})"
- using prems
+ using LAnd1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using LAnd1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a1>.M1 (u).N){y:=<c>.P}"
@@ -386,21 +386,21 @@
{ assume asm: "M1=Ax y a1"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.P})"
- using prems
+ using LAnd1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a1>.(Cut <c>.P (y). Ax y a1) (u).(N{y:=<c>.P})"
- using prems by simp
+ using LAnd1 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.P[c\<turnstile>c>a1] (u).(N{y:=<c>.P})"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LAnd1
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -422,7 +422,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using LAnd1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -444,15 +444,15 @@
{ assume asm: "M2\<noteq>Ax y a2"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.P})"
- using prems
+ using LAnd2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using LAnd2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a2>.M2 (u).N){y:=<c>.P}"
@@ -462,21 +462,21 @@
{ assume asm: "M2=Ax y a2"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.P})"
- using prems
+ using LAnd2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a2>.(Cut <c>.P (y). Ax y a2) (u).(N{y:=<c>.P})"
- using prems by simp
+ using LAnd2 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.P[c\<turnstile>c>a2] (u).(N{y:=<c>.P})"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LAnd2 asm
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -498,7 +498,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using LAnd2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -520,15 +520,15 @@
{ assume asm: "M\<noteq>Ax y a"
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.P})"
- using prems
+ using LOr1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using LOr1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x1).N1){y:=<c>.P}"
@@ -538,21 +538,21 @@
{ assume asm: "M=Ax y a"
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.P})"
- using prems
+ using LOr1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <c>.P (y). Ax y a) (x1).(N1{y:=<c>.P})"
- using prems by simp
+ using LOr1 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.P[c\<turnstile>c>a] (x1).(N1{y:=<c>.P})"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LOr1
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -574,7 +574,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using LOr1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -596,15 +596,15 @@
{ assume asm: "M\<noteq>Ax y a"
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.P})"
- using prems
+ using LOr2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using LOr2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x2).N2){y:=<c>.P}"
@@ -614,21 +614,21 @@
{ assume asm: "M=Ax y a"
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.P})"
- using prems
+ using LOr2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <c>.P (y). Ax y a) (x2).(N2{y:=<c>.P})"
- using prems by simp
+ using LOr2 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.P[c\<turnstile>c>a] (x2).(N2{y:=<c>.P})"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LOr2
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -650,7 +650,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using LOr2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -672,15 +672,15 @@
{ assume asm: "N\<noteq>Ax y d"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} =
Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
- using prems by (simp add: fresh_prod abs_fresh fresh_atm)
+ using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{y:=<c>.P}) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using LImp asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} \<longrightarrow>\<^isub>a*
@@ -691,21 +691,21 @@
{ assume asm: "N=Ax y d"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} =
Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
+ using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{y:=<c>.P}) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <d>.(Cut <c>.P (y).Ax y d) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
- using prems by simp
+ using LImp asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(P[c\<turnstile>c>d]) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
proof (cases "fic P c")
case True
assume "fic P c"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
@@ -719,7 +719,7 @@
next
case False
assume "\<not>fic P c"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutL)
@@ -731,7 +731,7 @@
apply(simp add: subst_with_ax2)
done
qed
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using LImp asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -810,32 +810,32 @@
proof -
{ assume asm: "M\<noteq>Ax u c"
have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} =
- (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using prems
+ (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
by (simp add: subst_fresh abs_fresh fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems
+ also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
by (auto intro: l_redu.intros simp add: subst_fresh)
- also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using LNot asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally have ?thesis by auto
}
moreover
{ assume asm: "M=Ax u c"
have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} =
- (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using prems
+ (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
by (simp add: subst_fresh abs_fresh fresh_atm)
- also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems
+ also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <b>.(N{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P))" using prems
+ also have "\<dots> = (Cut <b>.(N{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P))" using LNot asm
by simp
also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(P[y\<turnstile>n>u]))"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LNot
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
@@ -857,7 +857,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using LNot asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -878,15 +878,15 @@
{ assume asm: "N\<noteq>Ax u c"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} =
Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(N{c:=(y).P})"
- using prems
+ using LAnd1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using LAnd1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a1>.M1 (u).N){c:=(y).P}"
@@ -896,21 +896,21 @@
{ assume asm: "N=Ax u c"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} =
Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(N{c:=(y).P})"
- using prems
+ using LAnd1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a1>.(M1{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)"
- using prems by simp
+ using LAnd1 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(P[y\<turnstile>n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LAnd1
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
@@ -932,7 +932,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using LAnd1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -954,15 +954,15 @@
{ assume asm: "N\<noteq>Ax u c"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} =
Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(N{c:=(y).P})"
- using prems
+ using LAnd2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using LAnd2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a2>.M2 (u).N){c:=(y).P}"
@@ -972,21 +972,21 @@
{ assume asm: "N=Ax u c"
have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} =
Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(N{c:=(y).P})"
- using prems
+ using LAnd2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a2>.(M2{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)"
- using prems by simp
+ using LAnd2 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(P[y\<turnstile>n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LAnd2
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
@@ -1008,7 +1008,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using LAnd2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -1030,15 +1030,15 @@
{ assume asm: "N1\<noteq>Ax x1 c"
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
- using prems
+ using LOr1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using LOr1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x1).N1){c:=(y).P}"
@@ -1048,21 +1048,21 @@
{ assume asm: "N1=Ax x1 c"
have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
- using prems
+ using LOr1
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(M{c:=(y).P}) (x1).(Cut <c>.(Ax x1 c) (y).P)"
- using prems by simp
+ using LOr1 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(P[y\<turnstile>n>x1])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LOr1
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
@@ -1084,7 +1084,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using LOr1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -1106,15 +1106,15 @@
{ assume asm: "N2\<noteq>Ax x2 c"
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
- using prems
+ using LOr2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using LOr2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x2).N2){c:=(y).P}"
@@ -1124,21 +1124,21 @@
{ assume asm: "N2=Ax x2 c"
have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm)
+ using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
- using prems
+ using LOr2
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(M{c:=(y).P}) (x2).(Cut <c>.(Ax x2 c) (y).P)"
- using prems by simp
+ using LOr2 asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(P[y\<turnstile>n>x2])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LOr2
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
@@ -1160,7 +1160,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using LOr2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -1182,15 +1182,15 @@
{ assume asm: "M\<noteq>Ax x c \<and> Q\<noteq>Ax u c"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
- using prems by (simp add: fresh_prod abs_fresh fresh_atm)
+ using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} \<longrightarrow>\<^isub>a*
@@ -1201,21 +1201,21 @@
{ assume asm: "M=Ax x c \<and> Q\<noteq>Ax u c"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
+ using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(Q{c:=(y).P})"
- using prems by simp
+ using LImp asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(P[y\<turnstile>n>x])) (u).(Q{c:=(y).P})"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
@@ -1229,7 +1229,7 @@
next
case False
assume "\<not>fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
@@ -1241,7 +1241,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -1259,21 +1259,21 @@
{ assume asm: "M\<noteq>Ax x c \<and> Q=Ax u c"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
+ using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Cut <c>.Ax u c (y).P)"
- using prems by simp
+ using LImp asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(P[y\<turnstile>n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_starI)
@@ -1284,7 +1284,7 @@
next
case False
assume "\<not>fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
@@ -1295,7 +1295,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
@@ -1311,21 +1311,21 @@
{ assume asm: "M=Ax x c \<and> Q=Ax u c"
have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
- using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
+ using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
- using prems
+ using LImp
apply -
apply(rule a_starI)
apply(rule al_redu)
apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
done
also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(Cut <c>.Ax u c (y).P)"
- using prems by simp
+ using LImp asm by simp
also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(P[y\<turnstile>n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_starI)
@@ -1336,7 +1336,7 @@
next
case False
assume "\<not>fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
@@ -1351,7 +1351,7 @@
proof (cases "fin P y")
case True
assume "fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
@@ -1363,7 +1363,7 @@
next
case False
assume "\<not>fin P y"
- then show ?thesis using prems
+ then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
@@ -1375,7 +1375,7 @@
apply(simp add: subst_with_ax1)
done
qed
- also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
+ also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)