1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/NBE.thy Tue Jun 26 13:02:28 2007 +0200
1.3 @@ -0,0 +1,865 @@
1.4 +(* ID: $Id$
1.5 + Author: Klaus Aehlig, Tobias Nipkow
1.6 + Work in progress
1.7 +*)
1.8 +
1.9 +theory NBE imports Main ExecutableSet begin
1.10 +
1.11 +ML"set quick_and_dirty"
1.12 +
1.13 +declare Let_def[simp]
1.14 +
1.15 +consts_code undefined ("(raise Match)")
1.16 +
1.17 +(*typedecl const_name*)
1.18 +types lam_var_name = nat
1.19 + ml_var_name = nat
1.20 + const_name = nat
1.21 +
1.22 +datatype tm = Ct const_name | Vt lam_var_name | Lam tm | At tm tm
1.23 + | term_of ml (* function 'to_term' *)
1.24 +and ml = (* rep of universal datatype *)
1.25 + C const_name "ml list" | V lam_var_name "ml list"
1.26 + | Fun ml "ml list" nat
1.27 + | "apply" ml ml (* function 'apply' *)
1.28 + (* ML *)
1.29 + | V_ML ml_var_name | A_ML ml "ml list" | Lam_ML ml
1.30 + | CC const_name (* ref to compiled code *)
1.31 +
1.32 +lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (ml_list_size1 vs)"
1.33 +by (induct vs) auto
1.34 +lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (ml_list_size2 vs)"
1.35 +by (induct vs) auto
1.36 +lemma [simp]:"x \<in> set vs \<Longrightarrow> size x < Suc (size v + ml_list_size3 vs)"
1.37 +by (induct vs) auto
1.38 +lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (size v + ml_list_size4 vs)"
1.39 +by (induct vs) auto
1.40 +
1.41 +locale Vars =
1.42 + fixes r s t:: tm
1.43 + and rs ss ts :: "tm list"
1.44 + and u v w :: ml
1.45 + and us vs ws :: "ml list"
1.46 + and nm :: const_name
1.47 + and x :: lam_var_name
1.48 + and X :: ml_var_name
1.49 +
1.50 +consts Pure_tms :: "tm set"
1.51 +inductive Pure_tms
1.52 +intros
1.53 +"Ct s : Pure_tms"
1.54 +"Vt x : Pure_tms"
1.55 +"t : Pure_tms ==> Lam t : Pure_tms"
1.56 +"s : Pure_tms ==> t : Pure_tms ==> At s t : Pure_tms"
1.57 +
1.58 +consts
1.59 + R :: "(const_name * tm list * tm)set" (* reduction rules *)
1.60 + compR :: "(const_name * ml list * ml)set" (* compiled reduction rules *)
1.61 + tRed :: "(tm * tm)set" (* beta + R reduction on pure terms *)
1.62 + tRed_list :: "(tm list * tm list) set"
1.63 +
1.64 +fun
1.65 + lift_tm :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift") and
1.66 + lift_ml :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift")
1.67 +where
1.68 +"lift i (Ct nm) = Ct nm" |
1.69 +"lift i (Vt x) = Vt(if x < i then x else x+1)" |
1.70 +"lift i (Lam t) = Lam (lift (i+1) t)" |
1.71 +"lift i (At s t) = At (lift i s) (lift i t)" |
1.72 +"lift i (term_of v) = term_of (lift i v)" |
1.73 +
1.74 +"lift i (C nm vs) = C nm (map (lift i) vs)" |
1.75 +"lift i (V x vs) = V (if x < i then x else x+1) (map (lift i) vs)" |
1.76 +"lift i (Fun v vs n) = Fun (lift i v) (map (lift i) vs) n" |
1.77 +"lift i (apply u v) = apply (lift i u) (lift i v)" |
1.78 +"lift i (V_ML X) = V_ML X" |
1.79 +"lift i (A_ML v vs) = A_ML (lift i v) (map (lift i) vs)" |
1.80 +"lift i (Lam_ML v) = Lam_ML (lift i v)" |
1.81 +"lift i (CC nm) = CC nm"
1.82 +(*
1.83 +termination
1.84 +apply (relation "measure (sum_case (%(i,t). size t) (%(i,v). size v))")
1.85 +apply auto
1.86 +*)
1.87 +
1.88 +fun
1.89 + lift_tm_ML :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift\<^bsub>ML\<^esub>") and
1.90 + lift_ml_ML :: "nat \<Rightarrow> ml \<Rightarrow> ml" ("lift\<^bsub>ML\<^esub>")
1.91 +where
1.92 +"lift\<^bsub>ML\<^esub> i (Ct nm) = Ct nm" |
1.93 +"lift\<^bsub>ML\<^esub> i (Vt x) = Vt x" |
1.94 +"lift\<^bsub>ML\<^esub> i (Lam t) = Lam (lift\<^bsub>ML\<^esub> i t)" |
1.95 +"lift\<^bsub>ML\<^esub> i (At s t) = At (lift\<^bsub>ML\<^esub> i s) (lift\<^bsub>ML\<^esub> i t)" |
1.96 +"lift\<^bsub>ML\<^esub> i (term_of v) = term_of (lift\<^bsub>ML\<^esub> i v)" |
1.97 +
1.98 +"lift\<^bsub>ML\<^esub> i (C nm vs) = C nm (map (lift\<^bsub>ML\<^esub> i) vs)" |
1.99 +"lift\<^bsub>ML\<^esub> i (V x vs) = V x (map (lift\<^bsub>ML\<^esub> i) vs)" |
1.100 +"lift\<^bsub>ML\<^esub> i (Fun v vs n) = Fun (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs) n" |
1.101 +"lift\<^bsub>ML\<^esub> i (apply u v) = apply (lift\<^bsub>ML\<^esub> i u) (lift\<^bsub>ML\<^esub> i v)" |
1.102 +"lift\<^bsub>ML\<^esub> i (V_ML X) = V_ML (if X < i then X else X+1)" |
1.103 +"lift\<^bsub>ML\<^esub> i (A_ML v vs) = A_ML (lift\<^bsub>ML\<^esub> i v) (map (lift\<^bsub>ML\<^esub> i) vs)" |
1.104 +"lift\<^bsub>ML\<^esub> i (Lam_ML v) = Lam_ML (lift\<^bsub>ML\<^esub> (i+1) v)" |
1.105 +"lift\<^bsub>ML\<^esub> i (CC nm) = CC nm"
1.106 +(*
1.107 +termination
1.108 + by (relation "measure (sum_case (%(i,t). size t) (%(i,v). size v))") auto
1.109 +*)
1.110 +constdefs
1.111 + cons :: "tm \<Rightarrow> (nat \<Rightarrow> tm) \<Rightarrow> (nat \<Rightarrow> tm)" (infix "##" 65)
1.112 +"t##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> t | Suc j \<Rightarrow> lift 0 (f j)"
1.113 + cons_ML :: "ml \<Rightarrow> (nat \<Rightarrow> ml) \<Rightarrow> (nat \<Rightarrow> ml)" (infix "##" 65)
1.114 +"v##f \<equiv> \<lambda>i. case i of 0 \<Rightarrow> v::ml | Suc j \<Rightarrow> lift\<^bsub>ML\<^esub> 0 (f j)"
1.115 +
1.116 +(* Only for pure terms! *)
1.117 +consts subst :: "(nat \<Rightarrow> tm) \<Rightarrow> tm \<Rightarrow> tm"
1.118 +primrec
1.119 +"subst f (Ct nm) = Ct nm"
1.120 +"subst f (Vt x) = f x"
1.121 +"subst f (Lam t) = Lam (subst (Vt 0 ## f) t)"
1.122 +"subst f (At s t) = At (subst f s) (subst f t)"
1.123 +
1.124 +lemma size_lift[simp]: shows
1.125 + "size(lift i t) = size(t::tm)" and "size(lift i (v::ml)) = size v"
1.126 +and "ml_list_size1 (map (lift i) vs) = ml_list_size1 vs"
1.127 +and "ml_list_size2 (map (lift i) vs) = ml_list_size2 vs"
1.128 +and "ml_list_size3 (map (lift i) vs) = ml_list_size3 vs"
1.129 +and "ml_list_size4 (map (lift i) vs) = ml_list_size4 vs"
1.130 +by (induct arbitrary: i and i and i and i and i and i rule: tm_ml.inducts)
1.131 + simp_all
1.132 +
1.133 +lemma size_lift_ML[simp]: shows
1.134 + "size(lift\<^bsub>ML\<^esub> i t) = size(t::tm)" and "size(lift\<^bsub>ML\<^esub> i (v::ml)) = size v"
1.135 +and "ml_list_size1 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size1 vs"
1.136 +and "ml_list_size2 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size2 vs"
1.137 +and "ml_list_size3 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size3 vs"
1.138 +and "ml_list_size4 (map (lift\<^bsub>ML\<^esub> i) vs) = ml_list_size4 vs"
1.139 +by (induct arbitrary: i and i and i and i and i and i rule: tm_ml.inducts)
1.140 + simp_all
1.141 +
1.142 +fun
1.143 + subst_ml_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> ml \<Rightarrow> ml" ("subst\<^bsub>ML\<^esub>") and
1.144 + subst_tm_ML :: "(nat \<Rightarrow> ml) \<Rightarrow> tm \<Rightarrow> tm" ("subst\<^bsub>ML\<^esub>")
1.145 +where
1.146 +"subst\<^bsub>ML\<^esub> f (Ct nm) = Ct nm" |
1.147 +"subst\<^bsub>ML\<^esub> f (Vt x) = Vt x" |
1.148 +"subst\<^bsub>ML\<^esub> f (Lam t) = Lam (subst\<^bsub>ML\<^esub> (lift 0 o f) t)" |
1.149 +"subst\<^bsub>ML\<^esub> f (At s t) = At (subst\<^bsub>ML\<^esub> f s) (subst\<^bsub>ML\<^esub> f t)" |
1.150 +"subst\<^bsub>ML\<^esub> f (term_of v) = term_of (subst\<^bsub>ML\<^esub> f v)" |
1.151 +
1.152 +"subst\<^bsub>ML\<^esub> f (C nm vs) = C nm (map (subst\<^bsub>ML\<^esub> f) vs)" |
1.153 +"subst\<^bsub>ML\<^esub> f (V x vs) = V x (map (subst\<^bsub>ML\<^esub> f) vs)" |
1.154 +"subst\<^bsub>ML\<^esub> f (Fun v vs n) = Fun (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs) n" |
1.155 +"subst\<^bsub>ML\<^esub> f (apply u v) = apply (subst\<^bsub>ML\<^esub> f u) (subst\<^bsub>ML\<^esub> f v)" |
1.156 +"subst\<^bsub>ML\<^esub> f (V_ML X) = f X" |
1.157 +"subst\<^bsub>ML\<^esub> f (A_ML v vs) = A_ML (subst\<^bsub>ML\<^esub> f v) (map (subst\<^bsub>ML\<^esub> f) vs)" |
1.158 +"subst\<^bsub>ML\<^esub> f (Lam_ML v) = Lam_ML (subst\<^bsub>ML\<^esub> (V_ML 0 ## f) v)" |
1.159 +"subst\<^bsub>ML\<^esub> f (CC nm) = CC nm"
1.160 +
1.161 +(* FIXME currrently needed for code generator *)
1.162 +lemmas [code] = lift_tm_ML.simps lift_ml_ML.simps
1.163 +lemmas [code] = lift_tm.simps lift_ml.simps
1.164 +lemmas [code] = subst_tm_ML.simps subst_ml_ML.simps
1.165 +
1.166 +abbreviation
1.167 + subst_decr :: "nat \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" where
1.168 + "subst_decr k t == %n. if n<k then Vt n else if n=k then t else Vt(n - 1)"
1.169 +abbreviation
1.170 + subst_decr_ML :: "nat \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" where
1.171 + "subst_decr_ML k v == %n. if n<k then V_ML n else if n=k then v else V_ML(n - 1)"
1.172 +abbreviation
1.173 + subst1 :: "tm \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm" ("(_/[_'/_])" [300, 0, 0] 300) where
1.174 + "s[t/k] == subst (subst_decr k t) s"
1.175 +abbreviation
1.176 + subst1_ML :: "ml \<Rightarrow> ml \<Rightarrow> nat \<Rightarrow> ml" ("(_/[_'/_])" [300, 0, 0] 300) where
1.177 + "u[v/k] == subst\<^bsub>ML\<^esub> (subst_decr_ML k v) u"
1.178 +
1.179 +
1.180 +lemma size_subst_ML[simp]: shows
1.181 + "(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f t) = size(t::tm)" and
1.182 +"(!x. size(f x) = 0) \<longrightarrow> size(subst\<^bsub>ML\<^esub> f (v::ml)) = size v"
1.183 +and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size1 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size1 vs"
1.184 +and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size2 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size2 vs"
1.185 +and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size3 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size3 vs"
1.186 +and "(!x. size(f x) = 0) \<longrightarrow> ml_list_size4 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size4 vs"
1.187 +apply (induct arbitrary: f and f and f and f and f and f rule: tm_ml.inducts)
1.188 +apply (simp_all add:cons_ML_def split:nat.split)
1.189 +done
1.190 +
1.191 +lemma lift_lift: includes Vars shows
1.192 + "i < k+1 \<Longrightarrow> lift (Suc k) (lift i t) = lift i (lift k t)"
1.193 +and "i < k+1 \<Longrightarrow> lift (Suc k) (lift i v) = lift i (lift k v)"
1.194 +apply(induct t and v arbitrary: i and i rule:lift_tm_lift_ml.induct)
1.195 +apply(simp_all add:map_compose[symmetric])
1.196 +done
1.197 +
1.198 +corollary lift_o_lift: shows
1.199 + "i < k+1 \<Longrightarrow> lift_tm (Suc k) o (lift_tm i) = lift_tm i o lift_tm k" and
1.200 + "i < k+1 \<Longrightarrow> lift_ml (Suc k) o (lift_ml i) = lift_ml i o lift_ml k"
1.201 +by(rule ext, simp add:lift_lift)+
1.202 +
1.203 +lemma lift_lift_ML: includes Vars shows
1.204 + "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k t)"
1.205 +and "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k v)"
1.206 +apply(induct t and v arbitrary: i and i rule:lift_tm_ML_lift_ml_ML.induct)
1.207 +apply(simp_all add:map_compose[symmetric])
1.208 +done
1.209 +
1.210 +
1.211 +lemma lift_lift_ML_comm: includes Vars shows
1.212 + "lift j (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift j t)" and
1.213 + "lift j (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift j v)"
1.214 +apply(induct t and v arbitrary: i j and i j rule:lift_tm_ML_lift_ml_ML.induct)
1.215 +apply(simp_all add:map_compose[symmetric])
1.216 +done
1.217 +
1.218 +lemma [simp]:
1.219 + "V_ML 0 ## subst_decr_ML k v = subst_decr_ML (Suc k) (lift\<^bsub>ML\<^esub> 0 v)"
1.220 +by(rule ext)(simp add:cons_ML_def split:nat.split)
1.221 +
1.222 +lemma [simp]: "lift 0 o subst_decr_ML k v = subst_decr_ML k (lift 0 v)"
1.223 +by(rule ext)(simp add:cons_ML_def split:nat.split)
1.224 +
1.225 +lemma subst_lift_id[simp]: includes Vars shows
1.226 + "subst\<^bsub>ML\<^esub> (subst_decr_ML k v) (lift\<^bsub>ML\<^esub> k t) = t" and "(lift\<^bsub>ML\<^esub> k u)[v/k] = u"
1.227 +apply(induct k t and k u arbitrary: v and v rule: lift_tm_ML_lift_ml_ML.induct)
1.228 +apply (simp_all add:map_idI map_compose[symmetric])
1.229 +apply (simp cong:if_cong)
1.230 +done
1.231 +
1.232 +abbreviation
1.233 + tred :: "[tm, tm] => bool" (infixl "\<rightarrow>" 50) where
1.234 + "s \<rightarrow> t == (s, t) \<in> tRed"
1.235 +abbreviation
1.236 + treds :: "[tm, tm] => bool" (infixl "\<rightarrow>*" 50) where
1.237 + "s \<rightarrow>* t == (s, t) \<in> tRed^*"
1.238 +abbreviation
1.239 + treds_list :: "[tm list, tm list] \<Rightarrow> bool" (infixl "\<rightarrow>*" 50) where
1.240 + "ss \<rightarrow>* ts == (ss, ts) \<in> tRed_list"
1.241 +
1.242 +inductive tRed
1.243 +intros
1.244 +"At (Lam t) s \<rightarrow> t[s/0]"
1.245 +"(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t"
1.246 +"t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'"
1.247 +"s \<rightarrow> s' ==> At s t \<rightarrow> At s' t"
1.248 +"t \<rightarrow> t' ==> At s t \<rightarrow> At s t'"
1.249 +
1.250 +inductive tRed_list
1.251 +intros
1.252 +"[] \<rightarrow>* []"
1.253 +"ts \<rightarrow>* ts' ==> t \<rightarrow>* t' ==> t#ts \<rightarrow>* t'#ts'"
1.254 +
1.255 +declare tRed_list.intros[simp]
1.256 +
1.257 +lemma tRed_list_refl[simp]: includes Vars shows "ts \<rightarrow>* ts"
1.258 +by(induct ts) auto
1.259 +
1.260 +consts
1.261 + Red :: "(ml * ml)set"
1.262 + Redl :: "(ml list * ml list)set"
1.263 + Redt :: "(tm * tm)set"
1.264 +
1.265 +abbreviation
1.266 + red :: "[ml, ml] => bool" (infixl "\<Rightarrow>" 50) where
1.267 + "s \<Rightarrow> t == (s, t) \<in> Red"
1.268 +abbreviation
1.269 + redl :: "[ml list, ml list] => bool" (infixl "\<Rightarrow>" 50) where
1.270 + "s \<Rightarrow> t == (s, t) \<in> Redl"
1.271 +abbreviation
1.272 + redt :: "[tm, tm] => bool" (infixl "\<Rightarrow>" 50) where
1.273 + "s \<Rightarrow> t == (s, t) \<in> Redt"
1.274 +abbreviation
1.275 + reds :: "[ml, ml] => bool" (infixl "\<Rightarrow>*" 50) where
1.276 + "s \<Rightarrow>* t == (s, t) \<in> Red^*"
1.277 +abbreviation
1.278 + redts :: "[tm, tm] => bool" (infixl "\<Rightarrow>*" 50) where
1.279 + "s \<Rightarrow>* t == (s, t) \<in> Redt^*"
1.280 +
1.281 +
1.282 +fun ML_closed :: "nat \<Rightarrow> ml \<Rightarrow> bool"
1.283 +and ML_closed_t :: "nat \<Rightarrow> tm \<Rightarrow> bool" where
1.284 +"ML_closed i (C nm vs) = (ALL v:set vs. ML_closed i v)" |
1.285 +"ML_closed i (V nm vs) = (ALL v:set vs. ML_closed i v)" |
1.286 +"ML_closed i (Fun f vs n) = (ML_closed i f & (ALL v:set vs. ML_closed i v))" |
1.287 +"ML_closed i (A_ML v vs) = (ML_closed i v & (ALL v:set vs. ML_closed i v))" |
1.288 +"ML_closed i (apply v w) = (ML_closed i v & ML_closed i w)" |
1.289 +"ML_closed i (CC nm) = True" |
1.290 +"ML_closed i (V_ML X) = (X<i)" |
1.291 +"ML_closed i (Lam_ML v) = ML_closed (i+1) v" |
1.292 +"ML_closed_t i (term_of v) = ML_closed i v" |
1.293 +"ML_closed_t i (At r s) = (ML_closed_t i r & ML_closed_t i s)" |
1.294 +"ML_closed_t i (Lam t) = (ML_closed_t i t)" |
1.295 +"ML_closed_t i v = True"
1.296 +thm ML_closed.simps ML_closed_t.simps
1.297 +
1.298 +inductive Red Redt Redl
1.299 +intros
1.300 +(* ML *)
1.301 +"A_ML (Lam_ML u) [v] \<Rightarrow> u[v/0]"
1.302 +(* compiled rules *)
1.303 +"(nm,vs,v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs) \<Rightarrow> subst\<^bsub>ML\<^esub> f v"
1.304 +(* apply *)
1.305 +apply_Fun1: "apply (Fun f vs (Suc 0)) v \<Rightarrow> A_ML f (vs @ [v])"
1.306 +apply_Fun2: "n > 0 ==>
1.307 + apply (Fun f vs (Suc n)) v \<Rightarrow> Fun f (vs @ [v]) n"
1.308 +apply_C: "apply (C nm vs) v \<Rightarrow> C nm (vs @ [v])"
1.309 +apply_V: "apply (V x vs) v \<Rightarrow> V x (vs @ [v])"
1.310 +(* term_of *)
1.311 +term_of_C: "term_of (C nm vs) \<Rightarrow> foldl At (Ct nm) (map term_of vs)"
1.312 +term_of_V: "term_of (V x vs) \<Rightarrow> foldl At (Vt x) (map term_of vs)"
1.313 +term_of_Fun: "term_of(Fun vf vs n) \<Rightarrow>
1.314 + Lam (term_of ((apply (lift 0 (Fun vf vs n)) (V_ML 0))[V 0 []/0]))"
1.315 +(* Context *)
1.316 +ctxt_Lam: "t \<Rightarrow> t' ==> Lam t \<Rightarrow> Lam t'"
1.317 +ctxt_At1: "s \<Rightarrow> s' ==> At s t \<Rightarrow> At s' t"
1.318 +ctxt_At2: "t \<Rightarrow> t' ==> At s t \<Rightarrow> At s t'"
1.319 +ctxt_term_of: "v \<Rightarrow> v' ==> term_of v \<Rightarrow> term_of v'"
1.320 +ctxt_C: "vs \<Rightarrow> vs' ==> C nm vs \<Rightarrow> C nm vs'"
1.321 +ctxt_V: "vs \<Rightarrow> vs' ==> V x vs \<Rightarrow> V x vs'"
1.322 +ctxt_Fun1: "f \<Rightarrow> f' ==> Fun f vs n \<Rightarrow> Fun f' vs n"
1.323 +ctxt_Fun3: "vs \<Rightarrow> vs' ==> Fun f vs n \<Rightarrow> Fun f vs' n"
1.324 +ctxt_apply1: "s \<Rightarrow> s' ==> apply s t \<Rightarrow> apply s' t"
1.325 +ctxt_apply2: "t \<Rightarrow> t' ==> apply s t \<Rightarrow> apply s t'"
1.326 +ctxt_A_ML1: "f \<Rightarrow> f' ==> A_ML f vs \<Rightarrow> A_ML f' vs"
1.327 +ctxt_A_ML2: "vs \<Rightarrow> vs' ==> A_ML f vs \<Rightarrow> A_ML f vs'"
1.328 +ctxt_list1: "v \<Rightarrow> v' ==> v#vs \<Rightarrow> v'#vs"
1.329 +ctxt_list2: "vs \<Rightarrow> vs' ==> v#vs \<Rightarrow> v#vs'"
1.330 +
1.331 +
1.332 +consts
1.333 + ar :: "const_name \<Rightarrow> nat"
1.334 +
1.335 +axioms
1.336 +ar_pos: "ar nm > 0"
1.337 +
1.338 +types env = "ml list"
1.339 +
1.340 +consts eval :: "tm \<Rightarrow> env \<Rightarrow> ml"
1.341 +primrec
1.342 +"eval (Vt x) e = e!x"
1.343 +"eval (Ct nm) e = Fun (CC nm) [] (ar nm)"
1.344 +"eval (At s t) e = apply (eval s e) (eval t e)"
1.345 +"eval (Lam t) e = Fun (Lam_ML (eval t ((V_ML 0) # map (lift\<^bsub>ML\<^esub> 0) e))) [] 1"
1.346 +
1.347 +fun size' :: "ml \<Rightarrow> nat" where
1.348 +"size' (C nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" |
1.349 +"size' (V nm vs) = (\<Sum>v\<leftarrow>vs. size' v)+1" |
1.350 +"size' (Fun f vs n) = (size' f + (\<Sum>v\<leftarrow>vs. size' v))+1" |
1.351 +"size' (A_ML v vs) = (size' v + (\<Sum>v\<leftarrow>vs. size' v))+1" |
1.352 +"size' (apply v w) = (size' v + size' w)+1" |
1.353 +"size' (CC nm) = 1" |
1.354 +"size' (V_ML X) = 1" |
1.355 +"size' (Lam_ML v) = size' v + 1"
1.356 +
1.357 +lemma listsum_size'[simp]:
1.358 + "v \<in> set vs \<Longrightarrow> size' v < Suc(listsum (map size' vs))"
1.359 +sorry
1.360 +
1.361 +corollary cor_listsum_size'[simp]:
1.362 + "v \<in> set vs \<Longrightarrow> size' v < Suc(m + listsum (map size' vs))"
1.363 +using listsum_size'[of v vs] by arith
1.364 +
1.365 +lemma
1.366 +size_subst_ML[simp]: includes Vars assumes A: "!i. size(f i) = 0"
1.367 +shows "size(subst\<^bsub>ML\<^esub> f t) = size(t)"
1.368 +and "size(subst\<^bsub>ML\<^esub> f v) = size(v)"
1.369 +and "ml_list_size1 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size1 vs"
1.370 +and "ml_list_size2 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size2 vs"
1.371 +and "ml_list_size3 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size3 vs"
1.372 +and "ml_list_size4 (map (subst\<^bsub>ML\<^esub> f) vs) = ml_list_size4 vs"
1.373 +by (induct rule: tm_ml.inducts) (simp_all add: A cons_ML_def split:nat.split)
1.374 +
1.375 +lemma [simp]:
1.376 + "\<forall>i j. size'(f i) = size'(V_ML j) \<Longrightarrow> size' (subst\<^bsub>ML\<^esub> f v) = size' v"
1.377 +sorry
1.378 +
1.379 +lemma [simp]: "size' (lift i v) = size' v"
1.380 +sorry
1.381 +
1.382 +(* the kernel function as in Section 4.1 of "Operational aspects\<dots>" *)
1.383 +
1.384 +function kernel :: "ml \<Rightarrow> tm" ("_!" 300) where
1.385 +"(C nm vs)! = foldl At (Ct nm) (map kernel vs)" |
1.386 +"(Lam_ML v)! = Lam (((lift 0 v)[V 0 []/0])!)" |
1.387 +"(Fun f vs n)! = foldl At (f!) (map kernel vs)" |
1.388 +"(A_ML v vs)! = foldl At (v!) (map kernel vs)" |
1.389 +"(apply v w)! = At (v!) (w!)" |
1.390 +"(CC nm)! = Ct nm" |
1.391 +"(V x vs)! = foldl At (Vt x) (map kernel vs)" |
1.392 +"(V_ML X)! = undefined"
1.393 +by pat_completeness auto
1.394 +termination by(relation "measure size'") auto
1.395 +
1.396 +consts kernelt :: "tm \<Rightarrow> tm" ("_!" 300)
1.397 +primrec
1.398 +"(Ct nm)! = Ct nm"
1.399 +"(term_of v)! = v!"
1.400 +"(Vt x)! = Vt x"
1.401 +"(At s t)! = At (s!) (t!)"
1.402 +"(Lam t)! = Lam (t!)"
1.403 +
1.404 +abbreviation
1.405 + kernels :: "ml list \<Rightarrow> tm list" ("_!" 300) where
1.406 + "vs ! == map kernel vs"
1.407 +
1.408 +(* soundness of the code generator *)
1.409 +axioms
1.410 +compiler_correct:
1.411 +"(nm, vs, v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> (nm, (map (subst\<^bsub>ML\<^esub> f) vs)!, (subst\<^bsub>ML\<^esub> f v)!) : R"
1.412 +
1.413 +
1.414 +consts
1.415 + free_vars :: "tm \<Rightarrow> lam_var_name set"
1.416 +primrec
1.417 +"free_vars (Ct nm) = {}"
1.418 +"free_vars (Vt x) = {x}"
1.419 +"free_vars (Lam t) = {i. EX j : free_vars t. j = i+1}"
1.420 +"free_vars (At s t) = free_vars s \<union> free_vars t"
1.421 +
1.422 +lemma [simp]: "t : Pure_tms \<Longrightarrow> lift\<^bsub>ML\<^esub> k t = t"
1.423 +by (erule Pure_tms.induct) simp_all
1.424 +
1.425 +lemma kernel_pure: includes Vars assumes "t : Pure_tms" shows "t! = t"
1.426 +using assms by (induct) simp_all
1.427 +
1.428 +lemma lift_eval:
1.429 + "t : Pure_tms \<Longrightarrow> ALL e k. (ALL i : free_vars t. i < size e) --> lift k (eval t e) = eval t (map (lift k) e)"
1.430 +apply(induct set:Pure_tms)
1.431 +apply simp_all
1.432 +apply clarsimp
1.433 +apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE)
1.434 +apply simp
1.435 +apply(erule impE)
1.436 + apply clarsimp
1.437 + apply(case_tac i)apply simp
1.438 + apply simp
1.439 +apply (simp add: map_compose[symmetric])
1.440 +apply (simp add: o_def lift_lift_ML_comm)
1.441 +done
1.442 +
1.443 +lemma lift_ML_eval[rule_format]:
1.444 + "t : Pure_tms \<Longrightarrow> ALL e k. (ALL i : free_vars t. i < size e) --> lift\<^bsub>ML\<^esub> k (eval t e) = eval t (map (lift\<^bsub>ML\<^esub> k) e)"
1.445 +apply(induct set:Pure_tms)
1.446 +apply simp_all
1.447 +apply clarsimp
1.448 +apply(erule_tac x = "V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in allE)
1.449 +apply simp
1.450 +apply(erule impE)
1.451 + apply clarsimp
1.452 + apply(case_tac i)apply simp
1.453 + apply simp
1.454 +apply (simp add: map_compose[symmetric])
1.455 +apply (simp add:o_def lift_lift_ML)
1.456 +done
1.457 +
1.458 +lemma [simp]: includes Vars shows "(v ## f) 0 = v"
1.459 +by(simp add:cons_ML_def)
1.460 +
1.461 +lemma [simp]: includes Vars shows "(v ## f) (Suc n) = lift\<^bsub>ML\<^esub> 0 (f n)"
1.462 +by(simp add:cons_ML_def)
1.463 +
1.464 +lemma lift_o_shift: "lift k o (V_ML 0 ## f) = (V_ML 0 ## (lift k \<circ> f))"
1.465 +apply(rule ext)
1.466 +apply (simp add:cons_ML_def lift_lift_ML_comm split:nat.split)
1.467 +done
1.468 +
1.469 +lemma lift_subst_ML: shows
1.470 + "lift_tm k (subst\<^bsub>ML\<^esub> f t) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_tm k t)" and
1.471 + "lift_ml k (subst\<^bsub>ML\<^esub> f v) = subst\<^bsub>ML\<^esub> (lift_ml k o f) (lift_ml k v)"
1.472 +apply (induct t and v arbitrary: f k and f k rule: lift_tm_lift_ml.induct)
1.473 +apply (simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift)
1.474 +done
1.475 +
1.476 +corollary lift_subst_ML1: "\<forall>v k. lift_ml 0 (u[v/k]) = (lift_ml 0 u)[lift 0 v/k]"
1.477 +apply(rule measure_induct[where f = "size" and a = u])
1.478 +apply(case_tac x)
1.479 +apply(simp_all add:lift_lift map_compose[symmetric] lift_subst_ML)
1.480 +apply(subst lift_lift_ML_comm)apply simp
1.481 +done
1.482 +
1.483 +lemma lift_ML_lift_ML: includes Vars shows
1.484 + "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i t) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k t)"
1.485 +and "i < k+1 \<Longrightarrow> lift\<^bsub>ML\<^esub> (Suc k) (lift\<^bsub>ML\<^esub> i v) = lift\<^bsub>ML\<^esub> i (lift\<^bsub>ML\<^esub> k v)"
1.486 +apply (induct k t and k v arbitrary: i k and i k
1.487 + rule: lift_tm_ML_lift_ml_ML.induct)
1.488 +apply(simp_all add:map_compose[symmetric])
1.489 +done
1.490 +
1.491 +corollary lift_ML_o_lift_ML: shows
1.492 + "i < k+1 \<Longrightarrow> lift_tm_ML (Suc k) o (lift_tm_ML i) = lift_tm_ML i o lift_tm_ML k" and
1.493 + "i < k+1 \<Longrightarrow> lift_ml_ML (Suc k) o (lift_ml_ML i) = lift_ml_ML i o lift_ml_ML k"
1.494 +by(rule ext, simp add:lift_ML_lift_ML)+
1.495 +
1.496 +abbreviation insrt where
1.497 +"insrt k f == (%i. if i<k then lift_ml_ML k (f i) else if i=k then V_ML k else lift_ml_ML k (f(i - 1)))"
1.498 +
1.499 +lemma subst_insrt_lift: includes Vars shows
1.500 + "subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k t) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f t)" and
1.501 + "subst\<^bsub>ML\<^esub> (insrt k f) (lift\<^bsub>ML\<^esub> k v) = lift\<^bsub>ML\<^esub> k (subst\<^bsub>ML\<^esub> f v)"
1.502 +apply (induct k t and k v arbitrary: f k and f k rule: lift_tm_ML_lift_ml_ML.induct)
1.503 +apply (simp_all add:map_compose[symmetric] o_assoc lift_o_lift lift_o_shift)
1.504 + apply(subgoal_tac "lift 0 \<circ> insrt k f = insrt k (lift 0 \<circ> f)")
1.505 + apply simp
1.506 + apply(rule ext)
1.507 + apply (simp add:lift_lift_ML_comm)
1.508 +apply(subgoal_tac "V_ML 0 ## insrt k f = insrt (Suc k) (V_ML 0 ## f)")
1.509 + apply simp
1.510 + apply(rule ext)
1.511 + apply (simp add:lift_ML_lift_ML cons_ML_def split:nat.split)
1.512 +done
1.513 +
1.514 +corollary subst_cons_lift: includes Vars shows
1.515 + "subst\<^bsub>ML\<^esub> (V_ML 0 ## f) o (lift_ml_ML 0) = lift_ml_ML 0 o (subst_ml_ML f)"
1.516 +apply(rule ext)
1.517 +apply(simp add: cons_ML_def subst_insrt_lift[symmetric])
1.518 +apply(subgoal_tac "nat_case (V_ML 0) (\<lambda>j. lift\<^bsub>ML\<^esub> 0 (f j)) = (\<lambda>i. if i = 0 then V_ML 0 else lift\<^bsub>ML\<^esub> 0 (f (i - 1)))")
1.519 + apply simp
1.520 +apply(rule ext, simp split:nat.split)
1.521 +done
1.522 +
1.523 +lemma subst_eval[rule_format]: "t : Pure_tms \<Longrightarrow>
1.524 + ALL f e. (ALL i : free_vars t. i < size e) \<longrightarrow> subst\<^bsub>ML\<^esub> f (eval t e) = eval t (map (subst\<^bsub>ML\<^esub> f) e)"
1.525 +apply(induct set:Pure_tms)
1.526 +apply simp_all
1.527 +apply clarsimp
1.528 +apply(erule_tac x="V_ML 0 ## f" in allE)
1.529 +apply(erule_tac x= "(V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e)" in allE)
1.530 +apply(erule impE)
1.531 + apply clarsimp
1.532 + apply(case_tac i)apply simp
1.533 + apply simp
1.534 +apply (simp add:subst_cons_lift map_compose[symmetric])
1.535 +done
1.536 +
1.537 +
1.538 +theorem kernel_eval[rule_format]: includes Vars shows
1.539 + "t : Pure_tms ==>
1.540 + ALL e. (ALL i : free_vars t. i < size e) \<longrightarrow> (ALL i < size e. e!i = V i []) --> (eval t e)! = t!"
1.541 +apply(induct set:Pure_tms)
1.542 +apply simp_all
1.543 +apply clarsimp
1.544 +apply(subst lift_eval) apply simp
1.545 + apply clarsimp
1.546 + apply(case_tac i)apply simp
1.547 + apply simp
1.548 +apply(subst subst_eval) apply simp
1.549 + apply clarsimp
1.550 + apply(case_tac i)apply simp
1.551 + apply simp
1.552 +apply(erule_tac x="map (subst\<^bsub>ML\<^esub> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
1.553 + (map (lift 0) (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e))" in allE)
1.554 +apply(erule impE)
1.555 +apply(clarsimp)
1.556 + apply(case_tac i)apply simp
1.557 + apply simp
1.558 +apply(erule impE)
1.559 +apply(clarsimp)
1.560 + apply(case_tac i)apply simp
1.561 + apply simp
1.562 +apply simp
1.563 +done
1.564 +
1.565 +(*
1.566 +lemma subst_ML_compose:
1.567 + "subst_ml_ML f2 (subst_ml_ML f1 v) = subst_ml_ML (%i. subst_ml_ML f2 (f1 i)) v"
1.568 +sorry
1.569 +*)
1.570 +
1.571 +lemma map_eq_iff_nth:
1.572 + "(map f xs = map g xs) = (!i<size xs. f(xs!i) = g(xs!i))"
1.573 +sorry
1.574 +
1.575 +lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> lift\<^bsub>ML\<^esub> k v = v"
1.576 +sorry
1.577 +lemma [simp]: includes Vars shows "ML_closed 0 v \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
1.578 +sorry
1.579 +lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> ML_closed k (lift m v)"
1.580 +sorry
1.581 +
1.582 +lemma red_Lam[simp]: includes Vars shows "t \<rightarrow>* t' ==> Lam t \<rightarrow>* Lam t'"
1.583 +apply(induct rule:rtrancl_induct)
1.584 +apply(simp_all)
1.585 +apply(blast intro: rtrancl_into_rtrancl tRed.intros)
1.586 +done
1.587 +
1.588 +lemma red_At1[simp]: includes Vars shows "t \<rightarrow>* t' ==> At t s \<rightarrow>* At t' s"
1.589 +apply(induct rule:rtrancl_induct)
1.590 +apply(simp_all)
1.591 +apply(blast intro: rtrancl_into_rtrancl tRed.intros)
1.592 +done
1.593 +
1.594 +lemma red_At2[simp]: includes Vars shows "t \<rightarrow>* t' ==> At s t \<rightarrow>* At s t'"
1.595 +apply(induct rule:rtrancl_induct)
1.596 +apply(simp_all)
1.597 +apply(blast intro:rtrancl_into_rtrancl tRed.intros)
1.598 +done
1.599 +
1.600 +lemma tRed_list_foldl_At:
1.601 + "ts \<rightarrow>* ts' \<Longrightarrow> s \<rightarrow>* s' \<Longrightarrow> foldl At s ts \<rightarrow>* foldl At s' ts'"
1.602 +apply(induct arbitrary:s s' rule:tRed_list.induct)
1.603 +apply simp
1.604 +apply simp
1.605 +apply(blast dest: red_At1 red_At2 intro:rtrancl_trans)
1.606 +done
1.607 +
1.608 +lemma [trans]: "s = t \<Longrightarrow> t \<rightarrow> t' \<Longrightarrow> s \<rightarrow> t'"
1.609 +by simp
1.610 +
1.611 +
1.612 +lemma subst_foldl[simp]:
1.613 + "subst f (foldl At s ts) = foldl At (subst f s) (map (subst f) ts)"
1.614 +by (induct ts arbitrary: s) auto
1.615 +
1.616 +
1.617 +lemma foldl_At_size: "size ts = size ts' \<Longrightarrow>
1.618 + foldl At s ts = foldl At s' ts' \<longleftrightarrow> s = s' & ts = ts'"
1.619 +by (induct arbitrary: s s' rule:list_induct2) simp_all
1.620 +
1.621 +consts depth_At :: "tm \<Rightarrow> nat"
1.622 +primrec
1.623 +"depth_At(Ct cn) = 0"
1.624 +"depth_At(Vt x) = 0"
1.625 +"depth_At(Lam t) = 0"
1.626 +"depth_At(At s t) = depth_At s + 1"
1.627 +"depth_At(term_of v) = 0"
1.628 +
1.629 +lemma depth_At_foldl:
1.630 + "depth_At(foldl At s ts) = depth_At s + size ts"
1.631 +by (induct ts arbitrary: s) simp_all
1.632 +
1.633 +lemma foldl_At_eq_length:
1.634 + "foldl At s ts = foldl At s ts' \<Longrightarrow> length ts = length ts'"
1.635 +apply(subgoal_tac "depth_At(foldl At s ts) = depth_At(foldl At s ts')")
1.636 +apply(erule thin_rl)
1.637 + apply (simp add:depth_At_foldl)
1.638 +apply simp
1.639 +done
1.640 +
1.641 +lemma foldl_At_eq[simp]: "foldl At s ts = foldl At s ts' \<longleftrightarrow> ts = ts'"
1.642 +apply(rule)
1.643 + prefer 2 apply simp
1.644 +apply(blast dest:foldl_At_size foldl_At_eq_length)
1.645 +done
1.646 +
1.647 +lemma [simp]: "foldl At s ts ! = foldl At (s!) (map kernelt ts)"
1.648 +by (induct ts arbitrary: s) simp_all
1.649 +
1.650 +lemma [simp]: "(kernelt \<circ> term_of) = kernel"
1.651 +by(rule ext) simp
1.652 +
1.653 +lemma shift_subst_decr:
1.654 + "Vt 0 ## subst_decr k t = subst_decr (Suc k) (lift 0 t)"
1.655 +apply(rule ext)
1.656 +apply (simp add:cons_def split:nat.split)
1.657 +done
1.658 +
1.659 +lemma [simp]: "lift k (foldl At s ts) = foldl At (lift k s) (map (lift k) ts)"
1.660 +by(induct ts arbitrary:s) simp_all
1.661 +
1.662 +subsection "Horrible detour"
1.663 +
1.664 +definition "liftn n == lift_ml 0 ^ n"
1.665 +
1.666 +lemma [simp]: "liftn n (C i vs) = C i (map (liftn n) vs)"
1.667 +apply(unfold liftn_def)
1.668 +apply(induct n)
1.669 +apply (simp_all add: map_compose[symmetric])
1.670 +done
1.671 +
1.672 +lemma [simp]: "liftn n (CC nm) = CC nm"
1.673 +apply(unfold liftn_def)
1.674 +apply(induct n)
1.675 +apply (simp_all add: map_compose[symmetric])
1.676 +done
1.677 +
1.678 +lemma [simp]: "liftn n (apply v w) = apply (liftn n v) (liftn n w)"
1.679 +apply(unfold liftn_def)
1.680 +apply(induct n)
1.681 +apply (simp_all add: map_compose[symmetric])
1.682 +done
1.683 +
1.684 +lemma [simp]: "liftn n (A_ML v vs) = A_ML (liftn n v) (map (liftn n) vs)"
1.685 +apply(unfold liftn_def)
1.686 +apply(induct n)
1.687 +apply (simp_all add: map_compose[symmetric])
1.688 +done
1.689 +
1.690 +lemma [simp]:
1.691 + "liftn n (Fun v vs i) = Fun (liftn n v) (map (liftn n) vs) i"
1.692 +apply(unfold liftn_def)
1.693 +apply(induct n)
1.694 +apply (simp_all add: map_compose[symmetric] id_def)
1.695 +done
1.696 +
1.697 +lemma [simp]: "liftn n (Lam_ML v) = Lam_ML (liftn n v)"
1.698 +apply(unfold liftn_def)
1.699 +apply(induct n)
1.700 +apply (simp_all add: map_compose[symmetric] id_def)
1.701 +done
1.702 +
1.703 +lemma liftn_liftn_add: "liftn m (liftn n v) = liftn (m+n) v"
1.704 +by(simp add:liftn_def funpow_add)
1.705 +
1.706 +lemma [simp]: "liftn n (V_ML k) = V_ML k"
1.707 +apply(unfold liftn_def)
1.708 +apply(induct n)
1.709 +apply (simp_all)
1.710 +done
1.711 +
1.712 +lemma liftn_lift_ML_comm: "liftn n (lift\<^bsub>ML\<^esub> 0 v) = lift\<^bsub>ML\<^esub> 0 (liftn n v)"
1.713 +apply(unfold liftn_def)
1.714 +apply(induct n)
1.715 +apply (simp_all add:lift_lift_ML_comm)
1.716 +done
1.717 +
1.718 +lemma liftn_cons: "liftn n ((V_ML 0 ## f) x) = (V_ML 0 ## (liftn n o f)) x"
1.719 +apply(simp add:cons_ML_def liftn_lift_ML_comm split:nat.split)
1.720 +done
1.721 +
1.722 +text{* End of horrible detour *}
1.723 +
1.724 +lemma kernel_subst1:
1.725 +"ML_closed 1 u \<Longrightarrow> ML_closed 0 v \<Longrightarrow> kernel( u[v/0]) = (kernel((lift 0 u)[V 0 []/0]))[kernel v/0]"
1.726 +sorry
1.727 +
1.728 +lemma includes Vars shows foldl_Pure[simp]:
1.729 + "t : Pure_tms \<Longrightarrow> \<forall>t\<in>set ts. t : Pure_tms \<Longrightarrow>
1.730 + (!!s t. s : Pure_tms \<Longrightarrow> t : Pure_tms \<Longrightarrow> f s t : Pure_tms) \<Longrightarrow>
1.731 + foldl f t ts \<in> Pure_tms"
1.732 +by(induct ts arbitrary: t) simp_all
1.733 +
1.734 +declare Pure_tms.intros[simp]
1.735 +
1.736 +lemma includes Vars shows "ML_closed 0 v \<Longrightarrow> kernel v : Pure_tms"
1.737 +apply(induct rule:kernel.induct)
1.738 +apply simp_all
1.739 +apply(rule Pure_tms.intros);
1.740 +(* "ML_closed (Suc k) v \<Longrightarrow> ML_closed k (lift 0 v)" *)
1.741 +sorry
1.742 +
1.743 +lemma subst_Vt: includes Vars shows "subst Vt = id"
1.744 +sorry
1.745 +(*
1.746 +apply(rule ext)
1.747 +apply(induct_tac x)
1.748 +apply simp_all
1.749 +
1.750 +done
1.751 +*)
1.752 +(* klappt noch nicht ganz *)
1.753 +theorem Red_sound: includes Vars
1.754 + shows "v \<Rightarrow> v' \<Longrightarrow> ML_closed 0 v \<Longrightarrow> v! \<rightarrow>* v'! & ML_closed 0 v'"
1.755 + and "t \<Rightarrow> t' \<Longrightarrow> ML_closed_t 0 t \<Longrightarrow> kernelt t \<rightarrow>* kernelt t' & ML_closed_t 0 t'"
1.756 + and "(vs :: ml list) \<Rightarrow> vs' \<Longrightarrow> !v : set vs . ML_closed 0 v \<Longrightarrow> map kernel vs \<rightarrow>* map kernel vs' & (! v':set vs'. ML_closed 0 v')"
1.757 +proof(induct rule:Red_Redt_Redl.inducts)
1.758 + fix u v
1.759 + let ?v = "A_ML (Lam_ML u) [v]"
1.760 + assume cl: "ML_closed 0 (A_ML (Lam_ML u) [v])"
1.761 + let ?u' = "(lift_ml 0 u)[V 0 []/0]"
1.762 + have "?v! = At (Lam ((?u')!)) (v !)" by simp
1.763 + also have "\<dots> \<rightarrow> (?u' !)[v!/0]" (is "_ \<rightarrow> ?R") by(rule tRed.intros)
1.764 + also have "?R = u[v/0]!" using cl
1.765 +apply(cut_tac u = "u" and v = "v" in kernel_subst1)
1.766 +apply(simp_all)
1.767 +done
1.768 + finally have "kernel(A_ML (Lam_ML u) [v]) \<rightarrow>* kernel(u[v/0])" (is ?A) by(rule r_into_rtrancl)
1.769 + moreover have "ML_closed 0 (u[v/0])" (is "?C") using cl apply simp sorry
1.770 + ultimately show "?A & ?C" ..
1.771 +next
1.772 + case term_of_C thus ?case apply (auto simp:map_compose[symmetric])sorry
1.773 +next
1.774 + fix f :: "nat \<Rightarrow> ml" and nm vs v
1.775 + assume f: "\<forall>i. ML_closed 0 (f i)" and compR: "(nm, vs, v) \<in> compR"
1.776 + note tRed.intros(2)[OF compiler_correct[OF compR f], of Vt,simplified map_compose[symmetric]]
1.777 + hence red: "foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs) \<rightarrow>
1.778 + (subst\<^bsub>ML\<^esub> f v)!" (is "_ \<rightarrow> ?R") apply(simp add:map_compose) sorry
1.779 + have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! =
1.780 + foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs)" by (simp add:map_compose)
1.781 + also(* have "map (kernel o subst\<^bsub>ML\<^esub> f) vs = map (subst (kernel o f)) (vs!)"
1.782 + using closed_subst_kernel(2)[OF compiled_V_free1[OF compR]]
1.783 + by (simp add:map_compose[symmetric])
1.784 + also*) note red
1.785 + (*also have "?R = subst\<^bsub>ML\<^esub> f v!"
1.786 + using closed_subst_kernel(2)[OF compiled_V_free2[OF compR]] by simp*)
1.787 + finally have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! \<rightarrow>* subst\<^bsub>ML\<^esub> f v!" (is "?A")
1.788 + by(rule r_into_rtrancl) (*
1.789 + also have "?l = (subst\<^bsub>ML\<^esub> fa (A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)))!" (is "_ = ?l'") sorry
1.790 + also have "?r = subst\<^bsub>ML\<^esub> fa (subst\<^bsub>ML\<^esub> f v)!" (is "_ = ?r'") sorry
1.791 + finally have "?l' \<rightarrow>* ?r'" (is ?A) . *)
1.792 + moreover have "ML_closed 0 (subst\<^bsub>ML\<^esub> f v)" (is "?C") using prems sorry
1.793 + ultimately show "?A & ?C" ..
1.794 +next
1.795 + case term_of_V thus ?case apply (auto simp:map_compose[symmetric]) sorry
1.796 +next
1.797 + case (term_of_Fun n vf vs)
1.798 + hence "term_of (Fun vf vs n)! \<rightarrow>*
1.799 + Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!" sorry
1.800 + moreover
1.801 + have "ML_closed_t 0
1.802 + (Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0])))" sorry
1.803 + ultimately show ?case ..
1.804 +next
1.805 + case apply_Fun1 thus ?case by simp
1.806 +next
1.807 + case apply_Fun2 thus ?case by simp
1.808 +next
1.809 + case apply_C thus ?case by simp
1.810 +next
1.811 + case apply_V thus ?case by simp
1.812 +next
1.813 + case ctxt_Lam thus ?case by(auto)
1.814 +next
1.815 + case ctxt_At1 thus ?case by(auto)
1.816 +next
1.817 + case ctxt_At2 thus ?case by (auto)
1.818 +next
1.819 + case ctxt_term_of thus ?case by (auto)
1.820 +next
1.821 + case ctxt_C thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.822 +next
1.823 + case ctxt_V thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.824 +next
1.825 + case ctxt_Fun1 thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.826 +next
1.827 + case ctxt_Fun3 thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.828 +next
1.829 + case ctxt_apply1 thus ?case by auto
1.830 +next
1.831 + case ctxt_apply2 thus ?case by auto
1.832 +next
1.833 + case ctxt_A_ML1 thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.834 +next
1.835 + case ctxt_A_ML2 thus ?case by (fastsimp simp:tRed_list_foldl_At)
1.836 +next
1.837 + case ctxt_list1 thus ?case by simp
1.838 +next
1.839 + case ctxt_list2 thus ?case by simp
1.840 +qed
1.841 +
1.842 +
1.843 +inductive_cases tRedE: "Ct n \<rightarrow> u"
1.844 +thm tRedE
1.845 +
1.846 +lemma [simp]: "Ct n = foldl At t ts \<longleftrightarrow> t = Ct n & ts = []"
1.847 +by (induct ts arbitrary:t) auto
1.848 +
1.849 +corollary kernel_inv: includes Vars shows
1.850 + "(t :: tm) \<Rightarrow>* t' ==> ML_closed_t 0 t ==> t! \<rightarrow>* t'!"
1.851 +sorry
1.852 +
1.853 +theorem includes Vars
1.854 +assumes t: "t : Pure_tms" and t': "t' : Pure_tms" and
1.855 + closed: "free_vars t = {}" and reds: "term_of (eval t []) \<Rightarrow>* t'"
1.856 + shows "t \<rightarrow>* t' "
1.857 +proof -
1.858 + have ML_cl: "ML_closed_t 0 (term_of (eval t []))" sorry
1.859 + have "(eval t [])! = t!"
1.860 + using kernel_eval[OF t, where e="[]"] closed by simp
1.861 + hence "(term_of (eval t []))! = t!" by simp
1.862 + moreover have "term_of (eval t [])! \<rightarrow>* t'!"
1.863 + using kernel_inv[OF reds ML_cl] by auto
1.864 + ultimately have "t! \<rightarrow>* t'!" by simp
1.865 + thus ?thesis using kernel_pure t t' by auto
1.866 +qed
1.867 +
1.868 +end