1.1 --- a/src/HOL/Nominal/Examples/SN.thy Tue Jul 24 19:58:53 2007 +0200
1.2 +++ b/src/HOL/Nominal/Examples/SN.thy Tue Jul 24 20:34:11 2007 +0200
1.3 @@ -24,10 +24,9 @@
1.4
1.5 lemma fresh_fact:
1.6 fixes a::"name"
1.7 - assumes a: "a\<sharp>t1"
1.8 - and b: "a\<sharp>t2"
1.9 + assumes a: "a\<sharp>t1" "a\<sharp>t2"
1.10 shows "a\<sharp>t1[b::=t2]"
1.11 -using a b
1.12 +using a
1.13 by (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
1.14 (auto simp add: abs_fresh fresh_atm)
1.15
1.16 @@ -62,21 +61,16 @@
1.17 inductive
1.18 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
1.19 where
1.20 - b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
1.21 -| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
1.22 -| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
1.23 -| b4[intro!]: "a\<sharp>s2 \<Longrightarrow>(App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
1.24 + b1[intro!]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App s1 t \<longrightarrow>\<^isub>\<beta> App s2 t"
1.25 +| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2"
1.26 +| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> Lam [a].s1 \<longrightarrow>\<^isub>\<beta> Lam [a].s2"
1.27 +| b4[intro!]: "a\<sharp>s2 \<Longrightarrow> App (Lam [a].s1) s2\<longrightarrow>\<^isub>\<beta> (s1[a::=s2])"
1.28
1.29 equivariance Beta
1.30
1.31 nominal_inductive Beta
1.32 by (simp_all add: abs_fresh fresh_fact')
1.33
1.34 -abbreviation
1.35 - "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
1.36 -where
1.37 - "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"
1.38 -
1.39 lemma supp_beta:
1.40 assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
1.41 shows "(supp s)\<subseteq>((supp t)::name set)"
1.42 @@ -84,7 +78,11 @@
1.43 by (induct)
1.44 (auto intro!: simp add: abs_supp lam.supp subst_supp)
1.45
1.46 -lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
1.47 +lemma beta_abs:
1.48 + assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'"
1.49 + shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
1.50 +using a
1.51 +apply -
1.52 apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'")
1.53 apply(auto simp add: lam.distinct lam.inject)
1.54 apply(auto simp add: alpha)
1.55 @@ -156,9 +154,8 @@
1.56 assumes a: "a\<sharp>\<Gamma>"
1.57 shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
1.58 using a
1.59 -apply(induct \<Gamma>)
1.60 -apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
1.61 -done
1.62 +by (induct \<Gamma>)
1.63 + (auto simp add: fresh_prod fresh_list_cons fresh_atm)
1.64
1.65 inductive
1.66 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
1.67 @@ -193,20 +190,63 @@
1.68 thus "NORMAL (Var a)" by (force simp add: NORMAL_def)
1.69 qed
1.70
1.71 -constdefs
1.72 - "SN" :: "lam \<Rightarrow> bool"
1.73 - "SN t \<equiv> termip Beta t"
1.74 +inductive
1.75 + SN :: "lam \<Rightarrow> bool"
1.76 +where
1.77 + SN_intro: "(\<And>t'. t \<longrightarrow>\<^isub>\<beta> t' \<Longrightarrow> SN t') \<Longrightarrow> SN t"
1.78
1.79 -lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
1.80 -apply(simp add: SN_def)
1.81 -apply(drule_tac a="t2" in accp_downward)
1.82 -apply(auto)
1.83 -done
1.84 +lemma SN_elim:
1.85 + assumes a: "SN M"
1.86 + shows "(\<forall>M. (\<forall>N. M \<longrightarrow>\<^isub>\<beta> N \<longrightarrow> P N)\<longrightarrow> P M) \<longrightarrow> P M"
1.87 +using a
1.88 +by (induct rule: SN.SN.induct) (blast)
1.89
1.90 -lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
1.91 -apply(simp add: SN_def)
1.92 -apply(rule accp.accI)
1.93 -apply(auto)
1.94 +lemma SN_preserved:
1.95 + assumes a: "SN t1" "t1\<longrightarrow>\<^isub>\<beta> t2"
1.96 + shows "SN t2"
1.97 +using a
1.98 +by (cases) (auto)
1.99 +
1.100 +lemma double_SN_aux:
1.101 + assumes a: "SN a"
1.102 + and b: "SN b"
1.103 + and hyp: "\<And>x z.
1.104 + (\<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> SN y) \<Longrightarrow>
1.105 + (\<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> P y z) \<Longrightarrow>
1.106 + (\<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> SN u) \<Longrightarrow>
1.107 + (\<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> P x u) \<Longrightarrow> P x z"
1.108 + shows "P a b"
1.109 +proof -
1.110 + from a
1.111 + have r: "\<And>b. SN b \<Longrightarrow> P a b"
1.112 + proof (induct a rule: SN.SN.induct)
1.113 + case (SN_intro x)
1.114 + note SNI' = SN_intro
1.115 + have "SN b" by fact
1.116 + thus ?case
1.117 + proof (induct b rule: SN.SN.induct)
1.118 + case (SN_intro y)
1.119 + show ?case
1.120 + apply (rule hyp)
1.121 + apply (erule SNI')
1.122 + apply (erule SNI')
1.123 + apply (rule SN.SN_intro)
1.124 + apply (erule SN_intro)+
1.125 + done
1.126 + qed
1.127 + qed
1.128 + from b show ?thesis by (rule r)
1.129 +qed
1.130 +
1.131 +lemma double_SN[consumes 2]:
1.132 + assumes a: "SN a"
1.133 + and b: "SN b"
1.134 + and c: "\<And>x z. \<lbrakk>\<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> P y z; \<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z"
1.135 + shows "P a b"
1.136 +using a b c
1.137 +apply(rule_tac double_SN_aux)
1.138 +apply(assumption)+
1.139 +apply(blast)
1.140 done
1.141
1.142 section {* Candidates *}
1.143 @@ -217,43 +257,35 @@
1.144 nominal_primrec
1.145 "RED (TVar X) = {t. SN(t)}"
1.146 "RED (\<tau>\<rightarrow>\<sigma>) = {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
1.147 -apply(rule TrueI)+
1.148 -done
1.149 +by (rule TrueI)+
1.150
1.151 constdefs
1.152 NEUT :: "lam \<Rightarrow> bool"
1.153 - "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)"
1.154 + "NEUT t \<equiv> (\<exists>a. t = Var a) \<or> (\<exists>t1 t2. t = App t1 t2)"
1.155
1.156 (* a slight hack to get the first element of applications *)
1.157 +(* this is needed to get (SN t) from SN (App t s) *)
1.158 inductive
1.159 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
1.160 where
1.161 fst[intro!]: "(App t s) \<guillemotright> t"
1.162
1.163 -lemma fst_elim[elim!]:
1.164 - shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
1.165 -apply(ind_cases "App t s \<guillemotright> t'")
1.166 -apply(simp add: lam.inject)
1.167 -done
1.168 -
1.169 -lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
1.170 -apply(simp add: SN_def)
1.171 -apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termip Beta z")(*A*)
1.172 -apply(force)
1.173 -(*A*)
1.174 -apply(erule accp_induct)
1.175 -apply(clarify)
1.176 -apply(ind_cases "x \<guillemotright> z" for x z)
1.177 -apply(clarify)
1.178 -apply(rule accp.accI)
1.179 -apply(auto intro: b1)
1.180 -done
1.181 +lemma SN_of_FST_of_App:
1.182 + assumes a: "SN (App t s)"
1.183 + shows "SN t"
1.184 +using a
1.185 +proof -
1.186 + from a have "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> SN z"
1.187 + by (induct rule: SN.SN.induct)
1.188 + (blast elim: FST.cases intro: SN_intro)
1.189 + then show "SN t" by blast
1.190 +qed
1.191
1.192 section {* Candidates *}
1.193
1.194 constdefs
1.195 "CR1" :: "ty \<Rightarrow> bool"
1.196 - "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
1.197 + "CR1 \<tau> \<equiv> \<forall>t. (t\<in>RED \<tau> \<longrightarrow> SN t)"
1.198
1.199 "CR2" :: "ty \<Rightarrow> bool"
1.200 "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>"
1.201 @@ -267,59 +299,78 @@
1.202 "CR4" :: "ty \<Rightarrow> bool"
1.203 "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
1.204
1.205 -lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
1.206 -apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
1.207 -apply(blast)
1.208 -done
1.209 +lemma CR3_implies_CR4:
1.210 + assumes a: "CR3 \<tau>"
1.211 + shows "CR4 \<tau>"
1.212 +using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)
1.213
1.214 -lemma sub_ind:
1.215 - "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
1.216 -apply(simp add: SN_def)
1.217 -apply(erule accp_induct)
1.218 -apply(auto)
1.219 -apply(simp add: CR3_def)
1.220 -apply(rotate_tac 5)
1.221 -apply(drule_tac x="App t x" in spec)
1.222 -apply(drule mp)
1.223 -apply(rule conjI)
1.224 -apply(force simp only: NEUT_def)
1.225 -apply(simp (no_asm) add: CR3_RED_def)
1.226 -apply(clarify)
1.227 -apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
1.228 -apply(simp_all add: lam.inject)
1.229 -apply(simp only: CR3_RED_def)
1.230 -apply(drule_tac x="s2" in spec)
1.231 -apply(simp)
1.232 -apply(drule_tac x="s2" in spec)
1.233 -apply(simp)
1.234 -apply(drule mp)
1.235 -apply(simp (no_asm_use) add: CR2_def)
1.236 -apply(blast)
1.237 -apply(drule_tac x="ta" in spec)
1.238 -apply(force)
1.239 -apply(auto simp only: NEUT_def lam.inject lam.distinct)
1.240 -done
1.241 +(* sub_induction in the arrow-type case for the next proof *)
1.242 +lemma sub_induction:
1.243 + assumes a: "SN(u)"
1.244 + and b: "u\<in>RED \<tau>"
1.245 + and c1: "NEUT t"
1.246 + and c2: "CR2 \<tau>"
1.247 + and c3: "CR3 \<sigma>"
1.248 + and c4: "CR3_RED t (\<tau>\<rightarrow>\<sigma>)"
1.249 + shows "(App t u)\<in>RED \<sigma>"
1.250 +using a b
1.251 +proof (induct)
1.252 + fix u
1.253 + assume as: "u\<in>RED \<tau>"
1.254 + assume ih: " \<And>u'. \<lbrakk>u \<longrightarrow>\<^isub>\<beta> u'; u' \<in> RED \<tau>\<rbrakk> \<Longrightarrow> App t u' \<in> RED \<sigma>"
1.255 + have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
1.256 + moreover
1.257 + have "CR3_RED (App t u) \<sigma>" unfolding CR3_RED_def
1.258 + proof (intro strip)
1.259 + fix r
1.260 + assume red: "App t u \<longrightarrow>\<^isub>\<beta> r"
1.261 + moreover
1.262 + { assume "\<exists>t'. t \<longrightarrow>\<^isub>\<beta> t' \<and> r = App t' u"
1.263 + then obtain t' where a1: "t \<longrightarrow>\<^isub>\<beta> t'" and a2: "r = App t' u" by blast
1.264 + have "t'\<in>RED (\<tau>\<rightarrow>\<sigma>)" using c4 a1 by (simp add: CR3_RED_def)
1.265 + then have "App t' u\<in>RED \<sigma>" using as by simp
1.266 + then have "r\<in>RED \<sigma>" using a2 by simp
1.267 + }
1.268 + moreover
1.269 + { assume "\<exists>u'. u \<longrightarrow>\<^isub>\<beta> u' \<and> r = App t u'"
1.270 + then obtain u' where b1: "u \<longrightarrow>\<^isub>\<beta> u'" and b2: "r = App t u'" by blast
1.271 + have "u'\<in>RED \<tau>" using as b1 c2 by (auto simp add: CR2_def)
1.272 + with ih have "App t u' \<in> RED \<sigma>" using b1 by simp
1.273 + then have "r\<in>RED \<sigma>" using b2 by simp
1.274 + }
1.275 + moreover
1.276 + { assume "\<exists>x t'. t = Lam [x].t'"
1.277 + then obtain x t' where "t = Lam [x].t'" by blast
1.278 + then have "NEUT (Lam [x].t')" using c1 by simp
1.279 + then have "False" by (simp add: NEUT_def)
1.280 + then have "r\<in>RED \<sigma>" by simp
1.281 + }
1.282 + ultimately show "r \<in> RED \<sigma>" by (cases) (auto simp add: lam.inject)
1.283 + qed
1.284 + ultimately show "App t u \<in> RED \<sigma>" using c3 by (simp add: CR3_def)
1.285 +qed
1.286
1.287 +(* properties of the candiadates *)
1.288 lemma RED_props:
1.289 shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
1.290 proof (nominal_induct \<tau> rule: ty.induct)
1.291 case (TVar a)
1.292 { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
1.293 next
1.294 - case 2 show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
1.295 + case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
1.296 next
1.297 - case 3 show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
1.298 + case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
1.299 }
1.300 next
1.301 case (TArr \<tau>1 \<tau>2)
1.302 { case 1
1.303 have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
1.304 have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
1.305 - show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
1.306 - proof (simp add: CR1_def, intro strip)
1.307 + show "CR1 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR1_def
1.308 + proof (simp, intro strip)
1.309 fix t
1.310 assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
1.311 - from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4)
1.312 + from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4)
1.313 moreover
1.314 have "NEUT (Var a)" by (force simp add: NEUT_def)
1.315 moreover
1.316 @@ -327,160 +378,129 @@
1.317 ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
1.318 with a have "App t (Var a) \<in> RED \<tau>2" by simp
1.319 hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
1.320 - thus "SN(t)" by (rule qq3)
1.321 + thus "SN(t)" by (rule SN_of_FST_of_App)
1.322 qed
1.323 next
1.324 case 2
1.325 have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.326 have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
1.327 - show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
1.328 - proof (simp add: CR2_def, intro strip)
1.329 + show "CR2 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR2_def
1.330 + proof (simp, intro strip)
1.331 fix t1 t2 u
1.332 assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and> t1 \<longrightarrow>\<^isub>\<beta> t2"
1.333 and "u \<in> RED \<tau>1"
1.334 hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
1.335 - thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
1.336 + thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (auto simp add: CR2_def)
1.337 qed
1.338 next
1.339 case 3
1.340 have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
1.341 have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
1.342 have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
1.343 - show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
1.344 - proof (simp add: CR3_def, intro strip)
1.345 + show "CR3 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR3_def
1.346 + proof (simp, intro strip)
1.347 fix t u
1.348 assume a1: "u \<in> RED \<tau>1"
1.349 assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
1.350 - from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
1.351 - hence "u\<in>RED \<tau>1\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>1\<and>CR3 \<tau>2\<and>CR3_RED t (\<tau>1\<rightarrow>\<tau>2))\<longrightarrow>(App t u)\<in>RED \<tau>2)"
1.352 - by (rule sub_ind)
1.353 - with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
1.354 + have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def)
1.355 + then show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 a1 a2 by (blast intro: sub_induction)
1.356 qed
1.357 }
1.358 qed
1.359 -
1.360 -lemma double_acc_aux:
1.361 - assumes a_acc: "accp r a"
1.362 - and b_acc: "accp r b"
1.363 - and hyp: "\<And>x z.
1.364 - (\<And>y. r y x \<Longrightarrow> accp r y) \<Longrightarrow>
1.365 - (\<And>y. r y x \<Longrightarrow> P y z) \<Longrightarrow>
1.366 - (\<And>u. r u z \<Longrightarrow> accp r u) \<Longrightarrow>
1.367 - (\<And>u. r u z \<Longrightarrow> P x u) \<Longrightarrow> P x z"
1.368 - shows "P a b"
1.369 +
1.370 +(* not as simple as on paper, because of the stronger double_SN induction *)
1.371 +lemma abs_RED:
1.372 + assumes asm: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>"
1.373 + shows "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
1.374 proof -
1.375 - from a_acc
1.376 - have r: "\<And>b. accp r b \<Longrightarrow> P a b"
1.377 - proof (induct a rule: accp.induct)
1.378 - case (accI x)
1.379 - note accI' = accI
1.380 - have "accp r b" by fact
1.381 - thus ?case
1.382 - proof (induct b rule: accp.induct)
1.383 - case (accI y)
1.384 - show ?case
1.385 - apply (rule hyp)
1.386 - apply (erule accI')
1.387 - apply (erule accI')
1.388 - apply (rule accp.accI)
1.389 - apply (erule accI)
1.390 - apply (erule accI)
1.391 - apply (erule accI)
1.392 + have b1: "SN t"
1.393 + proof -
1.394 + have "Var x\<in>RED \<tau>"
1.395 + proof -
1.396 + have "CR4 \<tau>" by (simp add: RED_props CR3_implies_CR4)
1.397 + moreover
1.398 + have "NEUT (Var x)" by (auto simp add: NEUT_def)
1.399 + moreover
1.400 + have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
1.401 + ultimately show "Var x\<in>RED \<tau>" by (simp add: CR4_def)
1.402 + qed
1.403 + then have "t[x::=Var x]\<in>RED \<sigma>" using asm by simp
1.404 + then have "t\<in>RED \<sigma>" by (simp add: id_subs)
1.405 + moreover
1.406 + have "CR1 \<sigma>" by (simp add: RED_props)
1.407 + ultimately show "SN t" by (simp add: CR1_def)
1.408 + qed
1.409 + show "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
1.410 + proof (simp, intro strip)
1.411 + fix u
1.412 + assume b2: "u\<in>RED \<tau>"
1.413 + then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
1.414 + show "App (Lam [x].t) u \<in> RED \<sigma>" using b1 b3 b2 asm
1.415 + proof(induct t u rule: double_SN)
1.416 + fix t u
1.417 + assume ih1: "\<And>t'. \<lbrakk>t \<longrightarrow>\<^isub>\<beta> t'; u\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t'[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t') u \<in> RED \<sigma>"
1.418 + assume ih2: "\<And>u'. \<lbrakk>u \<longrightarrow>\<^isub>\<beta> u'; u'\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t) u' \<in> RED \<sigma>"
1.419 + assume as1: "u \<in> RED \<tau>"
1.420 + assume as2: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>"
1.421 + have "CR3_RED (App (Lam [x].t) u) \<sigma>" unfolding CR3_RED_def
1.422 + proof(intro strip)
1.423 + fix r
1.424 + assume red: "App (Lam [x].t) u \<longrightarrow>\<^isub>\<beta> r"
1.425 + moreover
1.426 + { assume "\<exists>t'. t \<longrightarrow>\<^isub>\<beta> t' \<and> r = App (Lam [x].t') u"
1.427 + then obtain t' where a1: "t \<longrightarrow>\<^isub>\<beta> t'" and a2: "r = App (Lam [x].t') u" by blast
1.428 + have "App (Lam [x].t') u\<in>RED \<sigma>" using ih1 a1 as1 as2
1.429 + apply(auto)
1.430 + apply(drule_tac x="t'" in meta_spec)
1.431 + apply(simp)
1.432 + apply(drule meta_mp)
1.433 + apply(auto)
1.434 + apply(drule_tac x="s" in bspec)
1.435 + apply(simp)
1.436 + apply(subgoal_tac "CR2 \<sigma>")
1.437 + apply(unfold CR2_def)[1]
1.438 + apply(drule_tac x="t[x::=s]" in spec)
1.439 + apply(drule_tac x="t'[x::=s]" in spec)
1.440 + apply(simp add: beta_subst)
1.441 + apply(simp add: RED_props)
1.442 + done
1.443 + then have "r\<in>RED \<sigma>" using a2 by simp
1.444 + }
1.445 + moreover
1.446 + { assume "\<exists>u'. u \<longrightarrow>\<^isub>\<beta> u' \<and> r = App (Lam [x].t) u'"
1.447 + then obtain u' where b1: "u \<longrightarrow>\<^isub>\<beta> u'" and b2: "r = App (Lam [x].t) u'" by blast
1.448 + have "App (Lam [x].t) u'\<in>RED \<sigma>" using ih2 b1 as1 as2
1.449 + apply(auto)
1.450 + apply(drule_tac x="u'" in meta_spec)
1.451 + apply(simp)
1.452 + apply(drule meta_mp)
1.453 + apply(subgoal_tac "CR2 \<tau>")
1.454 + apply(unfold CR2_def)[1]
1.455 + apply(drule_tac x="u" in spec)
1.456 + apply(drule_tac x="u'" in spec)
1.457 + apply(simp)
1.458 + apply(simp add: RED_props)
1.459 + apply(simp)
1.460 + done
1.461 + then have "r\<in>RED \<sigma>" using b2 by simp
1.462 + }
1.463 + moreover
1.464 + { assume "r = t[x::=u]"
1.465 + then have "r\<in>RED \<sigma>" using as1 as2 by auto
1.466 + }
1.467 + ultimately show "r \<in> RED \<sigma>"
1.468 + apply(cases)
1.469 + apply(auto simp add: lam.inject)
1.470 + apply(drule beta_abs)
1.471 + apply(auto simp add: alpha subst_rename)
1.472 done
1.473 qed
1.474 + moreover
1.475 + have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
1.476 + ultimately show "App (Lam [x].t) u \<in> RED \<sigma>" using RED_props by (simp add: CR3_def)
1.477 qed
1.478 - from b_acc show ?thesis by (rule r)
1.479 qed
1.480 -
1.481 -lemma double_acc:
1.482 - "\<lbrakk>accp r a; accp r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
1.483 -apply(rule_tac r="r" in double_acc_aux)
1.484 -apply(assumption)+
1.485 -apply(blast)
1.486 -done
1.487 -
1.488 -lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
1.489 -apply(simp)
1.490 -apply(clarify)
1.491 -apply(subgoal_tac "termip Beta t")(*1*)
1.492 -apply(erule rev_mp)
1.493 -apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
1.494 -apply(erule rev_mp)
1.495 -apply(rule_tac a="t" and b="u" in double_acc)
1.496 -apply(assumption)
1.497 -apply(subgoal_tac "CR1 \<tau>")(*A*)
1.498 -apply(simp add: CR1_def SN_def)
1.499 -(*A*)
1.500 -apply(force simp add: RED_props)
1.501 -apply(simp)
1.502 -apply(clarify)
1.503 -apply(subgoal_tac "CR3 \<sigma>")(*B*)
1.504 -apply(simp add: CR3_def)
1.505 -apply(rotate_tac 6)
1.506 -apply(drule_tac x="App(Lam[x].xa ) z" in spec)
1.507 -apply(drule mp)
1.508 -apply(rule conjI)
1.509 -apply(force simp add: NEUT_def)
1.510 -apply(simp add: CR3_RED_def)
1.511 -apply(clarify)
1.512 -apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
1.513 -apply(auto simp add: lam.inject lam.distinct)
1.514 -apply(drule beta_abs)
1.515 -apply(auto)
1.516 -apply(drule_tac x="t''" in spec)
1.517 -apply(simp)
1.518 -apply(drule mp)
1.519 -apply(clarify)
1.520 -apply(drule_tac x="s" in bspec)
1.521 -apply(assumption)
1.522 -apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta> t'' [ x ::= s ]")(*B*)
1.523 -apply(subgoal_tac "CR2 \<sigma>")(*C*)
1.524 -apply(simp (no_asm_use) add: CR2_def)
1.525 -apply(blast)
1.526 -(*C*)
1.527 -apply(force simp add: RED_props)
1.528 -(*B*)
1.529 -apply(force intro!: beta_subst)
1.530 -apply(assumption)
1.531 -apply(rotate_tac 3)
1.532 -apply(drule_tac x="s2" in spec)
1.533 -apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
1.534 -apply(simp)
1.535 -(*D*)
1.536 -apply(subgoal_tac "CR2 \<tau>")(*E*)
1.537 -apply(simp (no_asm_use) add: CR2_def)
1.538 -apply(blast)
1.539 -(*E*)
1.540 -apply(force simp add: RED_props)
1.541 -apply(simp add: alpha)
1.542 -apply(erule disjE)
1.543 -apply(force)
1.544 -apply(auto)
1.545 -apply(simp add: subst_rename)
1.546 -apply(drule_tac x="z" in bspec)
1.547 -apply(assumption)
1.548 -(*B*)
1.549 -apply(force simp add: RED_props)
1.550 -(*1*)
1.551 -apply(drule_tac x="Var x" in bspec)
1.552 -apply(subgoal_tac "CR3 \<tau>")(*2*)
1.553 -apply(drule CR3_CR4)
1.554 -apply(simp add: CR4_def)
1.555 -apply(drule_tac x="Var x" in spec)
1.556 -apply(drule mp)
1.557 -apply(rule conjI)
1.558 -apply(force simp add: NEUT_def)
1.559 -apply(simp add: NORMAL_def)
1.560 -apply(clarify)
1.561 -apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
1.562 -apply(auto simp add: lam.inject lam.distinct)
1.563 -apply(force simp add: RED_props)
1.564 -apply(simp add: id_subs)
1.565 -apply(subgoal_tac "CR1 \<sigma>")(*3*)
1.566 -apply(simp add: CR1_def SN_def)
1.567 -(*3*)
1.568 -apply(force simp add: RED_props)
1.569 -done
1.570 +qed
1.571
1.572 abbreviation
1.573 mapsto :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55)
1.574 @@ -506,7 +526,7 @@
1.575 using fresh \<theta>_cond fresh_context by simp
1.576 then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>"
1.577 using fresh by (simp add: psubst_subst)
1.578 - then have "(Lam [a].(\<theta><t>)) \<in> RED (\<sigma> \<rightarrow> \<tau>)" by (simp only: abs_RED)
1.579 + then have "Lam [a].(\<theta><t>) \<in> RED (\<sigma> \<rightarrow> \<tau>)" by (simp only: abs_RED)
1.580 then show "\<theta><(Lam [a].t)> \<in> RED (\<sigma> \<rightarrow> \<tau>)" using fresh by simp
1.581 qed auto
1.582
1.583 @@ -531,16 +551,15 @@
1.584
1.585 lemma id_apply:
1.586 shows "(id \<Gamma>)<t> = t"
1.587 -apply(nominal_induct t avoiding: \<Gamma> rule: lam.induct)
1.588 -apply(auto simp add: id_maps id_fresh)
1.589 -done
1.590 +by (nominal_induct t avoiding: \<Gamma> rule: lam.induct)
1.591 + (auto simp add: id_maps id_fresh)
1.592
1.593 lemma id_closes:
1.594 shows "(id \<Gamma>) closes \<Gamma>"
1.595 apply(auto)
1.596 apply(simp add: id_maps)
1.597 apply(subgoal_tac "CR3 T") --"A"
1.598 -apply(drule CR3_CR4)
1.599 +apply(drule CR3_implies_CR4)
1.600 apply(simp add: CR4_def)
1.601 apply(drule_tac x="Var x" in spec)
1.602 apply(force simp add: NEUT_def NORMAL_Var)