diff -r 92011cc923f5 -r 9be4ab2acc13 src/HOL/Nominal/Examples/Class2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/Class2.thy Thu Apr 22 22:01:06 2010 +0200 @@ -0,0 +1,6069 @@ +theory Class2 +imports Class1 +begin + +text {* Reduction *} + +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 \\<^isub>c M'" "c\M" "y\P" + shows "M{y:=.P} \\<^isub>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 \ 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 \\<^isub>c M'" "c\P" "y\M" + shows "M{c:=(y).P} \\<^isub>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 \ 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 \\<^isub>c M'" + shows "M{y:=.P} \\<^isub>c M'{y:=.P}" +using a +proof - + obtain y'::"name" where fs1: "y'\(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast) + obtain c'::"coname" where fs2: "c'\(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 "\ \\<^isub>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 \\<^isub>c M'" + shows "M{c:=(y).P} \\<^isub>c M'{c:=(y).P}" +using a +proof - + obtain y'::"name" where fs1: "y'\(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast) + obtain c'::"coname" where fs2: "c'\(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 "\ \\<^isub>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' \\<^isub>l M''" + shows "M \\<^isub>l M''" +using a by simp + +lemma aux2: + assumes a: "M \\<^isub>l M'" "M' = M''" + shows "M \\<^isub>l M''" +using a by simp + +lemma aux3: + assumes a: "M = M'" "M' \\<^isub>a* M''" + shows "M \\<^isub>a* M''" +using a by simp + +lemma aux4: + assumes a: "M = M'" + shows "M \\<^isub>a* M'" +using a by blast + +lemma l_redu_subst1: + assumes a: "M \\<^isub>l M'" + shows "M{y:=.P} \\<^isub>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 .NotR (u).(M{y:=.P}) a (v).NotL .(N{y:=.P}) v)" using prems + by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>l (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using prems + by (auto intro: l_redu.intros simp add: subst_fresh) + also have "\ = (Cut .N (u).M){y:=.P}" using prems + 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 .NotR (u).(M{y:=.P}) a (v).NotL .(N{y:=.P}) v)" using prems + by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using prems + 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 prems + by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL1 (u).(N{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} \\<^isub>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 .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL1 (u).(N{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL2 (u).(N{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} \\<^isub>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 .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL2 (u).(N{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .OrR1 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^isub>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 .OrR1 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .OrR2 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^isub>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 .OrR2 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .ImpR (x)..(M{y:=.P}) b (z).ImpL .(N{y:=.P}) (u).(Q{y:=.P}) z" + using prems by (simp add: fresh_prod abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} \\<^isub>a* + (Cut .(Cut .N (x).M) (u).Q){y:=.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 .ImpR (x)..(M{y:=.P}) b (z).ImpL .(N{y:=.P}) (u).(Q{y:=.P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) + also have "\ \\<^isub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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 prems + 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} \\<^isub>a* + (Cut .(Cut .N (x).M) (u).Q){y:=.P}" + by simp + } + ultimately show ?thesis by blast + qed +qed + +lemma l_redu_subst2: + assumes a: "M \\<^isub>l M'" + shows "M{c:=(y).P} \\<^isub>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 .NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using prems + by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>l (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems + by (auto intro: l_redu.intros simp add: subst_fresh) + also have "\ = (Cut .N (u).M){c:=(y).P}" using prems + 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 .NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using prems + by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems + 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 prems + by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} \\<^isub>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 .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})" + using prems + 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 prems + by (simp add: subst_fresh abs_fresh fresh_atm) + finally + have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} \\<^isub>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 .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .OrR1 .(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) + also have "\ \\<^isub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" + using prems + 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 prems + 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} \\<^isub>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 .OrR1 .(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) + also have "\ \\<^isub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .OrR2 .(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) + also have "\ \\<^isub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" + using prems + 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 prems + 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} \\<^isub>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 .OrR2 .(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) + also have "\ \\<^isub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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} \\<^isub>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 .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" + using prems by (simp add: fresh_prod abs_fresh fresh_atm) + also have "\ \\<^isub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" + using prems + 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 prems + 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} \\<^isub>a* + (Cut .(Cut .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 .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) + also have "\ \\<^isub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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 prems + 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} \\<^isub>a* + (Cut .(Cut .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 .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) + also have "\ \\<^isub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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 prems + 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} \\<^isub>a* + (Cut .(Cut .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 .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" + using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) + also have "\ \\<^isub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" + using prems + 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 prems by simp + also have "\ \\<^isub>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 prems + 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 prems + 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 "\ \\<^isub>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 prems + 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 prems + 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 prems + 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} \\<^isub>a* + (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" + by simp + } + ultimately show ?thesis by blast + qed +qed + +lemma a_redu_subst1: + assumes a: "M \\<^isub>a M'" + shows "M{y:=.P} \\<^isub>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 \\<^isub>a M'" + shows "M{c:=(y).P} \\<^isub>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 \\<^isub>a* M'" + shows "M{y:=.P} \\<^isub>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 \\<^isub>a* M'" + shows "M{c:=(y).P} \\<^isub>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 {* Candidates and SN *} + +text {* SNa *} + +inductive + SNa :: "trm \ bool" +where + SNaI: "(\M'. M \\<^isub>a M' \ SNa M') \ SNa M" + +lemma SNa_induct[consumes 1]: + assumes major: "SNa M" + assumes hyp: "\M'. SNa M' \ (\M''. M'\\<^isub>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. + (\y. x\\<^isub>a y \ SNa y) \ + (\y. x\\<^isub>a y \ P y z) \ + (\u. z\\<^isub>a u \ SNa u) \ + (\u. z\\<^isub>a u \ P x u) \ 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\\<^isub>ay \ P y z) \ (\u. z\\<^isub>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\\<^isub>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\\<^isub>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" + shows "SNa (AndR .M .N c)" +apply(rule_tac a="M" and b="N" in double_SNa) +apply(rule a)+ +apply(auto) +apply(rule SNaI) +apply(drule a_redu_AndR_elim) +apply(auto) +done + +lemma OrL_in_SNa: + assumes a: "SNa M" "SNa N" + shows "SNa (OrL (x).M (y).N z)" +apply(rule_tac a="M" and b="N" in double_SNa) +apply(rule a)+ +apply(auto) +apply(rule SNaI) +apply(drule a_redu_OrL_elim) +apply(auto) +done + +lemma ImpL_in_SNa: + assumes a: "SNa M" "SNa N" + shows "SNa (ImpL .M (y).N z)" +apply(rule_tac a="M" and b="N" in double_SNa) +apply(rule a)+ +apply(auto) +apply(rule SNaI) +apply(drule a_redu_ImpL_elim) +apply(auto) +done + +lemma SNa_eqvt: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "SNa M \ SNa (pi1\M)" + and "SNa M \ SNa (pi2\M)" +apply - +apply(induct rule: SNa.induct) +apply(rule SNaI) +apply(drule_tac pi="(rev pi1)" in a_redu.eqvt(1)) +apply(rotate_tac 1) +apply(drule_tac x="(rev pi1)\M'" in meta_spec) +apply(perm_simp) +apply(induct rule: SNa.induct) +apply(rule SNaI) +apply(drule_tac pi="(rev pi2)" in a_redu.eqvt(2)) +apply(rotate_tac 1) +apply(drule_tac x="(rev pi2)\M'" in meta_spec) +apply(perm_simp) +done + +text {* set operators *} + +definition AXIOMSn :: "ty \ ntrm set" where + "AXIOMSn B \ { (x):(Ax y b) | x y b. True }" + +definition AXIOMSc::"ty \ ctrm set" where + "AXIOMSc B \ { :(Ax y b) | a y b. True }" + +definition BINDINGn::"ty \ ctrm set \ ntrm set" where + "BINDINGn B X \ { (x):M | x M. \a P. :P\X \ SNa (M{x:=.P})}" + +definition BINDINGc::"ty \ ntrm set \ ctrm set" where + "BINDINGc B X \ { :M | a M. \x P. (x):P\X \ SNa (M{a:=(x).P})}" + +lemma BINDINGn_decreasing: + shows "X\Y \ BINDINGn B Y \ BINDINGn B X" +by (simp add: BINDINGn_def) (blast) + +lemma BINDINGc_decreasing: + shows "X\Y \ BINDINGc B Y \ BINDINGc B X" +by (simp add: BINDINGc_def) (blast) + +nominal_primrec + NOTRIGHT :: "ty \ ntrm set \ ctrm set" +where + "NOTRIGHT (NOT B) X = { :NotR (x).M a | a x M. fic (NotR (x).M a) a \ (x):M \ X }" +apply(rule TrueI)+ +done + +lemma NOTRIGHT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(1)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\(:NotR (xa).M a)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma NOTRIGHT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(2)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="<((rev pi)\a)>:NotR ((rev pi)\xa).((rev pi)\M) ((rev pi)\a)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +nominal_primrec + NOTLEFT :: "ty \ ctrm set \ ntrm set" +where + "NOTLEFT (NOT B) X = { (x):NotL .M x | a x M. fin (NotL .M x) x \ :M \ X }" +apply(rule TrueI)+ +done + +lemma NOTLEFT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(1)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x="(((rev pi)\xa)):NotL <((rev pi)\a)>.((rev pi)\M) ((rev pi)\xa)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma NOTLEFT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(2)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x="(((rev pi)\xa)):NotL <((rev pi)\a)>.((rev pi)\M) ((rev pi)\xa)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +nominal_primrec + ANDRIGHT :: "ty \ ctrm set \ ctrm set \ ctrm set" +where + "ANDRIGHT (B AND C) X Y = + { :AndR .M .N c | c a b M N. fic (AndR .M .N c) c \ :M \ X \ :N \ Y }" +apply(rule TrueI)+ +done + +lemma ANDRIGHT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\c" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(1)) +apply(simp) +apply(rule conjI) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x=":N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\(:AndR .M .N c)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\c" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma ANDRIGHT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\c" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(2)) +apply(simp) +apply(rule conjI) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x=":N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\(:AndR .M .N c)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\c" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fic.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp) +done + +nominal_primrec + ANDLEFT1 :: "ty \ ntrm set \ ntrm set" +where + "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y \ (x):M \ X }" +apply(rule TrueI)+ +done + +lemma ANDLEFT1_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(1)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):AndL1 (xa).M y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fin.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +done + +lemma ANDLEFT1_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(2)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):AndL1 (xa).M y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +nominal_primrec + ANDLEFT2 :: "ty \ ntrm set \ ntrm set" +where + "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y \ (x):M \ X }" +apply(rule TrueI)+ +done + +lemma ANDLEFT2_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(1)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):AndL2 (xa).M y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fin.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +done + +lemma ANDLEFT2_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(2)) +apply(simp) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):AndL2 (xa).M y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +nominal_primrec + ORLEFT :: "ty \ ntrm set \ ntrm set \ ntrm set" +where + "ORLEFT (B OR C) X Y = + { (z):OrL (x).M (y).N z | x y z M N. fin (OrL (x).M (y).N z) z \ (x):M \ X \ (y):N \ Y }" +apply(rule TrueI)+ +done + +lemma ORLEFT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\z" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(1)) +apply(simp) +apply(rule conjI) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(y):N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((z):OrL (xa).M (y).N z)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\z" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fin.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +done + +lemma ORLEFT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\z" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(2)) +apply(simp) +apply(rule conjI) +apply(rule_tac x="(xb):M" in exI) +apply(simp) +apply(rule_tac x="(y):N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((z):OrL (xa).M (y).N z)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\z" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +nominal_primrec + ORRIGHT1 :: "ty \ ctrm set \ ctrm set" +where + "ORRIGHT1 (B OR C) X = { :OrR1 .M b | a b M. fic (OrR1 .M b) b \ :M \ X }" +apply(rule TrueI)+ +done + +lemma ORRIGHT1_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(1)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\(:OrR1 .M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma ORRIGHT1_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(2)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\(:OrR1 .M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fic.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp) +done + +nominal_primrec + ORRIGHT2 :: "ty \ ctrm set \ ctrm set" +where + "ORRIGHT2 (B OR C) X = { :OrR2 .M b | a b M. fic (OrR2 .M b) b \ :M \ X }" +apply(rule TrueI)+ +done + +lemma ORRIGHT2_eqvt_name: + fixes pi::"name prm" + shows "(pi\(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(1)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\(:OrR2 .M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma ORRIGHT2_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\X)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(2)) +apply(simp) +apply(rule_tac x=":M" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\(:OrR2 .M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp) +apply(drule_tac pi="rev pi" in fic.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp) +done + +nominal_primrec + IMPRIGHT :: "ty \ ntrm set \ ctrm set \ ntrm set \ ctrm set \ ctrm set" +where + "IMPRIGHT (B IMP C) X Y Z U= + { :ImpR (x)..M b | x a b M. fic (ImpR (x)..M b) b + \ (\z P. x\(z,P) \ (z):P \ Z \ (x):(M{a:=(z).P}) \ X) + \ (\c Q. a\(c,Q) \ :Q \ U \ :(M{x:=.Q}) \ Y)}" +apply(rule TrueI)+ +done + +lemma IMPRIGHT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\X) (pi\Y) (pi\Z) (pi\U)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(1)) +apply(simp) +apply(rule conjI) +apply(auto)[1] +apply(rule_tac x="(xb):(M{a:=((rev pi)\z).((rev pi)\P)})" in exI) +apply(perm_simp add: csubst_eqvt) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +apply(simp add: fresh_right) +apply(auto)[1] +apply(rule_tac x=":(M{xb:=<((rev pi)\c)>.((rev pi)\Q)})" in exI) +apply(perm_simp add: nsubst_eqvt) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps fresh_left) +apply(rule_tac x="(rev pi)\(:ImpR xa..M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(1)) +apply(simp add: swap_simps) +apply(rule conjI) +apply(auto)[1] +apply(drule_tac x="pi\z" in spec) +apply(drule_tac x="pi\P" in spec) +apply(drule mp) +apply(simp add: fresh_right) +apply(rule_tac x="(z):P" in exI) +apply(simp) +apply(auto)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: csubst_eqvt fresh_right) +apply(auto)[1] +apply(drule_tac x="pi\c" in spec) +apply(drule_tac x="pi\Q" in spec) +apply(drule mp) +apply(simp add: swap_simps fresh_left) +apply(rule_tac x=":Q" in exI) +apply(simp add: swap_simps) +apply(auto)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: nsubst_eqvt) +done + +lemma IMPRIGHT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\X) (pi\Y) (pi\Z) (pi\U)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\b" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fic.eqvt(2)) +apply(simp) +apply(rule conjI) +apply(auto)[1] +apply(rule_tac x="(xb):(M{a:=((rev pi)\z).((rev pi)\P)})" in exI) +apply(perm_simp add: csubst_eqvt) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps fresh_left) +apply(auto)[1] +apply(rule_tac x=":(M{xb:=<((rev pi)\c)>.((rev pi)\Q)})" in exI) +apply(perm_simp add: nsubst_eqvt) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: fresh_right) +apply(rule_tac x="(rev pi)\(:ImpR xa..M b)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\b" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fic.eqvt(2)) +apply(simp add: swap_simps) +apply(rule conjI) +apply(auto)[1] +apply(drule_tac x="pi\z" in spec) +apply(drule_tac x="pi\P" in spec) +apply(simp add: swap_simps fresh_left) +apply(drule mp) +apply(rule_tac x="(z):P" in exI) +apply(simp add: swap_simps) +apply(auto)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: csubst_eqvt fresh_right) +apply(auto)[1] +apply(drule_tac x="pi\c" in spec) +apply(drule_tac x="pi\Q" in spec) +apply(simp add: fresh_right) +apply(drule mp) +apply(rule_tac x=":Q" in exI) +apply(simp) +apply(auto)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: nsubst_eqvt fresh_right) +done + +nominal_primrec + IMPLEFT :: "ty \ ctrm set \ ntrm set \ ntrm set" +where + "IMPLEFT (B IMP C) X Y = + { (y):ImpL .M (x).N y | x a y M N. fin (ImpL .M (x).N y) y \ :M \ X \ (x):N \ Y }" +apply(rule TrueI)+ +done + +lemma IMPLEFT_eqvt_name: + fixes pi::"name prm" + shows "(pi\(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(1)) +apply(simp) +apply(rule conjI) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x="(xb):N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):ImpL .M (xa).N y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(1)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: swap_simps) +done + +lemma IMPLEFT_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\X) (pi\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\M" in exI) +apply(rule_tac x="pi\N" in exI) +apply(simp) +apply(rule conjI) +apply(drule_tac pi="pi" in fin.eqvt(2)) +apply(simp) +apply(rule conjI) +apply(rule_tac x=":M" in exI) +apply(simp) +apply(rule_tac x="(xb):N" in exI) +apply(simp) +apply(rule_tac x="(rev pi)\((y):ImpL .M (xa).N y)" in exI) +apply(perm_simp) +apply(rule_tac x="(rev pi)\xa" in exI) +apply(rule_tac x="(rev pi)\a" in exI) +apply(rule_tac x="(rev pi)\y" in exI) +apply(rule_tac x="(rev pi)\M" in exI) +apply(rule_tac x="(rev pi)\N" in exI) +apply(simp add: swap_simps) +apply(drule_tac pi="rev pi" in fin.eqvt(2)) +apply(simp) +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: swap_simps) +done + +lemma sum_cases: + shows "(\y. x=Inl y) \ (\y. x=Inr y)" +apply(rule_tac s="x" in sumE) +apply(auto) +done + +function + NEGc::"ty \ ntrm set \ ctrm set" +and + NEGn::"ty \ ctrm set \ ntrm set" +where + "NEGc (PR A) X = AXIOMSc (PR A) \ BINDINGc (PR A) X" +| "NEGc (NOT C) X = AXIOMSc (NOT C) \ BINDINGc (NOT C) X + \ NOTRIGHT (NOT C) (lfp (NEGn C \ NEGc C))" +| "NEGc (C AND D) X = AXIOMSc (C AND D) \ BINDINGc (C AND D) X + \ ANDRIGHT (C AND D) (NEGc C (lfp (NEGn C \ NEGc C))) (NEGc D (lfp (NEGn D \ NEGc D)))" +| "NEGc (C OR D) X = AXIOMSc (C OR D) \ BINDINGc (C OR D) X + \ ORRIGHT1 (C OR D) (NEGc C (lfp (NEGn C \ NEGc C))) + \ ORRIGHT2 (C OR D) (NEGc D (lfp (NEGn D \ NEGc D)))" +| "NEGc (C IMP D) X = AXIOMSc (C IMP D) \ BINDINGc (C IMP D) X + \ IMPRIGHT (C IMP D) (lfp (NEGn C \ NEGc C)) (NEGc D (lfp (NEGn D \ NEGc D))) + (lfp (NEGn D \ NEGc D)) (NEGc C (lfp (NEGn C \ NEGc C)))" +| "NEGn (PR A) X = AXIOMSn (PR A) \ BINDINGn (PR A) X" +| "NEGn (NOT C) X = AXIOMSn (NOT C) \ BINDINGn (NOT C) X + \ NOTLEFT (NOT C) (NEGc C (lfp (NEGn C \ NEGc C)))" +| "NEGn (C AND D) X = AXIOMSn (C AND D) \ BINDINGn (C AND D) X + \ ANDLEFT1 (C AND D) (lfp (NEGn C \ NEGc C)) + \ ANDLEFT2 (C AND D) (lfp (NEGn D \ NEGc D))" +| "NEGn (C OR D) X = AXIOMSn (C OR D) \ BINDINGn (C OR D) X + \ ORLEFT (C OR D) (lfp (NEGn C \ NEGc C)) (lfp (NEGn D \ NEGc D))" +| "NEGn (C IMP D) X = AXIOMSn (C IMP D) \ BINDINGn (C IMP D) X + \ IMPLEFT (C IMP D) (NEGc C (lfp (NEGn C \ NEGc C))) (lfp (NEGn D \ NEGc D))" +using ty_cases sum_cases +apply(auto simp add: ty.inject) +apply(drule_tac x="x" in meta_spec) +apply(auto simp add: ty.inject) +apply(rotate_tac 10) +apply(drule_tac x="a" in meta_spec) +apply(auto simp add: ty.inject) +apply(blast) +apply(blast) +apply(blast) +apply(rotate_tac 10) +apply(drule_tac x="a" in meta_spec) +apply(auto simp add: ty.inject) +apply(blast) +apply(blast) +apply(blast) +done + +termination +apply(relation "measure (sum_case (size\fst) (size\fst))") +apply(simp_all) +done + +text {* Candidates *} + +lemma test1: + shows "x\(X\Y) = (x\X \ x\Y)" +by blast + +lemma test2: + shows "x\(X\Y) = (x\X \ x\Y)" +by blast + +lemma big_inter_eqvt: + fixes pi1::"name prm" + and X::"('a::pt_name) set set" + and pi2::"coname prm" + and Y::"('b::pt_coname) set set" + shows "(pi1\(\ X)) = \ (pi1\X)" + and "(pi2\(\ Y)) = \ (pi2\Y)" +apply(auto simp add: perm_set_eq) +apply(rule_tac x="(rev pi1)\x" in exI) +apply(perm_simp) +apply(rule ballI) +apply(drule_tac x="pi1\xa" in spec) +apply(auto) +apply(drule_tac x="xa" in spec) +apply(auto)[1] +apply(rule_tac x="(rev pi1)\xb" in exI) +apply(perm_simp) +apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst]) +apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst]) +apply(rule_tac x="(rev pi2)\x" in exI) +apply(perm_simp) +apply(rule ballI) +apply(drule_tac x="pi2\xa" in spec) +apply(auto) +apply(drule_tac x="xa" in spec) +apply(auto)[1] +apply(rule_tac x="(rev pi2)\xb" in exI) +apply(perm_simp) +apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: pt_set_bij[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst]) +done + +lemma lfp_eqvt: + fixes pi1::"name prm" + and f::"'a set \ ('a::pt_name) set" + and pi2::"coname prm" + and g::"'b set \ ('b::pt_coname) set" + shows "pi1\(lfp f) = lfp (pi1\f)" + and "pi2\(lfp g) = lfp (pi2\g)" +apply(simp add: lfp_def) +apply(simp add: big_inter_eqvt) +apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst]) +apply(subgoal_tac "{u. (pi1\f) u \ u} = {u. ((rev pi1)\((pi1\f) u)) \ ((rev pi1)\u)}") +apply(perm_simp) +apply(rule Collect_cong) +apply(rule iffI) +apply(rule subseteq_eqvt(1)[THEN iffD1]) +apply(simp add: perm_bool) +apply(drule subseteq_eqvt(1)[THEN iffD2]) +apply(simp add: perm_bool) +apply(simp add: lfp_def) +apply(simp add: big_inter_eqvt) +apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst]) +apply(subgoal_tac "{u. (pi2\g) u \ u} = {u. ((rev pi2)\((pi2\g) u)) \ ((rev pi2)\u)}") +apply(perm_simp) +apply(rule Collect_cong) +apply(rule iffI) +apply(rule subseteq_eqvt(2)[THEN iffD1]) +apply(simp add: perm_bool) +apply(drule subseteq_eqvt(2)[THEN iffD2]) +apply(simp add: perm_bool) +done + +abbreviation + CANDn::"ty \ ntrm set" ("\'(_')\" [60] 60) +where + "\(B)\ \ lfp (NEGn B \ NEGc B)" + +abbreviation + CANDc::"ty \ ctrm set" ("\<_>\" [60] 60) +where + "\\ \ NEGc B (\(B)\)" + +lemma NEGn_decreasing: + shows "X\Y \ NEGn B Y \ NEGn B X" +by (nominal_induct B rule: ty.strong_induct) + (auto dest: BINDINGn_decreasing) + +lemma NEGc_decreasing: + shows "X\Y \ NEGc B Y \ NEGc B X" +by (nominal_induct B rule: ty.strong_induct) + (auto dest: BINDINGc_decreasing) + +lemma mono_NEGn_NEGc: + shows "mono (NEGn B \ NEGc B)" + and "mono (NEGc B \ NEGn B)" +proof - + have "\X Y. X\Y \ NEGn B (NEGc B X) \ NEGn B (NEGc B Y)" + proof (intro strip) + fix X::"ntrm set" and Y::"ntrm set" + assume "X\Y" + then have "NEGc B Y \ NEGc B X" by (simp add: NEGc_decreasing) + then show "NEGn B (NEGc B X) \ NEGn B (NEGc B Y)" by (simp add: NEGn_decreasing) + qed + then show "mono (NEGn B \ NEGc B)" by (simp add: mono_def) +next + have "\X Y. X\Y \ NEGc B (NEGn B X) \ NEGc B (NEGn B Y)" + proof (intro strip) + fix X::"ctrm set" and Y::"ctrm set" + assume "X\Y" + then have "NEGn B Y \ NEGn B X" by (simp add: NEGn_decreasing) + then show "NEGc B (NEGn B X) \ NEGc B (NEGn B Y)" by (simp add: NEGc_decreasing) + qed + then show "mono (NEGc B \ NEGn B)" by (simp add: mono_def) +qed + +lemma NEG_simp: + shows "\\ = NEGc B (\(B)\)" + and "\(B)\ = NEGn B (\\)" +proof - + show "\\ = NEGc B (\(B)\)" by simp +next + have "\(B)\ \ lfp (NEGn B \ NEGc B)" by simp + then have "\(B)\ = (NEGn B \ NEGc B) (\(B)\)" using mono_NEGn_NEGc def_lfp_unfold by blast + then show "\(B)\ = NEGn B (\\)" by simp +qed + +lemma NEG_elim: + shows "M \ \\ \ M \ NEGc B (\(B)\)" + and "N \ \(B)\ \ N \ NEGn B (\\)" +using NEG_simp by (blast)+ + +lemma NEG_intro: + shows "M \ NEGc B (\(B)\) \ M \ \\" + and "N \ NEGn B (\\) \ N \ \(B)\" +using NEG_simp by (blast)+ + +lemma NEGc_simps: + shows "NEGc (PR A) (\(PR A)\) = AXIOMSc (PR A) \ BINDINGc (PR A) (\(PR A)\)" + and "NEGc (NOT C) (\(NOT C)\) = AXIOMSc (NOT C) \ BINDINGc (NOT C) (\(NOT C)\) + \ (NOTRIGHT (NOT C) (\(C)\))" + and "NEGc (C AND D) (\(C AND D)\) = AXIOMSc (C AND D) \ BINDINGc (C AND D) (\(C AND D)\) + \ (ANDRIGHT (C AND D) (\\) (\\))" + and "NEGc (C OR D) (\(C OR D)\) = AXIOMSc (C OR D) \ BINDINGc (C OR D) (\(C OR D)\) + \ (ORRIGHT1 (C OR D) (\\)) \ (ORRIGHT2 (C OR D) (\\))" + and "NEGc (C IMP D) (\(C IMP D)\) = AXIOMSc (C IMP D) \ BINDINGc (C IMP D) (\(C IMP D)\) + \ (IMPRIGHT (C IMP D) (\(C)\) (\\) (\(D)\) (\\))" +by (simp_all only: NEGc.simps) + +lemma AXIOMS_in_CANDs: + shows "AXIOMSn B \ (\(B)\)" + and "AXIOMSc B \ (\\)" +proof - + have "AXIOMSn B \ NEGn B (\\)" + by (nominal_induct B rule: ty.strong_induct) (auto) + then show "AXIOMSn B \ \(B)\" using NEG_simp by blast +next + have "AXIOMSc B \ NEGc B (\(B)\)" + by (nominal_induct B rule: ty.strong_induct) (auto) + then show "AXIOMSc B \ \\" using NEG_simp by blast +qed + +lemma Ax_in_CANDs: + shows "(y):Ax x a \ \(B)\" + and ":Ax x a \ \\" +proof - + have "(y):Ax x a \ AXIOMSn B" by (auto simp add: AXIOMSn_def) + also have "AXIOMSn B \ \(B)\" by (rule AXIOMS_in_CANDs) + finally show "(y):Ax x a \ \(B)\" by simp +next + have ":Ax x a \ AXIOMSc B" by (auto simp add: AXIOMSc_def) + also have "AXIOMSc B \ \\" by (rule AXIOMS_in_CANDs) + finally show ":Ax x a \ \\" by simp +qed + +lemma AXIOMS_eqvt_aux_name: + fixes pi::"name prm" + shows "M \ AXIOMSn B \ (pi\M) \ AXIOMSn B" + and "N \ AXIOMSc B \ (pi\N) \ AXIOMSc B" +apply(auto simp add: AXIOMSn_def AXIOMSc_def) +apply(rule_tac x="pi\x" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\b" in exI) +apply(simp) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\b" in exI) +apply(simp) +done + +lemma AXIOMS_eqvt_aux_coname: + fixes pi::"coname prm" + shows "M \ AXIOMSn B \ (pi\M) \ AXIOMSn B" + and "N \ AXIOMSc B \ (pi\N) \ AXIOMSc B" +apply(auto simp add: AXIOMSn_def AXIOMSc_def) +apply(rule_tac x="pi\x" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\b" in exI) +apply(simp) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\y" in exI) +apply(rule_tac x="pi\b" in exI) +apply(simp) +done + +lemma AXIOMS_eqvt_name: + fixes pi::"name prm" + shows "(pi\AXIOMSn B) = AXIOMSn B" + and "(pi\AXIOMSc B) = AXIOMSc B" +apply(auto) +apply(simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_name(1)) +apply(perm_simp) +apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(1)) +apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_name(2)) +apply(perm_simp) +apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(2)) +apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst]) +done + +lemma AXIOMS_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\AXIOMSn B) = AXIOMSn B" + and "(pi\AXIOMSc B) = AXIOMSc B" +apply(auto) +apply(simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst]) +apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(1)) +apply(perm_simp) +apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(1)) +apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst]) +apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(2)) +apply(perm_simp) +apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(2)) +apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst]) +done + +lemma BINDING_eqvt_name: + fixes pi::"name prm" + shows "(pi\(BINDINGn B X)) = BINDINGn B (pi\X)" + and "(pi\(BINDINGc B Y)) = BINDINGc B (pi\Y)" +apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="(rev pi)\a" in spec) +apply(drule_tac x="(rev pi)\P" in spec) +apply(drule mp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +apply(drule_tac ?pi1.0="pi" in SNa_eqvt(1)) +apply(perm_simp add: nsubst_eqvt) +apply(rule_tac x="(rev pi\xa):(rev pi\M)" in exI) +apply(perm_simp) +apply(rule_tac x="rev pi\xa" in exI) +apply(rule_tac x="rev pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="pi\a" in spec) +apply(drule_tac x="pi\P" in spec) +apply(drule mp) +apply(force) +apply(drule_tac ?pi1.0="rev pi" in SNa_eqvt(1)) +apply(perm_simp add: nsubst_eqvt) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="(rev pi)\x" in spec) +apply(drule_tac x="(rev pi)\P" in spec) +apply(drule mp) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp) +apply(drule_tac ?pi1.0="pi" in SNa_eqvt(1)) +apply(perm_simp add: csubst_eqvt) +apply(rule_tac x="<(rev pi\a)>:(rev pi\M)" in exI) +apply(perm_simp) +apply(rule_tac x="rev pi\a" in exI) +apply(rule_tac x="rev pi\M" in exI) +apply(simp add: swap_simps) +apply(auto)[1] +apply(drule_tac x="pi\x" in spec) +apply(drule_tac x="pi\P" in spec) +apply(drule mp) +apply(force) +apply(drule_tac ?pi1.0="rev pi" in SNa_eqvt(1)) +apply(perm_simp add: csubst_eqvt) +done + +lemma BINDING_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(BINDINGn B X)) = BINDINGn B (pi\X)" + and "(pi\(BINDINGc B Y)) = BINDINGc B (pi\Y)" +apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq) +apply(rule_tac x="pi\xb" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="(rev pi)\a" in spec) +apply(drule_tac x="(rev pi)\P" in spec) +apply(drule mp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp) +apply(drule_tac ?pi2.0="pi" in SNa_eqvt(2)) +apply(perm_simp add: nsubst_eqvt) +apply(rule_tac x="(rev pi\xa):(rev pi\M)" in exI) +apply(perm_simp) +apply(rule_tac x="rev pi\xa" in exI) +apply(rule_tac x="rev pi\M" in exI) +apply(simp add: swap_simps) +apply(auto)[1] +apply(drule_tac x="pi\a" in spec) +apply(drule_tac x="pi\P" in spec) +apply(drule mp) +apply(force) +apply(drule_tac ?pi2.0="rev pi" in SNa_eqvt(2)) +apply(perm_simp add: nsubst_eqvt) +apply(rule_tac x="pi\a" in exI) +apply(rule_tac x="pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="(rev pi)\x" in spec) +apply(drule_tac x="(rev pi)\P" in spec) +apply(drule mp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp) +apply(drule_tac ?pi2.0="pi" in SNa_eqvt(2)) +apply(perm_simp add: csubst_eqvt) +apply(rule_tac x="<(rev pi\a)>:(rev pi\M)" in exI) +apply(perm_simp) +apply(rule_tac x="rev pi\a" in exI) +apply(rule_tac x="rev pi\M" in exI) +apply(simp) +apply(auto)[1] +apply(drule_tac x="pi\x" in spec) +apply(drule_tac x="pi\P" in spec) +apply(drule mp) +apply(force) +apply(drule_tac ?pi2.0="rev pi" in SNa_eqvt(2)) +apply(perm_simp add: csubst_eqvt) +done + +lemma CAND_eqvt_name: + fixes pi::"name prm" + shows "(pi\(\(B)\)) = (\(B)\)" + and "(pi\(\\)) = (\\)" +proof (nominal_induct B rule: ty.strong_induct) + case (PR X) + { case 1 show ?case + apply - + apply(simp add: lfp_eqvt) + apply(simp add: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name) + apply(perm_simp) + done + next + case 2 show ?case + apply - + apply(simp only: NEGc_simps) + apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name) + apply(simp add: lfp_eqvt) + apply(simp add: comp_def) + apply(simp add: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name) + apply(perm_simp) + done + } +next + case (NOT B) + have ih1: "pi\(\(B)\) = (\(B)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have g: "pi\(\(NOT B)\) = (\(NOT B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name) + apply(perm_simp add: ih1 ih2) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name ih1 ih2 g) + } +next + case (AND A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A AND B)\) = (\(A AND B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name + ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name + ANDRIGHT_eqvt_name ANDLEFT1_eqvt_name ANDLEFT2_eqvt_name ih1 ih2 ih3 ih4 g) + } +next + case (OR A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A OR B)\) = (\(A OR B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name + ORRIGHT2_eqvt_name ORLEFT_eqvt_name) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name + ORRIGHT1_eqvt_name ORRIGHT2_eqvt_name ORLEFT_eqvt_name ih1 ih2 ih3 ih4 g) + } +next + case (IMP A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A IMP B)\) = (\(A IMP B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name + IMPRIGHT_eqvt_name IMPLEFT_eqvt_name ih1 ih2 ih3 ih4 g) + } +qed + +lemma CAND_eqvt_coname: + fixes pi::"coname prm" + shows "(pi\(\(B)\)) = (\(B)\)" + and "(pi\(\\)) = (\\)" +proof (nominal_induct B rule: ty.strong_induct) + case (PR X) + { case 1 show ?case + apply - + apply(simp add: lfp_eqvt) + apply(simp add: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname) + apply(perm_simp) + done + next + case 2 show ?case + apply - + apply(simp only: NEGc_simps) + apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname) + apply(simp add: lfp_eqvt) + apply(simp add: comp_def) + apply(simp add: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname) + apply(perm_simp) + done + } +next + case (NOT B) + have ih1: "pi\(\(B)\) = (\(B)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have g: "pi\(\(NOT B)\) = (\(NOT B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname + NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname) + apply(perm_simp add: ih1 ih2) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname + NOTRIGHT_eqvt_coname ih1 ih2 g) + } +next + case (AND A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A AND B)\) = (\(A AND B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname + ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname + ANDRIGHT_eqvt_coname ANDLEFT1_eqvt_coname ANDLEFT2_eqvt_coname ih1 ih2 ih3 ih4 g) + } +next + case (OR A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A OR B)\) = (\(A OR B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname + ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname + ORRIGHT1_eqvt_coname ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname ih1 ih2 ih3 ih4 g) + } +next + case (IMP A B) + have ih1: "pi\(\(A)\) = (\(A)\)" by fact + have ih2: "pi\(\\) = (\\)" by fact + have ih3: "pi\(\(B)\) = (\(B)\)" by fact + have ih4: "pi\(\\) = (\\)" by fact + have g: "pi\(\(A IMP B)\) = (\(A IMP B)\)" + apply - + apply(simp only: lfp_eqvt) + apply(simp only: comp_def) + apply(simp only: perm_fun_def [where 'a="ntrm \ bool"]) + apply(simp only: NEGc.simps NEGn.simps) + apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname + IMPLEFT_eqvt_coname) + apply(perm_simp add: ih1 ih2 ih3 ih4) + done + { case 1 show ?case by (rule g) + next + case 2 show ?case + by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname + IMPRIGHT_eqvt_coname IMPLEFT_eqvt_coname ih1 ih2 ih3 ih4 g) + } +qed + +text {* Elimination rules for the set-operators *} + +lemma BINDINGc_elim: + assumes a: ":M \ BINDINGc B (\(B)\)" + shows "\x P. ((x):P)\(\(B)\) \ SNa (M{a:=(x).P})" +using a +apply(auto simp add: BINDINGc_def) +apply(auto simp add: ctrm.inject alpha) +apply(drule_tac x="[(a,aa)]\x" in spec) +apply(drule_tac x="[(a,aa)]\P" in spec) +apply(drule mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname) +apply(drule_tac ?pi2.0="[(a,aa)]" in SNa_eqvt(2)) +apply(perm_simp add: csubst_eqvt) +done + +lemma BINDINGn_elim: + assumes a: "(x):M \ BINDINGn B (\\)" + shows "\c P. (:P)\(\\) \ SNa (M{x:=.P})" +using a +apply(auto simp add: BINDINGn_def) +apply(auto simp add: ntrm.inject alpha) +apply(drule_tac x="[(x,xa)]\c" in spec) +apply(drule_tac x="[(x,xa)]\P" in spec) +apply(drule mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name) +apply(drule_tac ?pi1.0="[(x,xa)]" in SNa_eqvt(1)) +apply(perm_simp add: nsubst_eqvt) +done + +lemma NOTRIGHT_elim: + assumes a: ":M \ NOTRIGHT (NOT B) (\(B)\)" + obtains x' M' where "M = NotR (x').M' a" and "fic (NotR (x').M' a) a" and "(x'):M' \ (\(B)\)" +using a +apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +done + +lemma NOTLEFT_elim: + assumes a: "(x):M \ NOTLEFT (NOT B) (\\)" + obtains a' M' where "M = NotL .M' x" and "fin (NotL .M' x) x" and ":M' \ (\\)" +using a +apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +done + +lemma ANDRIGHT_elim: + assumes a: ":M \ ANDRIGHT (B AND C) (\\) (\\)" + obtains d' M' e' N' where "M = AndR .M' .N' a" and "fic (AndR .M' .N' a) a" + and ":M' \ (\\)" and ":N' \ (\\)" +using a +apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(a,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(case_tac "a=b") +apply(simp) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(b,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "c=b") +apply(simp) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,b)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(aa,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(aa,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "c=aa") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,aa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(a,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(case_tac "a=aa") +apply(simp) +apply(case_tac "aa=b") +apply(simp) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(b,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "c=b") +apply(simp) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(aa,b)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(aa,c)]\M" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(aa,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "c=aa") +apply(simp) +apply(case_tac "a=b") +apply(simp) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(b,aa)]\M" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(b,aa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(b,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(b,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(b,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "aa=b") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,b)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,aa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "a=b") +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(drule_tac x="[(b,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "c=b") +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,b)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,c)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule meta_mp) +apply(drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +done + +lemma ANDLEFT1_elim: + assumes a: "(x):M \ ANDLEFT1 (B AND C) (\(B)\)" + obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' \ (\(B)\)" +using a +apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "y=xa") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +done + +lemma ANDLEFT2_elim: + assumes a: "(x):M \ ANDLEFT2 (B AND C) (\(C)\)" + obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' \ (\(C)\)" +using a +apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "y=xa") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +done + +lemma ORRIGHT1_elim: + assumes a: ":M \ ORRIGHT1 (B OR C) (\\)" + obtains a' M' where "M = OrR1 .M' a" and "fic (OrR1 .M' a) a" and ":M' \ (\\)" +using a +apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "b=aa") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +done + +lemma ORRIGHT2_elim: + assumes a: ":M \ ORRIGHT2 (B OR C) (\\)" + obtains a' M' where "M = OrR2 .M' a" and "fic (OrR2 .M' a) a" and ":M' \ (\\)" +using a +apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(case_tac "b=aa") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +apply(simp) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(simp) +done + +lemma ORLEFT_elim: + assumes a: "(x):M \ ORLEFT (B OR C) (\(B)\) (\(C)\)" + obtains y' M' z' N' where "M = OrL (y').M' (z').N' x" and "fin (OrL (y').M' (z').N' x) x" + and "(y'):M' \ (\(B)\)" and "(z'):N' \ (\(C)\)" +using a +apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(x,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=y") +apply(simp) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(y,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "z=y") +apply(simp) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(xa,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(xa,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "z=xa") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,xa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(x,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=xa") +apply(simp) +apply(case_tac "xa=y") +apply(simp) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(y,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "z=y") +apply(simp) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(xa,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(xa,z)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(xa,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "z=xa") +apply(simp) +apply(case_tac "x=y") +apply(simp) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(y,xa)]\M" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(y,xa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(y,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(y,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(y,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "xa=y") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,xa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "x=y") +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(drule_tac x="[(y,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "z=y") +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,z)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +done + +lemma IMPRIGHT_elim: + assumes a: ":M \ IMPRIGHT (B IMP C) (\(B)\) (\\) (\(C)\) (\\)" + obtains x' a' M' where "M = ImpR (x')..M' a" and "fic (ImpR (x')..M' a) a" + and "\z P. x'\(z,P) \ (z):P \ \(C)\ \ (x'):(M'{a':=(z).P}) \ \(B)\" + and "\c Q. a'\(c,Q) \ :Q \ \\ \ :(M'{x':=.Q}) \ \\" +using a +apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule_tac x="z" in spec) +apply(drule_tac x="[(a,b)]\P" in spec) +apply(simp add: fresh_prod fresh_left calc_atm) +apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\P)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname) +apply(rotate_tac 2) +apply(drule_tac x="[(a,b)]\c" in spec) +apply(drule_tac x="[(a,b)]\Q" in spec) +apply(simp add: fresh_prod fresh_left) +apply(drule mp) +apply(simp add: calc_atm) +apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) +apply(simp add: calc_atm) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule_tac x="z" in spec) +apply(drule_tac x="[(a,b)]\P" in spec) +apply(simp add: fresh_prod fresh_left calc_atm) +apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\P)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname) +apply(drule_tac x="[(a,b)]\c" in spec) +apply(drule_tac x="[(a,b)]\Q" in spec) +apply(simp) +apply(simp add: fresh_prod fresh_left) +apply(drule mp) +apply(simp add: calc_atm) +apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) +apply(simp add: calc_atm) +apply(simp) +apply(case_tac "b=aa") +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule_tac x="z" in spec) +apply(drule_tac x="[(a,aa)]\P" in spec) +apply(simp add: fresh_prod fresh_left calc_atm) +apply(drule_tac pi="[(a,aa)]" and x="(x):M{aa:=(z).([(a,aa)]\P)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname) +apply(drule_tac x="[(a,aa)]\c" in spec) +apply(drule_tac x="[(a,aa)]\Q" in spec) +apply(simp) +apply(simp add: fresh_prod fresh_left) +apply(drule mp) +apply(simp add: calc_atm) +apply(drule_tac pi="[(a,aa)]" and x=":M{x:=<([(a,aa)]\c)>.([(a,aa)]\Q)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) +apply(simp add: calc_atm) +apply(simp) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm CAND_eqvt_coname) +apply(drule_tac x="z" in spec) +apply(drule_tac x="[(a,b)]\P" in spec) +apply(simp add: fresh_prod fresh_left calc_atm) +apply(drule_tac pi="[(a,b)]" and x="(x):M{aa:=(z).([(a,b)]\P)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) +apply(drule meta_mp) +apply(auto)[1] +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname) +apply(drule_tac x="[(a,b)]\c" in spec) +apply(drule_tac x="[(a,b)]\Q" in spec) +apply(simp add: fresh_prod fresh_left) +apply(drule mp) +apply(simp add: calc_atm) +apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" + in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) +apply(simp add: calc_atm) +done + +lemma IMPLEFT_elim: + assumes a: "(x):M \ IMPLEFT (B IMP C) (\\) (\(C)\)" + obtains x' a' M' N' where "M = ImpL .M' (x').N' x" and "fin (ImpL .M' (x').N' x) x" + and ":M' \ \\" and "(x'):N' \ \(C)\" +using a +apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(x,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(drule_tac x="[(xa,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(xa,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(case_tac "y=xa") +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="[(x,xa)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" and x=":M" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +apply(simp) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="[(x,y)]\N" in meta_spec) +apply(simp) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(drule meta_mp) +apply(drule_tac pi="[(x,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm CAND_eqvt_name) +apply(simp) +done + +lemma CANDs_alpha: + shows ":M \ (\\) \ [a].M = [b].N \ :N \ (\\)" + and "(x):M \ (\(B)\) \ [x].M = [y].N \ (y):N \ (\(B)\)" +apply(auto simp add: alpha) +apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(perm_simp add: CAND_eqvt_coname calc_atm) +apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name calc_atm) +done + +lemma CAND_NotR_elim: + assumes a: ":NotR (x).M a \ (\\)" ":NotR (x).M a \ BINDINGc B (\(B)\)" + shows "\B'. B = NOT B' \ (x):M \ (\(B')\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +done + +lemma CAND_NotL_elim_aux: + assumes a: "(x):NotL .M x \ NEGn B (\\)" "(x):NotL .M x \ BINDINGn B (\\)" + shows "\B'. B = NOT B' \ :M \ (\\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +done + +lemmas CAND_NotL_elim = CAND_NotL_elim_aux[OF NEG_elim(2)] + +lemma CAND_AndR_elim: + assumes a: ":AndR .M .N a \ (\\)" ":AndR .M .N a \ BINDINGc B (\(B)\)" + shows "\B1 B2. B = B1 AND B2 \ :M \ (\\) \ :N \ (\\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "a=ba") +apply(simp) +apply(drule_tac pi="[(ba,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "ca=ba") +apply(simp) +apply(drule_tac pi="[(a,ba)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac pi="[(aa,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "ca=aa") +apply(simp) +apply(drule_tac pi="[(a,aa)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac pi="[(aa,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "ca=aa") +apply(simp) +apply(drule_tac pi="[(a,aa)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "a=ba") +apply(simp) +apply(drule_tac pi="[(ba,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "ca=ba") +apply(simp) +apply(drule_tac pi="[(a,ba)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_coname calc_atm) +apply(auto intro: CANDs_alpha)[1] +done + +lemma CAND_OrR1_elim: + assumes a: ":OrR1 .M a \ (\\)" ":OrR1 .M a \ BINDINGc B (\(B)\)" + shows "\B1 B2. B = B1 OR B2 \ :M \ (\\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(case_tac "ba=aa") +apply(simp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +done + +lemma CAND_OrR2_elim: + assumes a: ":OrR2 .M a \ (\\)" ":OrR2 .M a \ BINDINGc B (\(B)\)" + shows "\B1 B2. B = B1 OR B2 \ :M \ (\\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(case_tac "a=aa") +apply(simp) +apply(drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(case_tac "ba=aa") +apply(simp) +apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha) +done + +lemma CAND_OrL_elim_aux: + assumes a: "(x):(OrL (y).M (z).N x) \ NEGn B (\\)" "(x):(OrL (y).M (z).N x) \ BINDINGn B (\\)" + shows "\B1 B2. B = B1 OR B2 \ (y):M \ (\(B1)\) \ (z):N \ (\(B2)\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "x=ya") +apply(simp) +apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "za=ya") +apply(simp) +apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "za=xa") +apply(simp) +apply(drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "za=xa") +apply(simp) +apply(drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "x=ya") +apply(simp) +apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "za=ya") +apply(simp) +apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +done + +lemmas CAND_OrL_elim = CAND_OrL_elim_aux[OF NEG_elim(2)] + +lemma CAND_AndL1_elim_aux: + assumes a: "(x):(AndL1 (y).M x) \ NEGn B (\\)" "(x):(AndL1 (y).M x) \ BINDINGn B (\\)" + shows "\B1 B2. B = B1 AND B2 \ (y):M \ (\(B1)\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(case_tac "ya=xa") +apply(simp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +done + +lemmas CAND_AndL1_elim = CAND_AndL1_elim_aux[OF NEG_elim(2)] + +lemma CAND_AndL2_elim_aux: + assumes a: "(x):(AndL2 (y).M x) \ NEGn B (\\)" "(x):(AndL2 (y).M x) \ BINDINGn B (\\)" + shows "\B1 B2. B = B1 AND B2 \ (y):M \ (\(B2)\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(case_tac "ya=xa") +apply(simp) +apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha) +done + +lemmas CAND_AndL2_elim = CAND_AndL2_elim_aux[OF NEG_elim(2)] + +lemma CAND_ImpL_elim_aux: + assumes a: "(x):(ImpL .M (z).N x) \ NEGn B (\\)" "(x):(ImpL .M (z).N x) \ BINDINGn B (\\)" + shows "\B1 B2. B = B1 IMP B2 \ :M \ (\\) \ (z):N \ (\(B2)\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm) +apply(drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(x,y)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(case_tac "x=xa") +apply(simp) +apply(drule_tac pi="[(xa,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(case_tac "y=xa") +apply(simp) +apply(drule_tac pi="[(x,xa)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +apply(simp) +apply(drule_tac pi="[(x,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name calc_atm) +apply(auto intro: CANDs_alpha)[1] +done + +lemmas CAND_ImpL_elim = CAND_ImpL_elim_aux[OF NEG_elim(2)] + +lemma CAND_ImpR_elim: + assumes a: ":ImpR (x)..M a \ (\\)" ":ImpR (x)..M a \ BINDINGc B (\(B)\)" + shows "\B1 B2. B = B1 IMP B2 \ + (\z P. x\(z,P) \ (z):P \ \(B2)\ \ (x):(M{b:=(z).P}) \ \(B1)\) \ + (\c Q. b\(c,Q) \ :Q \ \\ \ :(M{x:=.Q}) \ \\)" +using a +apply(nominal_induct B rule: ty.strong_induct) +apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha) +apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm fresh_prod fresh_bij) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="ca" and z="c" in alpha_name_coname) +apply(simp) +apply(simp) +apply(simp) +apply(drule_tac x="[(xa,c)]\[(aa,ca)]\[(b,ca)]\[(x,c)]\z" in spec) +apply(drule_tac x="[(xa,c)]\[(aa,ca)]\[(b,ca)]\[(x,c)]\P" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(aa,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="cb" and z="ca" in alpha_name_coname) +apply(simp) +apply(simp) +apply(simp) +apply(drule_tac x="[(xa,ca)]\[(aa,cb)]\[(b,cb)]\[(x,ca)]\c" in spec) +apply(drule_tac x="[(xa,ca)]\[(aa,cb)]\[(b,cb)]\[(x,ca)]\Q" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(aa,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="ca" and z="c" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,ba)]\[(xa,c)]\[(ba,ca)]\[(b,ca)]\[(x,c)]\z" in spec) +apply(drule_tac x="[(a,ba)]\[(xa,c)]\[(ba,ca)]\[(b,ca)]\[(x,c)]\P" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(ba,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(ba,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="cb" and z="ca" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,ba)]\[(xa,ca)]\[(ba,cb)]\[(b,cb)]\[(x,ca)]\c" in spec) +apply(drule_tac x="[(a,ba)]\[(xa,ca)]\[(ba,cb)]\[(b,cb)]\[(x,ca)]\Q" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(ba,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(ba,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(case_tac "a=aa") +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="ca" and z="c" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(aa,ba)]\[(xa,c)]\[(ba,ca)]\[(b,ca)]\[(x,c)]\z" in spec) +apply(drule_tac x="[(aa,ba)]\[(xa,c)]\[(ba,ca)]\[(b,ca)]\[(x,c)]\P" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(ba,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ba)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ba)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(ba,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(simp) +apply(case_tac "ba=aa") +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="ca" and z="c" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,aa)]\[(xa,c)]\[(a,ca)]\[(b,ca)]\[(x,c)]\z" in spec) +apply(drule_tac x="[(a,aa)]\[(xa,c)]\[(a,ca)]\[(b,ca)]\[(x,c)]\P" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,aa)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,aa)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(a,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="ca" and z="c" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,ba)]\[(xa,c)]\[(aa,ca)]\[(b,ca)]\[(x,c)]\z" in spec) +apply(drule_tac x="[(a,ba)]\[(xa,c)]\[(aa,ca)]\[(b,ca)]\[(x,c)]\P" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ca)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,c)]" and X="\(ty2)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\(ty2)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(aa,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,ca)]" and X="\(ty1)\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,c)]" and X="\(ty1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(case_tac "a=aa") +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="cb" and z="ca" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(aa,ba)]\[(xa,ca)]\[(ba,cb)]\[(b,cb)]\[(x,ca)]\c" in spec) +apply(drule_tac x="[(aa,ba)]\[(xa,ca)]\[(ba,cb)]\[(b,cb)]\[(x,ca)]\Q" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(ba,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(ba,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(simp) +apply(case_tac "ba=aa") +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="cb" and z="ca" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,aa)]\[(xa,ca)]\[(a,cb)]\[(b,cb)]\[(x,ca)]\c" in spec) +apply(drule_tac x="[(a,aa)]\[(xa,ca)]\[(a,cb)]\[(b,cb)]\[(x,ca)]\Q" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,aa)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,aa)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(a,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(simp) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(drule_tac a="cb" and z="ca" in alpha_name_coname) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(auto)[1] +apply(simp) +apply(drule_tac x="[(a,ba)]\[(xa,ca)]\[(aa,cb)]\[(b,cb)]\[(x,ca)]\c" in spec) +apply(drule_tac x="[(a,ba)]\[(xa,ca)]\[(aa,cb)]\[(b,cb)]\[(x,ca)]\Q" in spec) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm fresh_prod fresh_atm)[1] +apply(rule conjI) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(aa,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(a,ba)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(xa,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(aa,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +apply(drule_tac pi="[(b,cb)]" and X="\\" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: CAND_eqvt_name CAND_eqvt_coname) +apply(drule_tac pi="[(x,ca)]" and X="\\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) +done + +text {* Main lemma 1 *} + +lemma AXIOMS_imply_SNa: + shows ":M \ AXIOMSc B \ SNa M" + and "(x):M \ AXIOMSn B \ SNa M" +apply - +apply(auto simp add: AXIOMSn_def AXIOMSc_def ntrm.inject ctrm.inject alpha) +apply(rule Ax_in_SNa)+ +done + +lemma BINDING_imply_SNa: + shows ":M \ BINDINGc B (\(B)\) \ SNa M" + and "(x):M \ BINDINGn B (\\) \ SNa M" +apply - +apply(auto simp add: BINDINGn_def BINDINGc_def ntrm.inject ctrm.inject alpha) +apply(drule_tac x="x" in spec) +apply(drule_tac x="Ax x a" in spec) +apply(drule mp) +apply(rule Ax_in_CANDs) +apply(drule a_star_preserves_SNa) +apply(rule subst_with_ax2) +apply(simp add: crename_id) +apply(drule_tac x="x" in spec) +apply(drule_tac x="Ax x aa" in spec) +apply(drule mp) +apply(rule Ax_in_CANDs) +apply(drule a_star_preserves_SNa) +apply(rule subst_with_ax2) +apply(simp add: crename_id SNa_eqvt) +apply(drule_tac x="a" in spec) +apply(drule_tac x="Ax x a" in spec) +apply(drule mp) +apply(rule Ax_in_CANDs) +apply(drule a_star_preserves_SNa) +apply(rule subst_with_ax1) +apply(simp add: nrename_id) +apply(drule_tac x="a" in spec) +apply(drule_tac x="Ax xa a" in spec) +apply(drule mp) +apply(rule Ax_in_CANDs) +apply(drule a_star_preserves_SNa) +apply(rule subst_with_ax1) +apply(simp add: nrename_id SNa_eqvt) +done + +lemma CANDs_imply_SNa: + shows ":M \ \\ \ SNa M" + and "(x):M \ \(B)\ \ SNa M" +proof(induct B arbitrary: a x M rule: ty.induct) + case (PR X) + { case 1 + have ":M \ \\" by fact + then have ":M \ NEGc (PR X) (\(PR X)\)" by simp + then have ":M \ AXIOMSc (PR X) \ BINDINGc (PR X) (\(PR X)\)" by simp + moreover + { assume ":M \ AXIOMSc (PR X)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume ":M \ BINDINGc (PR X) (\(PR X)\)" + then have "SNa M" by (simp add: BINDING_imply_SNa) + } + ultimately show "SNa M" by blast + next + case 2 + have "(x):M \ (\(PR X)\)" by fact + then have "(x):M \ NEGn (PR X) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (PR X) \ BINDINGn (PR X) (\\)" by simp + moreover + { assume "(x):M \ AXIOMSn (PR X)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume "(x):M \ BINDINGn (PR X) (\\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + ultimately show "SNa M" by blast + } +next + case (NOT B) + have ih1: "\a M. :M \ \\ \ SNa M" by fact + have ih2: "\x M. (x):M \ \(B)\ \ SNa M" by fact + { case 1 + have ":M \ (\\)" by fact + then have ":M \ NEGc (NOT B) (\(NOT B)\)" by simp + then have ":M \ AXIOMSc (NOT B) \ BINDINGc (NOT B) (\(NOT B)\) \ NOTRIGHT (NOT B) (\(B)\)" by simp + moreover + { assume ":M \ AXIOMSc (NOT B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume ":M \ BINDINGc (NOT B) (\(NOT B)\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume ":M \ NOTRIGHT (NOT B) (\(B)\)" + then obtain x' M' where eq: "M = NotR (x').M' a" and "(x'):M' \ (\(B)\)" + using NOTRIGHT_elim by blast + then have "SNa M'" using ih2 by blast + then have "SNa M" using eq by (simp add: NotR_in_SNa) + } + ultimately show "SNa M" by blast + next + case 2 + have "(x):M \ (\(NOT B)\)" by fact + then have "(x):M \ NEGn (NOT B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (NOT B) \ BINDINGn (NOT B) (\\) \ NOTLEFT (NOT B) (\\)" + by (simp only: NEGn.simps) + moreover + { assume "(x):M \ AXIOMSn (NOT B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume "(x):M \ BINDINGn (NOT B) (\\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume "(x):M \ NOTLEFT (NOT B) (\\)" + then obtain a' M' where eq: "M = NotL .M' x" and ":M' \ (\\)" + using NOTLEFT_elim by blast + then have "SNa M'" using ih1 by blast + then have "SNa M" using eq by (simp add: NotL_in_SNa) + } + ultimately show "SNa M" by blast + } +next + case (AND A B) + have ih1: "\a M. :M \ \\ \ SNa M" by fact + have ih2: "\x M. (x):M \ \(A)\ \ SNa M" by fact + have ih3: "\a M. :M \ \\ \ SNa M" by fact + have ih4: "\x M. (x):M \ \(B)\ \ SNa M" by fact + { case 1 + have ":M \ (\\)" by fact + then have ":M \ NEGc (A AND B) (\(A AND B)\)" by simp + then have ":M \ AXIOMSc (A AND B) \ BINDINGc (A AND B) (\(A AND B)\) + \ ANDRIGHT (A AND B) (\\) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A AND B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume ":M \ BINDINGc (A AND B) (\(A AND B)\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume ":M \ ANDRIGHT (A AND B) (\\) (\\)" + then obtain a' M' b' N' where eq: "M = AndR .M' .N' a" + and ":M' \ (\\)" and ":N' \ (\\)" + by (erule_tac ANDRIGHT_elim, blast) + then have "SNa M'" and "SNa N'" using ih1 ih3 by blast+ + then have "SNa M" using eq by (simp add: AndR_in_SNa) + } + ultimately show "SNa M" by blast + next + case 2 + have "(x):M \ (\(A AND B)\)" by fact + then have "(x):M \ NEGn (A AND B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A AND B) \ BINDINGn (A AND B) (\\) + \ ANDLEFT1 (A AND B) (\(A)\) \ ANDLEFT2 (A AND B) (\(B)\)" + by (simp only: NEGn.simps) + moreover + { assume "(x):M \ AXIOMSn (A AND B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume "(x):M \ BINDINGn (A AND B) (\\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume "(x):M \ ANDLEFT1 (A AND B) (\(A)\)" + then obtain x' M' where eq: "M = AndL1 (x').M' x" and "(x'):M' \ (\(A)\)" + using ANDLEFT1_elim by blast + then have "SNa M'" using ih2 by blast + then have "SNa M" using eq by (simp add: AndL1_in_SNa) + } + moreover + { assume "(x):M \ ANDLEFT2 (A AND B) (\(B)\)" + then obtain x' M' where eq: "M = AndL2 (x').M' x" and "(x'):M' \ (\(B)\)" + using ANDLEFT2_elim by blast + then have "SNa M'" using ih4 by blast + then have "SNa M" using eq by (simp add: AndL2_in_SNa) + } + ultimately show "SNa M" by blast + } +next + case (OR A B) + have ih1: "\a M. :M \ \\ \ SNa M" by fact + have ih2: "\x M. (x):M \ \(A)\ \ SNa M" by fact + have ih3: "\a M. :M \ \\ \ SNa M" by fact + have ih4: "\x M. (x):M \ \(B)\ \ SNa M" by fact + { case 1 + have ":M \ (\\)" by fact + then have ":M \ NEGc (A OR B) (\(A OR B)\)" by simp + then have ":M \ AXIOMSc (A OR B) \ BINDINGc (A OR B) (\(A OR B)\) + \ ORRIGHT1 (A OR B) (\\) \ ORRIGHT2 (A OR B) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A OR B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume ":M \ BINDINGc (A OR B) (\(A OR B)\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume ":M \ ORRIGHT1 (A OR B) (\\)" + then obtain a' M' where eq: "M = OrR1 .M' a" + and ":M' \ (\\)" + by (erule_tac ORRIGHT1_elim, blast) + then have "SNa M'" using ih1 by blast + then have "SNa M" using eq by (simp add: OrR1_in_SNa) + } + moreover + { assume ":M \ ORRIGHT2 (A OR B) (\\)" + then obtain a' M' where eq: "M = OrR2 .M' a" and ":M' \ (\\)" + using ORRIGHT2_elim by blast + then have "SNa M'" using ih3 by blast + then have "SNa M" using eq by (simp add: OrR2_in_SNa) + } + ultimately show "SNa M" by blast + next + case 2 + have "(x):M \ (\(A OR B)\)" by fact + then have "(x):M \ NEGn (A OR B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A OR B) \ BINDINGn (A OR B) (\\) + \ ORLEFT (A OR B) (\(A)\) (\(B)\)" + by (simp only: NEGn.simps) + moreover + { assume "(x):M \ AXIOMSn (A OR B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume "(x):M \ BINDINGn (A OR B) (\\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume "(x):M \ ORLEFT (A OR B) (\(A)\) (\(B)\)" + then obtain x' M' y' N' where eq: "M = OrL (x').M' (y').N' x" + and "(x'):M' \ (\(A)\)" and "(y'):N' \ (\(B)\)" + by (erule_tac ORLEFT_elim, blast) + then have "SNa M'" and "SNa N'" using ih2 ih4 by blast+ + then have "SNa M" using eq by (simp add: OrL_in_SNa) + } + ultimately show "SNa M" by blast + } +next + case (IMP A B) + have ih1: "\a M. :M \ \\ \ SNa M" by fact + have ih2: "\x M. (x):M \ \(A)\ \ SNa M" by fact + have ih3: "\a M. :M \ \\ \ SNa M" by fact + have ih4: "\x M. (x):M \ \(B)\ \ SNa M" by fact + { case 1 + have ":M \ (\\)" by fact + then have ":M \ NEGc (A IMP B) (\(A IMP B)\)" by simp + then have ":M \ AXIOMSc (A IMP B) \ BINDINGc (A IMP B) (\(A IMP B)\) + \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A IMP B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume ":M \ BINDINGc (A IMP B) (\(A IMP B)\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume ":M \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" + then obtain x' a' M' where eq: "M = ImpR (x')..M' a" + and imp: "\z P. x'\(z,P) \ (z):P \ \(B)\ \ (x'):(M'{a':=(z).P}) \ \(A)\" + by (erule_tac IMPRIGHT_elim, blast) + obtain z::"name" where fs: "z\x'" by (rule_tac exists_fresh, rule fin_supp, blast) + have "(z):Ax z a'\ \(B)\" by (simp add: Ax_in_CANDs) + with imp fs have "(x'):(M'{a':=(z).Ax z a'}) \ \(A)\" by (simp add: fresh_prod fresh_atm) + then have "SNa (M'{a':=(z).Ax z a'})" using ih2 by blast + moreover + have "M'{a':=(z).Ax z a'} \\<^isub>a* M'[a'\c>a']" by (simp add: subst_with_ax2) + ultimately have "SNa (M'[a'\c>a'])" by (simp add: a_star_preserves_SNa) + then have "SNa M'" by (simp add: crename_id) + then have "SNa M" using eq by (simp add: ImpR_in_SNa) + } + ultimately show "SNa M" by blast + next + case 2 + have "(x):M \ (\(A IMP B)\)" by fact + then have "(x):M \ NEGn (A IMP B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A IMP B) \ BINDINGn (A IMP B) (\\) + \ IMPLEFT (A IMP B) (\\) (\(B)\)" + by (simp only: NEGn.simps) + moreover + { assume "(x):M \ AXIOMSn (A IMP B)" + then have "SNa M" by (simp add: AXIOMS_imply_SNa) + } + moreover + { assume "(x):M \ BINDINGn (A IMP B) (\\)" + then have "SNa M" by (simp only: BINDING_imply_SNa) + } + moreover + { assume "(x):M \ IMPLEFT (A IMP B) (\\) (\(B)\)" + then obtain a' M' y' N' where eq: "M = ImpL .M' (y').N' x" + and ":M' \ (\\)" and "(y'):N' \ (\(B)\)" + by (erule_tac IMPLEFT_elim, blast) + then have "SNa M'" and "SNa N'" using ih1 ih4 by blast+ + then have "SNa M" using eq by (simp add: ImpL_in_SNa) + } + ultimately show "SNa M" by blast + } +qed + +text {* Main lemma 2 *} + +lemma AXIOMS_preserved: + shows ":M \ AXIOMSc B \ M \\<^isub>a* M' \ :M' \ AXIOMSc B" + and "(x):M \ AXIOMSn B \ M \\<^isub>a* M' \ (x):M' \ AXIOMSn B" + apply(simp_all add: AXIOMSc_def AXIOMSn_def) + apply(auto simp add: ntrm.inject ctrm.inject alpha) + apply(drule ax_do_not_a_star_reduce) + apply(auto) + apply(drule ax_do_not_a_star_reduce) + apply(auto) + apply(drule ax_do_not_a_star_reduce) + apply(auto) + apply(drule ax_do_not_a_star_reduce) + apply(auto) + done + +lemma BINDING_preserved: + shows ":M \ BINDINGc B (\(B)\) \ M \\<^isub>a* M' \ :M' \ BINDINGc B (\(B)\)" + and "(x):M \ BINDINGn B (\\) \ M \\<^isub>a* M' \ (x):M' \ BINDINGn B (\\)" +proof - + assume red: "M \\<^isub>a* M'" + assume asm: ":M \ BINDINGc B (\(B)\)" + { + fix x::"name" and P::"trm" + from asm have "((x):P) \ (\(B)\) \ SNa (M{a:=(x).P})" by (simp add: BINDINGc_elim) + moreover + have "M{a:=(x).P} \\<^isub>a* M'{a:=(x).P}" using red by (simp add: a_star_subst2) + ultimately + have "((x):P) \ (\(B)\) \ SNa (M'{a:=(x).P})" by (simp add: a_star_preserves_SNa) + } + then show ":M' \ BINDINGc B (\(B)\)" by (auto simp add: BINDINGc_def) +next + assume red: "M \\<^isub>a* M'" + assume asm: "(x):M \ BINDINGn B (\\)" + { + fix c::"coname" and P::"trm" + from asm have "(:P) \ (\\) \ SNa (M{x:=.P})" by (simp add: BINDINGn_elim) + moreover + have "M{x:=.P} \\<^isub>a* M'{x:=.P}" using red by (simp add: a_star_subst1) + ultimately + have "(:P) \ (\\) \ SNa (M'{x:=.P})" by (simp add: a_star_preserves_SNa) + } + then show "(x):M' \ BINDINGn B (\\)" by (auto simp add: BINDINGn_def) +qed + +lemma CANDs_preserved: + shows ":M \ \\ \ M \\<^isub>a* M' \ :M' \ \\" + and "(x):M \ \(B)\ \ M \\<^isub>a* M' \ (x):M' \ \(B)\" +proof(nominal_induct B arbitrary: a x M M' rule: ty.strong_induct) + case (PR X) + { case 1 + have asm: "M \\<^isub>a* M'" by fact + have ":M \ \\" by fact + then have ":M \ NEGc (PR X) (\(PR X)\)" by simp + then have ":M \ AXIOMSc (PR X) \ BINDINGc (PR X) (\(PR X)\)" by simp + moreover + { assume ":M \ AXIOMSc (PR X)" + then have ":M' \ AXIOMSc (PR X)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume ":M \ BINDINGc (PR X) (\(PR X)\)" + then have ":M' \ BINDINGc (PR X) (\(PR X)\)" using asm by (simp add: BINDING_preserved) + } + ultimately have ":M' \ AXIOMSc (PR X) \ BINDINGc (PR X) (\(PR X)\)" by blast + then have ":M' \ NEGc (PR X) (\(PR X)\)" by simp + then show ":M' \ (\\)" using NEG_simp by blast + next + case 2 + have asm: "M \\<^isub>a* M'" by fact + have "(x):M \ \(PR X)\" by fact + then have "(x):M \ NEGn (PR X) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (PR X) \ BINDINGn (PR X) (\\)" by simp + moreover + { assume "(x):M \ AXIOMSn (PR X)" + then have "(x):M' \ AXIOMSn (PR X)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume "(x):M \ BINDINGn (PR X) (\\)" + then have "(x):M' \ BINDINGn (PR X) (\\)" using asm by (simp only: BINDING_preserved) + } + ultimately have "(x):M' \ AXIOMSn (PR X) \ BINDINGn (PR X) (\\)" by blast + then have "(x):M' \ NEGn (PR X) (\\)" by simp + then show "(x):M' \ (\(PR X)\)" using NEG_simp by blast + } +next + case (IMP A B) + have ih1: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih2: "\x M M'. \(x):M \ \(A)\; M \\<^isub>a* M'\ \ (x):M' \ \(A)\" by fact + have ih3: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih4: "\x M M'. \(x):M \ \(B)\; M \\<^isub>a* M'\ \ (x):M' \ \(B)\" by fact + { case 1 + have asm: "M \\<^isub>a* M'" by fact + have ":M \ \\" by fact + then have ":M \ NEGc (A IMP B) (\(A IMP B)\)" by simp + then have ":M \ AXIOMSc (A IMP B) \ BINDINGc (A IMP B) (\(A IMP B)\) + \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A IMP B)" + then have ":M' \ AXIOMSc (A IMP B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume ":M \ BINDINGc (A IMP B) (\(A IMP B)\)" + then have ":M' \ BINDINGc (A IMP B) (\(A IMP B)\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume ":M \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" + then obtain x' a' N' where eq: "M = ImpR (x')..N' a" and fic: "fic (ImpR (x')..N' a) a" + and imp1: "\z P. x'\(z,P) \ (z):P \ \(B)\ \ (x'):(N'{a':=(z).P}) \ \(A)\" + and imp2: "\c Q. a'\(c,Q) \ :Q \ \\ \ :(N'{x':=.Q}) \ \\" + using IMPRIGHT_elim by blast + from eq asm obtain N'' where eq': "M' = ImpR (x')..N'' a" and red: "N' \\<^isub>a* N''" + using a_star_redu_ImpR_elim by (blast) + from imp1 have "\z P. x'\(z,P) \ (z):P \ \(B)\ \ (x'):(N''{a':=(z).P}) \ \(A)\" using red ih2 + apply(auto) + apply(drule_tac x="z" in spec) + apply(drule_tac x="P" in spec) + apply(simp) + apply(drule_tac a_star_subst2) + apply(blast) + done + moreover + from imp2 have "\c Q. a'\(c,Q) \ :Q \ \\ \ :(N''{x':=.Q}) \ \\" using red ih3 + apply(auto) + apply(drule_tac x="c" in spec) + apply(drule_tac x="Q" in spec) + apply(simp) + apply(drule_tac a_star_subst1) + apply(blast) + done + moreover + from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce) + ultimately have ":M' \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" using eq' by auto + } + ultimately have ":M' \ AXIOMSc (A IMP B) \ BINDINGc (A IMP B) (\(A IMP B)\) + \ IMPRIGHT (A IMP B) (\(A)\) (\\) (\(B)\) (\\)" by blast + then have ":M' \ NEGc (A IMP B) (\(A IMP B)\)" by simp + then show ":M' \ (\\)" using NEG_simp by blast + next + case 2 + have asm: "M \\<^isub>a* M'" by fact + have "(x):M \ \(A IMP B)\" by fact + then have "(x):M \ NEGn (A IMP B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A IMP B) \ BINDINGn (A IMP B) (\\) + \ IMPLEFT (A IMP B) (\\) (\(B)\)" by simp + moreover + { assume "(x):M \ AXIOMSn (A IMP B)" + then have "(x):M' \ AXIOMSn (A IMP B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume "(x):M \ BINDINGn (A IMP B) (\\)" + then have "(x):M' \ BINDINGn (A IMP B) (\\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume "(x):M \ IMPLEFT (A IMP B) (\\) (\(B)\)" + then obtain a' T' y' N' where eq: "M = ImpL .T' (y').N' x" + and fin: "fin (ImpL .T' (y').N' x) x" + and imp1: ":T' \ \\" and imp2: "(y'):N' \ \(B)\" + by (erule_tac IMPLEFT_elim, blast) + from eq asm obtain T'' N'' where eq': "M' = ImpL .T'' (y').N'' x" + and red1: "T' \\<^isub>a* T''" and red2: "N' \\<^isub>a* N''" + using a_star_redu_ImpL_elim by blast + from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce) + moreover + from imp1 red1 have ":T'' \ \\" using ih1 by simp + moreover + from imp2 red2 have "(y'):N'' \ \(B)\" using ih4 by simp + ultimately have "(x):M' \ IMPLEFT (A IMP B) (\\) (\(B)\)" using eq' by (simp, blast) + } + ultimately have "(x):M' \ AXIOMSn (A IMP B) \ BINDINGn (A IMP B) (\\) + \ IMPLEFT (A IMP B) (\\) (\(B)\)" by blast + then have "(x):M' \ NEGn (A IMP B) (\\)" by simp + then show "(x):M' \ (\(A IMP B)\)" using NEG_simp by blast + } +next + case (AND A B) + have ih1: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih2: "\x M M'. \(x):M \ \(A)\; M \\<^isub>a* M'\ \ (x):M' \ \(A)\" by fact + have ih3: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih4: "\x M M'. \(x):M \ \(B)\; M \\<^isub>a* M'\ \ (x):M' \ \(B)\" by fact + { case 1 + have asm: "M \\<^isub>a* M'" by fact + have ":M \ \\" by fact + then have ":M \ NEGc (A AND B) (\(A AND B)\)" by simp + then have ":M \ AXIOMSc (A AND B) \ BINDINGc (A AND B) (\(A AND B)\) + \ ANDRIGHT (A AND B) (\\) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A AND B)" + then have ":M' \ AXIOMSc (A AND B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume ":M \ BINDINGc (A AND B) (\(A AND B)\)" + then have ":M' \ BINDINGc (A AND B) (\(A AND B)\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume ":M \ ANDRIGHT (A AND B) (\\) (\\)" + then obtain a' T' b' N' where eq: "M = AndR .T' .N' a" + and fic: "fic (AndR .T' .N' a) a" + and imp1: ":T' \ \\" and imp2: ":N' \ \\" + using ANDRIGHT_elim by blast + from eq asm obtain T'' N'' where eq': "M' = AndR .T'' .N'' a" + and red1: "T' \\<^isub>a* T''" and red2: "N' \\<^isub>a* N''" + using a_star_redu_AndR_elim by blast + from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce) + moreover + from imp1 red1 have ":T'' \ \\" using ih1 by simp + moreover + from imp2 red2 have ":N'' \ \\" using ih3 by simp + ultimately have ":M' \ ANDRIGHT (A AND B) (\\) (\\)" using eq' by (simp, blast) + } + ultimately have ":M' \ AXIOMSc (A AND B) \ BINDINGc (A AND B) (\(A AND B)\) + \ ANDRIGHT (A AND B) (\\) (\\)" by blast + then have ":M' \ NEGc (A AND B) (\(A AND B)\)" by simp + then show ":M' \ (\\)" using NEG_simp by blast + next + case 2 + have asm: "M \\<^isub>a* M'" by fact + have "(x):M \ \(A AND B)\" by fact + then have "(x):M \ NEGn (A AND B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A AND B) \ BINDINGn (A AND B) (\\) + \ ANDLEFT1 (A AND B) (\(A)\) \ ANDLEFT2 (A AND B) (\(B)\)" by simp + moreover + { assume "(x):M \ AXIOMSn (A AND B)" + then have "(x):M' \ AXIOMSn (A AND B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume "(x):M \ BINDINGn (A AND B) (\\)" + then have "(x):M' \ BINDINGn (A AND B) (\\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume "(x):M \ ANDLEFT1 (A AND B) (\(A)\)" + then obtain y' N' where eq: "M = AndL1 (y').N' x" + and fin: "fin (AndL1 (y').N' x) x" and imp: "(y'):N' \ \(A)\" + by (erule_tac ANDLEFT1_elim, blast) + from eq asm obtain N'' where eq': "M' = AndL1 (y').N'' x" and red1: "N' \\<^isub>a* N''" + using a_star_redu_AndL1_elim by blast + from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce) + moreover + from imp red1 have "(y'):N'' \ \(A)\" using ih2 by simp + ultimately have "(x):M' \ ANDLEFT1 (A AND B) (\(A)\)" using eq' by (simp, blast) + } + moreover + { assume "(x):M \ ANDLEFT2 (A AND B) (\(B)\)" + then obtain y' N' where eq: "M = AndL2 (y').N' x" + and fin: "fin (AndL2 (y').N' x) x" and imp: "(y'):N' \ \(B)\" + by (erule_tac ANDLEFT2_elim, blast) + from eq asm obtain N'' where eq': "M' = AndL2 (y').N'' x" and red1: "N' \\<^isub>a* N''" + using a_star_redu_AndL2_elim by blast + from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce) + moreover + from imp red1 have "(y'):N'' \ \(B)\" using ih4 by simp + ultimately have "(x):M' \ ANDLEFT2 (A AND B) (\(B)\)" using eq' by (simp, blast) + } + ultimately have "(x):M' \ AXIOMSn (A AND B) \ BINDINGn (A AND B) (\\) + \ ANDLEFT1 (A AND B) (\(A)\) \ ANDLEFT2 (A AND B) (\(B)\)" by blast + then have "(x):M' \ NEGn (A AND B) (\\)" by simp + then show "(x):M' \ (\(A AND B)\)" using NEG_simp by blast + } +next + case (OR A B) + have ih1: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih2: "\x M M'. \(x):M \ \(A)\; M \\<^isub>a* M'\ \ (x):M' \ \(A)\" by fact + have ih3: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih4: "\x M M'. \(x):M \ \(B)\; M \\<^isub>a* M'\ \ (x):M' \ \(B)\" by fact + { case 1 + have asm: "M \\<^isub>a* M'" by fact + have ":M \ \\" by fact + then have ":M \ NEGc (A OR B) (\(A OR B)\)" by simp + then have ":M \ AXIOMSc (A OR B) \ BINDINGc (A OR B) (\(A OR B)\) + \ ORRIGHT1 (A OR B) (\\) \ ORRIGHT2 (A OR B) (\\)" by simp + moreover + { assume ":M \ AXIOMSc (A OR B)" + then have ":M' \ AXIOMSc (A OR B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume ":M \ BINDINGc (A OR B) (\(A OR B)\)" + then have ":M' \ BINDINGc (A OR B) (\(A OR B)\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume ":M \ ORRIGHT1 (A OR B) (\\)" + then obtain a' N' where eq: "M = OrR1 .N' a" + and fic: "fic (OrR1 .N' a) a" and imp1: ":N' \ \\" + using ORRIGHT1_elim by blast + from eq asm obtain N'' where eq': "M' = OrR1 .N'' a" and red1: "N' \\<^isub>a* N''" + using a_star_redu_OrR1_elim by blast + from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce) + moreover + from imp1 red1 have ":N'' \ \\" using ih1 by simp + ultimately have ":M' \ ORRIGHT1 (A OR B) (\\)" using eq' by (simp, blast) + } + moreover + { assume ":M \ ORRIGHT2 (A OR B) (\\)" + then obtain a' N' where eq: "M = OrR2 .N' a" + and fic: "fic (OrR2 .N' a) a" and imp1: ":N' \ \\" + using ORRIGHT2_elim by blast + from eq asm obtain N'' where eq': "M' = OrR2 .N'' a" and red1: "N' \\<^isub>a* N''" + using a_star_redu_OrR2_elim by blast + from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce) + moreover + from imp1 red1 have ":N'' \ \\" using ih3 by simp + ultimately have ":M' \ ORRIGHT2 (A OR B) (\\)" using eq' by (simp, blast) + } + ultimately have ":M' \ AXIOMSc (A OR B) \ BINDINGc (A OR B) (\(A OR B)\) + \ ORRIGHT1 (A OR B) (\\) \ ORRIGHT2 (A OR B) (\\)" by blast + then have ":M' \ NEGc (A OR B) (\(A OR B)\)" by simp + then show ":M' \ (\\)" using NEG_simp by blast + next + case 2 + have asm: "M \\<^isub>a* M'" by fact + have "(x):M \ \(A OR B)\" by fact + then have "(x):M \ NEGn (A OR B) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (A OR B) \ BINDINGn (A OR B) (\\) + \ ORLEFT (A OR B) (\(A)\) (\(B)\)" by simp + moreover + { assume "(x):M \ AXIOMSn (A OR B)" + then have "(x):M' \ AXIOMSn (A OR B)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume "(x):M \ BINDINGn (A OR B) (\\)" + then have "(x):M' \ BINDINGn (A OR B) (\\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume "(x):M \ ORLEFT (A OR B) (\(A)\) (\(B)\)" + then obtain y' T' z' N' where eq: "M = OrL (y').T' (z').N' x" + and fin: "fin (OrL (y').T' (z').N' x) x" + and imp1: "(y'):T' \ \(A)\" and imp2: "(z'):N' \ \(B)\" + by (erule_tac ORLEFT_elim, blast) + from eq asm obtain T'' N'' where eq': "M' = OrL (y').T'' (z').N'' x" + and red1: "T' \\<^isub>a* T''" and red2: "N' \\<^isub>a* N''" + using a_star_redu_OrL_elim by blast + from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce) + moreover + from imp1 red1 have "(y'):T'' \ \(A)\" using ih2 by simp + moreover + from imp2 red2 have "(z'):N'' \ \(B)\" using ih4 by simp + ultimately have "(x):M' \ ORLEFT (A OR B) (\(A)\) (\(B)\)" using eq' by (simp, blast) + } + ultimately have "(x):M' \ AXIOMSn (A OR B) \ BINDINGn (A OR B) (\\) + \ ORLEFT (A OR B) (\(A)\) (\(B)\)" by blast + then have "(x):M' \ NEGn (A OR B) (\\)" by simp + then show "(x):M' \ (\(A OR B)\)" using NEG_simp by blast + } +next + case (NOT A) + have ih1: "\a M M'. \:M \ \\; M \\<^isub>a* M'\ \ :M' \ \\" by fact + have ih2: "\x M M'. \(x):M \ \(A)\; M \\<^isub>a* M'\ \ (x):M' \ \(A)\" by fact + { case 1 + have asm: "M \\<^isub>a* M'" by fact + have ":M \ \\" by fact + then have ":M \ NEGc (NOT A) (\(NOT A)\)" by simp + then have ":M \ AXIOMSc (NOT A) \ BINDINGc (NOT A) (\(NOT A)\) + \ NOTRIGHT (NOT A) (\(A)\)" by simp + moreover + { assume ":M \ AXIOMSc (NOT A)" + then have ":M' \ AXIOMSc (NOT A)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume ":M \ BINDINGc (NOT A) (\(NOT A)\)" + then have ":M' \ BINDINGc (NOT A) (\(NOT A)\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume ":M \ NOTRIGHT (NOT A) (\(A)\)" + then obtain y' N' where eq: "M = NotR (y').N' a" + and fic: "fic (NotR (y').N' a) a" and imp: "(y'):N' \ \(A)\" + using NOTRIGHT_elim by blast + from eq asm obtain N'' where eq': "M' = NotR (y').N'' a" and red: "N' \\<^isub>a* N''" + using a_star_redu_NotR_elim by blast + from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce) + moreover + from imp red have "(y'):N'' \ \(A)\" using ih2 by simp + ultimately have ":M' \ NOTRIGHT (NOT A) (\(A)\)" using eq' by (simp, blast) + } + ultimately have ":M' \ AXIOMSc (NOT A) \ BINDINGc (NOT A) (\(NOT A)\) + \ NOTRIGHT (NOT A) (\(A)\)" by blast + then have ":M' \ NEGc (NOT A) (\(NOT A)\)" by simp + then show ":M' \ (\\)" using NEG_simp by blast + next + case 2 + have asm: "M \\<^isub>a* M'" by fact + have "(x):M \ \(NOT A)\" by fact + then have "(x):M \ NEGn (NOT A) (\\)" using NEG_simp by blast + then have "(x):M \ AXIOMSn (NOT A) \ BINDINGn (NOT A) (\\) + \ NOTLEFT (NOT A) (\\)" by simp + moreover + { assume "(x):M \ AXIOMSn (NOT A)" + then have "(x):M' \ AXIOMSn (NOT A)" using asm by (simp only: AXIOMS_preserved) + } + moreover + { assume "(x):M \ BINDINGn (NOT A) (\\)" + then have "(x):M' \ BINDINGn (NOT A) (\\)" using asm by (simp only: BINDING_preserved) + } + moreover + { assume "(x):M \ NOTLEFT (NOT A) (\\)" + then obtain a' N' where eq: "M = NotL .N' x" + and fin: "fin (NotL .N' x) x" and imp: ":N' \ \\" + by (erule_tac NOTLEFT_elim, blast) + from eq asm obtain N'' where eq': "M' = NotL .N'' x" and red1: "N' \\<^isub>a* N''" + using a_star_redu_NotL_elim by blast + from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce) + moreover + from imp red1 have ":N'' \ \\" using ih1 by simp + ultimately have "(x):M' \ NOTLEFT (NOT A) (\\)" using eq' by (simp, blast) + } + ultimately have "(x):M' \ AXIOMSn (NOT A) \ BINDINGn (NOT A) (\\) + \ NOTLEFT (NOT A) (\\)" by blast + then have "(x):M' \ NEGn (NOT A) (\\)" by simp + then show "(x):M' \ (\(NOT A)\)" using NEG_simp by blast + } +qed + +lemma CANDs_preserved_single: + shows ":M \ \\ \ M \\<^isub>a M' \ :M' \ \\" + and "(x):M \ \(B)\ \ M \\<^isub>a M' \ (x):M' \ \(B)\" +by (auto simp add: a_starI CANDs_preserved) + +lemma fic_CANDS: + assumes a: "\fic M a" + and b: ":M \ \\" + shows ":M \ AXIOMSc B \ :M \ BINDINGc B (\(B)\)" +using a b +apply(nominal_induct B rule: ty.strong_induct) +apply(simp) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ctrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(auto simp add: calc_atm)[1] +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ctrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(a,c)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ctrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ctrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) +apply(simp add: calc_atm) +done + +lemma fin_CANDS_aux: + assumes a: "\fin M x" + and b: "(x):M \ (NEGn B (\\))" + shows "(x):M \ AXIOMSn B \ (x):M \ BINDINGn B (\\)" +using a b +apply(nominal_induct B rule: ty.strong_induct) +apply(simp) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ntrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(auto simp add: calc_atm)[1] +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ntrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ntrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(x,z)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +apply(simp) +apply(erule disjE) +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto simp add: ntrm.inject)[1] +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(erule conjE)+ +apply(simp) +apply(drule_tac pi="[(x,y)]" in fin.eqvt(1)) +apply(simp add: calc_atm) +done + +lemma fin_CANDS: + assumes a: "\fin M x" + and b: "(x):M \ (\(B)\)" + shows "(x):M \ AXIOMSn B \ (x):M \ BINDINGn B (\\)" +apply(rule fin_CANDS_aux) +apply(rule a) +apply(rule NEG_elim) +apply(rule b) +done + +lemma BINDING_implies_CAND: + shows ":M \ BINDINGc B (\(B)\) \ :M \ (\\)" + and "(x):N \ BINDINGn B (\\) \ (x):N \ (\(B)\)" +apply - +apply(nominal_induct B rule: ty.strong_induct) +apply(auto) +apply(rule NEG_intro) +apply(nominal_induct B rule: ty.strong_induct) +apply(auto) +done + +end