1.1 --- a/src/HOL/Nominal/Examples/Class1.thy Thu Mar 03 22:06:15 2011 +0100
1.2 +++ b/src/HOL/Nominal/Examples/Class1.thy Fri Mar 04 00:09:47 2011 +0100
1.3 @@ -6532,7 +6532,7 @@
1.4 by (auto simp add: abs_fresh fresh_atm forget trm.inject)
1.5 next
1.6 case (Cut d M u M' x' y' c P)
1.7 - from prems show ?case
1.8 + with assms show ?case
1.9 apply(simp)
1.10 apply(auto)
1.11 apply(rule trans)
1.12 @@ -6840,7 +6840,7 @@
1.13 by (auto simp add: abs_fresh fresh_atm forget trm.inject)
1.14 next
1.15 case (Cut d M u M' x' y' c P)
1.16 - from prems show ?case
1.17 + with assms show ?case
1.18 apply(simp)
1.19 apply(auto simp add: trm.inject)
1.20 apply(rule trans)
1.21 @@ -7163,15 +7163,15 @@
1.22 case (Cut c M z N)
1.23 { assume asm: "M = Ax x c \<and> N = Ax z b"
1.24 have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
1.25 - using asm prems by simp
1.26 - also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using asm prems by (simp add: fresh_atm)
1.27 - also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using asm prems by (auto simp add: fresh_prod fresh_atm)
1.28 + using Cut asm by simp
1.29 + also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
1.30 + also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using Cut asm by (auto simp add: fresh_prod fresh_atm)
1.31 finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.(P{b:=(y).Q}) (y).Q)" by simp
1.32 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})}"
1.33 - using prems asm by (simp add: fresh_atm)
1.34 - also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using asm prems
1.35 + using Cut asm by (simp add: fresh_atm)
1.36 + also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using Cut asm
1.37 by (auto simp add: fresh_prod fresh_atm subst_fresh)
1.38 - also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using asm prems by (simp add: forget)
1.39 + also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using Cut asm by (simp add: forget)
1.40 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"
1.41 by simp
1.42 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})}"
1.43 @@ -7186,18 +7186,18 @@
1.44 case False then show ?thesis by (simp add: not_Ax1)
1.45 qed
1.46 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}"
1.47 - using asm prems by simp
1.48 - also have "\<dots> = (Cut <c>.(M{x:=<a>.P}) (z).N){b:=(y).Q}" using asm prems by (simp add: fresh_atm)
1.49 - also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (y).Q" using asm prems by (simp add: abs_fresh)
1.50 - also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" using asm prems by simp
1.51 + using Cut asm by simp
1.52 + also have "\<dots> = (Cut <c>.(M{x:=<a>.P}) (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
1.53 + also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (y).Q" using Cut asm by (simp add: abs_fresh)
1.54 + also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" using Cut asm by simp
1.55 finally
1.56 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"
1.57 by simp
1.58 have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
1.59 - (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using asm prems by simp
1.60 + (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using Cut asm by simp
1.61 also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})"
1.62 - using asm prems neq by (auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
1.63 - also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using asm prems by (simp add: forget)
1.64 + using Cut asm neq by (auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
1.65 + also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using Cut asm by (simp add: forget)
1.66 finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
1.67 = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" by simp
1.68 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})}"
1.69 @@ -7212,19 +7212,19 @@
1.70 case False then show ?thesis by (simp add: not_Ax2)
1.71 qed
1.72 have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}"
1.73 - using asm prems by simp
1.74 - also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using asm prems neq
1.75 + using Cut asm by simp
1.76 + also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq
1.77 by (simp add: abs_fresh)
1.78 - also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" using asm prems by simp
1.79 + 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
1.80 finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
1.81 = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
1.82 have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
1.83 = (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
1.84 - using asm prems by auto
1.85 + using Cut asm by auto
1.86 also have "\<dots> = (Cut <c>.M (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
1.87 - using asm prems by (auto simp add: fresh_atm)
1.88 + using Cut asm by (auto simp add: fresh_atm)
1.89 also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})"
1.90 - using asm prems by (simp add: fresh_prod fresh_atm subst_fresh)
1.91 + using Cut asm by (simp add: fresh_prod fresh_atm subst_fresh)
1.92 finally
1.93 have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}
1.94 = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
1.95 @@ -7246,17 +7246,17 @@
1.96 case False then show ?thesis by (simp add: not_Ax1)
1.97 qed
1.98 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}"
1.99 - using asm prems by simp
1.100 - also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using asm prems neq1
1.101 + using Cut asm by simp
1.102 + also have "\<dots> = Cut <c>.(M{x:=<a>.P}{b:=(y).Q}) (z).(N{x:=<a>.P}{b:=(y).Q})" using Cut asm neq1
1.103 by (simp add: abs_fresh)
1.104 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})})"
1.105 - using asm prems by simp
1.106 + using Cut asm by simp
1.107 finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q}
1.108 = 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
1.109 have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
1.110 - (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}" using asm neq1 prems by simp
1.111 + (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}" using Cut asm neq1 by simp
1.112 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})})"
1.113 - using asm neq2 prems by (simp add: fresh_prod fresh_atm subst_fresh)
1.114 + using Cut asm neq2 by (simp add: fresh_prod fresh_atm subst_fresh)
1.115 finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} =
1.116 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
1.117 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})}"
2.1 --- a/src/HOL/Nominal/Examples/Class2.thy Thu Mar 03 22:06:15 2011 +0100
2.2 +++ b/src/HOL/Nominal/Examples/Class2.thy Fri Mar 04 00:09:47 2011 +0100
2.3 @@ -300,32 +300,32 @@
2.4 proof -
2.5 { assume asm: "N\<noteq>Ax y b"
2.6 have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} =
2.7 - (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using prems
2.8 + (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
2.9 by (simp add: subst_fresh abs_fresh fresh_atm)
2.10 - also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using prems
2.11 + also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using LNot
2.12 by (auto intro: l_redu.intros simp add: subst_fresh)
2.13 - also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using prems
2.14 + also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using LNot asm
2.15 by (simp add: subst_fresh abs_fresh fresh_atm)
2.16 finally have ?thesis by auto
2.17 }
2.18 moreover
2.19 { assume asm: "N=Ax y b"
2.20 have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} =
2.21 - (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using prems
2.22 + (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
2.23 by (simp add: subst_fresh abs_fresh fresh_atm)
2.24 - also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using prems
2.25 + also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using LNot
2.26 apply -
2.27 apply(rule a_starI)
2.28 apply(rule al_redu)
2.29 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.30 done
2.31 - also have "\<dots> = (Cut <b>.(Cut <c>.P (y).Ax y b) (u).(M{y:=<c>.P}))" using prems
2.32 + also have "\<dots> = (Cut <b>.(Cut <c>.P (y).Ax y b) (u).(M{y:=<c>.P}))" using LNot asm
2.33 by simp
2.34 also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(P[c\<turnstile>c>b]) (u).(M{y:=<c>.P}))"
2.35 proof (cases "fic P c")
2.36 case True
2.37 assume "fic P c"
2.38 - then show ?thesis using prems
2.39 + then show ?thesis using LNot
2.40 apply -
2.41 apply(rule a_starI)
2.42 apply(rule better_CutL_intro)
2.43 @@ -347,7 +347,7 @@
2.44 apply(simp add: subst_with_ax2)
2.45 done
2.46 qed
2.47 - also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using prems
2.48 + also have "\<dots> = (Cut <b>.N (u).M){y:=<c>.P}" using LNot asm
2.49 apply -
2.50 apply(auto simp add: subst_fresh abs_fresh)
2.51 apply(simp add: trm.inject)
2.52 @@ -368,15 +368,15 @@
2.53 { assume asm: "M1\<noteq>Ax y a1"
2.54 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} =
2.55 Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
2.56 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.57 + using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.58 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.P})"
2.59 - using prems
2.60 + using LAnd1
2.61 apply -
2.62 apply(rule a_starI)
2.63 apply(rule al_redu)
2.64 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.65 done
2.66 - also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using prems
2.67 + also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using LAnd1 asm
2.68 by (simp add: subst_fresh abs_fresh fresh_atm)
2.69 finally
2.70 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a1>.M1 (u).N){y:=<c>.P}"
2.71 @@ -386,21 +386,21 @@
2.72 { assume asm: "M1=Ax y a1"
2.73 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} =
2.74 Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
2.75 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.76 + using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.77 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.P})"
2.78 - using prems
2.79 + using LAnd1
2.80 apply -
2.81 apply(rule a_starI)
2.82 apply(rule al_redu)
2.83 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.84 done
2.85 also have "\<dots> = Cut <a1>.(Cut <c>.P (y). Ax y a1) (u).(N{y:=<c>.P})"
2.86 - using prems by simp
2.87 + using LAnd1 asm by simp
2.88 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.P[c\<turnstile>c>a1] (u).(N{y:=<c>.P})"
2.89 proof (cases "fic P c")
2.90 case True
2.91 assume "fic P c"
2.92 - then show ?thesis using prems
2.93 + then show ?thesis using LAnd1
2.94 apply -
2.95 apply(rule a_starI)
2.96 apply(rule better_CutL_intro)
2.97 @@ -422,7 +422,7 @@
2.98 apply(simp add: subst_with_ax2)
2.99 done
2.100 qed
2.101 - also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using prems
2.102 + also have "\<dots> = (Cut <a1>.M1 (u).N){y:=<c>.P}" using LAnd1 asm
2.103 apply -
2.104 apply(auto simp add: subst_fresh abs_fresh)
2.105 apply(simp add: trm.inject)
2.106 @@ -444,15 +444,15 @@
2.107 { assume asm: "M2\<noteq>Ax y a2"
2.108 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} =
2.109 Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
2.110 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.111 + using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.112 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.P})"
2.113 - using prems
2.114 + using LAnd2
2.115 apply -
2.116 apply(rule a_starI)
2.117 apply(rule al_redu)
2.118 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.119 done
2.120 - also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using prems
2.121 + also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using LAnd2 asm
2.122 by (simp add: subst_fresh abs_fresh fresh_atm)
2.123 finally
2.124 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a2>.M2 (u).N){y:=<c>.P}"
2.125 @@ -462,21 +462,21 @@
2.126 { assume asm: "M2=Ax y a2"
2.127 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} =
2.128 Cut <b>.AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
2.129 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.130 + using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.131 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.P})"
2.132 - using prems
2.133 + using LAnd2
2.134 apply -
2.135 apply(rule a_starI)
2.136 apply(rule al_redu)
2.137 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.138 done
2.139 also have "\<dots> = Cut <a2>.(Cut <c>.P (y). Ax y a2) (u).(N{y:=<c>.P})"
2.140 - using prems by simp
2.141 + using LAnd2 asm by simp
2.142 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.P[c\<turnstile>c>a2] (u).(N{y:=<c>.P})"
2.143 proof (cases "fic P c")
2.144 case True
2.145 assume "fic P c"
2.146 - then show ?thesis using prems
2.147 + then show ?thesis using LAnd2 asm
2.148 apply -
2.149 apply(rule a_starI)
2.150 apply(rule better_CutL_intro)
2.151 @@ -498,7 +498,7 @@
2.152 apply(simp add: subst_with_ax2)
2.153 done
2.154 qed
2.155 - also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using prems
2.156 + also have "\<dots> = (Cut <a2>.M2 (u).N){y:=<c>.P}" using LAnd2 asm
2.157 apply -
2.158 apply(auto simp add: subst_fresh abs_fresh)
2.159 apply(simp add: trm.inject)
2.160 @@ -520,15 +520,15 @@
2.161 { assume asm: "M\<noteq>Ax y a"
2.162 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
2.163 Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
2.164 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.165 + using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.166 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.P})"
2.167 - using prems
2.168 + using LOr1
2.169 apply -
2.170 apply(rule a_starI)
2.171 apply(rule al_redu)
2.172 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.173 done
2.174 - also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using prems
2.175 + also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using LOr1 asm
2.176 by (simp add: subst_fresh abs_fresh fresh_atm)
2.177 finally
2.178 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x1).N1){y:=<c>.P}"
2.179 @@ -538,21 +538,21 @@
2.180 { assume asm: "M=Ax y a"
2.181 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
2.182 Cut <b>.OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
2.183 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.184 + using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.185 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.P})"
2.186 - using prems
2.187 + using LOr1
2.188 apply -
2.189 apply(rule a_starI)
2.190 apply(rule al_redu)
2.191 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.192 done
2.193 also have "\<dots> = Cut <a>.(Cut <c>.P (y). Ax y a) (x1).(N1{y:=<c>.P})"
2.194 - using prems by simp
2.195 + using LOr1 asm by simp
2.196 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.P[c\<turnstile>c>a] (x1).(N1{y:=<c>.P})"
2.197 proof (cases "fic P c")
2.198 case True
2.199 assume "fic P c"
2.200 - then show ?thesis using prems
2.201 + then show ?thesis using LOr1
2.202 apply -
2.203 apply(rule a_starI)
2.204 apply(rule better_CutL_intro)
2.205 @@ -574,7 +574,7 @@
2.206 apply(simp add: subst_with_ax2)
2.207 done
2.208 qed
2.209 - also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using prems
2.210 + also have "\<dots> = (Cut <a>.M (x1).N1){y:=<c>.P}" using LOr1 asm
2.211 apply -
2.212 apply(auto simp add: subst_fresh abs_fresh)
2.213 apply(simp add: trm.inject)
2.214 @@ -596,15 +596,15 @@
2.215 { assume asm: "M\<noteq>Ax y a"
2.216 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
2.217 Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
2.218 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.219 + using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.220 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.P})"
2.221 - using prems
2.222 + using LOr2
2.223 apply -
2.224 apply(rule a_starI)
2.225 apply(rule al_redu)
2.226 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.227 done
2.228 - also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using prems
2.229 + also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using LOr2 asm
2.230 by (simp add: subst_fresh abs_fresh fresh_atm)
2.231 finally
2.232 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x2).N2){y:=<c>.P}"
2.233 @@ -614,21 +614,21 @@
2.234 { assume asm: "M=Ax y a"
2.235 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} =
2.236 Cut <b>.OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
2.237 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.238 + using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.239 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.P})"
2.240 - using prems
2.241 + using LOr2
2.242 apply -
2.243 apply(rule a_starI)
2.244 apply(rule al_redu)
2.245 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.246 done
2.247 also have "\<dots> = Cut <a>.(Cut <c>.P (y). Ax y a) (x2).(N2{y:=<c>.P})"
2.248 - using prems by simp
2.249 + using LOr2 asm by simp
2.250 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.P[c\<turnstile>c>a] (x2).(N2{y:=<c>.P})"
2.251 proof (cases "fic P c")
2.252 case True
2.253 assume "fic P c"
2.254 - then show ?thesis using prems
2.255 + then show ?thesis using LOr2
2.256 apply -
2.257 apply(rule a_starI)
2.258 apply(rule better_CutL_intro)
2.259 @@ -650,7 +650,7 @@
2.260 apply(simp add: subst_with_ax2)
2.261 done
2.262 qed
2.263 - also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using prems
2.264 + also have "\<dots> = (Cut <a>.M (x2).N2){y:=<c>.P}" using LOr2 asm
2.265 apply -
2.266 apply(auto simp add: subst_fresh abs_fresh)
2.267 apply(simp add: trm.inject)
2.268 @@ -672,15 +672,15 @@
2.269 { assume asm: "N\<noteq>Ax y d"
2.270 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} =
2.271 Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
2.272 - using prems by (simp add: fresh_prod abs_fresh fresh_atm)
2.273 + using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
2.274 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{y:=<c>.P}) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
2.275 - using prems
2.276 + using LImp
2.277 apply -
2.278 apply(rule a_starI)
2.279 apply(rule al_redu)
2.280 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.281 done
2.282 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using prems
2.283 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using LImp asm
2.284 by (simp add: subst_fresh abs_fresh fresh_atm)
2.285 finally
2.286 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} \<longrightarrow>\<^isub>a*
2.287 @@ -691,21 +691,21 @@
2.288 { assume asm: "N=Ax y d"
2.289 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} =
2.290 Cut <b>.ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
2.291 - using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.292 + using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.293 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{y:=<c>.P}) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
2.294 - using prems
2.295 + using LImp
2.296 apply -
2.297 apply(rule a_starI)
2.298 apply(rule al_redu)
2.299 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.300 done
2.301 also have "\<dots> = Cut <a>.(Cut <d>.(Cut <c>.P (y).Ax y d) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
2.302 - using prems by simp
2.303 + using LImp asm by simp
2.304 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(P[c\<turnstile>c>d]) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
2.305 proof (cases "fic P c")
2.306 case True
2.307 assume "fic P c"
2.308 - then show ?thesis using prems
2.309 + then show ?thesis using LImp
2.310 apply -
2.311 apply(rule a_starI)
2.312 apply(rule better_CutL_intro)
2.313 @@ -719,7 +719,7 @@
2.314 next
2.315 case False
2.316 assume "\<not>fic P c"
2.317 - then show ?thesis using prems
2.318 + then show ?thesis using LImp
2.319 apply -
2.320 apply(rule a_star_CutL)
2.321 apply(rule a_star_CutL)
2.322 @@ -731,7 +731,7 @@
2.323 apply(simp add: subst_with_ax2)
2.324 done
2.325 qed
2.326 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using prems
2.327 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}" using LImp asm
2.328 apply -
2.329 apply(auto simp add: subst_fresh abs_fresh)
2.330 apply(simp add: trm.inject)
2.331 @@ -810,32 +810,32 @@
2.332 proof -
2.333 { assume asm: "M\<noteq>Ax u c"
2.334 have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} =
2.335 - (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using prems
2.336 + (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
2.337 by (simp add: subst_fresh abs_fresh fresh_atm)
2.338 - also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems
2.339 + also have "\<dots> \<longrightarrow>\<^isub>l (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
2.340 by (auto intro: l_redu.intros simp add: subst_fresh)
2.341 - also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using prems
2.342 + also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using LNot asm
2.343 by (simp add: subst_fresh abs_fresh fresh_atm)
2.344 finally have ?thesis by auto
2.345 }
2.346 moreover
2.347 { assume asm: "M=Ax u c"
2.348 have "(Cut <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} =
2.349 - (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using prems
2.350 + (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
2.351 by (simp add: subst_fresh abs_fresh fresh_atm)
2.352 - also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using prems
2.353 + also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
2.354 apply -
2.355 apply(rule a_starI)
2.356 apply(rule al_redu)
2.357 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.358 done
2.359 - also have "\<dots> = (Cut <b>.(N{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P))" using prems
2.360 + also have "\<dots> = (Cut <b>.(N{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P))" using LNot asm
2.361 by simp
2.362 also have "\<dots> \<longrightarrow>\<^isub>a* (Cut <b>.(N{c:=(y).P}) (u).(P[y\<turnstile>n>u]))"
2.363 proof (cases "fin P y")
2.364 case True
2.365 assume "fin P y"
2.366 - then show ?thesis using prems
2.367 + then show ?thesis using LNot
2.368 apply -
2.369 apply(rule a_starI)
2.370 apply(rule better_CutR_intro)
2.371 @@ -857,7 +857,7 @@
2.372 apply(simp add: subst_with_ax1)
2.373 done
2.374 qed
2.375 - also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using prems
2.376 + also have "\<dots> = (Cut <b>.N (u).M){c:=(y).P}" using LNot asm
2.377 apply -
2.378 apply(auto simp add: subst_fresh abs_fresh)
2.379 apply(simp add: trm.inject)
2.380 @@ -878,15 +878,15 @@
2.381 { assume asm: "N\<noteq>Ax u c"
2.382 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} =
2.383 Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z"
2.384 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.385 + using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.386 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(N{c:=(y).P})"
2.387 - using prems
2.388 + using LAnd1
2.389 apply -
2.390 apply(rule a_starI)
2.391 apply(rule al_redu)
2.392 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.393 done
2.394 - also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using prems
2.395 + also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using LAnd1 asm
2.396 by (simp add: subst_fresh abs_fresh fresh_atm)
2.397 finally
2.398 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a1>.M1 (u).N){c:=(y).P}"
2.399 @@ -896,21 +896,21 @@
2.400 { assume asm: "N=Ax u c"
2.401 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} =
2.402 Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z"
2.403 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.404 + using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.405 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(N{c:=(y).P})"
2.406 - using prems
2.407 + using LAnd1
2.408 apply -
2.409 apply(rule a_starI)
2.410 apply(rule al_redu)
2.411 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.412 done
2.413 also have "\<dots> = Cut <a1>.(M1{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)"
2.414 - using prems by simp
2.415 + using LAnd1 asm by simp
2.416 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a1>.(M1{c:=(y).P}) (u).(P[y\<turnstile>n>u])"
2.417 proof (cases "fin P y")
2.418 case True
2.419 assume "fin P y"
2.420 - then show ?thesis using prems
2.421 + then show ?thesis using LAnd1
2.422 apply -
2.423 apply(rule a_starI)
2.424 apply(rule better_CutR_intro)
2.425 @@ -932,7 +932,7 @@
2.426 apply(simp add: subst_with_ax1)
2.427 done
2.428 qed
2.429 - also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using prems
2.430 + also have "\<dots> = (Cut <a1>.M1 (u).N){c:=(y).P}" using LAnd1 asm
2.431 apply -
2.432 apply(auto simp add: subst_fresh abs_fresh)
2.433 apply(simp add: trm.inject)
2.434 @@ -954,15 +954,15 @@
2.435 { assume asm: "N\<noteq>Ax u c"
2.436 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} =
2.437 Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z"
2.438 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.439 + using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.440 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(N{c:=(y).P})"
2.441 - using prems
2.442 + using LAnd2
2.443 apply -
2.444 apply(rule a_starI)
2.445 apply(rule al_redu)
2.446 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.447 done
2.448 - also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using prems
2.449 + also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using LAnd2 asm
2.450 by (simp add: subst_fresh abs_fresh fresh_atm)
2.451 finally
2.452 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a2>.M2 (u).N){c:=(y).P}"
2.453 @@ -972,21 +972,21 @@
2.454 { assume asm: "N=Ax u c"
2.455 have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} =
2.456 Cut <b>.AndR <a1>.(M1{c:=(y).P}) <a2>.(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z"
2.457 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.458 + using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.459 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(N{c:=(y).P})"
2.460 - using prems
2.461 + using LAnd2
2.462 apply -
2.463 apply(rule a_starI)
2.464 apply(rule al_redu)
2.465 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.466 done
2.467 also have "\<dots> = Cut <a2>.(M2{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)"
2.468 - using prems by simp
2.469 + using LAnd2 asm by simp
2.470 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a2>.(M2{c:=(y).P}) (u).(P[y\<turnstile>n>u])"
2.471 proof (cases "fin P y")
2.472 case True
2.473 assume "fin P y"
2.474 - then show ?thesis using prems
2.475 + then show ?thesis using LAnd2
2.476 apply -
2.477 apply(rule a_starI)
2.478 apply(rule better_CutR_intro)
2.479 @@ -1008,7 +1008,7 @@
2.480 apply(simp add: subst_with_ax1)
2.481 done
2.482 qed
2.483 - also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using prems
2.484 + also have "\<dots> = (Cut <a2>.M2 (u).N){c:=(y).P}" using LAnd2 asm
2.485 apply -
2.486 apply(auto simp add: subst_fresh abs_fresh)
2.487 apply(simp add: trm.inject)
2.488 @@ -1030,15 +1030,15 @@
2.489 { assume asm: "N1\<noteq>Ax x1 c"
2.490 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
2.491 Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
2.492 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.493 + using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.494 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
2.495 - using prems
2.496 + using LOr1
2.497 apply -
2.498 apply(rule a_starI)
2.499 apply(rule al_redu)
2.500 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.501 done
2.502 - also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using prems
2.503 + also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using LOr1 asm
2.504 by (simp add: subst_fresh abs_fresh fresh_atm)
2.505 finally
2.506 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x1).N1){c:=(y).P}"
2.507 @@ -1048,21 +1048,21 @@
2.508 { assume asm: "N1=Ax x1 c"
2.509 have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
2.510 Cut <b>.OrR1 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
2.511 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.512 + using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
2.513 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
2.514 - using prems
2.515 + using LOr1
2.516 apply -
2.517 apply(rule a_starI)
2.518 apply(rule al_redu)
2.519 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.520 done
2.521 also have "\<dots> = Cut <a>.(M{c:=(y).P}) (x1).(Cut <c>.(Ax x1 c) (y).P)"
2.522 - using prems by simp
2.523 + using LOr1 asm by simp
2.524 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x1).(P[y\<turnstile>n>x1])"
2.525 proof (cases "fin P y")
2.526 case True
2.527 assume "fin P y"
2.528 - then show ?thesis using prems
2.529 + then show ?thesis using LOr1
2.530 apply -
2.531 apply(rule a_starI)
2.532 apply(rule better_CutR_intro)
2.533 @@ -1084,7 +1084,7 @@
2.534 apply(simp add: subst_with_ax1)
2.535 done
2.536 qed
2.537 - also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using prems
2.538 + also have "\<dots> = (Cut <a>.M (x1).N1){c:=(y).P}" using LOr1 asm
2.539 apply -
2.540 apply(auto simp add: subst_fresh abs_fresh)
2.541 apply(simp add: trm.inject)
2.542 @@ -1106,15 +1106,15 @@
2.543 { assume asm: "N2\<noteq>Ax x2 c"
2.544 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
2.545 Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
2.546 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.547 + using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.548 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
2.549 - using prems
2.550 + using LOr2
2.551 apply -
2.552 apply(rule a_starI)
2.553 apply(rule al_redu)
2.554 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.555 done
2.556 - also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using prems
2.557 + also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using LOr2 asm
2.558 by (simp add: subst_fresh abs_fresh fresh_atm)
2.559 finally
2.560 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \<longrightarrow>\<^isub>a* (Cut <a>.M (x2).N2){c:=(y).P}"
2.561 @@ -1124,21 +1124,21 @@
2.562 { assume asm: "N2=Ax x2 c"
2.563 have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
2.564 Cut <b>.OrR2 <a>.(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z"
2.565 - using prems by (simp add: subst_fresh abs_fresh fresh_atm)
2.566 + using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
2.567 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
2.568 - using prems
2.569 + using LOr2
2.570 apply -
2.571 apply(rule a_starI)
2.572 apply(rule al_redu)
2.573 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.574 done
2.575 also have "\<dots> = Cut <a>.(M{c:=(y).P}) (x2).(Cut <c>.(Ax x2 c) (y).P)"
2.576 - using prems by simp
2.577 + using LOr2 asm by simp
2.578 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(M{c:=(y).P}) (x2).(P[y\<turnstile>n>x2])"
2.579 proof (cases "fin P y")
2.580 case True
2.581 assume "fin P y"
2.582 - then show ?thesis using prems
2.583 + then show ?thesis using LOr2
2.584 apply -
2.585 apply(rule a_starI)
2.586 apply(rule better_CutR_intro)
2.587 @@ -1160,7 +1160,7 @@
2.588 apply(simp add: subst_with_ax1)
2.589 done
2.590 qed
2.591 - also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using prems
2.592 + also have "\<dots> = (Cut <a>.M (x2).N2){c:=(y).P}" using LOr2 asm
2.593 apply -
2.594 apply(auto simp add: subst_fresh abs_fresh)
2.595 apply(simp add: trm.inject)
2.596 @@ -1182,15 +1182,15 @@
2.597 { assume asm: "M\<noteq>Ax x c \<and> Q\<noteq>Ax u c"
2.598 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
2.599 Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
2.600 - using prems by (simp add: fresh_prod abs_fresh fresh_atm)
2.601 + using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
2.602 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
2.603 - using prems
2.604 + using LImp
2.605 apply -
2.606 apply(rule a_starI)
2.607 apply(rule al_redu)
2.608 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.609 done
2.610 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
2.611 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
2.612 by (simp add: subst_fresh abs_fresh fresh_atm)
2.613 finally
2.614 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} \<longrightarrow>\<^isub>a*
2.615 @@ -1201,21 +1201,21 @@
2.616 { assume asm: "M=Ax x c \<and> Q\<noteq>Ax u c"
2.617 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
2.618 Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
2.619 - using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.620 + using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.621 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
2.622 - using prems
2.623 + using LImp
2.624 apply -
2.625 apply(rule a_starI)
2.626 apply(rule al_redu)
2.627 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.628 done
2.629 also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(Q{c:=(y).P})"
2.630 - using prems by simp
2.631 + using LImp asm by simp
2.632 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(P[y\<turnstile>n>x])) (u).(Q{c:=(y).P})"
2.633 proof (cases "fin P y")
2.634 case True
2.635 assume "fin P y"
2.636 - then show ?thesis using prems
2.637 + then show ?thesis using LImp
2.638 apply -
2.639 apply(rule a_star_CutL)
2.640 apply(rule a_star_CutR)
2.641 @@ -1229,7 +1229,7 @@
2.642 next
2.643 case False
2.644 assume "\<not>fin P y"
2.645 - then show ?thesis using prems
2.646 + then show ?thesis using LImp
2.647 apply -
2.648 apply(rule a_star_CutL)
2.649 apply(rule a_star_CutR)
2.650 @@ -1241,7 +1241,7 @@
2.651 apply(simp add: subst_with_ax1)
2.652 done
2.653 qed
2.654 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
2.655 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
2.656 apply -
2.657 apply(auto simp add: subst_fresh abs_fresh)
2.658 apply(simp add: trm.inject)
2.659 @@ -1259,21 +1259,21 @@
2.660 { assume asm: "M\<noteq>Ax x c \<and> Q=Ax u c"
2.661 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
2.662 Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
2.663 - using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.664 + using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.665 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
2.666 - using prems
2.667 + using LImp
2.668 apply -
2.669 apply(rule a_starI)
2.670 apply(rule al_redu)
2.671 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.672 done
2.673 also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Cut <c>.Ax u c (y).P)"
2.674 - using prems by simp
2.675 + using LImp asm by simp
2.676 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(P[y\<turnstile>n>u])"
2.677 proof (cases "fin P y")
2.678 case True
2.679 assume "fin P y"
2.680 - then show ?thesis using prems
2.681 + then show ?thesis using LImp
2.682 apply -
2.683 apply(rule a_star_CutR)
2.684 apply(rule a_starI)
2.685 @@ -1284,7 +1284,7 @@
2.686 next
2.687 case False
2.688 assume "\<not>fin P y"
2.689 - then show ?thesis using prems
2.690 + then show ?thesis using LImp
2.691 apply -
2.692 apply(rule a_star_CutR)
2.693 apply(rule a_star_trans)
2.694 @@ -1295,7 +1295,7 @@
2.695 apply(simp add: subst_with_ax1)
2.696 done
2.697 qed
2.698 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
2.699 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
2.700 apply -
2.701 apply(auto simp add: subst_fresh abs_fresh)
2.702 apply(simp add: trm.inject)
2.703 @@ -1311,21 +1311,21 @@
2.704 { assume asm: "M=Ax x c \<and> Q=Ax u c"
2.705 have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} =
2.706 Cut <b>.ImpR (x).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
2.707 - using prems by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.708 + using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
2.709 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
2.710 - using prems
2.711 + using LImp
2.712 apply -
2.713 apply(rule a_starI)
2.714 apply(rule al_redu)
2.715 apply(auto intro: l_redu.intros simp add: subst_fresh abs_fresh)
2.716 done
2.717 also have "\<dots> = Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(Cut <c>.Ax u c (y).P)"
2.718 - using prems by simp
2.719 + using LImp asm by simp
2.720 also have "\<dots> \<longrightarrow>\<^isub>a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(Cut <c>.Ax x c (y).P)) (u).(P[y\<turnstile>n>u])"
2.721 proof (cases "fin P y")
2.722 case True
2.723 assume "fin P y"
2.724 - then show ?thesis using prems
2.725 + then show ?thesis using LImp
2.726 apply -
2.727 apply(rule a_star_CutR)
2.728 apply(rule a_starI)
2.729 @@ -1336,7 +1336,7 @@
2.730 next
2.731 case False
2.732 assume "\<not>fin P y"
2.733 - then show ?thesis using prems
2.734 + then show ?thesis using LImp
2.735 apply -
2.736 apply(rule a_star_CutR)
2.737 apply(rule a_star_trans)
2.738 @@ -1351,7 +1351,7 @@
2.739 proof (cases "fin P y")
2.740 case True
2.741 assume "fin P y"
2.742 - then show ?thesis using prems
2.743 + then show ?thesis using LImp
2.744 apply -
2.745 apply(rule a_star_CutL)
2.746 apply(rule a_star_CutR)
2.747 @@ -1363,7 +1363,7 @@
2.748 next
2.749 case False
2.750 assume "\<not>fin P y"
2.751 - then show ?thesis using prems
2.752 + then show ?thesis using LImp
2.753 apply -
2.754 apply(rule a_star_CutL)
2.755 apply(rule a_star_CutR)
2.756 @@ -1375,7 +1375,7 @@
2.757 apply(simp add: subst_with_ax1)
2.758 done
2.759 qed
2.760 - also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using prems
2.761 + also have "\<dots> = (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}" using LImp asm
2.762 apply -
2.763 apply(auto simp add: subst_fresh abs_fresh)
2.764 apply(simp add: trm.inject)
3.1 --- a/src/HOL/Nominal/Examples/SOS.thy Thu Mar 03 22:06:15 2011 +0100
3.2 +++ b/src/HOL/Nominal/Examples/SOS.thy Fri Mar 04 00:09:47 2011 +0100
3.3 @@ -536,7 +536,7 @@
3.4 case (Var x \<Gamma> \<theta> T)
3.5 have "\<Gamma> \<turnstile> (Var x) : T" by fact
3.6 then have "(x,T)\<in>set \<Gamma>" by (cases) (auto simp add: trm.inject)
3.7 - with prems have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T"
3.8 + with Var have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T"
3.9 by (auto intro!: Vs_reduce_to_themselves)
3.10 then show "\<exists>v. \<theta><Var x> \<Down> v \<and> v \<in> V T" by auto
3.11 qed
4.1 --- a/src/HOL/Nominal/Examples/W.thy Thu Mar 03 22:06:15 2011 +0100
4.2 +++ b/src/HOL/Nominal/Examples/W.thy Fri Mar 04 00:09:47 2011 +0100
4.3 @@ -433,7 +433,7 @@
4.4 assumes "x \<in> S"
4.5 and "S \<sharp>* z"
4.6 shows "x \<sharp> z"
4.7 -using prems by (simp add: fresh_star_def)
4.8 +using assms by (simp add: fresh_star_def)
4.9
4.10 lemma fresh_gen_set:
4.11 fixes X::"tvar"