| products/sources/formale sprachen/Isabelle/HOL/Nominal/Examples/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: xq.xml Sprache: IsabelleOriginal von: Isabelle© |
|
||||||
|
theory Class2
imports Class1 begin text \<open>Reduction\<close> lemma fin_not_Cut: assumes a: "fin M x" shows "\ using a by (induct) (auto) lemma fresh_not_fin: assumes a: "x\ shows "\ proof - have "fin M x \ with a show "\ qed lemma fresh_not_fic: assumes a: "a\ shows "\ proof - have "fic M a \ with a show "\ qed lemma c_redu_subst1: assumes a: "M \ 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 \ shows "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 \ shows "M{y:= using a proof - obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule f obtain c'::"coname" where fs2: "c'\<sharp>(M,M',P,P,c)" by (rule exists_fresh(2), rule f 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 "\ 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 "\ 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 \ shows "M{c:=(y).P} \ using a proof - obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule f obtain c'::"coname" where fs2: "c'\<sharp>(M,M',P,P,c)" by (rule exists_fresh(2), rule f have "M{c:=(y).P} = ([(c',c)]\ 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 "\ 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 "\ 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' \ shows "M \ using a by simp lemma aux2: assumes a: "M \ shows "M \ using a by simp lemma aux3: assumes a: "M = M'" "M' \ shows "M \ using a by simp lemma aux4: assumes a: "M = M'" shows "M \ using a by blast lemma l_redu_subst1: assumes a: "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 a_star_trans) apply(rule a_starI) apply(rule al_redu) apply(rule l_redu.intros) apply(simp add: subst_fresh) apply(simp add: fresh_atm) apply(rule fic_subst2) apply(simp_all) apply(rule aux4) apply(rule subst_comm') apply(simp_all) done next case LAxL then show ?case apply - apply(rule aux3) apply(rule better_Cut_substn) apply(simp add: abs_fresh) apply(simp) apply(simp add: trm.inject fresh_atm) apply(auto) apply(rule aux4) apply(rule sym) apply(rule fin_substn_nrename) apply(simp_all) apply(rule a_starI) apply(rule al_redu) apply(rule aux2) apply(rule l_redu.intros) apply(simp add: subst_fresh) apply(simp add: fresh_atm) apply(rule fin_subst1) apply(simp_all) apply(rule subst_comm') apply(simp_all) done next case (LNot v M N u a b) then show ?case proof - { assume asm: "N\ have "(Cut .NotR (u).M a (v).NotL .N v){y:= (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ by (auto intro: l_redu.intros simp add: subst_fresh) also have "\ 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 <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "\ by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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\ have "(Cut .AndR Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LAnd1 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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\ have "(Cut .AndR Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LAnd2 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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\ have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:= Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LOr1 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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\ have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:= Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LOr2 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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\ have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z" using LImp by (simp add: fresh_prod abs_fresh fresh_atm) also have "\ 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 "\ by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .ImpR (x)..M b (z).ImpL (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" by simp } moreover { assume asm: "N=Ax y d" have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "\ 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 "\ using LImp asm by simp also have "\ 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 "\ then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutL) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(simp add: subst_with_ax2) done qed also have "\ 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 <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" by simp } ultimately show ?thesis by blast qed qed lemma l_redu_subst2: assumes a: "M \ shows "M{c:=(y).P} \ using a proof(nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct) case LAxR then show ?case apply - apply(rule aux3) apply(rule better_Cut_substc) apply(simp add: abs_fresh) apply(simp add: abs_fresh) apply(simp add: trm.inject fresh_atm) apply(auto) apply(rule aux4) apply(rule sym) apply(rule fic_substc_crename) apply(simp_all) apply(rule a_starI) apply(rule al_redu) apply(rule aux2) apply(rule l_redu.intros) apply(simp add: subst_fresh) apply(simp add: fresh_atm) apply(rule fic_subst1) apply(simp_all) apply(rule subst_comm') apply(simp_all) done next case LAxL then show ?case apply - apply(rule aux3) apply(rule better_Cut_substc) apply(simp) apply(simp add: abs_fresh) apply(simp add: fresh_atm) apply(auto) apply(rule aux4) apply(simp add: trm.inject alpha calc_atm fresh_atm) apply(rule a_star_trans) apply(rule a_starI) apply(rule al_redu) apply(rule l_redu.intros) apply(simp add: subst_fresh) apply(simp add: fresh_atm) apply(rule fin_subst2) apply(simp_all) apply(rule aux4) apply(rule subst_comm') apply(simp_all) done next case (LNot v M N u a b) then show ?case proof - { assume asm: "M\ have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} = (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ by (auto intro: l_redu.intros simp add: subst_fresh) also have "\ by (simp add: subst_fresh abs_fresh fresh_atm) finally have ?thesis by auto } moreover { assume asm: "M=Ax u c" have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} = (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ apply - apply(rule a_starI) apply(rule al_redu) apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh) done also have "\ by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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} \ 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\ have "(Cut .AndR Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LAnd1 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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\ have "(Cut .AndR Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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 <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LAnd2 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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\ have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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} \ by simp } moreover { assume asm: "N1=Ax x1 c" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LOr1 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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} \ 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\ have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ 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} \ by simp } moreover { assume asm: "N2=Ax x2 c" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm) also have "\ 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 "\ using LOr2 asm by simp also have "\ 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 "\ then show ?thesis apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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} \ 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\ have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: fresh_prod abs_fresh fresh_atm) also have "\ 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 "\ by (simp add: subst_fresh abs_fresh fresh_atm) finally have "(Cut .ImpR (x)..M b (z).ImpL (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" by simp } moreover { assume asm: "M=Ax x c \ have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "\ 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 "\ using LImp asm by simp also have "\ proof (cases "fin P y") case True assume "fin P y" then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) apply(simp) done next case False assume "\ then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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 <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" by simp } moreover { assume asm: "M\ have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "\ 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 "\ using LImp asm by simp also have "\ 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 "\ then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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 <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" by simp } moreover { assume asm: "M=Ax x c \ have "(Cut .ImpR (x)..M b (z).ImpL Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod) also have "\ 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 "\ using LImp asm by simp also have "\ 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 "\ then show ?thesis using LImp apply - apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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 "\ then show ?thesis using LImp apply - apply(rule a_star_CutL) apply(rule a_star_CutR) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(simp add: subst_with_ax1) done qed also have "\ 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 <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" by simp } ultimately show ?thesis by blast qed qed lemma a_redu_subst1: assumes a: "M \ 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 a_star_trans) apply(rule a_star_CutL) apply(assumption) apply(rule a_star_trans) apply(rule_tac M'="P[c\ apply(case_tac "fic P c") apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxR_intro) apply(simp) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_left) apply(simp) apply(rule subst_with_ax2) apply(rule aux4) apply(simp add: trm.inject) apply(simp add: alpha fresh_atm) apply(simp add: crename_swap) apply(rule impI) apply(rule a_star_CutL) apply(auto) done next case (a_Cut_r a N x M M' y c P) then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_CutR) apply(auto)[1] apply(rule a_star_CutR) apply(auto)[1] done next case a_NotL then show ?case apply(auto) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_NotL) apply(auto)[1] apply(rule a_star_NotL) apply(auto)[1] done next case a_NotR then show ?case apply(auto) apply(rule a_star_NotR) apply(auto)[1] done next case a_AndR_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_AndR) apply(auto) done next case a_AndR_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_AndR) apply(auto) done next case a_AndL1 then show ?case apply(auto) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_AndL1) apply(auto)[1] apply(rule a_star_AndL1) apply(auto)[1] done next case a_AndL2 then show ?case apply(auto) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_AndL2) apply(auto)[1] apply(rule a_star_AndL2) apply(auto)[1] done next case a_OrR1 then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_OrR1) apply(auto) done next case a_OrR2 then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_OrR2) apply(auto) done next case a_OrL_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_OrL) apply(auto) apply(rule a_star_OrL) apply(auto) done next case a_OrL_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_OrL) apply(auto) apply(rule a_star_OrL) apply(auto) done next case a_ImpR then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_ImpR) apply(auto) done next case a_ImpL_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_ImpL) apply(auto) apply(rule a_star_ImpL) apply(auto) done next case a_ImpL_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "name") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutR) apply(rule a_star_ImpL) apply(auto) apply(rule a_star_ImpL) apply(auto) done qed lemma a_redu_subst2: assumes a: "M \ shows "M{c:=(y).P} \ using a proof(nominal_induct avoiding: y c P rule: a_redu.strong_induct) case al_redu then show ?case by (simp only: l_redu_subst2) next case ac_redu then show ?case apply - apply(rule a_starI) apply(rule a_redu.ac_redu) apply(simp only: c_redu_subst2') done next case (a_Cut_r a N x M M' y c P) then show ?case apply(simp add: subst_fresh fresh_a_redu) apply(rule conjI) apply(rule impI)+ apply(simp) apply(drule ax_do_not_a_reduce) apply(simp) apply(rule impI) apply(rule conjI) apply(rule impI) apply(simp) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="P" in meta_spec) apply(simp) apply(rule a_star_trans) apply(rule a_star_CutR) apply(assumption) apply(rule a_star_trans) apply(rule_tac N'="P[y\ apply(case_tac "fin P y") apply(rule a_starI) apply(rule al_redu) apply(rule better_LAxL_intro) apply(simp) apply(rule a_star_trans) apply(rule a_starI) apply(rule ac_redu) apply(rule better_right) apply(simp) apply(rule subst_with_ax1) apply(rule aux4) apply(simp add: trm.inject) apply(simp add: alpha fresh_atm) apply(simp add: nrename_swap) apply(rule impI) apply(rule a_star_CutR) apply(auto) done next case (a_Cut_l a N x M M' y c P) then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_CutL) apply(auto)[1] apply(rule a_star_CutL) apply(auto)[1] done next case a_NotR then show ?case apply(auto) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_NotR) apply(auto)[1] apply(rule a_star_NotR) apply(auto)[1] done next case a_NotL then show ?case apply(auto) apply(rule a_star_NotL) apply(auto)[1] done next case a_AndR_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_AndR) apply(auto) apply(rule a_star_AndR) apply(auto) done next case a_AndR_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_AndR) apply(auto) apply(rule a_star_AndR) apply(auto) done next case a_AndL1 then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_AndL1) apply(auto) done next case a_AndL2 then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_AndL2) apply(auto) done next case a_OrR1 then show ?case apply(auto) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_OrR1) apply(auto)[1] apply(rule a_star_OrR1) apply(auto)[1] done next case a_OrR2 then show ?case apply(auto) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_OrR2) apply(auto)[1] apply(rule a_star_OrR2) apply(auto)[1] done next case a_OrL_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_OrL) apply(auto) done next case a_OrL_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_OrL) apply(auto) done next case a_ImpR then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(generate_fresh "coname") apply(fresh_fun_simp) apply(fresh_fun_simp) apply(simp add: subst_fresh) apply(rule a_star_CutL) apply(rule a_star_ImpR) apply(auto) apply(rule a_star_ImpR) apply(auto) done next case a_ImpL_l then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_ImpL) apply(auto) done next case a_ImpL_r then show ?case apply(auto simp add: subst_fresh fresh_a_redu) apply(rule a_star_ImpL) apply(auto) done qed lemma a_star_subst1: assumes a: "M \ 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 \ shows "M{c:=(y).P} \ using a apply(induct) apply(blast) apply(drule_tac y="y" and c="c" and P="P" in a_redu_subst2) apply(auto) done text \<open>Candidates and SN\<close> text \<open>SNa\<close> inductive SNa :: "trm \ where SNaI: "(\ lemma SNa_induct[consumes 1]: assumes major: "SNa M" assumes hyp: "\ 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: "\ (\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> SNa y) \<Longrightarrow> (\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> P y z) \<Longrightarrow> (\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> SNa u) \<Longrightarrow> (\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> P x u) \<Longrightarrow> P x z" shows "P a b" proof - from a_SNa have r: "\ 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: "\ apply(rule_tac double_SNa_aux) apply(assumption)+ apply(blast) done lemma a_preserves_SNa: assumes a: "SNa M" "M\ shows "SNa M'" using a by (erule_tac SNa.cases) (simp) lemma a_star_preserves_SNa: assumes a: "SNa M" and b: "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)]\ apply(simp add: a_redu.eqvt) apply(subgoal_tac "NotL .([(a,aa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="NotR (x).([(x,xa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="AndL1 x.([(x,xa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="AndL2 x.([(x,xa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="OrR1 .([(a,aa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="OrR2 .([(a,aa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="ImpR (x)..([(a,aa)]\ apply(simp add: trm.inject alpha fresh_a_redu) apply(simp) apply(rotate_tac 1) apply(drule_tac x="[(x,xa)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="ImpR (x)..([(x,xa)]\ 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)]\ apply(simp add: a_redu.eqvt) apply(rule_tac s="ImpR (x)..([(a,aa)]\ apply(simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm) apply(simp add: fresh_left calc_atm fresh_a_redu) apply(simp) done lemma AndR_in_SNa: assumes a: "SNa M" "SNa N" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.110 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
