|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
metric_continuity.prf
Sprache: Isabelle
|
|
theory Class2
imports Class1
begin
text \<open>Reduction\<close>
lemma fin_not_Cut:
assumes a: "fin M x"
shows "\(\a M' x N'. M = Cut .M' (x).N')"
using a
by (induct) (auto)
lemma fresh_not_fin:
assumes a: "x\M"
shows "\fin M x"
proof -
have "fin M x \ x\M \ False" by (induct rule: fin.induct) (auto simp add: abs_fresh fresh_atm)
with a show "\fin M x" by blast
qed
lemma fresh_not_fic:
assumes a: "a\M"
shows "\fic M a"
proof -
have "fic M a \ a\M \ False" by (induct rule: fic.induct) (auto simp add: abs_fresh fresh_atm)
with a show "\fic M a" by blast
qed
lemma c_redu_subst1:
assumes a: "M \\<^sub>c M'" "c\M" "y\P"
shows "M{y:=.P} \\<^sub>c M'{y:=.P}"
using a
proof(nominal_induct avoiding: y c P rule: c_redu.strong_induct)
case (left M a N x)
then show ?case
apply -
apply(simp)
apply(rule conjI)
apply(force)
apply(auto)
apply(subgoal_tac "M{a:=(x).N}{y:=.P} = M{y:=.P}{a:=(x).(N{y:=.P})}")(*A*)
apply(simp)
apply(rule c_redu.intros)
apply(rule not_fic_subst1)
apply(simp)
apply(simp add: subst_fresh)
apply(simp add: subst_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(rule subst_subst2)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp)
done
next
case (right N x a M)
then show ?case
apply -
apply(simp)
apply(rule conjI)
(* case M = Ax y a *)
apply(rule impI)
apply(subgoal_tac "N{x:=.Ax y a}{y:=.P} = N{y:=.P}{x:=.P}")
apply(simp)
apply(rule c_redu.right)
apply(rule not_fin_subst2)
apply(simp)
apply(rule subst_fresh)
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
apply(rule sym)
apply(rule interesting_subst1')
apply(simp add: fresh_atm)
apply(simp)
apply(simp)
(* case M \<noteq> Ax y a*)
apply(rule impI)
apply(subgoal_tac "N{x:=.M}{y:=.P} = N{y:=.P}{x:=.(M{y:=.P})}")
apply(simp)
apply(rule c_redu.right)
apply(rule not_fin_subst2)
apply(simp)
apply(simp add: subst_fresh)
apply(simp add: subst_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(rule subst_subst3)
apply(simp_all add: fresh_atm fresh_prod)
done
qed
lemma c_redu_subst2:
assumes a: "M \\<^sub>c M'" "c\P" "y\M"
shows "M{c:=(y).P} \\<^sub>c M'{c:=(y).P}"
using a
proof(nominal_induct avoiding: y c P rule: c_redu.strong_induct)
case (right N x a M)
then show ?case
apply -
apply(simp)
apply(rule conjI)
apply(force)
apply(auto)
apply(subgoal_tac "N{x:=.M}{c:=(y).P} = N{c:=(y).P}{x:=.(M{c:=(y).P})}")(*A*)
apply(simp)
apply(rule c_redu.intros)
apply(rule not_fin_subst1)
apply(simp)
apply(simp add: subst_fresh)
apply(simp add: subst_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(rule subst_subst1)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp)
done
next
case (left M a N x)
then show ?case
apply -
apply(simp)
apply(rule conjI)
(* case N = Ax x c *)
apply(rule impI)
apply(subgoal_tac "M{a:=(x).Ax x c}{c:=(y).P} = M{c:=(y).P}{a:=(y).P}")
apply(simp)
apply(rule c_redu.left)
apply(rule not_fic_subst2)
apply(simp)
apply(simp)
apply(rule subst_fresh)
apply(simp add: abs_fresh)
apply(rule sym)
apply(rule interesting_subst2')
apply(simp add: fresh_atm)
apply(simp)
apply(simp)
(* case M \<noteq> Ax y a*)
apply(rule impI)
apply(subgoal_tac "M{a:=(x).N}{c:=(y).P} = M{c:=(y).P}{a:=(x).(N{c:=(y).P})}")
apply(simp)
apply(rule c_redu.left)
apply(rule not_fic_subst2)
apply(simp)
apply(simp add: subst_fresh)
apply(simp add: subst_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(rule subst_subst4)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_prod fresh_atm)
apply(simp)
done
qed
lemma c_redu_subst1':
assumes a: "M \\<^sub>c M'"
shows "M{y:=.P} \\<^sub>c M'{y:=.P}"
using a
proof -
obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain c'::"coname" where fs2: "c'\<sharp>(M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, blast)
have "M{y:=.P} = ([(y',y)]\M){y':=.([(c',c)]\P)}" using fs1 fs2
apply -
apply(rule trans)
apply(rule_tac y="y'" in subst_rename(3))
apply(simp)
apply(rule subst_rename(4))
apply(simp)
done
also have "\ \\<^sub>c ([(y',y)]\M'){y':=.([(c',c)]\P)}" using fs1 fs2
apply -
apply(rule c_redu_subst1)
apply(simp add: c_redu.eqvt a)
apply(simp_all add: fresh_left calc_atm fresh_prod)
done
also have "\ = M'{y:=.P}" using fs1 fs2
apply -
apply(rule sym)
apply(rule trans)
apply(rule_tac y="y'" in subst_rename(3))
apply(simp)
apply(rule subst_rename(4))
apply(simp)
done
finally show ?thesis by simp
qed
lemma c_redu_subst2':
assumes a: "M \\<^sub>c M'"
shows "M{c:=(y).P} \\<^sub>c M'{c:=(y).P}"
using a
proof -
obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)
obtain c'::"coname" where fs2: "c'\<sharp>(M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, blast)
have "M{c:=(y).P} = ([(c',c)]\M){c':=(y').([(y',y)]\P)}" using fs1 fs2
apply -
apply(rule trans)
apply(rule_tac c="c'" in subst_rename(1))
apply(simp)
apply(rule subst_rename(2))
apply(simp)
done
also have "\ \\<^sub>c ([(c',c)]\M'){c':=(y').([(y',y)]\P)}" using fs1 fs2
apply -
apply(rule c_redu_subst2)
apply(simp add: c_redu.eqvt a)
apply(simp_all add: fresh_left calc_atm fresh_prod)
done
also have "\ = M'{c:=(y).P}" using fs1 fs2
apply -
apply(rule sym)
apply(rule trans)
apply(rule_tac c="c'" in subst_rename(1))
apply(simp)
apply(rule subst_rename(2))
apply(simp)
done
finally show ?thesis by simp
qed
lemma aux1:
assumes a: "M = M'" "M' \\<^sub>l M''"
shows "M \\<^sub>l M''"
using a by simp
lemma aux2:
assumes a: "M \\<^sub>l M'" "M' = M''"
shows "M \\<^sub>l M''"
using a by simp
lemma aux3:
assumes a: "M = M'" "M' \\<^sub>a* M''"
shows "M \\<^sub>a* M''"
using a by simp
lemma aux4:
assumes a: "M = M'"
shows "M \\<^sub>a* M'"
using a by blast
lemma l_redu_subst1:
assumes a: "M \\<^sub>l M'"
shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
proof(nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)
case LAxR
then show ?case
apply -
apply(rule aux3)
apply(rule better_Cut_substn)
apply(simp add: abs_fresh)
apply(simp)
apply(simp add: fresh_atm)
apply(auto)
apply(rule aux4)
apply(simp add: trm.inject alpha calc_atm fresh_atm)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule al_redu)
apply(rule l_redu.intros)
apply(simp add: subst_fresh)
apply(simp add: fresh_atm)
apply(rule fic_subst2)
apply(simp_all)
apply(rule aux4)
apply(rule subst_comm')
apply(simp_all)
done
next
case LAxL
then show ?case
apply -
apply(rule aux3)
apply(rule better_Cut_substn)
apply(simp add: abs_fresh)
apply(simp)
apply(simp add: trm.inject fresh_atm)
apply(auto)
apply(rule aux4)
apply(rule sym)
apply(rule fin_substn_nrename)
apply(simp_all)
apply(rule a_starI)
apply(rule al_redu)
apply(rule aux2)
apply(rule l_redu.intros)
apply(simp add: subst_fresh)
apply(simp add: fresh_atm)
apply(rule fin_subst1)
apply(simp_all)
apply(rule subst_comm')
apply(simp_all)
done
next
case (LNot v M N u a b)
then show ?case
proof -
{ assume asm: "N\Ax y b"
have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} =
(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 "\ \\<^sub>l (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using LNot
by (auto intro: l_redu.intros simp add: subst_fresh)
also have "\ = (Cut .N (u).M){y:=.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 .NotR (u).M a (v).NotL .N v){y:=.P} =
(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 "\ \\<^sub>a* (Cut .(N{y:=.P}) (u).(M{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 "\ = (Cut .(Cut .P (y).Ax y b) (u).(M{y:=.P}))" using LNot asm
by simp
also have "\ \\<^sub>a* (Cut .(P[c\c>b]) (u).(M{y:=.P}))"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LNot
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis
apply -
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .N (u).M){y:=.P}" using LNot asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} \\<^sub>a* (Cut .N (u).M){y:=.P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LAnd1 b a1 M1 a2 M2 N z u)
then show ?case
proof -
{ assume asm: "M1\Ax y a1"
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})"
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 "\ = (Cut .M1 (u).N){y:=.P}" using LAnd1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} \\<^sub>a* (Cut .M1 (u).N){y:=.P}"
by simp
}
moreover
{ assume asm: "M1=Ax y a1"
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})"
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 "\ = Cut .(Cut .P (y). Ax y a1) (u).(N{y:=.P})"
using LAnd1 asm by simp
also have "\ \\<^sub>a* Cut .P[c\c>a1] (u).(N{y:=.P})"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LAnd1
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis
apply -
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .M1 (u).N){y:=.P}" using LAnd1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} \\<^sub>a* (Cut .M1 (u).N){y:=.P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LAnd2 b a1 M1 a2 M2 N z u)
then show ?case
proof -
{ assume asm: "M2\Ax y a2"
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})"
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 "\ = (Cut .M2 (u).N){y:=.P}" using LAnd2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} \\<^sub>a* (Cut .M2 (u).N){y:=.P}"
by simp
}
moreover
{ assume asm: "M2=Ax y a2"
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} =
Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})"
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 "\ = Cut .(Cut .P (y). Ax y a2) (u).(N{y:=.P})"
using LAnd2 asm by simp
also have "\ \\<^sub>a* Cut .P[c\c>a2] (u).(N{y:=.P})"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LAnd2 asm
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis
apply -
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .M2 (u).N){y:=.P}" using LAnd2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} \\<^sub>a* (Cut .M2 (u).N){y:=.P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LOr1 b a M N1 N2 z x1 x2 y c P)
then show ?case
proof -
{ assume asm: "M\Ax y a"
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})"
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 "\ = (Cut .M (x1).N1){y:=.P}" using LOr1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x1).N1){y:=.P}"
by simp
}
moreover
{ assume asm: "M=Ax y a"
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})"
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 "\ = Cut .(Cut .P (y). Ax y a) (x1).(N1{y:=.P})"
using LOr1 asm by simp
also have "\ \\<^sub>a* Cut .P[c\c>a] (x1).(N1{y:=.P})"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LOr1
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis
apply -
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .M (x1).N1){y:=.P}" using LOr1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x1).N1){y:=.P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LOr2 b a M N1 N2 z x1 x2 y c P)
then show ?case
proof -
{ assume asm: "M\Ax y a"
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})"
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 "\ = (Cut .M (x2).N2){y:=.P}" using LOr2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x2).N2){y:=.P}"
by simp
}
moreover
{ assume asm: "M=Ax y a"
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})"
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 "\ = Cut .(Cut .P (y). Ax y a) (x2).(N2{y:=.P})"
using LOr2 asm by simp
also have "\ \\<^sub>a* Cut .P[c\c>a] (x2).(N2{y:=.P})"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LOr2
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis
apply -
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .M (x2).N2){y:=.P}" using LOr2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x2).N2){y:=.P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LImp z N u Q x M b a d y c P)
then show ?case
proof -
{ assume asm: "N\Ax y d"
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.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 LImp by (simp add: fresh_prod abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})"
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 "\ = (Cut .(Cut .N (x).M) (u).Q){y:=.P}" using LImp asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}"
by simp
}
moreover
{ assume asm: "N=Ax y d"
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.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 LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\ \\<^sub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})"
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 "\ = Cut .(Cut .(Cut .P (y).Ax y d) (x).(M{y:=.P})) (u).(Q{y:=.P})"
using LImp asm by simp
also have "\ \\<^sub>a* Cut .(Cut .(P[c\c>d]) (x).(M{y:=.P})) (u).(Q{y:=.P})"
proof (cases "fic P c")
case True
assume "fic P c"
then show ?thesis using LImp
apply -
apply(rule a_starI)
apply(rule better_CutL_intro)
apply(rule a_Cut_l)
apply(simp add: subst_fresh abs_fresh)
apply(simp add: abs_fresh fresh_atm)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
done
next
case False
assume "\fic P c"
then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutL)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(simp add: subst_with_ax2)
done
qed
also have "\ = (Cut .(Cut .N (x).M) (u).Q){y:=.P}" using LImp asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(simp add: trm.inject)
apply(simp add: alpha)
apply(rule sym)
apply(rule crename_swap)
apply(simp)
done
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}"
by simp
}
ultimately show ?thesis by blast
qed
qed
lemma l_redu_subst2:
assumes a: "M \\<^sub>l M'"
shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
proof(nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)
case LAxR
then show ?case
apply -
apply(rule aux3)
apply(rule better_Cut_substc)
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
apply(simp add: trm.inject fresh_atm)
apply(auto)
apply(rule aux4)
apply(rule sym)
apply(rule fic_substc_crename)
apply(simp_all)
apply(rule a_starI)
apply(rule al_redu)
apply(rule aux2)
apply(rule l_redu.intros)
apply(simp add: subst_fresh)
apply(simp add: fresh_atm)
apply(rule fic_subst1)
apply(simp_all)
apply(rule subst_comm')
apply(simp_all)
done
next
case LAxL
then show ?case
apply -
apply(rule aux3)
apply(rule better_Cut_substc)
apply(simp)
apply(simp add: abs_fresh)
apply(simp add: fresh_atm)
apply(auto)
apply(rule aux4)
apply(simp add: trm.inject alpha calc_atm fresh_atm)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule al_redu)
apply(rule l_redu.intros)
apply(simp add: subst_fresh)
apply(simp add: fresh_atm)
apply(rule fin_subst2)
apply(simp_all)
apply(rule aux4)
apply(rule subst_comm')
apply(simp_all)
done
next
case (LNot v M N u a b)
then show ?case
proof -
{ assume asm: "M\Ax u c"
have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} =
(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 "\ \\<^sub>l (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
by (auto intro: l_redu.intros simp add: subst_fresh)
also have "\ = (Cut .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 .NotR (u).M a (v).NotL .N v){c:=(y).P} =
(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 "\ \\<^sub>a* (Cut .(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 "\ = (Cut .(N{c:=(y).P}) (u).(Cut .(Ax u c) (y).P))" using LNot asm
by simp
also have "\ \\<^sub>a* (Cut .(N{c:=(y).P}) (u).(P[y\n>u]))"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LNot
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .N (u).M){c:=(y).P}" using LNot asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule nrename_swap)
apply(simp)
done
finally have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} \\<^sub>a* (Cut .N (u).M){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LAnd1 b a1 M1 a2 M2 N z u)
then show ?case
proof -
{ assume asm: "N\Ax u c"
have "(Cut .AndR .M1 .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 LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})"
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 "\ = (Cut .M1 (u).N){c:=(y).P}" using LAnd1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M1 (u).N){c:=(y).P}"
by simp
}
moreover
{ assume asm: "N=Ax u c"
have "(Cut .AndR .M1 .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 LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})"
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 "\ = Cut .(M1{c:=(y).P}) (u).(Cut .(Ax u c) (y).P)"
using LAnd1 asm by simp
also have "\ \\<^sub>a* Cut .(M1{c:=(y).P}) (u).(P[y\n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LAnd1
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .M1 (u).N){c:=(y).P}" using LAnd1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule nrename_swap)
apply(simp)
done
finally
have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M1 (u).N){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LAnd2 b a1 M1 a2 M2 N z u)
then show ?case
proof -
{ assume asm: "N\Ax u c"
have "(Cut .AndR .M1 .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 LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})"
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 "\ = (Cut .M2 (u).N){c:=(y).P}" using LAnd2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M2 (u).N){c:=(y).P}"
by simp
}
moreover
{ assume asm: "N=Ax u c"
have "(Cut .AndR .M1 .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 LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})"
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 "\ = Cut .(M2{c:=(y).P}) (u).(Cut .(Ax u c) (y).P)"
using LAnd2 asm by simp
also have "\ \\<^sub>a* Cut .(M2{c:=(y).P}) (u).(P[y\n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LAnd2
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .M2 (u).N){c:=(y).P}" using LAnd2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule nrename_swap)
apply(simp)
done
finally
have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M2 (u).N){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LOr1 b a M N1 N2 z x1 x2 y c P)
then show ?case
proof -
{ assume asm: "N1\Ax x1 c"
have "(Cut .OrR1 .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 LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
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 "\ = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x1).N1){c:=(y).P}"
by simp
}
moreover
{ assume asm: "N1=Ax x1 c"
have "(Cut .OrR1 .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 LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
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 "\ = Cut .(M{c:=(y).P}) (x1).(Cut .(Ax x1 c) (y).P)"
using LOr1 asm by simp
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x1).(P[y\n>x1])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LOr1
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule nrename_swap)
apply(simp)
done
finally
have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x1).N1){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LOr2 b a M N1 N2 z x1 x2 y c P)
then show ?case
proof -
{ assume asm: "N2\Ax x2 c"
have "(Cut .OrR2 .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 LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
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 "\ = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x2).N2){c:=(y).P}"
by simp
}
moreover
{ assume asm: "N2=Ax x2 c"
have "(Cut .OrR2 .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 LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
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 "\ = Cut .(M{c:=(y).P}) (x2).(Cut .(Ax x2 c) (y).P)"
using LOr2 asm by simp
also have "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x2).(P[y\n>x2])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LOr2
apply -
apply(rule a_starI)
apply(rule better_CutR_intro)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asm
apply -
apply(auto simp add: subst_fresh abs_fresh)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(rule sym)
apply(rule nrename_swap)
apply(simp)
done
finally
have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x2).N2){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
next
case (LImp z N u Q x M b a d y c P)
then show ?case
proof -
{ assume asm: "M\Ax x c \ Q\Ax u c"
have "(Cut .ImpR (x)..M b (z).ImpL .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 LImp by (simp add: fresh_prod abs_fresh fresh_atm)
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
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 "\ = (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" using LImp asm
by (simp add: subst_fresh abs_fresh fresh_atm)
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
by simp
}
moreover
{ assume asm: "M=Ax x c \ Q\Ax u c"
have "(Cut .ImpR (x)..M b (z).ImpL .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 LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
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 "\ = Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(Q{c:=(y).P})"
using LImp asm by simp
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(P[y\n>x])) (u).(Q{c:=(y).P})"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .(Cut .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)
apply(simp add: alpha fresh_atm)
apply(simp add: trm.inject)
apply(simp add: alpha)
apply(simp add: nrename_swap)
done
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
by simp
}
moreover
{ assume asm: "M\Ax x c \ Q=Ax u c"
have "(Cut .ImpR (x)..M b (z).ImpL .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 LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
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 "\ = Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Cut .Ax u c (y).P)"
using LImp asm by simp
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(P[y\n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .(Cut .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)
apply(simp add: alpha fresh_atm)
apply(simp add: nrename_swap)
done
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
by simp
}
moreover
{ assume asm: "M=Ax x c \ Q=Ax u c"
have "(Cut .ImpR (x)..M b (z).ImpL .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 LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
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 "\ = Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(Cut .Ax u c (y).P)"
using LImp asm by simp
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(P[y\n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(P[y\n>x])) (u).(P[y\n>u])"
proof (cases "fin P y")
case True
assume "fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
done
next
case False
assume "\fin P y"
then show ?thesis using LImp
apply -
apply(rule a_star_CutL)
apply(rule a_star_CutR)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(simp add: subst_with_ax1)
done
qed
also have "\ = (Cut .(Cut .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)
apply(rule conjI)
apply(simp add: alpha fresh_atm trm.inject)
apply(simp add: nrename_swap)
apply(simp add: alpha fresh_atm trm.inject)
apply(simp add: nrename_swap)
done
finally
have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} \\<^sub>a*
(Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
by simp
}
ultimately show ?thesis by blast
qed
qed
lemma a_redu_subst1:
assumes a: "M \\<^sub>a M'"
shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
proof(nominal_induct avoiding: y c P rule: a_redu.strong_induct)
case al_redu
then show ?case by (simp only: l_redu_subst1)
next
case ac_redu
then show ?case
apply -
apply(rule a_starI)
apply(rule a_redu.ac_redu)
apply(simp only: c_redu_subst1')
done
next
case (a_Cut_l a N x M M' y c P)
then show ?case
apply(simp add: subst_fresh fresh_a_redu)
apply(rule conjI)
apply(rule impI)+
apply(simp)
apply(drule ax_do_not_a_reduce)
apply(simp)
apply(rule impI)
apply(rule conjI)
apply(rule impI)
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="P" in meta_spec)
apply(simp)
apply(rule a_star_trans)
apply(rule a_star_CutL)
apply(assumption)
apply(rule a_star_trans)
apply(rule_tac M'="P[c\c>a]" in a_star_CutL)
apply(case_tac "fic P c")
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxR_intro)
apply(simp)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_left)
apply(simp)
apply(rule subst_with_ax2)
apply(rule aux4)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(simp add: crename_swap)
apply(rule impI)
apply(rule a_star_CutL)
apply(auto)
done
next
case (a_Cut_r a N x M M' y c P)
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_CutR)
apply(auto)[1]
apply(rule a_star_CutR)
apply(auto)[1]
done
next
case a_NotL
then show ?case
apply(auto)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_NotL)
apply(auto)[1]
apply(rule a_star_NotL)
apply(auto)[1]
done
next
case a_NotR
then show ?case
apply(auto)
apply(rule a_star_NotR)
apply(auto)[1]
done
next
case a_AndR_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_AndR)
apply(auto)
done
next
case a_AndR_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_AndR)
apply(auto)
done
next
case a_AndL1
then show ?case
apply(auto)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_AndL1)
apply(auto)[1]
apply(rule a_star_AndL1)
apply(auto)[1]
done
next
case a_AndL2
then show ?case
apply(auto)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_AndL2)
apply(auto)[1]
apply(rule a_star_AndL2)
apply(auto)[1]
done
next
case a_OrR1
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_OrR1)
apply(auto)
done
next
case a_OrR2
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_OrR2)
apply(auto)
done
next
case a_OrL_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_OrL)
apply(auto)
apply(rule a_star_OrL)
apply(auto)
done
next
case a_OrL_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_OrL)
apply(auto)
apply(rule a_star_OrL)
apply(auto)
done
next
case a_ImpR
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_ImpR)
apply(auto)
done
next
case a_ImpL_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_ImpL)
apply(auto)
apply(rule a_star_ImpL)
apply(auto)
done
next
case a_ImpL_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "name")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutR)
apply(rule a_star_ImpL)
apply(auto)
apply(rule a_star_ImpL)
apply(auto)
done
qed
lemma a_redu_subst2:
assumes a: "M \\<^sub>a M'"
shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
proof(nominal_induct avoiding: y c P rule: a_redu.strong_induct)
case al_redu
then show ?case by (simp only: l_redu_subst2)
next
case ac_redu
then show ?case
apply -
apply(rule a_starI)
apply(rule a_redu.ac_redu)
apply(simp only: c_redu_subst2')
done
next
case (a_Cut_r a N x M M' y c P)
then show ?case
apply(simp add: subst_fresh fresh_a_redu)
apply(rule conjI)
apply(rule impI)+
apply(simp)
apply(drule ax_do_not_a_reduce)
apply(simp)
apply(rule impI)
apply(rule conjI)
apply(rule impI)
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="P" in meta_spec)
apply(simp)
apply(rule a_star_trans)
apply(rule a_star_CutR)
apply(assumption)
apply(rule a_star_trans)
apply(rule_tac N'="P[y\n>x]" in a_star_CutR)
apply(case_tac "fin P y")
apply(rule a_starI)
apply(rule al_redu)
apply(rule better_LAxL_intro)
apply(simp)
apply(rule a_star_trans)
apply(rule a_starI)
apply(rule ac_redu)
apply(rule better_right)
apply(simp)
apply(rule subst_with_ax1)
apply(rule aux4)
apply(simp add: trm.inject)
apply(simp add: alpha fresh_atm)
apply(simp add: nrename_swap)
apply(rule impI)
apply(rule a_star_CutR)
apply(auto)
done
next
case (a_Cut_l a N x M M' y c P)
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_CutL)
apply(auto)[1]
apply(rule a_star_CutL)
apply(auto)[1]
done
next
case a_NotR
then show ?case
apply(auto)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_NotR)
apply(auto)[1]
apply(rule a_star_NotR)
apply(auto)[1]
done
next
case a_NotL
then show ?case
apply(auto)
apply(rule a_star_NotL)
apply(auto)[1]
done
next
case a_AndR_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_AndR)
apply(auto)
apply(rule a_star_AndR)
apply(auto)
done
next
case a_AndR_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_AndR)
apply(auto)
apply(rule a_star_AndR)
apply(auto)
done
next
case a_AndL1
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_AndL1)
apply(auto)
done
next
case a_AndL2
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_AndL2)
apply(auto)
done
next
case a_OrR1
then show ?case
apply(auto)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_OrR1)
apply(auto)[1]
apply(rule a_star_OrR1)
apply(auto)[1]
done
next
case a_OrR2
then show ?case
apply(auto)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_OrR2)
apply(auto)[1]
apply(rule a_star_OrR2)
apply(auto)[1]
done
next
case a_OrL_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_OrL)
apply(auto)
done
next
case a_OrL_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_OrL)
apply(auto)
done
next
case a_ImpR
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
apply(simp add: subst_fresh)
apply(rule a_star_CutL)
apply(rule a_star_ImpR)
apply(auto)
apply(rule a_star_ImpR)
apply(auto)
done
next
case a_ImpL_l
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_ImpL)
apply(auto)
done
next
case a_ImpL_r
then show ?case
apply(auto simp add: subst_fresh fresh_a_redu)
apply(rule a_star_ImpL)
apply(auto)
done
qed
lemma a_star_subst1:
assumes a: "M \\<^sub>a* M'"
shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
apply(induct)
apply(blast)
apply(drule_tac y="y" and c="c" and P="P" in a_redu_subst1)
apply(auto)
done
lemma a_star_subst2:
assumes a: "M \\<^sub>a* M'"
shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
apply(induct)
apply(blast)
apply(drule_tac y="y" and c="c" and P="P" in a_redu_subst2)
apply(auto)
done
text \<open>Candidates and SN\<close>
text \<open>SNa\<close>
inductive
SNa :: "trm \ bool"
where
SNaI: "(\M'. M \\<^sub>a M' \ SNa M') \ SNa M"
lemma SNa_induct[consumes 1]:
assumes major: "SNa M"
assumes hyp: "\M'. SNa M' \ (\M''. M'\\<^sub>a M'' \ P M'' \ P M')"
shows "P M"
apply (rule major[THEN SNa.induct])
apply (rule hyp)
apply (rule SNaI)
apply (blast)+
done
lemma double_SNa_aux:
assumes a_SNa: "SNa a"
and b_SNa: "SNa b"
and hyp: "\x z.
(\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> SNa y) \<Longrightarrow>
(\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> P y z) \<Longrightarrow>
(\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> SNa u) \<Longrightarrow>
(\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> P x u) \<Longrightarrow> P x z"
shows "P a b"
proof -
from a_SNa
have r: "\b. SNa b \ P a b"
proof (induct a rule: SNa.induct)
case (SNaI x)
note SNa' = this
have "SNa b" by fact
thus ?case
proof (induct b rule: SNa.induct)
case (SNaI y)
show ?case
apply (rule hyp)
apply (erule SNa')
apply (erule SNa')
apply (rule SNa.SNaI)
apply (erule SNaI)+
done
qed
qed
from b_SNa show ?thesis by (rule r)
qed
lemma double_SNa:
"\SNa a; SNa b; \x z. ((\y. x\\<^sub>ay \ P y z) \ (\u. z\\<^sub>a u \ P x u)) \ P x z\ \ P a b"
apply(rule_tac double_SNa_aux)
apply(assumption)+
apply(blast)
done
lemma a_preserves_SNa:
assumes a: "SNa M" "M\\<^sub>a M'"
shows "SNa M'"
using a
by (erule_tac SNa.cases) (simp)
lemma a_star_preserves_SNa:
assumes a: "SNa M" and b: "M\\<^sub>a* M'"
shows "SNa M'"
using b a
by (induct) (auto simp add: a_preserves_SNa)
lemma Ax_in_SNa:
shows "SNa (Ax x a)"
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
done
lemma NotL_in_SNa:
assumes a: "SNa M"
shows "SNa (NotL .M x)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(a,aa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(subgoal_tac "NotL .([(a,aa)]\M'a) x = NotL .M'a x")
apply(simp)
apply(simp add: trm.inject alpha fresh_a_redu)
done
lemma NotR_in_SNa:
assumes a: "SNa M"
shows "SNa (NotR (x).M a)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(x,xa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="NotR (x).([(x,xa)]\M'a) a" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
done
lemma AndL1_in_SNa:
assumes a: "SNa M"
shows "SNa (AndL1 (x).M y)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(x,xa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="AndL1 x.([(x,xa)]\M'a) y" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
done
lemma AndL2_in_SNa:
assumes a: "SNa M"
shows "SNa (AndL2 (x).M y)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(x,xa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="AndL2 x.([(x,xa)]\M'a) y" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
done
lemma OrR1_in_SNa:
assumes a: "SNa M"
shows "SNa (OrR1 .M b)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(a,aa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="OrR1 .([(a,aa)]\M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
done
lemma OrR2_in_SNa:
assumes a: "SNa M"
shows "SNa (OrR2 .M b)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha)
apply(rotate_tac 1)
apply(drule_tac x="[(a,aa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="OrR2 .([(a,aa)]\M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
done
lemma ImpR_in_SNa:
assumes a: "SNa M"
shows "SNa (ImpR (x)..M b)"
using a
apply(induct)
apply(rule SNaI)
apply(erule a_redu.cases, auto)
apply(erule l_redu.cases, auto)
apply(erule c_redu.cases, auto)
apply(auto simp add: trm.inject alpha abs_fresh abs_perm calc_atm)
apply(rotate_tac 1)
apply(drule_tac x="[(a,aa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="ImpR (x)..([(a,aa)]\M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu)
apply(simp)
apply(rotate_tac 1)
apply(drule_tac x="[(x,xa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="ImpR (x)..([(x,xa)]\M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm)
apply(simp)
apply(rotate_tac 1)
apply(drule_tac x="[(a,aa)]\[(x,xa)]\M'a" in meta_spec)
apply(simp add: a_redu.eqvt)
apply(rule_tac s="ImpR (x)..([(a,aa)]\[(x,xa)]\M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm)
apply(simp add: fresh_left calc_atm fresh_a_redu)
apply(simp)
done
lemma AndR_in_SNa:
assumes a: "SNa M" "SNa N"
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.68Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
