Example for using the generalized version of nominal_inductive.
authorberghofe
Tue Oct 21 21:22:02 2008 +0200 (2008-10-21)
changeset 286552822c56dd1cf
parent 28654 2f9857126498
child 28656 e92c79b3b154
Example for using the generalized version of nominal_inductive.
src/HOL/Nominal/Examples/W.thy
     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