| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Nominal/Examples/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 236 kB |
|
Quellcode-Bibliothek Class2.thySprache: Isabelle |
|||||||||||||||
|
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 fr 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 fr with a show "¬fic M a" by blast qed lemma c_redu_subst1: assumes a: "M ⟶🪙c M'" "c♯M" "y♯P" shows "M{y:= 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:= 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:= apply(simp) apply(rule c_redu.right) apply(rule not_fin_subst2) apply(simp) apply(rule subst_fresh) apply(simp add: abs_fresh) apply(simp add: abs_fresh) apply(rule sym) apply(rule interesting_subst1') apply(simp add: fresh_atm) apply(simp) apply(simp) (* case M \<noteq> Ax y a*) apply(rule impI) apply(subgoal_tac "N{x:=.M}{y:= 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 ⟶🪙c M'" "c♯P" "y♯M" shows "M{c:=(y).P} ⟶🪙c M'{c:=(y).P}" using a proof(nominal_induct avoiding: y c P rule: c_redu.strong_induct) case (right N x a M) then show ?case apply - apply(simp) apply(rule conjI) apply(force) apply(auto) apply(subgoal_tac "N{x:=.M}{c:=(y).P} = N{c:=(y).P}{x:=.(M{c:=(y).P})}")(*A*) apply(simp) apply(rule c_redu.intros) apply(rule not_fin_subst1) apply(simp) apply(simp add: subst_fresh) apply(simp add: subst_fresh) apply(simp add: abs_fresh fresh_atm) apply(rule subst_subst1) apply(simp add: fresh_prod fresh_atm) apply(simp add: fresh_prod fresh_atm) apply(simp add: fresh_prod fresh_atm) apply(simp) done next case (left M a N x) then show ?case apply - apply(simp) apply(rule conjI) (* case N = Ax x c *) apply(rule impI) apply(subgoal_tac "M{a:=(x).Ax x c}{c:=(y).P} = M{c:=(y).P}{a:=(y).P}") apply(simp) apply(rule c_redu.left) apply(rule not_fic_subst2) apply(simp) apply(simp) apply(rule subst_fresh) apply(simp add: abs_fresh) apply(rule sym) apply(rule interesting_subst2') apply(simp add: fresh_atm) apply(simp) apply(simp) (* case M \<noteq> Ax y a*) apply(rule impI) apply(subgoal_tac "M{a:=(x).N}{c:=(y).P} = M{c:=(y).P}{a:=(x).(N{c:=(y).P})}") apply(simp) apply(rule c_redu.left) apply(rule not_fic_subst2) apply(simp) apply(simp add: subst_fresh) apply(simp add: subst_fresh) apply(simp add: abs_fresh fresh_atm) apply(rule subst_subst4) apply(simp add: fresh_prod fresh_atm) apply(simp add: fresh_prod fresh_atm) apply(simp add: fresh_prod fresh_atm) apply(simp add: fresh_prod fresh_atm) apply(simp) done qed lemma c_redu_subst1': assumes a: "M ⟶🪙c M'" shows "M{y:= using a proof - obtain y'::"name" where fs1: "y'♯(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, bl obtain c'::"coname" where fs2: "c'♯(M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, have "M{y:= 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 "… ⟶🪙c ([(y',y)]∙M'){y':= 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:= 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 ⟶🪙c M'" shows "M{c:=(y).P} ⟶🪙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, bl obtain c'::"coname" where fs2: "c'♯(M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, 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 "… ⟶🪙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' ⟶🪙l M''" shows "M ⟶🪙l M''" using a by simp lemma aux2: assumes a: "M ⟶🪙l M'" "M' = M''" shows "M ⟶🪙l M''" using a by simp lemma aux3: assumes a: "M = M'" "M' ⟶🪙a* M''" shows "M ⟶🪙a* M''" using a by simp lemma aux4: assumes a: "M = M'" shows "M ⟶🪙a* M'" using a by blast lemma l_redu_subst1: assumes a: "M ⟶🪙l M'" shows "M{y:= 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 rtranclp_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:= (Cut .NotR (u).(M{y:= by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙l (Cut .(N{y:= by (auto intro: l_redu.intros simp add: subst_fresh) also have "… = (Cut .N (u).M){y:= 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:= (Cut .NotR (u).(M{y:= by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* (Cut .(N{y:= 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 by simp also have "… ⟶🪙a* (Cut .(P[c⊨c>b]) (u).(M{y:= proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LNot apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis apply - apply(rule a_star_CutL) apply(rule rtranclp_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:= 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:= 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 Cut .AndR using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .AndR by simp } moreover { assume asm: "M1=Ax y a1" have "(Cut .AndR Cut .AndR using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut using LAnd1 asm by simp also have "… ⟶🪙a* Cut proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LAnd1 apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis apply - apply(rule a_star_CutL) apply(rule rtranclp_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 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 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 Cut .AndR using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .AndR by simp } moreover { assume asm: "M2=Ax y a2" have "(Cut .AndR Cut .AndR using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut using LAnd2 asm by simp also have "… ⟶🪙a* Cut proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LAnd2 asm apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis apply - apply(rule a_star_CutL) apply(rule rtranclp_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 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 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:= Cut .OrR1 .(M{y:= using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{y:= using LOr1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .M (x1).N1){y:= by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:= by simp } moreover { assume asm: "M=Ax y a" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:= Cut .OrR1 .(M{y:= using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{y:= using LOr1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LOr1 asm by simp also have "… ⟶🪙a* Cut .P[c⊨c>a] (x1).(N1{y:= proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LOr1 apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis apply - apply(rule a_star_CutL) apply(rule rtranclp_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:= 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:= 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:= Cut .OrR2 .(M{y:= using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{y:= using LOr2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .M (x2).N2){y:= by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:= by simp } moreover { assume asm: "M=Ax y a" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:= Cut .OrR2 .(M{y:= using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{y:= using LOr2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LOr2 asm by simp also have "… ⟶🪙a* Cut .P[c⊨c>a] (x2).(N2{y:= proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LOr2 apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis apply - apply(rule a_star_CutL) apply(rule rtranclp_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:= 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:= 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 Cut .ImpR (x)..(M{y:= using LImp by (simp add: fresh_prod abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .(Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .ImpR (x)..M b (z).ImpL (Cut .(Cut by simp } moreover { assume asm: "N=Ax y d" have "(Cut .ImpR (x)..M b (z).ImpL Cut .ImpR (x)..(M{y:= using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LImp asm by simp also have "… ⟶🪙a* Cut .(Cut proof (cases "fic P c") case True assume "fic P c" then show ?thesis using LImp apply - apply(rule a_starI) apply(rule better_CutL_intro) apply(rule a_Cut_l) apply(simp add: subst_fresh abs_fresh) apply(simp add: abs_fresh fresh_atm) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) done next case False assume "¬fic P c" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutL) apply(rule rtranclp_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 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 (Cut .(Cut by simp } ultimately show ?thesis by blast qed qed lemma l_redu_subst2: assumes a: "M ⟶🪙l M'" shows "M{c:=(y).P} ⟶🪙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 rtranclp_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 LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙l (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot by (auto intro: l_redu.intros simp add: subst_fresh) also have "… = (Cut .N (u).M){c:=(y).P}" using LNot asm by (simp add: subst_fresh abs_fresh fresh_atm) finally have ?thesis by auto } moreover { assume asm: "M=Ax u c" have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} = (Cut .NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .(N{c:=(y).P}) (u).(Cut by simp also have "… ⟶🪙a* (Cut .(N{c:=(y).P}) (u).(P[y⊨n>u]))" proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LNot apply - apply(rule a_starI) apply(rule better_CutR_intro) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis apply - apply(rule a_star_CutR) apply(rule rtranclp_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "… = (Cut .N (u).M){c:=(y).P}" using LNot asm apply - apply(auto simp add: subst_fresh abs_fresh) apply(simp add: trm.inject) apply(simp add: alpha fresh_atm) apply(rule sym) apply(rule nrename_swap) apply(simp) done finally have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} ⟶🪙a* (Cut .N (u).M){c:= 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 Cut .AndR using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .AndR by simp } moreover { assume asm: "N=Ax u c" have "(Cut .AndR Cut .AndR using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut using LAnd1 asm by simp also have "… ⟶🪙a* Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LAnd1 apply - apply(rule a_starI) apply(rule better_CutR_intro) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis apply - apply(rule a_star_CutR) apply(rule rtranclp_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 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 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 Cut .AndR using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .AndR by simp } moreover { assume asm: "N=Ax u c" have "(Cut .AndR Cut .AndR using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut using LAnd2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut using LAnd2 asm by simp also have "… ⟶🪙a* Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LAnd2 apply - apply(rule a_starI) apply(rule better_CutR_intro) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis apply - apply(rule a_star_CutR) apply(rule rtranclp_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 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 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 LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" using LOr1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asm by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶🪙a* (Cut .M (x1).N1) 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 LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" using LOr1 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(M{c:=(y).P}) (x1).(Cut using LOr1 asm by simp also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x1).(P[y⊨n>x1])" proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LOr1 apply - apply(rule a_starI) apply(rule better_CutR_intro) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis apply - apply(rule a_star_CutR) apply(rule rtranclp_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "… = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asm apply - apply(auto simp add: subst_fresh abs_fresh) apply(simp add: trm.inject) apply(simp add: alpha fresh_atm) apply(rule sym) apply(rule nrename_swap) apply(simp) done finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶🪙a* (Cut .M (x1).N1) 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 LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" using LOr2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asm by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶🪙a* (Cut .M (x2).N2) 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 LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" using LOr2 apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(M{c:=(y).P}) (x2).(Cut using LOr2 asm by simp also have "… ⟶🪙a* Cut .(M{c:=(y).P}) (x2).(P[y⊨n>x2])" proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LOr2 apply - apply(rule a_starI) apply(rule better_CutR_intro) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis apply - apply(rule a_star_CutR) apply(rule rtranclp_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "… = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asm apply - apply(auto simp add: subst_fresh abs_fresh) apply(simp add: trm.inject) apply(simp add: alpha fresh_atm) apply(rule sym) apply(rule nrename_swap) apply(simp) done finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶🪙a* (Cut .M (x2).N2) 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 Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL using LImp by (simp add: fresh_prod abs_fresh fresh_atm) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = (Cut .(Cut by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .ImpR (x)..M b (z).ImpL (Cut .(Cut by simp } moreover { assume asm: "M=Ax x c ∧ Q≠Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LImp asm by simp also have "… ⟶🪙a* Cut .(Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule rtranclp_trans) apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) apply(simp) done next case False assume "¬fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule rtranclp_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 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 (Cut .(Cut by simp } moreover { assume asm: "M≠Ax x c ∧ Q=Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LImp asm by simp also have "… ⟶🪙a* Cut .(Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule rtranclp_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 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 (Cut .(Cut by simp } moreover { assume asm: "M=Ax x c ∧ Q=Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "… ⟶🪙a* Cut .(Cut using LImp apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "… = Cut .(Cut using LImp asm by simp also have "… ⟶🪙a* Cut .(Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule rtranclp_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 "… ⟶🪙a* Cut .(Cut proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) done next case False assume "¬fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule rtranclp_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 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 (Cut .(Cut by simp } ultimately show ?thesis by blast qed qed lemma a_redu_subst1: assumes a: "M ⟶🪙a M'" shows "M{y:= 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 rtranclp_trans) apply(rule a_star_CutL) apply(assumption) apply(rule rtranclp_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 rtranclp_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 ⟶🪙a M'" shows "M{c:=(y).P} ⟶🪙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 rtranclp_trans) apply(rule a_star_CutR) apply(assumption) apply(rule rtranclp_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 rtranclp_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 ⟶🪙a* M'" shows "M{y:= 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 ⟶🪙a* M'" shows "M{c:=(y).P} ⟶🪙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 ⟶🪙a M' ==> SNa M') ==> SNa M" lemma SNa_induct[consumes 1]: assumes major: "SNa M" assumes hyp: "∧M'. SNa M' ==> (∀M''. M'⟶🪙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⟶🪙a y ==> SNa y) ==> (∧y. x⟶🪙a y ==> P y z) ==> (∧u. z⟶🪙a u ==> SNa u) ==> (∧u. z⟶🪙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⟶🪙ay ⟶ P y z) ∧ (∀u. z⟶🪙a u ⟶ P x u)) ⟶ P x z] == apply(rule_tac double_SNa_aux) apply(assumption)+ apply(blast) done lemma a_preserves_SNa: assumes a: "SNa M" "M⟶🪙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⟶🪙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 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_def) 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_def) 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_def) 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_def) 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 = { 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_def) 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)∙( 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_def) 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)∙( 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) 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_def) 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_def) 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) 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_def) 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_def) 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) 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_def) 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_def) 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_def) 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_def) 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_def) 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_def) 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) ∧ 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 apply(auto simp add: perm_set_def) 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=" 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 apply(auto simp add: perm_set_def) 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=" 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_def) 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_def) 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 ∘ NEG | "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(fastforce simp add: ty.inject) done termination apply(relation "measure (case_sum (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_def) 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)∙ 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)∙ 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 bl 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 A ∪ (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) (∥ and "NEGc (C IMP D) (∥(C IMP D)∥) = AXIOMSc (C IMP D) ∪ BINDINGc (C IMP D) (∥(C I ∪ (IMPRIGHT (C IMP D) (∥(C)∥) (∥ 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_def) 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_def) 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) 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) 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) apply(simp only: NEGc.simps NEGn.simps) apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTL 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_n } 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) 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) 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) apply(simp only: NEGc.simps NEGn.simps) apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPL 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) 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) 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) 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) apply(simp only: NEGc.simps NEGn.simps) apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_cona 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) apply(simp only: NEGc.simps NEGn.simps) apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_cona 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) apply(simp only: NEGc.simps NEGn.simps) apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_cona 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. ( 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' ∈ (∥( 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)]∙Ma" 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 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)]∙Ma" 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 and " 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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=" 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)]∙Ma" 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_ 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_ 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)]∙Ma" 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_ 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)]∙Ma" 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_ 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)]∙Ma" 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_i 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)]∙Ma" 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_ 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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' ∈ ( using a [[ hypsubst_thin = true ]] 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' ∈ ( using a [[ hypsubst_thin = true ]] 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 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)]∙Ma" 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)]∙Ma" 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)]∙Ma" 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)]∙Ma" 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 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)]∙Ma" 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)]∙Ma" 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)]∙Ma" 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)]∙Ma" 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)]∙Ma" 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_in 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)]∙Ma" 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_in 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)]∙Ma" 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_in 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)]∙Ma" 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_in 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)]∙Ma" 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_ 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)]∙Ma" 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_i 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)]∙Ma" 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_in 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)]∙Ma" 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_in 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_i 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)]∙Ma" 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_in 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)]∙Ma" 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_i 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)]∙Ma" 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_in 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)]∙Ma" 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_in 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)]∙Ma" 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_in apply(simp add: calc_atm CAND_eqvt_name) apply(simp) done lemma IMPRIGHT_elim: assumes a: ":M ∈ IMPRIGHT (B IMP C) (∥(B)∥) (∥ obtains x' a' M' where "M = ImpR (x'). and "∀z P. x'♯(z,P) ∧ (z):P ∈ ∥(C)∥ ⟶ (x'):(M'{a':=(z).P}) ∈ ∥(B)∥" and "∀c Q. a'♯(c,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)]∙Ma" 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):Ma{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=":Ma{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)]∙Ma" 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):Ma{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=":Ma{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)]∙Ma" 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):Ma{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=" 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)]∙Ma" 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):Ma{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=" 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 and " 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)]∙Ma" 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_in 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)]∙Ma" 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_ 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)]∙Ma" 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=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_ins 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_ 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)]∙Ma" 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_i 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 shows "∃B1 B2. B = B1 AND 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,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname 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 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 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=" 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=" apply(simp add: CAND_eqvt_coname calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(drule_tac pi="[(a,ca)]" and x=" 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=" 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=" apply(simp add: CAND_eqvt_coname calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(drule_tac pi="[(a,ca)]" and x=" 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 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=" 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=" apply(simp add: CAND_eqvt_coname calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(drule_tac pi="[(a,ca)]" and x=" 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=" 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=" apply(simp add: CAND_eqvt_coname calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(drule_tac pi="[(a,ca)]" and x=" 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) ∉ BINDI 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_ apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_ 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_ 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_nam 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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_nam 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 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 apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_ 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_nam 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 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 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_nam 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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 shows "∃B1 B2. B = B1 IMP B2 ∧ :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,y)]" and x=" apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_i apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,y)]" and x=" 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name 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):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_ 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) ∧ 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_pro 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_ 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_co 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_c 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 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 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_c 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_co 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_ 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="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(aa,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(aa,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(x,ca)]" and X="∥ 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_ 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_co 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_c 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 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_co 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_co 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 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_c 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_co 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_ 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="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(ba,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(ba,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(x,ca)]" and X="∥ 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_ 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_co 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_c 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 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_c 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_c 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 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_c 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_co 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_ 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_ 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_co 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_co 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 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_co 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_co 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 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_co 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_co 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_ 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_ 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_co 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_c 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 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_co 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_co 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 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_c 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_co 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_ 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="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(ba,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(aa,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(aa,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(ba,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(x,ca)]" and X="∥ 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="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,aa)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,aa)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(a,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(x,ca)]" and X="∥ 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="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(aa,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(a,ba)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(xa,ca)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(aa,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt) apply(drule_tac pi="[(b,cb)]" and X="∥ apply(simp add: CAND_eqvt_name CAND_eqvt_coname) apply(drule_tac pi="[(x,ca)]" and X="∥ 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 ∈ ∥ 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) (∥ then have "(x):M ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ 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 ∈ (∥ then have ":M ∈ NEGc (NOT B) (∥(NOT B)∥)" by simp then have ":M ∈ AXIOMSc (NOT B) ∪ BINDINGc (NOT B) (∥(NOT B)∥) ∪ NOTRIGHT (NOT B) 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) (∥ then have "(x):M ∈ AXIOMSn (NOT B) ∪ BINDINGn (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 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 and " 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 and " 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 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'). 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'} ⟶🪙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 and " 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 ⟶🪙a* M' ==> :M' ∈ AXIOMSc B" and "(x):M ∈ AXIOMSn B ==> M ⟶🪙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 ⟶🪙a* M' ==> :M' ∈ BINDINGc B (∥(B)∥)" and "(x):M ∈ BINDINGn B (∥∥) ==> M ⟶🪙a* M' ==> (x):M' ∈ BINDINGn B (∥∥)" proof - assume red: "M ⟶🪙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} ⟶🪙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 ⟶🪙a* M'" assume asm: "(x):M ∈ BINDINGn B (∥∥)" { fix c::"coname" and P::"trm" from asm have "( moreover have "M{x:= ultimately have "( } then show "(x):M' ∈ BINDINGn B (∥∥)" by (auto simp add: BINDINGn_def) qed lemma CANDs_preserved: shows ":M ∈ ∥∥ ==> M ⟶🪙a* M' ==> :M' ∈ ∥∥" and "(x):M ∈ ∥(B)∥ ==> M ⟶🪙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 ⟶🪙a* M'" by fact have ":M ∈ ∥ 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' ∈ (∥ next case 2 have asm: "M ⟶🪙a* M'" by fact have "(x):M ∈ ∥(PR X)∥" by fact then have "(x):M ∈ NEGn (PR X) (∥ then have "(x):M ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ 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) (∥ } ultimately have "(x):M' ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ then have "(x):M' ∈ NEGn (PR X) (∥ then show "(x):M' ∈ (∥(PR X)∥)" using NEG_simp by blast } next case (IMP A B) have ih1: "∧a M M'. [:M ∈ ∥∥; M ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih2: "∧x M M'. [(x):M ∈ ∥(A)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(A)∥" by fact have ih3: "∧a M M'. [:M ∈ ∥∥; M ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih4: "∧x M M'. [(x):M ∈ ∥(B)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(B)∥" by fact { case 1 have asm: "M ⟶🪙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_pres } moreover { assume ":M ∈ IMPRIGHT (A IMP B) (∥(A)∥) (∥∥) (∥(B)∥) (∥∥)" then obtain x' a' N' where eq: "M = ImpR (x'). and imp1: "∀z P. x'♯(z,P) ∧ (z):P ∈ ∥(B)∥ ⟶ (x'):(N'{a':=(z).P}) ∈ ∥(A)∥" and imp2: "∀c Q. a'♯(c,Q) ∧ using IMPRIGHT_elim by blast from eq asm obtain N'' where eq': "M' = ImpR (x'). 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)∥" usin 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) ∧ 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 ⟶🪙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 and fin: "fin (ImpL and imp1: " by (erule_tac IMPLEFT_elim, blast) from eq asm obtain T'' N'' where eq': "M' = ImpL and red1: "T' ⟶🪙a* T''" and red2: "N' ⟶🪙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 " 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 ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih2: "∧x M M'. [(x):M ∈ ∥(A)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(A)∥" by fact have ih3: "∧a M M'. [:M ∈ ∥∥; M ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih4: "∧x M M'. [(x):M ∈ ∥(B)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(B)∥" by fact { case 1 have asm: "M ⟶🪙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_pres } moreover { assume ":M ∈ ANDRIGHT (A AND B) (∥∥) (∥∥)" then obtain a' T' b' N' where eq: "M = AndR and fic: "fic (AndR and imp1: " using ANDRIGHT_elim by blast from eq asm obtain T'' N'' where eq': "M' = AndR and red1: "T' ⟶🪙a* T''" and red2: "N' ⟶🪙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 " moreover from imp2 red2 have " 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 ⟶🪙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' ⟶🪙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' ⟶🪙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 ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih2: "∧x M M'. [(x):M ∈ ∥(A)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(A)∥" by fact have ih3: "∧a M M'. [:M ∈ ∥∥; M ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih4: "∧x M M'. [(x):M ∈ ∥(B)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(B)∥" by fact { case 1 have asm: "M ⟶🪙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_preser } moreover { assume ":M ∈ ORRIGHT1 (A OR B) (∥∥)" then obtain a' N' where eq: "M = OrR1 and fic: "fic (OrR1 using ORRIGHT1_elim by blast from eq asm obtain N'' where eq': "M' = OrR1 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 " 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 and fic: "fic (OrR2 using ORRIGHT2_elim by blast from eq asm obtain N'' where eq': "M' = OrR2 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 " 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 ⟶🪙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' ⟶🪙a* T''" and red2: "N' ⟶🪙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 ⟶🪙a* M'] ==> :M' ∈ ∥∥" by fact have ih2: "∧x M M'. [(x):M ∈ ∥(A)∥; M ⟶🪙a* M'] ==> (x):M' ∈ ∥(A)∥" by fact { case 1 have asm: "M ⟶🪙a* M'" by fact have ":M ∈ ∥ 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_preserve } 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' ⟶🪙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' ∈ (∥ next case 2 have asm: "M ⟶🪙a* M'" by fact have "(x):M ∈ ∥(NOT A)∥" by fact then have "(x):M ∈ NEGn (NOT A) (∥ 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) (∥ } moreover { assume "(x):M ∈ NOTLEFT (NOT A) (∥∥)" then obtain a' N' where eq: "M = NotL and fin: "fin (NotL by (erule_tac NOTLEFT_elim, blast) from eq asm obtain N'' where eq': "M' = NotL 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 " 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) (∥ then show "(x):M' ∈ (∥(NOT A)∥)" using NEG_simp by blast } qed lemma CANDs_preserved_single: shows ":M ∈ ∥∥ ==> M ⟶🪙a M' ==> :M' ∈ ∥∥" and "(x):M ∈ ∥(B)∥ ==> M ⟶🪙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 " 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.347Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-03) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26