1.1 --- a/src/HOL/Nominal/Examples/SN.thy Sun Dec 04 12:14:03 2005 +0100
1.2 +++ b/src/HOL/Nominal/Examples/SN.thy Sun Dec 04 12:14:27 2005 +0100
1.3 @@ -836,7 +836,7 @@
1.4 apply(auto simp add: fresh_prod fresh_list_cons)
1.5 done
1.6
1.7 -lemma psubs_subs[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
1.8 +lemma psubst_subst[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
1.9 apply(nominal_induct t avoiding: \<theta> c s rule: lam_induct)
1.10 apply(auto dest: fresh_domain)
1.11 apply(drule fresh_at)
1.12 @@ -849,148 +849,42 @@
1.13 apply(simp add: fresh_list_cons fresh_prod)
1.14 done
1.15
1.16 +thm fresh_context
1.17 +
1.18 lemma all_RED:
1.19 - "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
1.20 + assumes a: "\<Gamma>\<turnstile>t:\<tau>"
1.21 + and b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)"
1.22 + shows "t[<\<theta>>]\<in>RED \<tau>"
1.23 +using a b
1.24 +proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
1.25 + case (Lam a t) --"lambda case"
1.26 + have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow>
1.27 + (\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>)
1.28 + \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>"
1.29 + and \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>"
1.30 + and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>"
1.31 + and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
1.32 + hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
1.33 + then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
1.34 + from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
1.35 + by (force dest: fresh_context simp add: psubst_subst)
1.36 + hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
1.37 + thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
1.38 +qed (force dest!: t1_elim t2_elim)+
1.39 +
1.40 +lemma all_RED:
1.41 + assumes a: "\<Gamma>\<turnstile>t:\<tau>"
1.42 + and b: "\<And>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<Longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)"
1.43 + shows "t[<\<theta>>]\<in>RED \<tau>"
1.44 +using a b
1.45 apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
1.46 (* Variables *)
1.47 apply(force dest: t1_elim)
1.48 (* Applications *)
1.49 apply(atomize)
1.50 apply(force dest!: t2_elim)
1.51 -(* Abstractions *)
1.52 -apply(auto dest!: t3_elim simp only:)
1.53 -apply(simp only: fresh_prod psubst_Lam)
1.54 +(* Abstractions *)
1.55 +apply(auto dest!: t3_elim simp only: psubst_Lam)
1.56 apply(rule abs_RED[THEN mp])
1.57 apply(force dest: fresh_context simp add: psubs_subs)
1.58 -done
1.59 -
1.60 -lemma all_RED:
1.61 - "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
1.62 -apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
1.63 -(* Variables *)
1.64 -apply(force dest: t1_elim)
1.65 -(* Applications *)
1.66 -apply(atomize)
1.67 -apply(clarify)
1.68 -apply(drule t2_elim)
1.69 -apply(erule exE, erule conjE)
1.70 -apply(drule_tac x="\<Gamma>" in spec)
1.71 -apply(drule_tac x="\<Gamma>" in spec)
1.72 -apply(drule_tac x="\<tau>'\<rightarrow>\<tau>" in spec)
1.73 -apply(drule_tac x="\<tau>'" in spec)
1.74 -apply(drule_tac x="\<theta>" in spec)
1.75 -apply(drule_tac x="\<theta>" in spec)
1.76 -apply(force)
1.77 -(* Abstractions *)
1.78 -apply(clarify)
1.79 -apply(drule t3_elim)
1.80 -apply(simp add: fresh_prod)
1.81 -apply(erule exE)+
1.82 -apply(erule conjE)
1.83 -apply(simp only: fresh_prod psubst_Lam)
1.84 -apply(rule abs_RED[THEN mp])
1.85 -apply(clarify)
1.86 -apply(atomize)
1.87 -apply(force dest: fresh_context simp add: psubs_subs)
1.88 -done
1.89 -
1.90 -
1.91 -lemma all_RED:
1.92 - "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
1.93 -proof(nominal_induct t rule: lam_induct)
1.94 - case Var
1.95 - show ?case by (force dest: t1_elim)
1.96 -next
1.97 - case App
1.98 - thus ?case by (force dest!: t2_elim)
1.99 -(* HERE *)
1.100 -next
1.101 - case (Lam \<Gamma> \<tau> \<theta> a t)
1.102 - have ih:
1.103 - "\<forall>\<Gamma> \<tau> \<theta>. (\<forall>\<sigma> c. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>) \<and> \<Gamma> \<turnstile> t : \<tau> \<longrightarrow> t[<\<theta>>]\<in>RED \<tau>"
1.104 - by fact
1.105 - have "a\<sharp>(\<Gamma>,\<tau>,\<theta>)" by fact
1.106 - hence b1: "a\<sharp>\<Gamma>" and b2: "a\<sharp>\<tau>" and b3: "a\<sharp>\<theta>" by (simp_all add: fresh_prod)
1.107 - from b1 have c1: "\<not>(\<exists>\<tau>. (a,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
1.108 - show ?case using b1
1.109 - proof (auto dest!: t3_elim simp only: psubst_Lam)
1.110 - fix \<sigma>1::"ty" and \<sigma>2::"ty"
1.111 - assume a1: "((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2"
1.112 - and a3: "\<forall>(\<sigma>\<Colon>ty) (c\<Colon>name). (c,\<sigma>) \<in> set \<Gamma> \<longrightarrow> c \<in> set (domain \<theta>) \<and> \<theta> <c> \<in> RED \<sigma>"
1.113 - have "\<forall>s\<in>RED \<sigma>1. (t[<\<theta>>])[a::=s]\<in>RED \<sigma>2"
1.114 - proof
1.115 -(* HERE *)
1.116 -
1.117 - fix s::"lam"
1.118 - assume a4: "s \<in> RED \<sigma>1"
1.119 - from ih have "\<forall>\<sigma> c. (c,\<sigma>)\<in>set ((a,\<sigma>1)#\<Gamma>) \<longrightarrow> c\<in>set (domain ((c,s)#\<theta>)) \<and> (((c,s)#\<theta>)<c>)\<in>RED \<sigma>"
1.120 - using c1 a4 proof (auto)
1.121 -apply(simp)
1.122 - apply(rule allI)+
1.123 - apply(rule conjI)
1.124 -
1.125 - proof (auto) *)
1.126 - have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,s)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 b3
1.127 - proof(blast dest: fresh_context)
1.128 -
1.129 - show "(t[<\<theta>>])[a::=s] \<in> RED \<sigma>2"
1.130 -
1.131 - qed
1.132 - thus "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" by (simp only: abs_RED)
1.133 - qed
1.134 -qed
1.135 -
1.136 -
1.137 -
1.138 -
1.139 -
1.140 - have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 sorry
1.141 - hence "t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using a1 by simp
1.142 - hence "t[<\<theta>>][a::=u] \<in> RED \<sigma>2" using b3 by (simp add: psubs_subs)
1.143 - show "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)"
1.144 - hence "Lam [a].(t[<\<theta>>]) \<in> RED (\<tau>\<rightarrow>\<sigma>)" using a2 abs_RED by force
1.145 - show "App (Lam [a].(t[<\<theta>>])) u \<in> RED \<sigma>2"
1.146 -
1.147 -
1.148 -
1.149 - thus ?case using t2_elim
1.150 - proof(auto, blast)
1.151 -
1.152 -qed
1.153 -
1.154 -(* Variables *)
1.155 -apply(force dest: t1_elim)
1.156 -(* Applications *)
1.157 -apply(clarify)
1.158 -apply(drule t2_elim)
1.159 -apply(erule exE, erule conjE)
1.160 -apply(drule_tac x="a" in spec)
1.161 -apply(drule_tac x="a" in spec)
1.162 -apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
1.163 -apply(drule_tac x="\<tau>" in spec)
1.164 -apply(drule_tac x="b" in spec)
1.165 -apply(drule_tac x="b" in spec)
1.166 -apply(force)
1.167 -(* Abstractions *)
1.168 -apply(clarify)
1.169 -apply(drule t3_elim)
1.170 -apply(simp add: fresh_prod)
1.171 -apply(erule exE)+
1.172 -apply(erule conjE)
1.173 -apply(simp only: fresh_prod psubst_Lam)
1.174 -apply(rule abs_RED)
1.175 -apply(auto)
1.176 -apply(drule_tac x="(ab,\<tau>)#a" in spec)
1.177 -apply(drule_tac x="\<tau>'" in spec)
1.178 -apply(drule_tac x="(ab,s)#b" in spec)
1.179 -apply(simp)
1.180 -apply(auto)
1.181 -apply(drule fresh_context)
1.182 -apply(simp)
1.183 -apply(simp add: psubs_subs)
1.184 -done
1.185 -
1.186 -
1.187 -
1.188 -done
1.189 -
1.190 +done
1.191 \ No newline at end of file