# HG changeset patch # User paulson # Date 1721490424 -3600 # Node ID 1effd04264ccc571794657176e3ad5bf96085224 # Parent ffef122946a301cd28f3d933cd891d09e9ebd98d Got rid of another 250 apply-lines diff -r ffef122946a3 -r 1effd04264cc src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Fri Jul 19 22:29:32 2024 +0100 +++ b/src/HOL/Nominal/Examples/Class1.thy Sat Jul 20 16:47:04 2024 +0100 @@ -1087,9 +1087,8 @@ lemma forget: shows "x\M \ M{x:=.P} = M" and "c\M \ M{c:=(x).P} = M" -apply(nominal_induct M avoiding: x c P rule: trm.strong_induct) -apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp) -done + by (nominal_induct M avoiding: x c P rule: trm.strong_induct) + (auto simp: fresh_atm abs_fresh abs_supp fin_supp) lemma substc_rename1: assumes a: "c\(M,a)" @@ -2119,108 +2118,51 @@ by simp (metis abs_fresh(1) fin.intros(6) fin_ImpL_elim fresh_prod subst_fresh(5)) qed (use fin_rest_elims in force)+ + lemma fin_substn_nrename: - assumes a: "fin M x" "x\y" "x\P" + assumes "fin M x" "x\y" "x\P" shows "M[x\n>y]{y:=.P} = Cut .P (x).(M{y:=.P})" -using a [[simproc del: defined_all]] -apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct) -apply(drule fin_Ax_elim) -apply(simp) -apply(simp add: trm.inject) -apply(simp add: alpha calc_atm fresh_atm) -apply(simp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_NotL_elim) -apply(simp) -apply(subgoal_tac "\z::name. z\(trm,y,x,P,trm[x\n>y]{y:=.P})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotL) -apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh) -apply(rule conjI) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(rule subst_fresh) -apply(simp) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_AndL1_elim) -apply(simp) -apply(subgoal_tac "\z::name. z\(name2,name1,P,trm[name2\n>y]{y:=.P},y,P,trm)") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL1) -apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh) -apply(rule conjI) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(rule subst_fresh) -apply(simp) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(drule fin_AndL2_elim) -apply(simp) -apply(subgoal_tac "\z::name. z\(name2,name1,P,trm[name2\n>y]{y:=.P},y,P,trm)") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL2) -apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh) -apply(rule conjI) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(rule subst_fresh) -apply(simp) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_OrL_elim) -apply(simp add: abs_fresh) -apply(simp add: subst_fresh rename_fresh) -apply(subgoal_tac "\z::name. z\(name3,name2,name1,P,trm1[name3\n>y]{y:=.P},trm2[name3\n>y]{y:=.P},y,P,trm1,trm2)") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrL) -apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh) -apply(rule conjI) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(drule fin_rest_elims) -apply(simp) -apply(drule fin_ImpL_elim) -apply(simp add: abs_fresh) -apply(simp add: subst_fresh rename_fresh) -apply(subgoal_tac "\z::name. z\(name1,x,P,trm1[x\n>y]{y:=.P},trm2[x\n>y]{y:=.P},y,P,trm1,trm2)") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpL) -apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh) -apply(rule conjI) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(simp add: nsubst_eqvt calc_atm) -apply(simp add: perm_fresh_fresh) -apply(simp add: nrename_fresh) -apply(rule exists_fresh') -apply(rule fin_supp) -done +using assms [[simproc del: defined_all]] +proof (nominal_induct M avoiding: x y c P rule: trm.strong_induct) + case (Ax name coname) + then show ?case + by (metis fin_Ax_elim fresh_atm(1,3) fresh_prod nrename_swap subst_rename(3) substn.simps(1) trm.fresh(1)) +next + case (NotL coname trm name) + obtain z::name where "z \ (trm,y,x,P,trm[x\n>y]{y:=.P})" + by (meson exists_fresh(1) fs_name1) + with NotL show ?case + apply (clarsimp simp add: fresh_prod fresh_fun_simp_NotL trm.inject alpha fresh_atm calc_atm abs_fresh) + by (metis fin_NotL_elim nrename_fresh nrename_swap substn_nrename_comm') +next + case (AndL1 name1 trm name2) + obtain z::name where "z \ (name2,name1,P,trm[name2\n>y]{y:=.P},y,P,trm)" + by (meson exists_fresh(1) fs_name1) + with AndL1 show ?case + using fin_AndL1_elim[OF AndL1.prems(1)] + by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod nrename_fresh subst_fresh(3)) +next + case (AndL2 name1 trm name2) + obtain z::name where "z \ (name2,name1,P,trm[name2\n>y]{y:=.P},y,P,trm)" + by (meson exists_fresh(1) fs_name1) + with AndL2 show ?case + using fin_AndL2_elim[OF AndL2.prems(1)] + by simp (metis abs_fresh(1) fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod nrename_fresh subst_fresh(3)) +next + case (OrL name1 trm1 name2 trm2 name3) + obtain z::name where "z \ (name3,name2,name1,P,trm1[name3\n>y]{y:=.P},trm2[name3\n>y]{y:=.P},y,P,trm1,trm2)" + by (meson exists_fresh(1) fs_name1) + with OrL show ?case + using fin_OrL_elim[OF OrL.prems(1)] + by (auto simp add: abs_fresh fresh_fun_simp_OrL fresh_atm(1) nrename_fresh subst_fresh(3)) +next + case (ImpL coname trm1 name1 trm2 name2) + obtain z::name where "z \ (name1,x,P,trm1[x\n>y]{y:=.P},trm2[x\n>y]{y:=.P},y,P,trm1,trm2)" + by (meson exists_fresh(1) fs_name1) + with ImpL show ?case + using fin_ImpL_elim[OF ImpL.prems(1)] + by (auto simp add: abs_fresh fresh_fun_simp_ImpL fresh_atm(1) nrename_fresh subst_fresh(3)) +qed (use fin_rest_elims in force)+ inductive fic :: "trm \ coname \ bool" @@ -2283,157 +2225,110 @@ (auto simp: calc_atm simp add: fresh_left abs_fresh) lemma not_fic_subst1: - assumes a: "\(fic M a)" + assumes "\(fic M a)" shows "\(fic (M{y:=.P}) a)" -using a -apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct) -apply(auto) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(drule fic_elims) -apply(auto)[1] -apply(drule freshc_after_substn) -apply(simp add: fic.intros) -apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotL) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(1)[OF fs_name1]) -apply(drule fic_elims, simp) -apply(drule fic_elims) -apply(auto)[1] -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substn) -apply(drule freshc_after_substn) -apply(simp add: fic.intros abs_fresh) -apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL1) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(1)[OF fs_name1]) -apply(drule fic_elims, simp) -apply(subgoal_tac "\x'::name. x'\(trm{y:=.P},P,name1,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL2) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(1)[OF fs_name1]) -apply(drule fic_elims, simp) -apply(drule fic_elims) -apply(auto)[1] -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substn) -apply(simp add: fic.intros abs_fresh) -apply(drule fic_elims) -apply(auto)[1] -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substn) -apply(simp add: fic.intros abs_fresh) -apply(subgoal_tac "\x'::name. x'\(trm1{y:=.P},trm2{y:=.P},P,name1,name2,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrL) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(1)[OF fs_name1]) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substn) -apply(simp add: fic.intros abs_fresh) -apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},trm2{name2:=.P},P,name1,name2,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpL) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(1)[OF fs_name1]) -apply(drule fic_elims, simp) -done +using assms +proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct) + case (Ax name coname) + then show ?case + using fic_rest_elims(1) substn.simps(1) by presburger +next + case (Cut coname trm1 name trm2) + then show ?case + by (metis abs_fresh(2) better_Cut_substn fic_rest_elims(1) fresh_prod) +next + case (NotR name trm coname) + then show ?case + by (metis fic.intros(2) fic_NotR_elim fresh_prod freshc_after_substn substn.simps(3)) +next + case (NotL coname trm name) + obtain x'::name where "x' \ (trm{y:=.P},P,a)" + by (meson exists_fresh(1) fs_name1) + with NotL show ?case + by (simp add: fic.intros fresh_prod) (metis fic_rest_elims(1,2) fresh_fun_simp_NotL) +next + case (AndR coname1 trm1 coname2 trm2 coname3) + then show ?case + by simp (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substn) +next + case (AndL1 name1 trm name2) + obtain x'::name where "x' \ (trm{y:=.P},P,name1,a)" + by (meson exists_fresh(1) fs_name1) + with AndL1 fic_rest_elims show ?case + by (simp add: fic.intros fresh_prod)(metis fresh_fun_simp_AndL1) +next + case (AndL2 name1 trm name2) + obtain x'::name where "x' \ (trm{y:=.P},P,name1,a)" + by (meson exists_fresh(1) fs_name1) + with AndL2 fic_rest_elims show ?case + by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_AndL2) +next + case (OrR1 coname1 trm coname2) + then show ?case + by simp (metis abs_fresh(2) fic.simps fic_OrR1_elim freshc_after_substn) +next + case (OrR2 coname1 trm coname2) + then show ?case + by simp (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substn) +next + case (OrL name1 trm1 name2 trm2 name3) + obtain x'::name where "x' \ (trm1{y:=.P},trm2{y:=.P},P,name1,name2,a)" + by (meson exists_fresh(1) fs_name1) + with OrL fic_rest_elims show ?case + by (simp add: fic.intros fresh_prod) (metis fresh_fun_simp_OrL) +next + case (ImpR name coname1 trm coname2) + then show ?case + by simp (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substn) +next + case (ImpL coname trm1 name1 trm2 name2) + obtain x'::name where "x' \ (trm1{name2:=.P},trm2{name2:=.P},P,name1,name2,a)" + by (meson exists_fresh(1) fs_name1) + with ImpL fic_rest_elims fresh_fun_simp_ImpL show ?case + by (simp add: fresh_prod) fastforce +qed lemma not_fic_subst2: - assumes a: "\(fic M a)" + assumes "\(fic M a)" shows "\(fic (M{c:=(y).P}) a)" -using a -apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct) -apply(auto) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(subgoal_tac "\c'::coname. c'\(trm{coname:=(y).P},P,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotR) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(2)[OF fs_coname1]) -apply(drule fic_elims, simp) -apply(drule freshc_after_substc) -apply(simp) -apply(simp add: fic.intros abs_fresh) -apply(drule fic_elims, simp) -apply(subgoal_tac "\c'::coname. c'\(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndR) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(2)[OF fs_coname1]) -apply(drule fic_elims, simp) -apply(auto)[1] -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substc) -apply(simp) -apply(drule freshc_after_substc) -apply(simp) -apply(simp add: fic.intros abs_fresh) -apply(drule fic_elims, simp) -apply(drule fic_elims, simp) -apply(subgoal_tac "\c'::coname. c'\(trm{coname2:=(y).P},P,coname1,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR1) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(2)[OF fs_coname1]) -apply(drule fic_elims, simp) -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substc) -apply(simp) -apply(simp add: fic.intros abs_fresh) -apply(subgoal_tac "\c'::coname. c'\(trm{coname2:=(y).P},P,coname1,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR2) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(2)[OF fs_coname1]) -apply(drule fic_elims, simp) -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substc) -apply(simp) -apply(simp add: fic.intros abs_fresh) -apply(drule fic_elims, simp) -apply(subgoal_tac "\c'::coname. c'\(trm{coname2:=(y).P},P,coname1,a)") -apply(erule exE) -apply(simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpR) -apply(drule fic_elims, simp) -apply(rule exists_fresh'(2)[OF fs_coname1]) -apply(drule fic_elims, simp) -apply(simp add: abs_fresh fresh_atm) -apply(drule freshc_after_substc) -apply(simp) -apply(simp add: fic.intros abs_fresh) -apply(drule fic_elims, simp) -done +using assms +proof (nominal_induct M avoiding: a c y P rule: trm.strong_induct) + case (NotR name trm coname) + obtain c'::coname where "c'\(trm{coname:=(y).P},P,a)" + by (meson exists_fresh'(2) fs_coname1) + with NotR fic_rest_elims show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_NotR) + by (metis fic.intros(2) fic_NotR_elim freshc_after_substc) +next + case (AndR coname1 trm1 coname2 trm2 coname3) + obtain c'::coname where "c'\(trm1{coname3:=(y).P},trm2{coname3:=(y).P},P,coname1,coname2,a)" + by (meson exists_fresh'(2) fs_coname1) + with AndR fic_rest_elims show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_AndR) + by (metis abs_fresh(2) fic.intros(3) fic_AndR_elim freshc_after_substc) +next + case (OrR1 coname1 trm coname2) + obtain c'::coname where "c'\(trm{coname2:=(y).P},P,coname1,a)" + by (meson exists_fresh'(2) fs_coname1) + with OrR1 fic_rest_elims show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1) + by (metis abs_fresh(2) fic.intros(4) fic_OrR1_elim freshc_after_substc) +next + case (OrR2 coname1 trm coname2) + obtain c'::coname where "c'\(trm{coname2:=(y).P},P,coname1,a)" + by (meson exists_fresh'(2) fs_coname1) + with OrR2 fic_rest_elims show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2) + by (metis abs_fresh(2) fic.simps fic_OrR2_elim freshc_after_substc) +next + case (ImpR name coname1 trm coname2) + obtain c'::coname where "c'\(trm{coname2:=(y).P},P,coname1,a)" + by (meson exists_fresh'(2) fs_coname1) + with ImpR fic_rest_elims show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR) + by (metis abs_fresh(2) fic.intros(6) fic_ImpR_elim freshc_after_substc) +qed (use fic_rest_elims in auto) + lemma fic_subst1: assumes a: "fic M a" "a\b" "a\P"