--- a/src/HOL/Nominal/Examples/Class1.thy Sat Jul 27 11:41:17 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy Sun Jul 28 14:45:41 2024 +0100
@@ -4293,7 +4293,7 @@
lemma interesting_subst1:
assumes a: "x\<noteq>y" "x\<sharp>P" "y\<sharp>P"
shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}"
-using a
+ using a
proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct)
case (Cut d M u M' x' y' c P)
with assms show ?case
@@ -4302,57 +4302,57 @@
next
case (NotL d M u)
obtain x'::name and x''::name
- where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)"
- and "x''\<sharp> (P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)"
+ where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)"
+ and "x''\<sharp> (P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)"
by (meson exists_fresh(1) fs_name1)
then show ?case
using NotL
by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget
- fresh_atm abs_fresh fresh_fun_simp_NotL fresh_prod)
+ fresh_atm abs_fresh fresh_fun_simp_NotL fresh_prod)
next
case (AndL1 u M d)
obtain x'::name and x''::name
- where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
- and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+ where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+ and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
by (meson exists_fresh(1) fs_name1)
then show ?case
using AndL1
by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget
- fresh_atm abs_fresh fresh_fun_simp_AndL1 fresh_prod)
+ fresh_atm abs_fresh fresh_fun_simp_AndL1 fresh_prod)
next
case (AndL2 u M d)
obtain x'::name and x''::name
- where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
- and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+ where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
+ and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)"
by (meson exists_fresh(1) fs_name1)
then show ?case
using AndL2
by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget
- fresh_atm abs_fresh fresh_fun_simp_AndL2 fresh_prod)
+ fresh_atm abs_fresh fresh_fun_simp_AndL2 fresh_prod)
next
case (OrL x1 M x2 M' x3)
obtain x'::name and x''::name
- where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
+ where "x' \<sharp> (P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
- and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},
+ and "x''\<sharp> (P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},
M'{x:=<c>.Ax y c},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)"
by (meson exists_fresh(1) fs_name1)
then show ?case
using OrL
by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget
- fresh_atm abs_fresh fresh_fun_simp_OrL fresh_prod subst_fresh)
+ fresh_atm abs_fresh fresh_fun_simp_OrL fresh_prod subst_fresh)
next
case (ImpL a M x1 M' x2)
obtain x'::name and x''::name
- where "x' \<sharp> (P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
+ where "x' \<sharp> (P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)"
- and "x''\<sharp> (P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
+ and "x''\<sharp> (P,Ax y c,M{x2:=<c>.Ax y c},M{x2:=<c>.Ax y c}{y:=<c>.P},
M'{x2:=<c>.Ax y c},M'{x2:=<c>.Ax y c}{y:=<c>.P},x1,x2,y,x)"
by (meson exists_fresh(1) fs_name1)
then show ?case
using ImpL
by (auto simp: perm_fresh_fresh(1) swap_simps(3,7) trm.inject alpha forget
- fresh_atm abs_fresh fresh_fun_simp_ImpL fresh_prod subst_fresh)
+ fresh_atm abs_fresh fresh_fun_simp_ImpL fresh_prod subst_fresh)
qed (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
lemma interesting_subst1':
@@ -4394,22 +4394,22 @@
next
case (NotR u M d)
obtain a' a''::coname
- where "a' \<sharp> (b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)"
- and "a'' \<sharp> (P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)"
+ where "a' \<sharp> (b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)"
+ and "a'' \<sharp> (P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)"
by (meson exists_fresh'(2) fs_coname1)
with NotR show ?case
by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_NotR)
next
case (AndR d1 M d2 M' d3)
obtain a' a''::coname
- where "a' \<sharp> (P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
+ where "a' \<sharp> (P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)"
- and "a'' \<sharp> (P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P},
+ and "a'' \<sharp> (P,Ax y a,M{d3:=(y).Ax y a},M{d3:=(y).Ax y a}{a:=(y).P},
M'{d3:=(y).Ax y a},M'{d3:=(y).Ax y a}{a:=(y).P},d1,d2,d3,y,b)"
by (meson exists_fresh'(2) fs_coname1)
with AndR show ?case
apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
- apply(auto simp only: fresh_prod fresh_fun_simp_AndR)
+ apply(auto simp only: fresh_prod fresh_fun_simp_AndR)
apply (force simp: forget abs_fresh subst_fresh fresh_atm)+
done
next
@@ -4424,7 +4424,7 @@
case (OrR1 d M e)
obtain a' a''::coname
where "a' \<sharp> (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
- and "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
+ and "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
by (meson exists_fresh'(2) fs_coname1)
with OrR1 show ?case
by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR1)
@@ -4432,7 +4432,7 @@
case (OrR2 d M e)
obtain a' a''::coname
where "a' \<sharp> (b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)"
- and "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
+ and "a'' \<sharp> (b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)"
by (meson exists_fresh'(2) fs_coname1)
with OrR2 show ?case
by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_OrR2)
@@ -4448,7 +4448,7 @@
case (ImpR u e M d)
obtain a' a''::coname
where "a' \<sharp> (b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})"
- and "a'' \<sharp> (e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})"
+ and "a'' \<sharp> (e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})"
by (meson exists_fresh'(2) fs_coname1)
with ImpR show ?case
by (auto simp: abs_fresh fresh_atm forget fresh_prod fresh_fun_simp_ImpR)
@@ -4470,299 +4470,84 @@
qed
qed
+
lemma subst_subst1:
assumes a: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P"
shows "M{x:=<a>.P}{b:=(y).Q} = M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
-using a
+ using a
proof(nominal_induct M avoiding: x a P b y Q rule: trm.strong_induct)
case (Ax z c)
- have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact+
- { assume asm: "z=x \<and> c=b"
- have "(Ax x b){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax x b){b:=(y).Q}" using fs by simp
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q"
- using fs by (simp_all add: fresh_prod fresh_atm)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using fs by (simp add: forget)
- also have "\<dots> = (Cut <b>.Ax x b (y).Q){x:=<a>.(P{b:=(y).Q})}"
- using fs asm by (auto simp: fresh_prod fresh_atm subst_fresh)
- also have "\<dots> = (Ax x b){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using fs by simp
- finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
- using asm by simp
- }
- moreover
- { assume asm: "z\<noteq>x \<and> c=b"
- have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}" using asm by simp
- also have "\<dots> = Cut <b>.Ax z c (y).Q" using fs asm by simp
- also have "\<dots> = Cut <b>.(Ax z c{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})"
- using fs asm by (simp add: forget)
- also have "\<dots> = (Cut <b>.Ax z c (y).Q){x:=<a>.(P{b:=(y).Q})}" using asm fs
- by (auto simp: trm.inject subst_fresh fresh_prod fresh_atm abs_fresh)
- also have "\<dots> = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using asm fs by simp
- finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" by simp
- }
- moreover
- { assume asm: "z=x \<and> c\<noteq>b"
- have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax z c){b:=(y).Q}" using fs asm by simp
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (x).Ax z c" using fs asm by (auto simp: trm.inject abs_fresh)
- also have "\<dots> = (Ax z c){x:=<a>.(P{b:=(y).Q})}" using fs asm by simp
- also have "\<dots> = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using asm by auto
- finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" by simp
- }
- moreover
- { assume asm: "z\<noteq>x \<and> c\<noteq>b"
- have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using asm by auto
- }
- ultimately show ?case by blast
+ then show ?case
+ by (auto simp add: abs_fresh fresh_prod fresh_atm subst_fresh trm.inject forget)
next
case (Cut c M z N)
- { assume asm: "M = Ax x c \<and> N = Ax z b"
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
- using Cut asm by simp
- also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
- also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using Cut asm by (auto simp: fresh_prod fresh_atm)
- finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.(P{b:=(y).Q}) (y).Q)" by simp
- have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = (Cut <c>.M (y).Q){x:=<a>.(P{b:=(y).Q})}"
- using Cut asm by (simp add: fresh_atm)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using Cut asm
- by (auto simp: fresh_prod fresh_atm subst_fresh)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using Cut asm by (simp add: forget)
- finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = Cut <a>.(P{b:=(y).Q}) (y).Q"
- by simp
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
- using eq1 eq2 by simp
- }
- moreover
- { assume asm: "M \<noteq> Ax x c \<and> N = Ax z b"
- have neq: "M{b:=(y).Q} \<noteq> Ax x c"
- proof (cases "b\<sharp>M")
- case True then show ?thesis using asm by (simp add: forget)
- next
- case False then show ?thesis by (simp add: not_Ax1)
- qed
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.(M{x:=<a>.P}) (z).(N{x:=<a>.P})){b:=(y).Q}"
- using Cut asm by simp
- also have "\<dots> = (Cut <c>.(M{x:=<a>.P}) (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
- also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (y).Q" using Cut asm by (simp add: abs_fresh)
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" using Cut asm by simp
- finally
- have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q"
- by simp
- have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
- (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using Cut asm by simp
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})"
- using Cut asm neq by (auto simp: fresh_prod fresh_atm subst_fresh abs_fresh)
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using Cut asm by (simp add: forget)
- finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
- = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" by simp
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
- using eq1 eq2 by simp
- }
- moreover
- { assume asm: "M = Ax x c \<and> N \<noteq> Ax z b"
- have neq: "N{x:=<a>.P} \<noteq> Ax z b"
- proof (cases "x\<sharp>N")
- case True then show ?thesis using asm by (simp add: forget)
- next
- case False then show ?thesis by (simp add: not_Ax2)
- qed
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
- using Cut asm by simp
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq
- by (simp add: abs_fresh)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" using Cut asm by simp
- finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
- = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
- have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
- = (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
- using Cut asm by auto
- also have "\<dots> = (Cut <c>.M (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
- using Cut asm by (auto simp: fresh_atm)
- also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using Cut asm by (simp add: fresh_prod fresh_atm subst_fresh)
- finally
- have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
- = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
- using eq1 eq2 by simp
- }
- moreover
- { assume asm: "M \<noteq> Ax x c \<and> N \<noteq> Ax z b"
- have neq1: "N{x:=<a>.P} \<noteq> Ax z b"
- proof (cases "x\<sharp>N")
- case True then show ?thesis using asm by (simp add: forget)
- next
- case False then show ?thesis by (simp add: not_Ax2)
- qed
- have neq2: "M{b:=(y).Q} \<noteq> Ax x c"
- proof (cases "b\<sharp>M")
- case True then show ?thesis using asm by (simp add: forget)
- next
- case False then show ?thesis by (simp add: not_Ax1)
- qed
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.(M{x:=<a>.P}) (z).(N{x:=<a>.P})){b:=(y).Q}"
- using Cut asm by simp
- also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq1
- by (simp add: abs_fresh)
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using Cut asm by simp
- finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
- = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
- have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
- (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}" using Cut asm neq1 by simp
- also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
- using Cut asm neq2 by (simp add: fresh_prod fresh_atm subst_fresh)
- finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
- Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
- have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
- using eq1 eq2 by simp
- }
- ultimately show ?case by blast
+ then show ?case
+ apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh)
+ apply (metis forget not_Ax1 not_Ax2)
+ done
next
case (NotR z M c)
then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(M{c:=(y).Q},M{c:=(y).Q}{x:=<a>.P{c:=(y).Q}},Q,a,P,c,y)")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
- apply(simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
- apply(simp add: forget)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_NotR)
next
case (NotL c M z)
- then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},y,Q)")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain x'::name where "x' \<sharp> (P,M{x:=<a>.P},P{b:=(y).Q},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},y,Q)"
+ by (meson exists_fresh(1) fs_name1)
+ with NotL show ?case
+ apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh subst_fresh fresh_fun_simp_NotL)
+ by (metis fresh_fun_simp_NotL fresh_prod subst_fresh(5))
next
case (AndR c1 M c2 N c3)
then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c3:=(y).Q},M{c3:=(y).Q}{x:=<a>.P{c3:=(y).Q}},c2,c3,a,
- P{c3:=(y).Q},N{c3:=(y).Q},N{c3:=(y).Q}{x:=<a>.P{c3:=(y).Q}},c1)")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp_all add: fresh_atm abs_fresh subst_fresh)
- apply(simp add: forget)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_AndR)
next
case (AndL1 z1 M z2)
- then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain x'::name where "x' \<sharp> (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})"
+ by (meson exists_fresh(1) fs_name1)
+ with AndL1 show ?case
+ apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL1)
+ by (metis fresh_atm(1) fresh_fun_simp_AndL1 fresh_prod subst_fresh(5))
next
case (AndL2 z1 M z2)
- then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain x'::name where "x' \<sharp> (P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})"
+ by (meson exists_fresh(1) fs_name1)
+ with AndL2 show ?case
+ apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_AndL2)
+ by (metis fresh_atm(1) fresh_fun_simp_AndL2 fresh_prod subst_fresh(5))
next
case (OrL z1 M z2 N z3)
- then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z2,z3,a,y,Q,
- P{b:=(y).Q},N{x:=<a>.P},N{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z1)")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp_all add: fresh_atm subst_fresh)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain x'::name where "x' \<sharp> (P,M{x:=<a>.P},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z2,z3,a,y,Q,
+ P{b:=(y).Q},N{x:=<a>.P},N{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z1)"
+ by (meson exists_fresh(1) fs_name1)
+ with OrL show ?case
+ apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_OrL)
+ by (metis (full_types) fresh_atm(1) fresh_fun_simp_OrL fresh_prod subst_fresh(5))
next
case (OrR1 c1 M c2)
then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c2:=(y).Q},a,P{c2:=(y).Q},c1,
- M{c2:=(y).Q}{x:=<a>.P{c2:=(y).Q}})")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
- apply(simp_all add: fresh_atm subst_fresh abs_fresh)
- apply(simp add: forget)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR1)
next
case (OrR2 c1 M c2)
then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c2:=(y).Q},a,P{c2:=(y).Q},c1,
- M{c2:=(y).Q}{x:=<a>.P{c2:=(y).Q}})")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
- apply(simp_all add: fresh_atm subst_fresh abs_fresh)
- apply(simp add: forget)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_OrR2)
next
case (ImpR z c M d)
then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{d:=(y).Q},a,P{d:=(y).Q},c,
- M{d:=(y).Q}{x:=<a>.P{d:=(y).Q}})")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm)
- apply(simp_all add: fresh_atm subst_fresh forget abs_fresh)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by (auto simp: forget fresh_prod fresh_atm subst_fresh abs_fresh fresh_fun_simp_ImpR)
next
case (ImpL c M z N u)
- then show ?case
- apply(auto simp: fresh_prod fresh_atm subst_fresh)
- apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,P{b:=(y).Q},M{u:=<a>.P},N{u:=<a>.P},y,Q,
- M{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},N{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},z)")
- apply(erule exE)
- apply(simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp_all add: fresh_atm subst_fresh forget)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain z'::name where "z' \<sharp> (P,P{b:=(y).Q},M{u:=<a>.P},N{u:=<a>.P},y,Q,
+ M{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},N{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},z)"
+ by (meson exists_fresh(1) fs_name1)
+ with ImpL show ?case
+ apply(auto simp: fresh_prod fresh_atm abs_fresh subst_fresh fresh_fun_simp_ImpL)
+ by (metis (full_types) fresh_atm(1) fresh_prod subst_fresh(5) fresh_fun_simp_ImpL)
qed
lemma subst_subst2:
assumes a: "a\<sharp>(b,P,N)" "x\<sharp>(y,P,M)" "b\<sharp>(M,N)" "y\<sharp>P"
shows "M{a:=(x).N}{y:=<b>.P} = M{y:=<b>.P}{a:=(x).N{y:=<b>.P}}"
-using a
+ using a
proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct)
case (Ax z c)
then show ?case
@@ -4770,142 +4555,54 @@
next
case (Cut d M' u M'')
then show ?case
- apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
- apply(auto)
- apply(simp add: fresh_atm)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_prod fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: forget)
- apply(simp add: fresh_atm)
- apply(case_tac "a\<sharp>M'")
- apply(simp add: forget)
- apply(simp add: not_Ax1)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_prod fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(auto)[1]
- apply(case_tac "y\<sharp>M''")
- apply(simp add: forget)
- apply(simp add: not_Ax2)
- apply(simp add: forget)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto)[1]
- apply(case_tac "y\<sharp>M''")
- apply(simp add: forget)
- apply(simp add: not_Ax2)
- apply(case_tac "a\<sharp>M'")
- apply(simp add: forget)
- apply(simp add: not_Ax1)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh)
- apply(simp add: subst_fresh abs_fresh)
- apply(simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm)
- apply(simp add: subst_fresh abs_fresh)
- apply(auto)[1]
- apply(case_tac "y\<sharp>M''")
- apply(simp add: forget)
- apply(simp add: not_Ax2)
+ apply (clarsimp simp add: abs_fresh fresh_prod fresh_atm subst_fresh)
+ apply (metis forget not_Ax1 not_Ax2)
done
next
case (NotR z M' d)
- then show ?case
- apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(y,P,N,N{y:=<b>.P},M'{d:=(x).N},M'{y:=<b>.P}{d:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotR)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(2)[OF fs_coname1])
+ obtain a'::coname where "a' \<sharp> (y,P,N,N{y:=<b>.P},M'{d:=(x).N},M'{y:=<b>.P}{d:=(x).N{y:=<b>.P}})"
+ by (meson exists_fresh'(2) fs_coname1)
+ with NotR show ?case
+ apply(simp add: fresh_atm subst_fresh)
+ apply(auto simp only: fresh_prod fresh_fun_simp_NotR; simp add: abs_fresh NotR)
done
next
case (NotL d M' z)
- then show ?case
- apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(z,y,P,N,N{y:=<b>.P},M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ obtain x'::name where "x' \<sharp> (z,y,P,N,N{y:=<b>.P},M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})"
+ by (meson exists_fresh(1) fs_name1)
+ with NotL show ?case
+ apply(simp add: fresh_prod fresh_atm abs_fresh)
+ apply(auto simp only: fresh_fun_simp_NotL)
+ by (auto simp: subst_fresh abs_fresh fresh_atm forget)
next
case (AndR d M' e M'' f)
- then show ?case
- apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+ obtain a'::coname where "a' \<sharp> (P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N},
+ M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{f:=(x).N{y:=<b>.P}})"
+ by (meson exists_fresh'(2) fs_coname1)
+ with AndR show ?case
+ apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod)
apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N},
M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndR)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(simp)
+ apply(erule exE, simp add: fresh_prod)
+ apply(erule conjE)+
+ apply(simp add: fresh_fun_simp_AndR)
+ 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])
done
next
case (AndL1 z M' u)
- then show ?case
- apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+ obtain x'::name where "x' \<sharp> (P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.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 "\<exists>x'::name. x'\<sharp>(P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL1)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp)
+ 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
next
@@ -4913,20 +4610,10 @@
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL2)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp)
+ 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
next
@@ -4935,22 +4622,10 @@
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,b,u,w,v,N,N{y:=<b>.P},M'{y:=<b>.P},M''{y:=<b>.P},
M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(simp)
+ 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
next
@@ -4959,19 +4634,10 @@
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR1)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp)
+ 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])
done
next
@@ -4980,42 +4646,24 @@
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR2)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp)
+ 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])
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 "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
+ apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpR)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(simp add: fresh_atm trm.inject alpha abs_fresh fin_supp abs_supp)
- apply(rule exists_fresh'(2)[OF fs_coname1])
+ 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)
done
next
@@ -5024,21 +4672,10 @@
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,b,e,w,v,N,N{y:=<b>.P},M'{w:=<b>.P},M''{w:=<b>.P},
M'{w:=<b>.P}{a:=(x).N{w:=<b>.P}},M''{w:=<b>.P}{a:=(x).N{w:=<b>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh fresh_atm abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
+ 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
qed
@@ -5046,7 +4683,7 @@
lemma subst_subst3:
assumes a: "a\<sharp>(P,N,c)" "c\<sharp>(M,N)" "x\<sharp>(y,P,M)" "y\<sharp>(P,x)" "M\<noteq>Ax y a"
shows "N{x:=<a>.M}{y:=<c>.P} = N{y:=<c>.P}{x:=<a>.(M{y:=<c>.P})}"
-using a
+ using a
proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
case (Ax z c)
then show ?case
@@ -5056,37 +4693,17 @@
then show ?case
apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
apply(auto)
- apply(simp add: fresh_atm)
- apply(simp add: trm.inject)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(subgoal_tac "P \<noteq> Ax x c")
- apply(simp)
- apply(simp add: forget)
- apply(clarify)
- apply(simp add: fresh_atm)
- apply(case_tac "x\<sharp>M'")
- apply(simp add: forget)
- apply(simp add: not_Ax2)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(auto)
- apply(case_tac "y\<sharp>M'")
- apply(simp add: forget)
- apply(simp add: not_Ax2)
- done
+ apply(auto simp add: fresh_atm trm.inject forget)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
+ apply (metis forget(1) not_Ax2)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
+ apply(rule sym)
+ apply(rule trans)
+ apply(rule better_Cut_substn)
+ apply(simp add: abs_fresh subst_fresh)
+ apply(simp add: fresh_prod subst_fresh fresh_atm)
+ apply(simp)
+ by (metis forget(1) not_Ax2)
next
case NotR
then show ?case
@@ -5095,39 +4712,17 @@
case (NotL d M' u)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotL)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
+ apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
+ apply(erule exE, simp add: fresh_prod)
+ apply(erule conjE)+
+ apply(simp add: fresh_fun_simp_NotL)
+ 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])
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(x,y,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_atm subst_fresh fresh_prod)
- apply(subgoal_tac "P \<noteq> Ax x c")
- apply(simp)
- apply(simp add: forget trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(clarify)
- apply(simp add: fresh_atm)
+ apply(erule exE, simp add: fresh_prod)
+ apply(erule conjE)+
+ apply(simp add: fresh_fun_simp_NotL)
+ 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
next
@@ -5138,78 +4733,34 @@
case (AndL1 u M' v)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL1)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
+ apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.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])
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(x,y,u,v,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL1)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_atm subst_fresh fresh_prod)
- apply(subgoal_tac "P \<noteq> Ax x c")
- apply(simp)
- apply(simp add: forget trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(clarify)
- apply(simp add: fresh_atm)
+ 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
next
case (AndL2 u M' v)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL2)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
+ apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.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])
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(x,y,u,v,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL2)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_atm subst_fresh fresh_prod)
- apply(subgoal_tac "P \<noteq> Ax x c")
- apply(simp)
- apply(simp add: forget trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(clarify)
- apply(simp add: fresh_atm)
+ 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
next
@@ -5224,44 +4775,19 @@
case (OrL x1 M' x2 M'' x3)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
+ apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
x1,x2,x3,M''{x:=<a>.M},M''{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrL)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
+ 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])
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(x,y,P,M,M'{y:=<c>.P},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
x1,x2,x3,M''{y:=<c>.P},M''{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_atm subst_fresh fresh_prod)
- apply(simp add: fresh_prod fresh_atm)
- apply(auto)
- apply(simp add: fresh_atm)
- apply(simp add: forget trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(simp add: fresh_atm)
+ 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
next
@@ -5272,42 +4798,19 @@
case (ImpL d M' x1 M'' x2)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x2:=<a>.M},M'{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}},
+ apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x2:=<a>.M},M'{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}},
x1,x2,M''{x2:=<a>.M},M''{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpL)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
- apply(rule exists_fresh'(1)[OF fs_name1])
+ 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])
apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(x,y,P,M,M'{x2:=<c>.P},M'{x2:=<c>.P}{x:=<a>.M{x2:=<c>.P}},
x1,x2,M''{x2:=<c>.P},M''{x2:=<c>.P}{x:=<a>.M{x2:=<c>.P}})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpL)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substn)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp add: fresh_atm subst_fresh fresh_prod)
- apply(simp add: fresh_prod fresh_atm)
- apply(auto)
- apply(simp add: fresh_atm)
- apply(simp add: forget trm.inject alpha)
- apply(rule trans)
- apply(rule substn.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm subst_fresh)
- apply(simp add: fresh_atm)
+ 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
qed
@@ -5315,239 +4818,96 @@
lemma subst_subst4:
assumes a: "x\<sharp>(P,N,y)" "y\<sharp>(M,N)" "a\<sharp>(c,P,M)" "c\<sharp>(P,a)" "M\<noteq>Ax x c"
shows "N{a:=(x).M}{c:=(y).P} = N{c:=(y).P}{a:=(x).(M{c:=(y).P})}"
-using a
+ using a
proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
- case (Ax z c)
- then show ?case
- by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
-next
case (Cut d M' u M'')
then show ?case
apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
apply(auto)
- apply(simp add: fresh_atm)
- apply(simp add: trm.inject)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: abs_fresh subst_fresh fresh_atm)
- apply(simp add: fresh_prod subst_fresh abs_fresh fresh_atm)
- apply(subgoal_tac "P \<noteq> Ax y a")
- apply(simp)
- apply(simp add: forget)
- apply(clarify)
- apply(simp add: fresh_atm)
- apply(case_tac "a\<sharp>M''")
- apply(simp add: forget)
- apply(simp add: not_Ax1)
+ apply(simp add: fresh_atm)
+ apply(simp add: trm.inject)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
+ apply (metis forget(2) not_Ax1)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(rule sym)
apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp add: abs_fresh subst_fresh)
- apply(simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: fresh_prod subst_fresh fresh_atm)
- apply(simp add: abs_fresh subst_fresh)
+ apply(rule better_Cut_substc)
+ apply(simp add: fresh_prod subst_fresh fresh_atm)
+ apply(simp add: abs_fresh subst_fresh)
apply(auto)
- apply(case_tac "c\<sharp>M''")
- apply(simp add: forget)
- apply(simp add: not_Ax1)
- done
-next
- case NotL
- then show ?case
- by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+ by (metis forget(2) not_Ax1)
next
case (NotR u M' d)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(generate_fresh "coname")
- apply(fresh_fun_simp)
- apply(fresh_fun_simp)
- apply(simp add: abs_fresh subst_fresh)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp)
- apply(simp add: abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_prod fresh_atm)
- apply(auto simp: fresh_atm fresh_prod)[1]
+ apply(generate_fresh "coname")
+ apply(fresh_fun_simp)
+ apply(fresh_fun_simp)
+ apply(simp add: abs_fresh subst_fresh)
+ apply(simp add: abs_fresh subst_fresh)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: fresh_prod fresh_atm subst_fresh)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto simp: fresh_atm)
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(simp add: fresh_atm subst_fresh)
- apply(auto simp: fresh_prod fresh_atm)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
done
next
- case AndL1
- then show ?case
- by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
-next
- case AndL2
- then show ?case
- by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
-next
case (AndR d M e M' f)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(generate_fresh "coname")
- apply(fresh_fun_simp)
- apply(fresh_fun_simp)
- apply(simp add: abs_fresh subst_fresh)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp)
- apply(simp add: abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(simp)
- apply(auto simp: fresh_atm fresh_prod)[1]
+ apply(generate_fresh "coname")
+ apply(fresh_fun_simp)
+ apply(fresh_fun_simp)
+ apply(simp add: abs_fresh subst_fresh)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm fresh_prod)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto simp: fresh_atm)[1]
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(simp)
- apply(auto simp: fresh_atm fresh_prod)[1]
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
done
next
- case OrL
- then show ?case
- by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
-next
case (OrR1 d M' e)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+ apply(generate_fresh "coname")
+ apply(fresh_fun_simp)
+ apply(fresh_fun_simp)
+ apply(simp add: abs_fresh subst_fresh)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
- apply(simp add: abs_fresh subst_fresh)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp)
- apply(simp add: abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(generate_fresh "coname")
- apply(fresh_fun_simp)
- apply(fresh_fun_simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm fresh_prod)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto simp: fresh_atm)[1]
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
done
next
case (OrR2 d M' e)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(generate_fresh "coname")
- apply(fresh_fun_simp)
- apply(fresh_fun_simp)
- apply(simp add: abs_fresh subst_fresh)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp)
- apply(simp add: abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+ apply(generate_fresh "coname")
+ apply(fresh_fun_simp)
+ apply(fresh_fun_simp)
+ apply(simp add: abs_fresh subst_fresh)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm fresh_prod)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto simp: fresh_atm)[1]
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
done
next
- case ImpL
- then show ?case
- by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
-next
case (ImpR u d M' e)
then show ?case
apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
- apply(generate_fresh "coname")
- apply(fresh_fun_simp)
- apply(fresh_fun_simp)
- apply(simp add: abs_fresh subst_fresh)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp)
- apply(simp add: abs_fresh)
- apply(simp)
- apply(simp add: trm.inject alpha)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
+ apply(generate_fresh "coname")
+ apply(fresh_fun_simp)
+ apply(fresh_fun_simp)
+ apply(simp add: abs_fresh subst_fresh)
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)
apply(generate_fresh "coname")
apply(fresh_fun_simp)
apply(fresh_fun_simp)
- apply(rule sym)
- apply(rule trans)
- apply(rule better_Cut_substc)
- apply(simp add: subst_fresh fresh_atm fresh_prod)
- apply(simp add: abs_fresh subst_fresh)
- apply(auto simp: fresh_atm)[1]
- apply(simp add: trm.inject alpha forget)
- apply(rule trans)
- apply(rule substc.simps)
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
- apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
+ apply (force simp add: trm.inject alpha forget fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)+
done
-qed
+qed (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+
end