diff -r 11382acb0fc4 -r 2cffa664482d src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Mon Jul 29 16:22:12 2024 +0100 +++ b/src/HOL/Nominal/Examples/Class1.thy Wed Jul 31 18:47:05 2024 +0100 @@ -4594,90 +4594,57 @@ obtain x'::name where "x' \ (P,b,z,u,x,N,M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.P}})" by (meson exists_fresh(1) fs_name1) with AndL1 show ?case - apply(simp add: fresh_prod fresh_atm abs_fresh) - apply(auto simp only: fresh_fun_simp_AndL1) - apply (auto simp: subst_fresh abs_fresh fresh_atm forget) - - apply(subgoal_tac "\x'::name. x'\(P,b,z,u,x,N,M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_AndL1) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(1)[OF fs_name1]) - done + by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL1 subst_fresh abs_fresh forget) next case (AndL2 z M' u) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\x'::name. x'\(P,b,z,u,x,N,M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_AndL2) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(1)[OF fs_name1]) - done + obtain x'::name where "x' \ (P,b,z,u,x,N,M'{y:=.P},M'{y:=.P}{a:=(x).N{y:=.P}})" + by (meson exists_fresh(1) fs_name1) + with AndL2 show ?case + by (force simp add: fresh_prod fresh_atm fresh_fun_simp_AndL2 subst_fresh abs_fresh forget) next case (OrL u M' v M'' w) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\z'::name. z'\(P,b,u,w,v,N,N{y:=.P},M'{y:=.P},M''{y:=.P}, - M'{y:=.P}{a:=(x).N{y:=.P}},M''{y:=.P}{a:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_OrL) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(1)[OF fs_name1]) - done + obtain x'::name where "x' \ (P,b,u,w,v,N,N{y:=.P},M'{y:=.P},M''{y:=.P}, + M'{y:=.P}{a:=(x).N{y:=.P}},M''{y:=.P}{a:=(x).N{y:=.P}})" + by (meson exists_fresh(1) fs_name1) + with OrL show ?case + by (force simp add: fresh_prod fresh_atm fresh_fun_simp_OrL subst_fresh abs_fresh forget) next case (OrR1 e M' f) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\c'::coname. c'\(P,b,e,f,x,N,N{y:=.P}, - M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_OrR1) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(2)[OF fs_coname1]) + obtain c'::coname where c': "c' \ (P,b,e,f,x,N,N{y:=.P}, + M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})" + by (meson exists_fresh(2) fs_coname1) + with OrR1 show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR1) + apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) + using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR1) done next case (OrR2 e M' f) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\c'::coname. c'\(P,b,e,f,x,N,N{y:=.P}, - M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_OrR2) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(2)[OF fs_coname1]) + obtain c'::coname where c': "c' \ (P,b,e,f,x,N,N{y:=.P}, + M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})" + by (meson exists_fresh(2) fs_coname1) + with OrR2 show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_OrR2) + apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) + using c' apply (auto simp: fresh_prod fresh_fun_simp_OrR2) done next case (ImpR x e M' f) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\c'::coname. c'\(P,b,e,f,x,N,N{y:=.P}, - M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_ImpR) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(simp add: fresh_atm trm.inject alpha abs_fresh fin_supp abs_supp) - apply(rule exists_fresh'(2)[OF fs_coname1]) - apply(simp add: fresh_atm trm.inject alpha abs_fresh fin_supp abs_supp) + obtain c'::coname where c': "c' \ (P,b,e,f,x,N,N{y:=.P}, + M'{f:=(x).N},M'{y:=.P}{f:=(x).N{y:=.P}})" + by (meson exists_fresh(2) fs_coname1) + with ImpR show ?case + apply (clarsimp simp: fresh_prod fresh_fun_simp_ImpR) + apply (clarsimp simp: subst_fresh abs_fresh fresh_atm) + using c' apply (auto simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_fun_simp_ImpR) done next case (ImpL e M' v M'' w) - then show ?case - apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject) - apply(subgoal_tac "\z'::name. z'\(P,b,e,w,v,N,N{y:=.P},M'{w:=.P},M''{w:=.P}, - M'{w:=.P}{a:=(x).N{w:=.P}},M''{w:=.P}{a:=(x).N{w:=.P}})") - apply(erule exE, simp add: fresh_prod) - apply(erule conjE)+ - apply(simp add: fresh_fun_simp_ImpL) - apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp) - apply(rule exists_fresh'(1)[OF fs_name1]) - done + obtain z'::name where z': "z' \ (P,b,e,w,v,N,N{y:=.P},M'{w:=.P},M''{w:=.P}, + M'{w:=.P}{a:=(x).N{w:=.P}},M''{w:=.P}{a:=(x).N{w:=.P}})" + by (meson exists_fresh(1) fs_name1) + with ImpL show ?case + by (force simp add: fresh_prod fresh_atm fresh_fun_simp_ImpL subst_fresh abs_fresh forget) qed lemma subst_subst3: