1.1 --- a/src/HOL/Nominal/Examples/W.thy Tue Oct 21 21:20:46 2008 +0200
1.2 +++ b/src/HOL/Nominal/Examples/W.thy Tue Oct 21 21:22:02 2008 +0200
1.3 @@ -1,9 +1,317 @@
1.4 (* "$Id$" *)
1.5
1.6 theory W
1.7 -imports "Nominal"
1.8 +imports Nominal
1.9 begin
1.10
1.11 -text {* stub until a cleaned-up version will appear here *}
1.12 +text {* Example for strong induction rules avoiding sets of atoms. *}
1.13 +
1.14 +atom_decl tvar var
1.15 +
1.16 +abbreviation
1.17 + "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60)
1.18 +where
1.19 + "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
1.20 +
1.21 +lemma difference_eqvt_tvar[eqvt]:
1.22 + fixes pi::"tvar prm"
1.23 + and Xs Ys::"tvar list"
1.24 + shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)"
1.25 +by (induct Xs) (simp_all add: eqvts)
1.26 +
1.27 +lemma difference_fresh:
1.28 + fixes X::"tvar"
1.29 + and Xs Ys::"tvar list"
1.30 + assumes a: "X\<in>set Ys"
1.31 + shows "X\<sharp>(Xs - Ys)"
1.32 +using a
1.33 +by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)
1.34 +
1.35 +nominal_datatype ty =
1.36 + TVar "tvar"
1.37 + | Fun "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
1.38 +
1.39 +nominal_datatype tyS =
1.40 + Ty "ty"
1.41 + | ALL "\<guillemotleft>tvar\<guillemotright>tyS" ("\<forall>[_]._" [100,100] 100)
1.42 +
1.43 +nominal_datatype trm =
1.44 + Var "var"
1.45 + | App "trm" "trm"
1.46 + | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
1.47 + | Let "\<guillemotleft>var\<guillemotright>trm" "trm"
1.48 +
1.49 +abbreviation
1.50 + LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100)
1.51 +where
1.52 + "Let x be t1 in t2 \<equiv> trm.Let x t2 t1"
1.53 +
1.54 +types
1.55 + Ctxt = "(var\<times>tyS) list"
1.56 +
1.57 +text {* free type variables *}
1.58 +consts
1.59 + ftv :: "'a \<Rightarrow> tvar list"
1.60 +
1.61 +primrec (ftv_of_prod)
1.62 + "ftv (x,y) = (ftv x)@(ftv y)"
1.63 +
1.64 +defs (overloaded)
1.65 + ftv_of_tvar[simp]: "ftv X \<equiv> [(X::tvar)]"
1.66 + ftv_of_var[simp]: "ftv (x::var) \<equiv> []"
1.67 +
1.68 +primrec (ftv_of_list)
1.69 + "ftv [] = []"
1.70 + "ftv (x#xs) = (ftv x)@(ftv xs)"
1.71 +
1.72 +(* free type-variables of types *)
1.73 +nominal_primrec (ftv_ty)
1.74 + "ftv (TVar X) = [X]"
1.75 + "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
1.76 +by (rule TrueI)+
1.77 +
1.78 +lemma ftv_ty_eqvt[eqvt]:
1.79 + fixes pi::"tvar prm"
1.80 + and T::"ty"
1.81 + shows "pi\<bullet>(ftv T) = ftv (pi\<bullet>T)"
1.82 +by (nominal_induct T rule: ty.strong_induct)
1.83 + (perm_simp add: append_eqvt)+
1.84 +
1.85 +nominal_primrec (ftv_tyS)
1.86 + "ftv (Ty T) = ftv T"
1.87 + "ftv (\<forall>[X].S) = (ftv S) - [X]"
1.88 +apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
1.89 +apply(rule TrueI)+
1.90 +apply(rule difference_fresh)
1.91 +apply(simp)
1.92 +apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
1.93 +done
1.94 +
1.95 +lemma ftv_tyS_eqvt[eqvt]:
1.96 + fixes pi::"tvar prm"
1.97 + and S::"tyS"
1.98 + shows "pi\<bullet>(ftv S) = ftv (pi\<bullet>S)"
1.99 +apply(nominal_induct S rule: tyS.strong_induct)
1.100 +apply(simp add: eqvts)
1.101 +apply(simp only: ftv_tyS.simps)
1.102 +apply(simp only: eqvts)
1.103 +apply(simp add: eqvts)
1.104 +done
1.105 +
1.106 +lemma ftv_Ctxt_eqvt[eqvt]:
1.107 + fixes pi::"tvar prm"
1.108 + and \<Gamma>::"Ctxt"
1.109 + shows "pi\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)"
1.110 +by (induct \<Gamma>) (auto simp add: eqvts)
1.111 +
1.112 +text {* Valid *}
1.113 +inductive
1.114 + valid :: "Ctxt \<Rightarrow> bool"
1.115 +where
1.116 + V_Nil[intro]: "valid []"
1.117 +| V_Cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,S)#\<Gamma>)"
1.118 +
1.119 +equivariance valid
1.120 +
1.121 +text {* General *}
1.122 +consts
1.123 + gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"
1.124 +
1.125 +primrec
1.126 + "gen T [] = Ty T"
1.127 + "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
1.128 +
1.129 +lemma gen_eqvt[eqvt]:
1.130 + fixes pi::"tvar prm"
1.131 + shows "pi\<bullet>(gen T Xs) = gen (pi\<bullet>T) (pi\<bullet>Xs)"
1.132 +by (induct Xs) (simp_all add: eqvts)
1.133 +
1.134 +abbreviation
1.135 + close :: "Ctxt \<Rightarrow> ty \<Rightarrow> tyS"
1.136 +where
1.137 + "close \<Gamma> T \<equiv> gen T ((ftv T) - (ftv \<Gamma>))"
1.138 +
1.139 +lemma close_eqvt[eqvt]:
1.140 + fixes pi::"tvar prm"
1.141 + shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)"
1.142 +by (simp_all only: eqvts)
1.143 +
1.144 +text {* Substitution *}
1.145 +
1.146 +types Subst = "(tvar\<times>ty) list"
1.147 +
1.148 +consts
1.149 + psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a" ("_<_>" [100,60] 120)
1.150 +
1.151 +abbreviation
1.152 + subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100)
1.153 +where
1.154 + "smth[X::=T] \<equiv> ([(X,T)])<smth>"
1.155 +
1.156 +fun
1.157 + lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty"
1.158 +where
1.159 + "lookup [] X = TVar X"
1.160 +| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
1.161 +
1.162 +lemma lookup_eqvt[eqvt]:
1.163 + fixes pi::"tvar prm"
1.164 + shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
1.165 +by (induct \<theta>) (auto simp add: eqvts)
1.166 +
1.167 +nominal_primrec (psubst_ty)
1.168 + "\<theta><TVar X> = lookup \<theta> X"
1.169 + "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
1.170 +by (rule TrueI)+
1.171 +
1.172 +lemma psubst_ty_eqvt[eqvt]:
1.173 + fixes pi1::"tvar prm"
1.174 + and \<theta>::"Subst"
1.175 + and T::"ty"
1.176 + shows "pi1\<bullet>(\<theta><T>) = (pi1\<bullet>\<theta>)<(pi1\<bullet>T)>"
1.177 +by (induct T rule: ty.induct) (simp_all add: eqvts)
1.178 +
1.179 +text {* instance *}
1.180 +inductive
1.181 + general :: "ty \<Rightarrow> tyS \<Rightarrow> bool"("_ \<prec> _" [50,51] 50)
1.182 +where
1.183 + G_Ty[intro]: "T \<prec> (Ty T)"
1.184 +| G_All[intro]: "\<lbrakk>X\<sharp>T'; (T::ty) \<prec> S\<rbrakk> \<Longrightarrow> T[X::=T'] \<prec> \<forall>[X].S"
1.185 +
1.186 +equivariance general[tvar]
1.187 +
1.188 +text{* typing judgements *}
1.189 +inductive
1.190 + typing :: "Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (" _ \<turnstile> _ : _ " [60,60,60] 60)
1.191 +where
1.192 + T_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,S)\<in>set \<Gamma>; T \<prec> S\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
1.193 +| T_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
1.194 +| T_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,Ty T\<^isub>1)#\<Gamma>) \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
1.195 +| T_LET[intro]: "\<lbrakk>x\<sharp>\<Gamma>; \<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1; ((x,close \<Gamma> T\<^isub>1)#\<Gamma>) \<turnstile> t\<^isub>2 : T\<^isub>2; set (ftv T\<^isub>1 - ftv \<Gamma>) \<sharp>* T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^isub>1 in t\<^isub>2 : T\<^isub>2"
1.196 +
1.197 +lemma fresh_star_tvar_eqvt[eqvt]:
1.198 + "(pi::tvar prm) \<bullet> ((Xs::tvar set) \<sharp>* (x::'a::{cp_tvar_tvar,pt_tvar})) = (pi \<bullet> Xs) \<sharp>* (pi \<bullet> x)"
1.199 + by (simp only: pt_fresh_star_bij_ineq(1) [OF pt_tvar_inst pt_tvar_inst at_tvar_inst cp_tvar_tvar_inst] perm_bool)
1.200 +
1.201 +equivariance typing[tvar]
1.202 +
1.203 +lemma fresh_tvar_trm: "(X::tvar) \<sharp> (t::trm)"
1.204 + by (nominal_induct t rule: trm.strong_induct) (simp_all add: fresh_atm abs_fresh)
1.205 +
1.206 +lemma ftv_ty: "supp (T::ty) = set (ftv T)"
1.207 + by (nominal_induct T rule: ty.strong_induct) (simp_all add: ty.supp supp_atm)
1.208 +
1.209 +lemma ftv_tyS: "supp (s::tyS) = set (ftv s)"
1.210 + by (nominal_induct s rule: tyS.strong_induct) (auto simp add: tyS.supp abs_supp ftv_ty)
1.211 +
1.212 +lemma ftv_Ctxt: "supp (\<Gamma>::Ctxt) = set (ftv \<Gamma>)"
1.213 + apply (induct \<Gamma>)
1.214 + apply (simp_all add: supp_list_nil supp_list_cons)
1.215 + apply (case_tac a)
1.216 + apply (simp add: supp_prod supp_atm ftv_tyS)
1.217 + done
1.218 +
1.219 +lemma ftv_tvars: "supp (Tvs::tvar list) = set Tvs"
1.220 + by (induct Tvs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
1.221 +
1.222 +lemma difference_supp: "((supp ((xs::tvar list) - ys))::tvar set) = supp xs - supp ys"
1.223 + by (induct xs) (auto simp add: supp_list_nil supp_list_cons ftv_tvars)
1.224 +
1.225 +lemma set_supp_eq: "set (xs::tvar list) = supp xs"
1.226 + by (induct xs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
1.227 +
1.228 +nominal_inductive2 typing
1.229 + avoids T_LET: "set (ftv T\<^isub>1 - ftv \<Gamma>)"
1.230 + apply (simp add: fresh_star_def fresh_def ftv_Ctxt)
1.231 + apply (simp add: fresh_star_def fresh_tvar_trm)
1.232 + apply assumption
1.233 + apply simp
1.234 + done
1.235 +
1.236 +lemma perm_fresh_fresh_aux:
1.237 + "\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (z::'a::pt_tvar) = z"
1.238 + apply (induct pi rule: rev_induct)
1.239 + apply simp
1.240 + apply (simp add: split_paired_all pt_tvar2)
1.241 + apply (frule_tac x="(a, b)" in bspec)
1.242 + apply simp
1.243 + apply (simp add: perm_fresh_fresh)
1.244 + done
1.245 +
1.246 +lemma freshs_mem: "x \<in> (S::tvar set) \<Longrightarrow> S \<sharp>* z \<Longrightarrow> x \<sharp> z"
1.247 + by (simp add: fresh_star_def)
1.248 +
1.249 +lemma fresh_gen_set:
1.250 + fixes X::"tvar"
1.251 + and Xs::"tvar list"
1.252 + assumes asm: "X\<in>set Xs"
1.253 + shows "X\<sharp>gen T Xs"
1.254 +using asm
1.255 +apply(induct Xs)
1.256 +apply(simp)
1.257 +apply(case_tac "X=a")
1.258 +apply(simp add: abs_fresh)
1.259 +apply(simp add: abs_fresh)
1.260 +done
1.261 +
1.262 +lemma close_fresh:
1.263 + fixes \<Gamma>::"Ctxt"
1.264 + shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> T)"
1.265 +by (simp add: fresh_gen_set)
1.266 +
1.267 +lemma gen_supp: "(supp (gen T Xs)::tvar set) = supp T - supp Xs"
1.268 + by (induct Xs) (auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm)
1.269 +
1.270 +lemma minus_Int_eq: "T - (T - U) = T \<inter> U"
1.271 + by blast
1.272 +
1.273 +lemma close_supp: "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)"
1.274 + apply (simp add: gen_supp difference_supp ftv_ty ftv_Ctxt)
1.275 + apply (simp only: set_supp_eq minus_Int_eq)
1.276 + done
1.277 +
1.278 +lemma better_T_LET:
1.279 + assumes x: "x\<sharp>\<Gamma>"
1.280 + and t1: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1"
1.281 + and t2: "((x,close \<Gamma> T\<^isub>1)#\<Gamma>) \<turnstile> t\<^isub>2 : T\<^isub>2"
1.282 + shows "\<Gamma> \<turnstile> Let x be t\<^isub>1 in t\<^isub>2 : T\<^isub>2"
1.283 +proof -
1.284 + have fin: "finite (set (ftv T\<^isub>1 - ftv \<Gamma>))" by simp
1.285 + obtain pi where pi1: "(pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>)) \<sharp>* (T\<^isub>2, \<Gamma>)"
1.286 + and pi2: "set pi \<subseteq> set (ftv T\<^isub>1 - ftv \<Gamma>) \<times> (pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>))"
1.287 + by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^isub>2, \<Gamma>)"])
1.288 + from pi1 have pi1': "(pi \<bullet> set (ftv T\<^isub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>"
1.289 + by (simp add: fresh_star_prod)
1.290 + have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>"
1.291 + apply (rule ballI)
1.292 + apply (simp add: split_paired_all)
1.293 + apply (drule subsetD [OF pi2])
1.294 + apply (erule SigmaE)
1.295 + apply (drule freshs_mem [OF _ pi1'])
1.296 + apply (simp add: ftv_Ctxt [symmetric] fresh_def)
1.297 + done
1.298 + have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^isub>1 \<and> y \<sharp> close \<Gamma> T\<^isub>1"
1.299 + apply (rule ballI)
1.300 + apply (simp add: split_paired_all)
1.301 + apply (drule subsetD [OF pi2])
1.302 + apply (erule SigmaE)
1.303 + apply (drule bspec [OF close_fresh])
1.304 + apply (drule freshs_mem [OF _ pi1'])
1.305 + apply (simp add: fresh_def close_supp ftv_Ctxt)
1.306 + done
1.307 + note x
1.308 + moreover from Gamma_fresh perm_boolI [OF t1, of pi]
1.309 + have "\<Gamma> \<turnstile> t\<^isub>1 : pi \<bullet> T\<^isub>1"
1.310 + by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
1.311 + moreover from t2 close_fresh'
1.312 + have "(x,(pi \<bullet> close \<Gamma> T\<^isub>1))#\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
1.313 + by (simp add: perm_fresh_fresh_aux)
1.314 + with Gamma_fresh have "(x,close \<Gamma> (pi \<bullet> T\<^isub>1))#\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
1.315 + by (simp add: close_eqvt perm_fresh_fresh_aux)
1.316 + moreover from pi1 Gamma_fresh
1.317 + have "set (ftv (pi \<bullet> T\<^isub>1) - ftv \<Gamma>) \<sharp>* T\<^isub>2"
1.318 + by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux)
1.319 + ultimately show ?thesis by (rule T_LET)
1.320 +qed
1.321
1.322 end