src/HOL/W0/W0.thy
changeset 12944 fa6a3ddec27f
child 12945 95853fbcc718
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/W0/W0.thy	Tue Feb 26 00:19:04 2002 +0100
     1.3 @@ -0,0 +1,947 @@
     1.4 +(*  Title:      HOL/W0/W0.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, and Markus Wenzel
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +*)
     1.9 +
    1.10 +theory W0 = Main:
    1.11 +
    1.12 +section {* Universal error monad *}
    1.13 +
    1.14 +datatype 'a maybe = Ok 'a | Fail
    1.15 +
    1.16 +constdefs
    1.17 +  bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60)
    1.18 +  "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
    1.19 +
    1.20 +syntax
    1.21 +  "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
    1.22 +translations
    1.23 +  "P := E; F" == "E \<bind> (\<lambda>P. F)"
    1.24 +
    1.25 +lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)"
    1.26 +  by (simp add: bind_def)
    1.27 +
    1.28 +lemma bind_Fail [simp]: "Fail \<bind> f = Fail"
    1.29 +  by (simp add: bind_def)
    1.30 +
    1.31 +lemma split_bind:
    1.32 +    "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))"
    1.33 +  by (induct res) simp_all
    1.34 +
    1.35 +lemma split_bind_asm:
    1.36 +  "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))"
    1.37 +  by (simp split: split_bind)
    1.38 +
    1.39 +lemmas bind_splits = split_bind split_bind_asm
    1.40 +
    1.41 +lemma bind_eq_Fail [simp]:
    1.42 +  "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> f p = Fail))"
    1.43 +  by (simp split: split_bind)
    1.44 +
    1.45 +lemma rotate_Ok: "(y = Ok x) = (Ok x = y)"
    1.46 +  by (rule eq_sym_conv)
    1.47 +
    1.48 +
    1.49 +section {* MiniML-types and type substitutions *}
    1.50 +
    1.51 +axclass type_struct \<subseteq> type
    1.52 +  -- {* new class for structures containing type variables *}
    1.53 +
    1.54 +datatype "typ" = TVar nat | TFun "typ" "typ"    (infixr "->" 70)
    1.55 +  -- {* type expressions *}
    1.56 +
    1.57 +types subst = "nat => typ"
    1.58 +  -- {* type variable substitution *}
    1.59 +
    1.60 +instance "typ" :: type_struct ..
    1.61 +instance list :: (type_struct) type_struct ..
    1.62 +instance fun :: (type, type_struct) type_struct ..
    1.63 +
    1.64 +
    1.65 +subsection {* Substitutions *}
    1.66 +
    1.67 +consts
    1.68 +  app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
    1.69 +  -- {* extension of substitution to type structures *}
    1.70 +primrec
    1.71 +  app_subst_TVar: "$s (TVar n) = s n"
    1.72 +  app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
    1.73 +
    1.74 +defs (overloaded)
    1.75 +  app_subst_list: "$s \<equiv> map ($s)"
    1.76 +
    1.77 +consts
    1.78 +  free_tv :: "'a::type_struct \<Rightarrow> nat set"
    1.79 +  -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
    1.80 +
    1.81 +primrec
    1.82 +  "free_tv (TVar m) = {m}"
    1.83 +  "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
    1.84 +
    1.85 +primrec
    1.86 +  "free_tv [] = {}"
    1.87 +  "free_tv (x # xs) = free_tv x \<union> free_tv xs"
    1.88 +
    1.89 +constdefs
    1.90 +  dom :: "subst \<Rightarrow> nat set"
    1.91 +  "dom s \<equiv> {n. s n \<noteq> TVar n}"
    1.92 +  -- {* domain of a substitution *}
    1.93 +
    1.94 +  cod :: "subst \<Rightarrow> nat set"
    1.95 +  "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
    1.96 +  -- {* codomain of a substitutions: the introduced variables *}
    1.97 +
    1.98 +defs
    1.99 +  free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
   1.100 +
   1.101 +text {*
   1.102 +  @{text "new_tv s n"} checks whether @{text n} is a new type variable
   1.103 +  wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
   1.104 +  than any type variable occuring in the type structure.
   1.105 +*}
   1.106 +
   1.107 +constdefs
   1.108 +  new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
   1.109 +  "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
   1.110 +
   1.111 +
   1.112 +subsubsection {* Identity substitution *}
   1.113 +
   1.114 +constdefs
   1.115 +  id_subst :: subst
   1.116 +  "id_subst \<equiv> \<lambda>n. TVar n"
   1.117 +
   1.118 +lemma app_subst_id_te [simp]:
   1.119 +  "$id_subst = (\<lambda>t::typ. t)"
   1.120 +  -- {* application of @{text id_subst} does not change type expression *}
   1.121 +proof
   1.122 +  fix t :: "typ"
   1.123 +  show "$id_subst t = t"
   1.124 +    by (induct t) (simp_all add: id_subst_def)
   1.125 +qed
   1.126 +
   1.127 +lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)"
   1.128 +  -- {* application of @{text id_subst} does not change list of type expressions *}
   1.129 +proof
   1.130 +  fix ts :: "typ list"
   1.131 +  show "$id_subst ts = ts"
   1.132 +    by (induct ts) (simp_all add: app_subst_list)
   1.133 +qed
   1.134 +
   1.135 +lemma o_id_subst [simp]: "$s o id_subst = s"
   1.136 +  by (rule ext) (simp add: id_subst_def)
   1.137 +
   1.138 +lemma dom_id_subst [simp]: "dom id_subst = {}"
   1.139 +  by (simp add: dom_def id_subst_def empty_def)
   1.140 +
   1.141 +lemma cod_id_subst [simp]: "cod id_subst = {}"
   1.142 +  by (simp add: cod_def)
   1.143 +
   1.144 +lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
   1.145 +  by (simp add: free_tv_subst)
   1.146 +
   1.147 +
   1.148 +lemma cod_app_subst [simp]:
   1.149 +  assumes free: "v \<in> free_tv (s n)"
   1.150 +    and neq: "v \<noteq> n"
   1.151 +  shows "v \<in> cod s"
   1.152 +proof -
   1.153 +  have "s n \<noteq> TVar n"
   1.154 +  proof
   1.155 +    assume "s n = TVar n"
   1.156 +    with free have "v = n" by simp
   1.157 +    with neq show False ..
   1.158 +  qed
   1.159 +  with free show ?thesis
   1.160 +    by (auto simp add: dom_def cod_def)
   1.161 +qed
   1.162 +
   1.163 +lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t"
   1.164 +  -- {* composition of substitutions *}
   1.165 +  by (induct t) simp_all
   1.166 +
   1.167 +lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts"
   1.168 +  by (induct ts) (simp_all add: app_subst_list subst_comp_te)
   1.169 +
   1.170 +
   1.171 +lemma app_subst_Nil [simp]: "$s [] = []"
   1.172 +  by (simp add: app_subst_list)
   1.173 +
   1.174 +lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
   1.175 +  by (simp add: app_subst_list)
   1.176 +
   1.177 +lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
   1.178 +  by (simp add: new_tv_def)
   1.179 +
   1.180 +lemma new_tv_Fun [simp]:
   1.181 +  "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
   1.182 +  by (auto simp add: new_tv_def)
   1.183 +
   1.184 +lemma new_tv_Nil [simp]: "new_tv n []"
   1.185 +  by (simp add: new_tv_def)
   1.186 +
   1.187 +lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)"
   1.188 +  by (auto simp add: new_tv_def)
   1.189 +
   1.190 +lemma new_tv_id_subst [simp]: "new_tv n id_subst"
   1.191 +  by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
   1.192 +
   1.193 +lemma new_tv_subst:
   1.194 +  "new_tv n s =
   1.195 +    ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
   1.196 +     (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
   1.197 +  apply (unfold new_tv_def)
   1.198 +  apply (tactic "safe_tac HOL_cs")
   1.199 +  -- {* @{text \<Longrightarrow>} *}
   1.200 +    apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
   1.201 +      addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
   1.202 +   apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
   1.203 +    apply (tactic "safe_tac HOL_cs")
   1.204 +     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
   1.205 +       addsimps [thm "free_tv_subst"])) 1 *})
   1.206 +    apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
   1.207 +    apply simp
   1.208 +   apply (tactic {* fast_tac (set_cs addss (simpset()
   1.209 +     addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   1.210 +  -- {* @{text \<Longleftarrow>} *}
   1.211 +  apply (unfold free_tv_subst cod_def dom_def)
   1.212 +  apply (tactic "safe_tac set_cs")
   1.213 +   apply (cut_tac m = m and n = n in less_linear)
   1.214 +   apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
   1.215 +  apply (cut_tac m = ma and n = n in less_linear)
   1.216 +  apply (fast intro!: less_or_eq_imp_le)
   1.217 +  done
   1.218 +
   1.219 +lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
   1.220 +  by (induct x) simp_all
   1.221 +
   1.222 +lemma subst_te_new_tv [simp]:
   1.223 +  "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
   1.224 +  -- {* substitution affects only variables occurring freely *}
   1.225 +  by (induct t) simp_all
   1.226 +
   1.227 +lemma subst_tel_new_tv [simp]:
   1.228 +  "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
   1.229 +  by (induct ts) simp_all
   1.230 +
   1.231 +lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
   1.232 +  -- {* all greater variables are also new *}
   1.233 +proof (induct t)
   1.234 +  case (TVar n)
   1.235 +  thus ?case by (auto intro: less_le_trans)
   1.236 +next
   1.237 +  case TFun
   1.238 +  thus ?case by simp
   1.239 +qed
   1.240 +
   1.241 +lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
   1.242 +  by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
   1.243 +
   1.244 +lemma new_tv_list_le:
   1.245 +  "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
   1.246 +proof (induct ts)
   1.247 +  case Nil
   1.248 +  thus ?case by simp
   1.249 +next
   1.250 +  case Cons
   1.251 +  thus ?case by (auto intro: new_tv_le)
   1.252 +qed
   1.253 +
   1.254 +lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
   1.255 +  by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
   1.256 +
   1.257 +lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
   1.258 +  apply (simp add: new_tv_subst)
   1.259 +  apply clarify
   1.260 +  apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
   1.261 +    apply clarify
   1.262 +    apply (simp_all add: new_tv_le)
   1.263 +  done
   1.264 +
   1.265 +lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
   1.266 +  by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
   1.267 +
   1.268 +lemma new_tv_subst_var:
   1.269 +    "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
   1.270 +  -- {* @{text new_tv} property remains if a substitution is applied *}
   1.271 +  by (simp add: new_tv_subst)
   1.272 +
   1.273 +lemma new_tv_subst_te [simp]:
   1.274 +    "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
   1.275 +  by (induct t) (auto simp add: new_tv_subst)
   1.276 +
   1.277 +lemma new_tv_subst_tel [simp]:
   1.278 +    "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
   1.279 +  by (induct ts) (fastsimp simp add: new_tv_subst)+
   1.280 +
   1.281 +lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
   1.282 +  -- {* auxilliary lemma *}
   1.283 +  by (simp add: new_tv_list)
   1.284 +
   1.285 +lemma new_tv_subst_comp_1 [simp]:
   1.286 +    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
   1.287 +  -- {* composition of substitutions preserves @{text new_tv} proposition *}
   1.288 +  by (simp add: new_tv_subst)
   1.289 +
   1.290 +lemma new_tv_subst_comp_2 [simp]:
   1.291 +    "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
   1.292 +  by (simp add: new_tv_subst)
   1.293 +
   1.294 +lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
   1.295 +  -- {* new type variables do not occur freely in a type structure *}
   1.296 +  by (auto simp add: new_tv_def)
   1.297 +
   1.298 +lemma ftv_mem_sub_ftv_list [simp]:
   1.299 +    "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
   1.300 +  by (induct ts) auto
   1.301 +
   1.302 +text {*
   1.303 +  If two substitutions yield the same result if applied to a type
   1.304 +  structure the substitutions coincide on the free type variables
   1.305 +  occurring in the type structure.
   1.306 +*}
   1.307 +
   1.308 +lemma eq_subst_te_eq_free:
   1.309 +    "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
   1.310 +  by (induct t) auto
   1.311 +
   1.312 +lemma eq_free_eq_subst_te:
   1.313 +    "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
   1.314 +  by (induct t) auto
   1.315 +
   1.316 +lemma eq_subst_tel_eq_free:
   1.317 +    "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
   1.318 +  by (induct ts) (auto intro: eq_subst_te_eq_free)
   1.319 +
   1.320 +lemma eq_free_eq_subst_tel:
   1.321 +    "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
   1.322 +  by (induct ts) (auto intro: eq_free_eq_subst_te)
   1.323 +
   1.324 +text {*
   1.325 +  \medskip Some useful lemmas.
   1.326 +*}
   1.327 +
   1.328 +lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
   1.329 +  by (simp add: free_tv_subst)
   1.330 +
   1.331 +lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
   1.332 +  by (simp add: free_tv_subst dom_def)
   1.333 +
   1.334 +lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
   1.335 +  by (unfold new_tv_def) fast
   1.336 +
   1.337 +lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
   1.338 +  by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
   1.339 +
   1.340 +lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
   1.341 +  by (induct t) (auto simp add: free_tv_subst_var)
   1.342 +
   1.343 +lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
   1.344 +  apply (induct ts)
   1.345 +   apply simp
   1.346 +  apply (cut_tac free_tv_app_subst_te)
   1.347 +  apply fastsimp
   1.348 +  done
   1.349 +
   1.350 +lemma free_tv_comp_subst:
   1.351 +    "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   1.352 +  apply (unfold free_tv_subst dom_def)
   1.353 +  apply (tactic {*
   1.354 +    fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
   1.355 +    thm "free_tv_subst_var" RS subsetD]
   1.356 +    addss (simpset() delsimps bex_simps
   1.357 +    addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   1.358 +  done
   1.359 +
   1.360 +
   1.361 +subsection {* Most general unifiers *}
   1.362 +
   1.363 +consts
   1.364 +  mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
   1.365 +axioms
   1.366 +  mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
   1.367 +  mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
   1.368 +  mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
   1.369 +  mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
   1.370 +
   1.371 +lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
   1.372 +  -- {* @{text mgu} does not introduce new type variables *}
   1.373 +  by (unfold new_tv_def) (blast dest: mgu_free)
   1.374 +
   1.375 +
   1.376 +section {* Mini-ML with type inference rules *}
   1.377 +
   1.378 +datatype
   1.379 +  expr = Var nat | Abs expr | App expr expr
   1.380 +
   1.381 +
   1.382 +text {* Type inference rules. *}
   1.383 +
   1.384 +consts
   1.385 +  has_type :: "(typ list \<times> expr \<times> typ) set"
   1.386 +
   1.387 +syntax
   1.388 +  "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
   1.389 +    ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   1.390 +translations
   1.391 +  "a |- e :: t" == "(a, e, t) \<in> has_type"
   1.392 +
   1.393 +inductive has_type
   1.394 +  intros
   1.395 +    Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
   1.396 +    Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
   1.397 +    App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
   1.398 +      \<Longrightarrow> a |- App e1 e2 :: t1"
   1.399 +
   1.400 +
   1.401 +text {* Type assigment is closed wrt.\ substitution. *}
   1.402 +
   1.403 +lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
   1.404 +proof -
   1.405 +  assume "a |- e :: t"
   1.406 +  thus ?thesis (is "?P a e t")
   1.407 +  proof induct
   1.408 +    case (Var a n)
   1.409 +    hence "n < length (map ($ s) a)" by simp
   1.410 +    hence "map ($ s) a |- Var n :: map ($ s) a ! n"
   1.411 +      by (rule has_type.Var)
   1.412 +    also have "map ($ s) a ! n = $ s (a ! n)"
   1.413 +      by (rule nth_map)
   1.414 +    also have "map ($ s) a = $ s a"
   1.415 +      by (simp only: app_subst_list)
   1.416 +    finally show "?P a (Var n) (a ! n)" .
   1.417 +  next
   1.418 +    case (Abs a e t1 t2)
   1.419 +    hence "$ s t1 # map ($ s) a |- e :: $ s t2"
   1.420 +      by (simp add: app_subst_list)
   1.421 +    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
   1.422 +      by (rule has_type.Abs)
   1.423 +    thus "?P a (Abs e) (t1 -> t2)"
   1.424 +      by (simp add: app_subst_list)
   1.425 +  next
   1.426 +    case App
   1.427 +    thus ?case by (simp add: has_type.App)
   1.428 +  qed
   1.429 +qed
   1.430 +
   1.431 +
   1.432 +section {* Correctness and completeness of the type inference algorithm @{text \<W>} *}
   1.433 +
   1.434 +consts
   1.435 +  W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
   1.436 +
   1.437 +primrec
   1.438 +  "\<W> (Var i) a n =
   1.439 +    (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
   1.440 +  "\<W> (Abs e) a n =
   1.441 +    ((s, t, m) := \<W> e (TVar n # a) (Suc n);
   1.442 +     Ok (s, (s n) -> t, m))"
   1.443 +  "\<W> (App e1 e2) a n =
   1.444 +    ((s1, t1, m1) := \<W> e1 a n;
   1.445 +     (s2, t2, m2) := \<W> e2 ($s1 a) m1;
   1.446 +     u := mgu ($ s2 t1) (t2 -> TVar m2);
   1.447 +     Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
   1.448 +
   1.449 +theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
   1.450 +  (is "PROP ?P e")
   1.451 +proof (induct e)
   1.452 +  fix a s t m n
   1.453 +  {
   1.454 +    fix i
   1.455 +    assume "Ok (s, t, m) = \<W> (Var i) a n"
   1.456 +    thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
   1.457 +  next
   1.458 +    fix e assume hyp: "PROP ?P e"
   1.459 +    assume "Ok (s, t, m) = \<W> (Abs e) a n"
   1.460 +    then obtain t' where "t = s n -> t'"
   1.461 +        and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
   1.462 +      by (auto split: bind_splits)
   1.463 +    with hyp show "$s a |- Abs e :: t"
   1.464 +      by (force intro: has_type.Abs)
   1.465 +  next
   1.466 +    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
   1.467 +    assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
   1.468 +    then obtain s1 t1 n1 s2 t2 n2 u where
   1.469 +          s: "s = $u o $s2 o s1"
   1.470 +        and t: "t = u n2"
   1.471 +        and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
   1.472 +        and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
   1.473 +        and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
   1.474 +      by (auto split: bind_splits simp: that)
   1.475 +    show "$s a |- App e1 e2 :: t"
   1.476 +    proof (rule has_type.App)
   1.477 +      from s have s': "$u ($s2 ($s1 a)) = $s a"
   1.478 +        by (simp add: subst_comp_tel o_def)
   1.479 +      show "$s a |- e1 :: $u t2 -> t"
   1.480 +      proof -
   1.481 +        from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
   1.482 +        hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
   1.483 +          by (intro has_type_subst_closed)
   1.484 +        with s' t mgu_ok show ?thesis by simp
   1.485 +      qed
   1.486 +      show "$s a |- e2 :: $u t2"
   1.487 +      proof -
   1.488 +        from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
   1.489 +        hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
   1.490 +          by (rule has_type_subst_closed)
   1.491 +        with s' show ?thesis by simp
   1.492 +      qed
   1.493 +    qed
   1.494 +  }
   1.495 +qed
   1.496 +
   1.497 +
   1.498 +inductive_cases has_type_casesE:
   1.499 +  "s |- Var n :: t"
   1.500 +  "s |- Abs e :: t"
   1.501 +  "s |- App e1 e2 ::t"
   1.502 +
   1.503 +
   1.504 +lemmas [simp] = Suc_le_lessD
   1.505 +  and [simp del] = less_imp_le ex_simps all_simps
   1.506 +
   1.507 +lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
   1.508 +  -- {* the resulting type variable is always greater or equal than the given one *}
   1.509 +  apply (atomize (full))
   1.510 +  apply (induct e)
   1.511 +    txt {* case @{text "Var n"} *}
   1.512 +    apply clarsimp
   1.513 +   txt {* case @{text "Abs e"} *}
   1.514 +   apply (simp split add: split_bind)
   1.515 +   apply (fast dest: Suc_leD)
   1.516 +  txt {* case @{text "App e1 e2"} *}
   1.517 +  apply (simp (no_asm) split add: split_bind)
   1.518 +  apply (intro strip)
   1.519 +  apply (rename_tac s t na sa ta nb sb)
   1.520 +  apply (erule_tac x = a in allE)
   1.521 +  apply (erule_tac x = n in allE)
   1.522 +  apply (erule_tac x = "$s a" in allE)
   1.523 +  apply (erule_tac x = s in allE)
   1.524 +  apply (erule_tac x = t in allE)
   1.525 +  apply (erule_tac x = na in allE)
   1.526 +  apply (erule_tac x = na in allE)
   1.527 +  apply (simp add: eq_sym_conv)
   1.528 +  done
   1.529 +
   1.530 +lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
   1.531 +  by (simp add: eq_sym_conv)
   1.532 +
   1.533 +lemma new_tv_W: "!!n a s t m.
   1.534 +  new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
   1.535 +  -- {* resulting type variable is new *}
   1.536 +  apply (atomize (full))
   1.537 +  apply (induct e)
   1.538 +    txt {* case @{text "Var n"} *}
   1.539 +    apply clarsimp
   1.540 +    apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
   1.541 +   txt {* case @{text "Abs e"} *}
   1.542 +   apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
   1.543 +   apply (intro strip)
   1.544 +   apply (erule_tac x = "Suc n" in allE)
   1.545 +   apply (erule_tac x = "TVar n # a" in allE)
   1.546 +   apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
   1.547 +  txt {* case @{text "App e1 e2"} *}
   1.548 +  apply (simp (no_asm) split add: split_bind)
   1.549 +  apply (intro strip)
   1.550 +  apply (rename_tac s t na sa ta nb sb)
   1.551 +  apply (erule_tac x = n in allE)
   1.552 +  apply (erule_tac x = a in allE)
   1.553 +  apply (erule_tac x = s in allE)
   1.554 +  apply (erule_tac x = t in allE)
   1.555 +  apply (erule_tac x = na in allE)
   1.556 +  apply (erule_tac x = na in allE)
   1.557 +  apply (simp add: eq_sym_conv)
   1.558 +  apply (erule_tac x = "$s a" in allE)
   1.559 +  apply (erule_tac x = sa in allE)
   1.560 +  apply (erule_tac x = ta in allE)
   1.561 +  apply (erule_tac x = nb in allE)
   1.562 +  apply (simp add: o_def rotate_Ok)
   1.563 +  apply (rule conjI)
   1.564 +   apply (rule new_tv_subst_comp_2)
   1.565 +    apply (rule new_tv_subst_comp_2)
   1.566 +     apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
   1.567 +     apply (rule_tac n = na in new_tv_subst_le)
   1.568 +      apply (simp add: rotate_Ok)
   1.569 +     apply (simp (no_asm_simp))
   1.570 +    apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   1.571 +      lessI [THEN less_imp_le, THEN new_tv_subst_le])
   1.572 +   apply (erule sym [THEN mgu_new])
   1.573 +    apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
   1.574 +      lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
   1.575 +      new_tv_le)
   1.576 +   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   1.577 +     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   1.578 +     addss (simpset())) 1 *})
   1.579 +  apply (rule lessI [THEN new_tv_subst_var])
   1.580 +  apply (erule sym [THEN mgu_new])
   1.581 +    apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
   1.582 +      dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   1.583 +        lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   1.584 +  apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   1.585 +    addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   1.586 +    addss (simpset())) 1 *})
   1.587 +  done
   1.588 +
   1.589 +lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
   1.590 +    (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
   1.591 +  apply (atomize (full))
   1.592 +  apply (induct e)
   1.593 +    txt {* case @{text "Var n"} *}
   1.594 +    apply clarsimp
   1.595 +    apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   1.596 +   txt {* case @{text "Abs e"} *}
   1.597 +   apply (simp add: free_tv_subst split add: split_bind)
   1.598 +   apply (intro strip)
   1.599 +   apply (rename_tac s t n1 v)
   1.600 +   apply (erule_tac x = "Suc n" in allE)
   1.601 +   apply (erule_tac x = "TVar n # a" in allE)
   1.602 +   apply (erule_tac x = s in allE)
   1.603 +   apply (erule_tac x = t in allE)
   1.604 +   apply (erule_tac x = n1 in allE)
   1.605 +   apply (erule_tac x = v in allE)
   1.606 +   apply (force elim!: allE intro: cod_app_subst)
   1.607 +  txt {* case @{text "App e1 e2"} *}
   1.608 +  apply (simp (no_asm) split add: split_bind)
   1.609 +  apply (intro strip)
   1.610 +  apply (rename_tac s t n1 s1 t1 n2 s3 v)
   1.611 +  apply (erule_tac x = n in allE)
   1.612 +  apply (erule_tac x = a in allE)
   1.613 +  apply (erule_tac x = s in allE)
   1.614 +  apply (erule_tac x = t in allE)
   1.615 +  apply (erule_tac x = n1 in allE)
   1.616 +  apply (erule_tac x = n1 in allE)
   1.617 +  apply (erule_tac x = v in allE)
   1.618 +  txt {* second case *}
   1.619 +  apply (erule_tac x = "$ s a" in allE)
   1.620 +  apply (erule_tac x = s1 in allE)
   1.621 +  apply (erule_tac x = t1 in allE)
   1.622 +  apply (erule_tac x = n2 in allE)
   1.623 +  apply (erule_tac x = v in allE)
   1.624 +  apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
   1.625 +   apply (simp add: rotate_Ok o_def)
   1.626 +   apply (drule W_var_geD)
   1.627 +   apply (drule W_var_geD)
   1.628 +   apply (frule less_le_trans, assumption)
   1.629 +   apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
   1.630 +     free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
   1.631 +  apply simp
   1.632 +  apply (drule sym [THEN W_var_geD])
   1.633 +  apply (drule sym [THEN W_var_geD])
   1.634 +  apply (frule less_le_trans, assumption)
   1.635 +  apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
   1.636 +    thm "free_tv_subst_var" RS subsetD,
   1.637 +    thm "free_tv_app_subst_te" RS subsetD,
   1.638 +    thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
   1.639 +    addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
   1.640 +      -- {* builtin arithmetic in simpset messes things up *}
   1.641 +  done
   1.642 +
   1.643 +text {*
   1.644 +  \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
   1.645 +*}
   1.646 +
   1.647 +lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
   1.648 +    (\<exists>s t. (\<exists>m. \<W> e a n = Ok (s, t, m)) \<and> (\<exists>r. $s' a = $r ($s a) \<and> t' = $r t))"
   1.649 +  apply (atomize (full))
   1.650 +  apply (induct e)
   1.651 +    txt {* case @{text "Var n"} *}
   1.652 +    apply (intro strip)
   1.653 +    apply (simp (no_asm) cong add: conj_cong)
   1.654 +    apply (erule has_type_casesE)
   1.655 +    apply (simp add: eq_sym_conv app_subst_list)
   1.656 +    apply (rule_tac x = s' in exI)
   1.657 +    apply simp
   1.658 +   txt {* case @{text "Abs e"} *}
   1.659 +   apply (intro strip)
   1.660 +   apply (erule has_type_casesE)
   1.661 +   apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
   1.662 +   apply (erule_tac x = "TVar n # a" in allE)
   1.663 +   apply (erule_tac x = t2 in allE)
   1.664 +   apply (erule_tac x = "Suc n" in allE)
   1.665 +   apply (fastsimp cong add: conj_cong split add: split_bind)
   1.666 +  txt {* case @{text "App e1 e2"} *}
   1.667 +  apply (intro strip)
   1.668 +  apply (erule has_type_casesE)
   1.669 +  apply (erule_tac x = s' in allE)
   1.670 +  apply (erule_tac x = a in allE)
   1.671 +  apply (erule_tac x = "t2 -> t'" in allE)
   1.672 +  apply (erule_tac x = n in allE)
   1.673 +  apply (tactic "safe_tac HOL_cs")
   1.674 +  apply (erule_tac x = r in allE)
   1.675 +  apply (erule_tac x = "$s a" in allE)
   1.676 +  apply (erule_tac x = t2 in allE)
   1.677 +  apply (erule_tac x = m in allE)
   1.678 +  apply simp
   1.679 +  apply (tactic "safe_tac HOL_cs")
   1.680 +   apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
   1.681 +     thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
   1.682 +  apply (subgoal_tac
   1.683 +    "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   1.684 +      else ra x)) ($ sa t) =
   1.685 +    $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   1.686 +      else ra x)) (ta -> (TVar ma))")
   1.687 +   apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
   1.688 +     else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
   1.689 +     s = "($ ra ta) -> t'" in ssubst)
   1.690 +    prefer 2
   1.691 +    apply (simp add: subst_comp_te)
   1.692 +    apply (rule eq_free_eq_subst_te)
   1.693 +    apply (intro strip)
   1.694 +    apply (subgoal_tac "na \<noteq> ma")
   1.695 +     prefer 2
   1.696 +     apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
   1.697 +    apply (case_tac "na \<in> free_tv sa")
   1.698 +     txt {* @{text "na \<notin> free_tv sa"} *}
   1.699 +     prefer 2
   1.700 +     apply (frule not_free_impl_id)
   1.701 +     apply simp
   1.702 +    txt {* @{text "na \<in> free_tv sa"} *}
   1.703 +    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
   1.704 +    apply (drule_tac eq_subst_tel_eq_free)
   1.705 +     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   1.706 +    apply simp
   1.707 +    apply (case_tac "na \<in> dom sa")
   1.708 +     prefer 2
   1.709 +     txt {* @{text "na \<noteq> dom sa"} *}
   1.710 +     apply (simp add: dom_def)
   1.711 +    txt {* @{text "na \<in> dom sa"} *}
   1.712 +    apply (rule eq_free_eq_subst_te)
   1.713 +    apply (intro strip)
   1.714 +    apply (subgoal_tac "nb \<noteq> ma")
   1.715 +     prefer 2
   1.716 +     apply (frule new_tv_W, assumption)
   1.717 +     apply (erule conjE)
   1.718 +     apply (drule new_tv_subst_tel)
   1.719 +      apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   1.720 +     apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
   1.721 +    apply (fastsimp simp add: cod_def free_tv_subst)
   1.722 +   prefer 2
   1.723 +   apply (simp (no_asm))
   1.724 +   apply (rule eq_free_eq_subst_te)
   1.725 +   apply (intro strip)
   1.726 +   apply (subgoal_tac "na \<noteq> ma")
   1.727 +    prefer 2
   1.728 +    apply (frule new_tv_W, assumption)
   1.729 +    apply (erule conjE)
   1.730 +    apply (drule sym [THEN W_var_geD])
   1.731 +    apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
   1.732 +   apply (case_tac "na \<in> free_tv t - free_tv sa")
   1.733 +    prefer 2
   1.734 +    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   1.735 +    apply simp
   1.736 +    defer
   1.737 +    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   1.738 +    apply simp
   1.739 +    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
   1.740 +    apply (drule eq_subst_tel_eq_free)
   1.741 +     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   1.742 +    apply (simp add: free_tv_subst dom_def)
   1.743 +   prefer 2 apply fast
   1.744 +  apply (simp (no_asm_simp) split add: split_bind)
   1.745 +  apply (tactic "safe_tac HOL_cs")
   1.746 +   apply (drule mgu_Ok)
   1.747 +   apply fastsimp
   1.748 +  apply (drule mgu_mg, assumption)
   1.749 +  apply (erule exE)
   1.750 +  apply (rule_tac x = rb in exI)
   1.751 +  apply (rule conjI)
   1.752 +   prefer 2
   1.753 +   apply (drule_tac x = ma in fun_cong)
   1.754 +   apply (simp add: eq_sym_conv)
   1.755 +  apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
   1.756 +  apply (rule subst_comp_tel [symmetric, THEN [2] trans])
   1.757 +  apply (simp add: o_def eq_sym_conv)
   1.758 +  apply (rule eq_free_eq_subst_tel)
   1.759 +  apply (tactic "safe_tac HOL_cs")
   1.760 +  apply (subgoal_tac "ma \<noteq> na")
   1.761 +   prefer 2
   1.762 +   apply (frule new_tv_W, assumption)
   1.763 +   apply (erule conjE)
   1.764 +   apply (drule new_tv_subst_tel)
   1.765 +    apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   1.766 +   apply (frule_tac n = m in new_tv_W, assumption)
   1.767 +   apply (erule conjE)
   1.768 +   apply (drule free_tv_app_subst_tel [THEN subsetD])
   1.769 +   apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
   1.770 +     thm "codD", thm "new_tv_not_free_tv"]) 1 *})
   1.771 +  apply (case_tac "na \<in> free_tv t - free_tv sa")
   1.772 +   prefer 2
   1.773 +   txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   1.774 +   apply simp
   1.775 +   defer
   1.776 +   txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   1.777 +   apply simp
   1.778 +   apply (drule free_tv_app_subst_tel [THEN subsetD])
   1.779 +   apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
   1.780 +     eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
   1.781 +  apply fast
   1.782 +  done
   1.783 +
   1.784 +lemma W_complete: "[] |- e :: t' ==>
   1.785 +    \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
   1.786 +  apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
   1.787 +    apply simp_all
   1.788 +  done
   1.789 +
   1.790 +
   1.791 +section {* Equivalence of @{text \<W>} and @{text \<I>} *}
   1.792 +
   1.793 +text {*
   1.794 +  Recursive definition of type inference algorithm @{text \<I>} for
   1.795 +  Mini-ML.
   1.796 +*}
   1.797 +
   1.798 +consts
   1.799 +  I :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<I>")
   1.800 +primrec
   1.801 +  "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
   1.802 +  "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
   1.803 +    Ok (s, TVar n -> t, m))"
   1.804 +  "\<I> (App e1 e2) a n s =
   1.805 +    ((s1, t1, m1) := \<I> e1 a n s;
   1.806 +    (s2, t2, m2) := \<I> e2 a m1 s1;
   1.807 +    u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   1.808 +    Ok($u o s2, TVar m2, Suc m2))"
   1.809 +
   1.810 +text {* \medskip Correctness. *}
   1.811 +
   1.812 +lemma I_correct_wrt_W: "!!a m s s' t n.
   1.813 +    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
   1.814 +    \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
   1.815 +  apply (atomize (full))
   1.816 +  apply (induct e)
   1.817 +    txt {* case @{text "Var n"} *}
   1.818 +    apply (simp add: app_subst_list split: split_if)
   1.819 +   txt {* case @{text "Abs e"} *}
   1.820 +   apply (tactic {* asm_full_simp_tac
   1.821 +     (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
   1.822 +   apply (intro strip)
   1.823 +   apply (rule conjI)
   1.824 +    apply (intro strip)
   1.825 +    apply (erule allE)+
   1.826 +    apply (erule impE)
   1.827 +     prefer 2 apply (fastsimp simp add: new_tv_subst)
   1.828 +    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   1.829 +      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   1.830 +   apply (intro strip)
   1.831 +   apply (erule allE)+
   1.832 +   apply (erule impE)
   1.833 +    prefer 2 apply (fastsimp simp add: new_tv_subst)
   1.834 +   apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   1.835 +     thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   1.836 +  txt {* case @{text "App e1 e2"} *}
   1.837 +  apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
   1.838 +  apply (intro strip)
   1.839 +  apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   1.840 +  apply (rule conjI)
   1.841 +   apply fastsimp
   1.842 +  apply (intro strip)
   1.843 +  apply (rename_tac s1 t1' n1')
   1.844 +  apply (erule_tac x = a in allE)
   1.845 +  apply (erule_tac x = m in allE)
   1.846 +  apply (erule_tac x = s in allE)
   1.847 +  apply (erule_tac x = s1' in allE)
   1.848 +  apply (erule_tac x = t1 in allE)
   1.849 +  apply (erule_tac x = n1 in allE)
   1.850 +  apply (erule_tac x = a in allE)
   1.851 +  apply (erule_tac x = n1 in allE)
   1.852 +  apply (erule_tac x = s1' in allE)
   1.853 +  apply (erule_tac x = s2' in allE)
   1.854 +  apply (erule_tac x = t2 in allE)
   1.855 +  apply (erule_tac x = n2 in allE)
   1.856 +  apply (rule conjI)
   1.857 +   apply (intro strip)
   1.858 +   apply (rule notI)
   1.859 +   apply simp
   1.860 +   apply (erule impE)
   1.861 +    apply (frule new_tv_subst_tel, assumption)
   1.862 +    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   1.863 +    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   1.864 +   apply (fastsimp simp add: subst_comp_tel)
   1.865 +  apply (intro strip)
   1.866 +  apply (rename_tac s2 t2' n2')
   1.867 +  apply (rule conjI)
   1.868 +   apply (intro strip)
   1.869 +   apply (rule notI)
   1.870 +   apply simp
   1.871 +   apply (erule impE)
   1.872 +   apply (frule new_tv_subst_tel, assumption)
   1.873 +   apply (drule_tac a = "$s a" in new_tv_W, assumption)
   1.874 +    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   1.875 +   apply (fastsimp simp add: subst_comp_tel subst_comp_te)
   1.876 +  apply (intro strip)
   1.877 +  apply (erule (1) notE impE)
   1.878 +  apply (erule (1) notE impE)
   1.879 +  apply (erule exE)
   1.880 +  apply (erule conjE)
   1.881 +  apply (erule impE)
   1.882 +   apply (frule new_tv_subst_tel, assumption)
   1.883 +   apply (drule_tac a = "$s a" in new_tv_W, assumption)
   1.884 +   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   1.885 +  apply (erule (1) notE impE)
   1.886 +  apply (erule exE conjE)+
   1.887 +  apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   1.888 +  apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
   1.889 +   apply (simp add: new_tv_subst)
   1.890 +  apply (frule new_tv_subst_tel, assumption)
   1.891 +  apply (drule_tac a = "$s a" in new_tv_W, assumption)
   1.892 +  apply (tactic "safe_tac HOL_cs")
   1.893 +    apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   1.894 +   apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   1.895 +  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
   1.896 +  apply (drule new_tv_subst_tel, assumption)
   1.897 +  apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   1.898 +  apply (drule new_tv_subst_tel, assumption)
   1.899 +  apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
   1.900 +  done
   1.901 +
   1.902 +lemma I_complete_wrt_W: "!!a m s.
   1.903 +    new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
   1.904 +  apply (atomize (full))
   1.905 +  apply (induct e)
   1.906 +    apply (simp add: app_subst_list)
   1.907 +   apply (simp (no_asm))
   1.908 +   apply (intro strip)
   1.909 +   apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
   1.910 +    apply (tactic {* asm_simp_tac (HOL_ss addsimps
   1.911 +      [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
   1.912 +    apply (erule conjE)
   1.913 +    apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
   1.914 +    apply (simp (no_asm_simp))
   1.915 +  apply (simp (no_asm_simp))
   1.916 +  apply (intro strip)
   1.917 +  apply (erule exE)+
   1.918 +  apply (erule conjE)+
   1.919 +  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   1.920 +   apply fast
   1.921 +  apply (erule exE)
   1.922 +  apply (erule conjE)
   1.923 +  apply hypsubst
   1.924 +  apply (simp (no_asm_simp))
   1.925 +  apply (erule disjE)
   1.926 +   apply (rule disjI1)
   1.927 +   apply (simp (no_asm_use) add: o_def subst_comp_tel)
   1.928 +   apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
   1.929 +     erule_tac [2] asm_rl, erule_tac [2] asm_rl)
   1.930 +   apply (rule conjI)
   1.931 +    apply (fast intro: W_var_ge [THEN new_tv_list_le])
   1.932 +   apply (rule new_tv_subst_comp_2)
   1.933 +    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   1.934 +   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   1.935 +  apply (rule disjI2)
   1.936 +  apply (erule exE)+
   1.937 +  apply (erule conjE)
   1.938 +  apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   1.939 +   apply (rule conjI)
   1.940 +   apply (fast intro: W_var_ge [THEN new_tv_list_le])
   1.941 +   apply (rule new_tv_subst_comp_1)
   1.942 +   apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   1.943 +   apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   1.944 +  apply (erule exE)
   1.945 +  apply (erule conjE)
   1.946 +  apply hypsubst
   1.947 +  apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
   1.948 +  done
   1.949 +
   1.950 +end