src/HOL/W0/W0.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 26360 cd956c4eadff
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/W0/W0.thy
     2     ID:         $Id$
     3     Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel
     4 *)
     5 
     6 theory W0
     7 imports Main
     8 begin
     9 
    10 section {* Universal error monad *}
    11 
    12 datatype 'a maybe = Ok 'a | Fail
    13 
    14 definition
    15   bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60) where
    16   "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)"
    17 
    18 syntax
    19   "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
    20 translations
    21   "P := E; F" == "E \<bind> (\<lambda>P. F)"
    22 
    23 lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)"
    24   by (simp add: bind_def)
    25 
    26 lemma bind_Fail [simp]: "Fail \<bind> f = Fail"
    27   by (simp add: bind_def)
    28 
    29 lemma split_bind:
    30     "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))"
    31   by (induct res) simp_all
    32 
    33 lemma split_bind_asm:
    34   "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))"
    35   by (simp split: split_bind)
    36 
    37 lemmas bind_splits = split_bind split_bind_asm
    38 
    39 lemma bind_eq_Fail [simp]:
    40   "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> f p = Fail))"
    41   by (simp split: split_bind)
    42 
    43 lemma rotate_Ok: "(y = Ok x) = (Ok x = y)"
    44   by (rule eq_sym_conv)
    45 
    46 
    47 section {* MiniML-types and type substitutions *}
    48 
    49 axclass type_struct \<subseteq> type
    50   -- {* new class for structures containing type variables *}
    51 
    52 datatype "typ" = TVar nat | TFun "typ" "typ"    (infixr "->" 70)
    53   -- {* type expressions *}
    54 
    55 types subst = "nat => typ"
    56   -- {* type variable substitution *}
    57 
    58 instance "typ" :: type_struct ..
    59 instance list :: (type_struct) type_struct ..
    60 instance "fun" :: (type, type_struct) type_struct ..
    61 
    62 
    63 subsection {* Substitutions *}
    64 
    65 consts
    66   app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct"    ("$")
    67   -- {* extension of substitution to type structures *}
    68 primrec (app_subst_typ)
    69   app_subst_TVar: "$s (TVar n) = s n"
    70   app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
    71 
    72 defs (overloaded)
    73   app_subst_list: "$s \<equiv> map ($s)"
    74 
    75 consts
    76   free_tv :: "'a::type_struct \<Rightarrow> nat set"
    77   -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
    78 
    79 primrec (free_tv_typ)
    80   "free_tv (TVar m) = {m}"
    81   "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2"
    82 
    83 primrec (free_tv_list)
    84   "free_tv [] = {}"
    85   "free_tv (x # xs) = free_tv x \<union> free_tv xs"
    86 
    87 definition
    88   dom :: "subst \<Rightarrow> nat set" where
    89   "dom s = {n. s n \<noteq> TVar n}"
    90   -- {* domain of a substitution *}
    91 
    92 definition
    93   cod :: "subst \<Rightarrow> nat set" where
    94   "cod s = (\<Union>m \<in> dom s. free_tv (s m))"
    95   -- {* codomain of a substitutions: the introduced variables *}
    96 
    97 defs (overloaded)
    98   free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
    99 
   100 text {*
   101   @{text "new_tv s n"} checks whether @{text n} is a new type variable
   102   wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
   103   than any type variable occuring in the type structure.
   104 *}
   105 
   106 definition
   107   new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool" where
   108   "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)"
   109 
   110 
   111 subsubsection {* Identity substitution *}
   112 
   113 definition
   114   id_subst :: subst where
   115   "id_subst = (\<lambda>n. TVar n)"
   116 
   117 lemma app_subst_id_te [simp]:
   118   "$id_subst = (\<lambda>t::typ. t)"
   119   -- {* application of @{text id_subst} does not change type expression *}
   120 proof
   121   fix t :: "typ"
   122   show "$id_subst t = t"
   123     by (induct t) (simp_all add: id_subst_def)
   124 qed
   125 
   126 lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)"
   127   -- {* application of @{text id_subst} does not change list of type expressions *}
   128 proof
   129   fix ts :: "typ list"
   130   show "$id_subst ts = ts"
   131     by (induct ts) (simp_all add: app_subst_list)
   132 qed
   133 
   134 lemma o_id_subst [simp]: "$s o id_subst = s"
   135   by (rule ext) (simp add: id_subst_def)
   136 
   137 lemma dom_id_subst [simp]: "dom id_subst = {}"
   138   by (simp add: dom_def id_subst_def)
   139 
   140 lemma cod_id_subst [simp]: "cod id_subst = {}"
   141   by (simp add: cod_def)
   142 
   143 lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
   144   by (simp add: free_tv_subst)
   145 
   146 
   147 lemma cod_app_subst [simp]:
   148   assumes free: "v \<in> free_tv (s n)"
   149     and neq: "v \<noteq> n"
   150   shows "v \<in> cod s"
   151 proof -
   152   have "s n \<noteq> TVar n"
   153   proof
   154     assume "s n = TVar n"
   155     with free have "v = n" by simp
   156     with neq show False ..
   157   qed
   158   with free show ?thesis
   159     by (auto simp add: dom_def cod_def)
   160 qed
   161 
   162 lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t"
   163   -- {* composition of substitutions *}
   164   by (induct t) simp_all
   165 
   166 lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts"
   167   by (induct ts) (simp_all add: app_subst_list subst_comp_te)
   168 
   169 
   170 lemma app_subst_Nil [simp]: "$s [] = []"
   171   by (simp add: app_subst_list)
   172 
   173 lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
   174   by (simp add: app_subst_list)
   175 
   176 lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
   177   by (simp add: new_tv_def)
   178 
   179 lemma new_tv_Fun [simp]:
   180   "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
   181   by (auto simp add: new_tv_def)
   182 
   183 lemma new_tv_Nil [simp]: "new_tv n []"
   184   by (simp add: new_tv_def)
   185 
   186 lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)"
   187   by (auto simp add: new_tv_def)
   188 
   189 lemma new_tv_id_subst [simp]: "new_tv n id_subst"
   190   by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
   191 
   192 lemma new_tv_subst:
   193   "new_tv n s =
   194     ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
   195      (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
   196   apply (unfold new_tv_def)
   197   apply (tactic "safe_tac HOL_cs")
   198   -- {* @{text \<Longrightarrow>} *}
   199     apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
   200       addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
   201    apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
   202     apply (tactic "safe_tac HOL_cs")
   203      apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset}
   204        addsimps [thm "free_tv_subst"])) 1 *})
   205     apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
   206     apply simp
   207     apply (unfold free_tv_subst cod_def dom_def)
   208     apply clarsimp
   209   apply safe
   210   apply metis
   211   apply (metis linorder_not_less)+
   212   done
   213 
   214 lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
   215   by (induct x) simp_all
   216 
   217 lemma subst_te_new_tv [simp]:
   218   "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
   219   -- {* substitution affects only variables occurring freely *}
   220   by (induct t) simp_all
   221 
   222 lemma subst_tel_new_tv [simp]:
   223   "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
   224   by (induct ts) simp_all
   225 
   226 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
   227   -- {* all greater variables are also new *}
   228 proof (induct t)
   229   case (TVar n)
   230   then show ?case by (auto intro: less_le_trans)
   231 next
   232   case TFun
   233   then show ?case by simp
   234 qed
   235 
   236 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
   237   by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
   238 
   239 lemma new_tv_list_le:
   240   assumes "n \<le> m"
   241   shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
   242 proof (induct ts)
   243   case Nil
   244   then show ?case by simp
   245 next
   246   case Cons
   247   with `n \<le> m` show ?case by (auto intro: new_tv_le)
   248 qed
   249 
   250 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
   251   by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
   252 
   253 lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
   254   apply (simp add: new_tv_subst)
   255   apply clarify
   256   apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
   257     apply clarify
   258     apply (simp_all add: new_tv_le)
   259   done
   260 
   261 lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
   262   by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
   263 
   264 lemma new_tv_subst_var:
   265     "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
   266   -- {* @{text new_tv} property remains if a substitution is applied *}
   267   by (simp add: new_tv_subst)
   268 
   269 lemma new_tv_subst_te [simp]:
   270     "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
   271   by (induct t) (auto simp add: new_tv_subst)
   272 
   273 lemma new_tv_subst_tel [simp]:
   274     "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
   275   by (induct ts) (fastsimp simp add: new_tv_subst)+
   276 
   277 lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
   278   -- {* auxilliary lemma *}
   279   by (simp add: new_tv_list)
   280 
   281 lemma new_tv_subst_comp_1 [simp]:
   282     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
   283   -- {* composition of substitutions preserves @{text new_tv} proposition *}
   284   by (simp add: new_tv_subst)
   285 
   286 lemma new_tv_subst_comp_2 [simp]:
   287     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
   288   by (simp add: new_tv_subst)
   289 
   290 lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
   291   -- {* new type variables do not occur freely in a type structure *}
   292   by (auto simp add: new_tv_def)
   293 
   294 lemma ftv_mem_sub_ftv_list [simp]:
   295     "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
   296   by (induct ts) auto
   297 
   298 text {*
   299   If two substitutions yield the same result if applied to a type
   300   structure the substitutions coincide on the free type variables
   301   occurring in the type structure.
   302 *}
   303 
   304 lemma eq_subst_te_eq_free:
   305     "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
   306   by (induct t) auto
   307 
   308 lemma eq_free_eq_subst_te:
   309     "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
   310   by (induct t) auto
   311 
   312 lemma eq_subst_tel_eq_free:
   313     "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
   314   by (induct ts) (auto intro: eq_subst_te_eq_free)
   315 
   316 lemma eq_free_eq_subst_tel:
   317     "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
   318   by (induct ts) (auto intro: eq_free_eq_subst_te)
   319 
   320 text {*
   321   \medskip Some useful lemmas.
   322 *}
   323 
   324 lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
   325   by (simp add: free_tv_subst)
   326 
   327 lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
   328   by (simp add: free_tv_subst dom_def)
   329 
   330 lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
   331   by (unfold new_tv_def) fast
   332 
   333 lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
   334   by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
   335 
   336 lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
   337   by (induct t) (auto simp add: free_tv_subst_var)
   338 
   339 lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
   340   apply (induct ts)
   341    apply simp
   342   apply (cut_tac free_tv_app_subst_te)
   343   apply fastsimp
   344   done
   345 
   346 lemma free_tv_comp_subst:
   347     "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   348   apply (unfold free_tv_subst dom_def)
   349   apply (auto dest!: free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD]
   350     simp add: cod_def dom_def simp del: bex_simps)
   351   done
   352 
   353 
   354 subsection {* Most general unifiers *}
   355 
   356 consts
   357   mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
   358 axioms
   359   mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
   360   mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
   361   mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
   362   mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
   363 
   364 lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
   365   -- {* @{text mgu} does not introduce new type variables *}
   366   by (unfold new_tv_def) (blast dest: mgu_free)
   367 
   368 
   369 section {* Mini-ML with type inference rules *}
   370 
   371 datatype
   372   expr = Var nat | Abs expr | App expr expr
   373 
   374 
   375 text {* Type inference rules. *}
   376 
   377 inductive
   378   has_type :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   379   where
   380     Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
   381   | Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
   382   | App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
   383       \<Longrightarrow> a |- App e1 e2 :: t1"
   384 
   385 
   386 text {* Type assigment is closed wrt.\ substitution. *}
   387 
   388 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
   389 proof (induct set: has_type)
   390   case (Var n a)
   391   then have "n < length (map ($ s) a)" by simp
   392   then have "map ($ s) a |- Var n :: map ($ s) a ! n"
   393     by (rule has_type.Var)
   394   also have "map ($ s) a ! n = $ s (a ! n)"
   395     by (rule nth_map) (rule Var)
   396   also have "map ($ s) a = $ s a"
   397     by (simp only: app_subst_list)
   398   finally show ?case .
   399 next
   400   case (Abs t1 a e t2)
   401   then have "$ s t1 # map ($ s) a |- e :: $ s t2"
   402     by (simp add: app_subst_list)
   403   then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
   404     by (rule has_type.Abs)
   405   then show ?case
   406     by (simp add: app_subst_list)
   407 next
   408   case App
   409   then show ?case by (simp add: has_type.App)
   410 qed
   411 
   412 
   413 section {* Correctness and completeness of the type inference algorithm W *}
   414 
   415 consts
   416   "\<W>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
   417 primrec
   418   "\<W> (Var i) a n =
   419     (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
   420   "\<W> (Abs e) a n =
   421     ((s, t, m) := \<W> e (TVar n # a) (Suc n);
   422      Ok (s, (s n) -> t, m))"
   423   "\<W> (App e1 e2) a n =
   424     ((s1, t1, m1) := \<W> e1 a n;
   425      (s2, t2, m2) := \<W> e2 ($s1 a) m1;
   426      u := mgu ($ s2 t1) (t2 -> TVar m2);
   427      Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
   428 
   429 theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
   430 proof (induct e arbitrary: a s t m n)
   431   case (Var i)
   432   from `Ok (s, t, m) = \<W> (Var i) a n`
   433   show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
   434 next
   435   case (Abs e)
   436   from `Ok (s, t, m) = \<W> (Abs e) a n`
   437   obtain t' where "t = s n -> t'"
   438       and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
   439     by (auto split: bind_splits)
   440   with Abs.hyps show "$s a |- Abs e :: t"
   441     by (force intro: has_type.Abs)
   442 next
   443   case (App e1 e2)
   444   from `Ok (s, t, m) = \<W> (App e1 e2) a n`
   445   obtain s1 t1 n1 s2 t2 n2 u where
   446           s: "s = $u o $s2 o s1"
   447       and t: "t = u n2"
   448       and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
   449       and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
   450       and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
   451     by (auto split: bind_splits simp: that)
   452   show "$s a |- App e1 e2 :: t"
   453   proof (rule has_type.App)
   454     from s have s': "$u ($s2 ($s1 a)) = $s a"
   455       by (simp add: subst_comp_tel o_def)
   456     show "$s a |- e1 :: $u t2 -> t"
   457     proof -
   458       from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps(1))
   459       then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
   460         by (intro has_type_subst_closed)
   461       with s' t mgu_ok show ?thesis by simp
   462     qed
   463     show "$s a |- e2 :: $u t2"
   464     proof -
   465       from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps(2))
   466       then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
   467         by (rule has_type_subst_closed)
   468       with s' show ?thesis by simp
   469     qed
   470   qed
   471 qed
   472 
   473 
   474 inductive_cases has_type_casesE:
   475   "s |- Var n :: t"
   476   "s |- Abs e :: t"
   477   "s |- App e1 e2 ::t"
   478 
   479 
   480 lemmas [simp] = Suc_le_lessD
   481   and [simp del] = less_imp_le ex_simps all_simps
   482 
   483 lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
   484   -- {* the resulting type variable is always greater or equal than the given one *}
   485   apply (atomize (full))
   486   apply (induct e)
   487     txt {* case @{text "Var n"} *}
   488     apply clarsimp
   489    txt {* case @{text "Abs e"} *}
   490    apply (simp split add: split_bind)
   491    apply (fast dest: Suc_leD)
   492   txt {* case @{text "App e1 e2"} *}
   493   apply (simp (no_asm) split add: split_bind)
   494   apply (intro strip)
   495   apply (rename_tac s t na sa ta nb sb)
   496   apply (erule_tac x = a in allE)
   497   apply (erule_tac x = n in allE)
   498   apply (erule_tac x = "$s a" in allE)
   499   apply (erule_tac x = s in allE)
   500   apply (erule_tac x = t in allE)
   501   apply (erule_tac x = na in allE)
   502   apply (erule_tac x = na in allE)
   503   apply (simp add: eq_sym_conv)
   504   done
   505 
   506 lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
   507   by (simp add: eq_sym_conv)
   508 
   509 lemma new_tv_W: "!!n a s t m.
   510   new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
   511   -- {* resulting type variable is new *}
   512   apply (atomize (full))
   513   apply (induct e)
   514     txt {* case @{text "Var n"} *}
   515     apply clarsimp
   516     apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
   517    txt {* case @{text "Abs e"} *}
   518    apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
   519    apply (intro strip)
   520    apply (erule_tac x = "Suc n" in allE)
   521    apply (erule_tac x = "TVar n # a" in allE)
   522    apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
   523   txt {* case @{text "App e1 e2"} *}
   524   apply (simp (no_asm) split add: split_bind)
   525   apply (intro strip)
   526   apply (rename_tac s t na sa ta nb sb)
   527   apply (erule_tac x = n in allE)
   528   apply (erule_tac x = a in allE)
   529   apply (erule_tac x = s in allE)
   530   apply (erule_tac x = t in allE)
   531   apply (erule_tac x = na in allE)
   532   apply (erule_tac x = na in allE)
   533   apply (simp add: eq_sym_conv)
   534   apply (erule_tac x = "$s a" in allE)
   535   apply (erule_tac x = sa in allE)
   536   apply (erule_tac x = ta in allE)
   537   apply (erule_tac x = nb in allE)
   538   apply (simp add: o_def rotate_Ok)
   539   apply (rule conjI)
   540    apply (rule new_tv_subst_comp_2)
   541     apply (rule new_tv_subst_comp_2)
   542      apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
   543      apply (rule_tac n = na in new_tv_subst_le)
   544       apply (simp add: rotate_Ok)
   545      apply (simp (no_asm_simp))
   546     apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   547       lessI [THEN less_imp_le, THEN new_tv_subst_le])
   548    apply (erule sym [THEN mgu_new])
   549     apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
   550       lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
   551       new_tv_le)
   552    apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   553      addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   554      addss @{simpset}) 1 *})
   555   apply (rule lessI [THEN new_tv_subst_var])
   556   apply (erule sym [THEN mgu_new])
   557     apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
   558       dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   559         lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   560   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   561     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   562     addss @{simpset}) 1 *})
   563   done
   564 
   565 lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
   566     (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
   567   apply (atomize (full))
   568   apply (induct e)
   569     txt {* case @{text "Var n"} *}
   570     apply clarsimp
   571     apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   572    txt {* case @{text "Abs e"} *}
   573    apply (simp add: free_tv_subst split add: split_bind)
   574    apply (intro strip)
   575    apply (rename_tac s t n1 v)
   576    apply (erule_tac x = "Suc n" in allE)
   577    apply (erule_tac x = "TVar n # a" in allE)
   578    apply (erule_tac x = s in allE)
   579    apply (erule_tac x = t in allE)
   580    apply (erule_tac x = n1 in allE)
   581    apply (erule_tac x = v in allE)
   582    apply (force elim!: allE intro: cod_app_subst)
   583   txt {* case @{text "App e1 e2"} *}
   584   apply (simp (no_asm) split add: split_bind)
   585   apply (intro strip)
   586   apply (rename_tac s t n1 s1 t1 n2 s3 v)
   587   apply (erule_tac x = n in allE)
   588   apply (erule_tac x = a in allE)
   589   apply (erule_tac x = s in allE)
   590   apply (erule_tac x = t in allE)
   591   apply (erule_tac x = n1 in allE)
   592   apply (erule_tac x = n1 in allE)
   593   apply (erule_tac x = v in allE)
   594   txt {* second case *}
   595   apply (erule_tac x = "$ s a" in allE)
   596   apply (erule_tac x = s1 in allE)
   597   apply (erule_tac x = t1 in allE)
   598   apply (erule_tac x = n2 in allE)
   599   apply (erule_tac x = v in allE)
   600   apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
   601    apply (simp add: rotate_Ok o_def)
   602    apply (drule W_var_geD)
   603    apply (drule W_var_geD)
   604    apply (frule less_le_trans, assumption)
   605    apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
   606      free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
   607   apply simp
   608   apply (drule sym [THEN W_var_geD])
   609   apply (drule sym [THEN W_var_geD])
   610   apply (frule less_le_trans, assumption)
   611   apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
   612     thm "free_tv_subst_var" RS subsetD,
   613     thm "free_tv_app_subst_te" RS subsetD,
   614     thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
   615     addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *})
   616       -- {* builtin arithmetic in simpset messes things up *}
   617   done
   618 
   619 text {*
   620   \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
   621 *}
   622 
   623 lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
   624     (\<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))"
   625   apply (atomize (full))
   626   apply (induct e)
   627     txt {* case @{text "Var n"} *}
   628     apply (intro strip)
   629     apply (simp (no_asm) cong add: conj_cong)
   630     apply (erule has_type_casesE)
   631     apply (simp add: eq_sym_conv app_subst_list)
   632     apply (rule_tac x = s' in exI)
   633     apply simp
   634    txt {* case @{text "Abs e"} *}
   635    apply (intro strip)
   636    apply (erule has_type_casesE)
   637    apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
   638    apply (erule_tac x = "TVar n # a" in allE)
   639    apply (erule_tac x = t2 in allE)
   640    apply (erule_tac x = "Suc n" in allE)
   641    apply (fastsimp cong add: conj_cong split add: split_bind)
   642   txt {* case @{text "App e1 e2"} *}
   643   apply (intro strip)
   644   apply (erule has_type_casesE)
   645   apply (erule_tac x = s' in allE)
   646   apply (erule_tac x = a in allE)
   647   apply (erule_tac x = "t2 -> t'" in allE)
   648   apply (erule_tac x = n in allE)
   649   apply (tactic "safe_tac HOL_cs")
   650   apply (erule_tac x = r in allE)
   651   apply (erule_tac x = "$s a" in allE)
   652   apply (erule_tac x = t2 in allE)
   653   apply (erule_tac x = m in allE)
   654   apply simp
   655   apply (tactic "safe_tac HOL_cs")
   656    apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
   657      thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
   658   apply (subgoal_tac
   659     "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   660       else ra x)) ($ sa t) =
   661     $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   662       else ra x)) (ta -> (TVar ma))")
   663    apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
   664      else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
   665      s = "($ ra ta) -> t'" in ssubst)
   666     prefer 2
   667     apply (simp add: subst_comp_te)
   668     apply (rule eq_free_eq_subst_te)
   669     apply (intro strip)
   670     apply (subgoal_tac "na \<noteq> ma")
   671      prefer 2
   672      apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
   673     apply (case_tac "na \<in> free_tv sa")
   674      txt {* @{text "na \<notin> free_tv sa"} *}
   675      prefer 2
   676      apply (frule not_free_impl_id)
   677      apply simp
   678     txt {* @{text "na \<in> free_tv sa"} *}
   679     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   680     apply (drule_tac eq_subst_tel_eq_free)
   681      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   682     apply simp
   683     apply (case_tac "na \<in> dom sa")
   684      prefer 2
   685      txt {* @{text "na \<noteq> dom sa"} *}
   686      apply (simp add: dom_def)
   687     txt {* @{text "na \<in> dom sa"} *}
   688     apply (rule eq_free_eq_subst_te)
   689     apply (intro strip)
   690     apply (subgoal_tac "nb \<noteq> ma")
   691      prefer 2
   692      apply (frule new_tv_W, assumption)
   693      apply (erule conjE)
   694      apply (drule new_tv_subst_tel)
   695       apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   696      apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
   697     apply (fastsimp simp add: cod_def free_tv_subst)
   698    prefer 2
   699    apply (simp (no_asm))
   700    apply (rule eq_free_eq_subst_te)
   701    apply (intro strip)
   702    apply (subgoal_tac "na \<noteq> ma")
   703     prefer 2
   704     apply (frule new_tv_W, assumption)
   705     apply (erule conjE)
   706     apply (drule sym [THEN W_var_geD])
   707     apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
   708    apply (case_tac "na \<in> free_tv t - free_tv sa")
   709     prefer 2
   710     txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   711     apply simp
   712     defer
   713     txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   714     apply simp
   715     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   716     apply (drule eq_subst_tel_eq_free)
   717      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   718     apply (simp add: free_tv_subst dom_def)
   719    prefer 2 apply fast
   720   apply (simp (no_asm_simp) split add: split_bind)
   721   apply (tactic "safe_tac HOL_cs")
   722    apply (drule mgu_Ok)
   723    apply fastsimp
   724   apply (drule mgu_mg, assumption)
   725   apply (erule exE)
   726   apply (rule_tac x = rb in exI)
   727   apply (rule conjI)
   728    prefer 2
   729    apply (drule_tac x = ma in fun_cong)
   730    apply (simp add: eq_sym_conv)
   731   apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
   732   apply (rule subst_comp_tel [symmetric, THEN [2] trans])
   733   apply (simp add: o_def eq_sym_conv)
   734   apply (rule eq_free_eq_subst_tel)
   735   apply (tactic "safe_tac HOL_cs")
   736   apply (subgoal_tac "ma \<noteq> na")
   737    prefer 2
   738    apply (frule new_tv_W, assumption)
   739    apply (erule conjE)
   740    apply (drule new_tv_subst_tel)
   741     apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   742    apply (frule_tac n = m in new_tv_W, assumption)
   743    apply (erule conjE)
   744    apply (drule free_tv_app_subst_tel [THEN subsetD])
   745    apply (auto dest: W_var_geD [OF sym] new_tv_list_le
   746      codD new_tv_not_free_tv)
   747   apply (case_tac "na \<in> free_tv t - free_tv sa")
   748    prefer 2
   749    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   750    apply simp
   751    defer
   752    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   753    apply simp
   754    apply (drule free_tv_app_subst_tel [THEN subsetD])
   755    apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
   756      eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
   757   done
   758 
   759 lemma W_complete: "[] |- e :: t' ==>
   760     \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
   761   apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
   762     apply simp_all
   763   done
   764 
   765 
   766 section {* Equivalence of W and I *}
   767 
   768 text {*
   769   Recursive definition of type inference algorithm @{text \<I>} for
   770   Mini-ML.
   771 *}
   772 
   773 consts
   774   "\<I>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
   775 primrec
   776   "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
   777   "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
   778     Ok (s, TVar n -> t, m))"
   779   "\<I> (App e1 e2) a n s =
   780     ((s1, t1, m1) := \<I> e1 a n s;
   781     (s2, t2, m2) := \<I> e2 a m1 s1;
   782     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   783     Ok($u o s2, TVar m2, Suc m2))"
   784 
   785 text {* \medskip Correctness. *}
   786 
   787 lemma I_correct_wrt_W: "!!a m s s' t n.
   788     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
   789     \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
   790   apply (atomize (full))
   791   apply (induct e)
   792     txt {* case @{text "Var n"} *}
   793     apply (simp add: app_subst_list split: split_if)
   794    txt {* case @{text "Abs e"} *}
   795    apply (tactic {* asm_full_simp_tac
   796      (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
   797    apply (intro strip)
   798    apply (rule conjI)
   799     apply (intro strip)
   800     apply (erule allE)+
   801     apply (erule impE)
   802      prefer 2 apply (fastsimp simp add: new_tv_subst)
   803     apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   804       thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
   805    apply (intro strip)
   806    apply (erule allE)+
   807    apply (erule impE)
   808     prefer 2 apply (fastsimp simp add: new_tv_subst)
   809    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   810      thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
   811   txt {* case @{text "App e1 e2"} *}
   812   apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
   813   apply (intro strip)
   814   apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   815   apply (rule conjI)
   816    apply fastsimp
   817   apply (intro strip)
   818   apply (rename_tac s1 t1' n1')
   819   apply (erule_tac x = a in allE)
   820   apply (erule_tac x = m in allE)
   821   apply (erule_tac x = s in allE)
   822   apply (erule_tac x = s1' in allE)
   823   apply (erule_tac x = t1 in allE)
   824   apply (erule_tac x = n1 in allE)
   825   apply (erule_tac x = a in allE)
   826   apply (erule_tac x = n1 in allE)
   827   apply (erule_tac x = s1' in allE)
   828   apply (erule_tac x = s2' in allE)
   829   apply (erule_tac x = t2 in allE)
   830   apply (erule_tac x = n2 in allE)
   831   apply (rule conjI)
   832    apply (intro strip)
   833    apply (rule notI)
   834    apply simp
   835    apply (erule impE)
   836     apply (frule new_tv_subst_tel, assumption)
   837     apply (drule_tac a = "$s a" in new_tv_W, assumption)
   838     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   839    apply (fastsimp simp add: subst_comp_tel)
   840   apply (intro strip)
   841   apply (rename_tac s2 t2' n2')
   842   apply (rule conjI)
   843    apply (intro strip)
   844    apply (rule notI)
   845    apply simp
   846    apply (erule impE)
   847    apply (frule new_tv_subst_tel, assumption)
   848    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   849     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   850    apply (fastsimp simp add: subst_comp_tel subst_comp_te)
   851   apply (intro strip)
   852   apply (erule (1) notE impE)
   853   apply (erule (1) notE impE)
   854   apply (erule exE)
   855   apply (erule conjE)
   856   apply (erule impE)
   857    apply (frule new_tv_subst_tel, assumption)
   858    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   859    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   860   apply (erule (1) notE impE)
   861   apply (erule exE conjE)+
   862   apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   863   apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
   864    apply (simp add: new_tv_subst)
   865   apply (frule new_tv_subst_tel, assumption)
   866   apply (drule_tac a = "$s a" in new_tv_W, assumption)
   867   apply (tactic "safe_tac HOL_cs")
   868     apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   869    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   870   apply (drule_tac e = e1 in sym [THEN W_var_geD])
   871   apply (drule new_tv_subst_tel, assumption)
   872   apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   873   apply (drule new_tv_subst_tel, assumption)
   874   apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
   875   done
   876 
   877 lemma I_complete_wrt_W: "!!a m s.
   878     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
   879   apply (atomize (full))
   880   apply (induct e)
   881     apply (simp add: app_subst_list)
   882    apply (simp (no_asm))
   883    apply (intro strip)
   884    apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
   885     apply (tactic {* asm_simp_tac (HOL_ss addsimps
   886       [thm "new_tv_Suc_list", @{thm lessI} RS @{thm less_imp_le} RS thm "new_tv_subst_le"]) 1 *})
   887     apply (erule conjE)
   888     apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
   889     apply (simp (no_asm_simp))
   890   apply (simp (no_asm_simp))
   891   apply (intro strip)
   892   apply (erule exE)+
   893   apply (erule conjE)+
   894   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   895    apply fast
   896   apply (erule exE)
   897   apply (erule conjE)
   898   apply hypsubst
   899   apply (simp (no_asm_simp))
   900   apply (erule disjE)
   901    apply (rule disjI1)
   902    apply (simp (no_asm_use) add: o_def subst_comp_tel)
   903    apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
   904      erule_tac [2] asm_rl, erule_tac [2] asm_rl)
   905    apply (rule conjI)
   906     apply (fast intro: W_var_ge [THEN new_tv_list_le])
   907    apply (rule new_tv_subst_comp_2)
   908     apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   909    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   910   apply (rule disjI2)
   911   apply (erule exE)+
   912   apply (erule conjE)
   913   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   914    apply (rule conjI)
   915    apply (fast intro: W_var_ge [THEN new_tv_list_le])
   916    apply (rule new_tv_subst_comp_1)
   917    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   918    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   919   apply (erule exE)
   920   apply (erule conjE)
   921   apply hypsubst
   922   apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
   923   done
   924 
   925 end