added an Isar-proof for the abs_ALL lemma
authorurbanc
Sun Dec 04 12:14:27 2005 +0100 (2005-12-04)
changeset 18345d37fb71754fe
parent 18344 95083a68cbbb
child 18346 c9be8266325f
added an Isar-proof for the abs_ALL lemma
src/HOL/Nominal/Examples/SN.thy
     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