src/HOL/W0/W0.thy
author wenzelm
Wed Dec 06 01:12:36 2006 +0100 (2006-12-06)
changeset 21669 c68717c16013
parent 21404 eb85850d3eb7
child 22548 6ce4bddf3bcb
permissions -rw-r--r--
removed legacy ML bindings;
     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 [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 (tactic {* fast_tac (set_cs addss (simpset()
   208      addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   209   -- {* @{text \<Longleftarrow>} *}
   210   apply (unfold free_tv_subst cod_def dom_def)
   211   apply (tactic "safe_tac set_cs")
   212    apply (cut_tac m = m and n = n in less_linear)
   213    apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
   214   apply (cut_tac m = ma and n = n in less_linear)
   215   apply (fast intro!: less_or_eq_imp_le)
   216   done
   217 
   218 lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
   219   by (induct x) simp_all
   220 
   221 lemma subst_te_new_tv [simp]:
   222   "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
   223   -- {* substitution affects only variables occurring freely *}
   224   by (induct t) simp_all
   225 
   226 lemma subst_tel_new_tv [simp]:
   227   "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
   228   by (induct ts) simp_all
   229 
   230 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
   231   -- {* all greater variables are also new *}
   232 proof (induct t)
   233   case (TVar n)
   234   then show ?case by (auto intro: less_le_trans)
   235 next
   236   case TFun
   237   then show ?case by simp
   238 qed
   239 
   240 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
   241   by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
   242 
   243 lemma new_tv_list_le:
   244   assumes "n \<le> m"
   245   shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
   246 proof (induct ts)
   247   case Nil
   248   then show ?case by simp
   249 next
   250   case Cons
   251   with `n \<le> m` show ?case by (auto intro: new_tv_le)
   252 qed
   253 
   254 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
   255   by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
   256 
   257 lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
   258   apply (simp add: new_tv_subst)
   259   apply clarify
   260   apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
   261     apply clarify
   262     apply (simp_all add: new_tv_le)
   263   done
   264 
   265 lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
   266   by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
   267 
   268 lemma new_tv_subst_var:
   269     "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
   270   -- {* @{text new_tv} property remains if a substitution is applied *}
   271   by (simp add: new_tv_subst)
   272 
   273 lemma new_tv_subst_te [simp]:
   274     "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
   275   by (induct t) (auto simp add: new_tv_subst)
   276 
   277 lemma new_tv_subst_tel [simp]:
   278     "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
   279   by (induct ts) (fastsimp simp add: new_tv_subst)+
   280 
   281 lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
   282   -- {* auxilliary lemma *}
   283   by (simp add: new_tv_list)
   284 
   285 lemma new_tv_subst_comp_1 [simp]:
   286     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
   287   -- {* composition of substitutions preserves @{text new_tv} proposition *}
   288   by (simp add: new_tv_subst)
   289 
   290 lemma new_tv_subst_comp_2 [simp]:
   291     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
   292   by (simp add: new_tv_subst)
   293 
   294 lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
   295   -- {* new type variables do not occur freely in a type structure *}
   296   by (auto simp add: new_tv_def)
   297 
   298 lemma ftv_mem_sub_ftv_list [simp]:
   299     "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
   300   by (induct ts) auto
   301 
   302 text {*
   303   If two substitutions yield the same result if applied to a type
   304   structure the substitutions coincide on the free type variables
   305   occurring in the type structure.
   306 *}
   307 
   308 lemma eq_subst_te_eq_free:
   309     "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
   310   by (induct t) auto
   311 
   312 lemma eq_free_eq_subst_te:
   313     "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
   314   by (induct t) auto
   315 
   316 lemma eq_subst_tel_eq_free:
   317     "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
   318   by (induct ts) (auto intro: eq_subst_te_eq_free)
   319 
   320 lemma eq_free_eq_subst_tel:
   321     "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
   322   by (induct ts) (auto intro: eq_free_eq_subst_te)
   323 
   324 text {*
   325   \medskip Some useful lemmas.
   326 *}
   327 
   328 lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
   329   by (simp add: free_tv_subst)
   330 
   331 lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
   332   by (simp add: free_tv_subst dom_def)
   333 
   334 lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
   335   by (unfold new_tv_def) fast
   336 
   337 lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
   338   by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
   339 
   340 lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
   341   by (induct t) (auto simp add: free_tv_subst_var)
   342 
   343 lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
   344   apply (induct ts)
   345    apply simp
   346   apply (cut_tac free_tv_app_subst_te)
   347   apply fastsimp
   348   done
   349 
   350 lemma free_tv_comp_subst:
   351     "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   352   apply (unfold free_tv_subst dom_def)
   353   apply (tactic {*
   354     fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
   355     thm "free_tv_subst_var" RS subsetD]
   356     addss (simpset() delsimps (thms "bex_simps")
   357     addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   358   done
   359 
   360 
   361 subsection {* Most general unifiers *}
   362 
   363 consts
   364   mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
   365 axioms
   366   mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
   367   mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
   368   mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
   369   mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
   370 
   371 lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
   372   -- {* @{text mgu} does not introduce new type variables *}
   373   by (unfold new_tv_def) (blast dest: mgu_free)
   374 
   375 
   376 section {* Mini-ML with type inference rules *}
   377 
   378 datatype
   379   expr = Var nat | Abs expr | App expr expr
   380 
   381 
   382 text {* Type inference rules. *}
   383 
   384 consts
   385   has_type :: "(typ list \<times> expr \<times> typ) set"
   386 
   387 abbreviation
   388   has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60) where
   389   "a |- e :: t == (a, e, t) \<in> has_type"
   390 
   391 inductive has_type
   392   intros
   393     Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
   394     Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
   395     App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
   396       \<Longrightarrow> a |- App e1 e2 :: t1"
   397 
   398 
   399 text {* Type assigment is closed wrt.\ substitution. *}
   400 
   401 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
   402 proof (induct set: has_type)
   403   case (Var a n)
   404   then have "n < length (map ($ s) a)" by simp
   405   then have "map ($ s) a |- Var n :: map ($ s) a ! n"
   406     by (rule has_type.Var)
   407   also have "map ($ s) a ! n = $ s (a ! n)"
   408     by (rule nth_map)
   409   also have "map ($ s) a = $ s a"
   410     by (simp only: app_subst_list)
   411   finally show ?case .
   412 next
   413   case (Abs a e t1 t2)
   414   then have "$ s t1 # map ($ s) a |- e :: $ s t2"
   415     by (simp add: app_subst_list)
   416   then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
   417     by (rule has_type.Abs)
   418   then show ?case
   419     by (simp add: app_subst_list)
   420 next
   421   case App
   422   then show ?case by (simp add: has_type.App)
   423 qed
   424 
   425 
   426 section {* Correctness and completeness of the type inference algorithm W *}
   427 
   428 consts
   429   "\<W>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
   430 primrec
   431   "\<W> (Var i) a n =
   432     (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
   433   "\<W> (Abs e) a n =
   434     ((s, t, m) := \<W> e (TVar n # a) (Suc n);
   435      Ok (s, (s n) -> t, m))"
   436   "\<W> (App e1 e2) a n =
   437     ((s1, t1, m1) := \<W> e1 a n;
   438      (s2, t2, m2) := \<W> e2 ($s1 a) m1;
   439      u := mgu ($ s2 t1) (t2 -> TVar m2);
   440      Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
   441 
   442 theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
   443 proof (induct e arbitrary: a s t m n)
   444   case (Var i)
   445   from `Ok (s, t, m) = \<W> (Var i) a n`
   446   show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
   447 next
   448   case (Abs e)
   449   from `Ok (s, t, m) = \<W> (Abs e) a n`
   450   obtain t' where "t = s n -> t'"
   451       and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
   452     by (auto split: bind_splits)
   453   with Abs.hyps show "$s a |- Abs e :: t"
   454     by (force intro: has_type.Abs)
   455 next
   456   case (App e1 e2)
   457   from `Ok (s, t, m) = \<W> (App e1 e2) a n`
   458   obtain s1 t1 n1 s2 t2 n2 u where
   459           s: "s = $u o $s2 o s1"
   460       and t: "t = u n2"
   461       and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
   462       and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
   463       and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
   464     by (auto split: bind_splits simp: that)
   465   show "$s a |- App e1 e2 :: t"
   466   proof (rule has_type.App)
   467     from s have s': "$u ($s2 ($s1 a)) = $s a"
   468       by (simp add: subst_comp_tel o_def)
   469     show "$s a |- e1 :: $u t2 -> t"
   470     proof -
   471       from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps(1))
   472       then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
   473         by (intro has_type_subst_closed)
   474       with s' t mgu_ok show ?thesis by simp
   475     qed
   476     show "$s a |- e2 :: $u t2"
   477     proof -
   478       from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps(2))
   479       then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
   480         by (rule has_type_subst_closed)
   481       with s' show ?thesis by simp
   482     qed
   483   qed
   484 qed
   485 
   486 
   487 inductive_cases has_type_casesE:
   488   "s |- Var n :: t"
   489   "s |- Abs e :: t"
   490   "s |- App e1 e2 ::t"
   491 
   492 
   493 lemmas [simp] = Suc_le_lessD
   494   and [simp del] = less_imp_le ex_simps all_simps
   495 
   496 lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
   497   -- {* the resulting type variable is always greater or equal than the given one *}
   498   apply (atomize (full))
   499   apply (induct e)
   500     txt {* case @{text "Var n"} *}
   501     apply clarsimp
   502    txt {* case @{text "Abs e"} *}
   503    apply (simp split add: split_bind)
   504    apply (fast dest: Suc_leD)
   505   txt {* case @{text "App e1 e2"} *}
   506   apply (simp (no_asm) split add: split_bind)
   507   apply (intro strip)
   508   apply (rename_tac s t na sa ta nb sb)
   509   apply (erule_tac x = a in allE)
   510   apply (erule_tac x = n in allE)
   511   apply (erule_tac x = "$s a" in allE)
   512   apply (erule_tac x = s in allE)
   513   apply (erule_tac x = t in allE)
   514   apply (erule_tac x = na in allE)
   515   apply (erule_tac x = na in allE)
   516   apply (simp add: eq_sym_conv)
   517   done
   518 
   519 lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
   520   by (simp add: eq_sym_conv)
   521 
   522 lemma new_tv_W: "!!n a s t m.
   523   new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
   524   -- {* resulting type variable is new *}
   525   apply (atomize (full))
   526   apply (induct e)
   527     txt {* case @{text "Var n"} *}
   528     apply clarsimp
   529     apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
   530    txt {* case @{text "Abs e"} *}
   531    apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
   532    apply (intro strip)
   533    apply (erule_tac x = "Suc n" in allE)
   534    apply (erule_tac x = "TVar n # a" in allE)
   535    apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
   536   txt {* case @{text "App e1 e2"} *}
   537   apply (simp (no_asm) split add: split_bind)
   538   apply (intro strip)
   539   apply (rename_tac s t na sa ta nb sb)
   540   apply (erule_tac x = n in allE)
   541   apply (erule_tac x = a in allE)
   542   apply (erule_tac x = s in allE)
   543   apply (erule_tac x = t in allE)
   544   apply (erule_tac x = na in allE)
   545   apply (erule_tac x = na in allE)
   546   apply (simp add: eq_sym_conv)
   547   apply (erule_tac x = "$s a" in allE)
   548   apply (erule_tac x = sa in allE)
   549   apply (erule_tac x = ta in allE)
   550   apply (erule_tac x = nb in allE)
   551   apply (simp add: o_def rotate_Ok)
   552   apply (rule conjI)
   553    apply (rule new_tv_subst_comp_2)
   554     apply (rule new_tv_subst_comp_2)
   555      apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
   556      apply (rule_tac n = na in new_tv_subst_le)
   557       apply (simp add: rotate_Ok)
   558      apply (simp (no_asm_simp))
   559     apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   560       lessI [THEN less_imp_le, THEN new_tv_subst_le])
   561    apply (erule sym [THEN mgu_new])
   562     apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
   563       lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
   564       new_tv_le)
   565    apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   566      addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   567      addss (simpset())) 1 *})
   568   apply (rule lessI [THEN new_tv_subst_var])
   569   apply (erule sym [THEN mgu_new])
   570     apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
   571       dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   572         lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   573   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   574     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   575     addss (simpset())) 1 *})
   576   done
   577 
   578 lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
   579     (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
   580   apply (atomize (full))
   581   apply (induct e)
   582     txt {* case @{text "Var n"} *}
   583     apply clarsimp
   584     apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   585    txt {* case @{text "Abs e"} *}
   586    apply (simp add: free_tv_subst split add: split_bind)
   587    apply (intro strip)
   588    apply (rename_tac s t n1 v)
   589    apply (erule_tac x = "Suc n" in allE)
   590    apply (erule_tac x = "TVar n # a" in allE)
   591    apply (erule_tac x = s in allE)
   592    apply (erule_tac x = t in allE)
   593    apply (erule_tac x = n1 in allE)
   594    apply (erule_tac x = v in allE)
   595    apply (force elim!: allE intro: cod_app_subst)
   596   txt {* case @{text "App e1 e2"} *}
   597   apply (simp (no_asm) split add: split_bind)
   598   apply (intro strip)
   599   apply (rename_tac s t n1 s1 t1 n2 s3 v)
   600   apply (erule_tac x = n in allE)
   601   apply (erule_tac x = a in allE)
   602   apply (erule_tac x = s in allE)
   603   apply (erule_tac x = t in allE)
   604   apply (erule_tac x = n1 in allE)
   605   apply (erule_tac x = n1 in allE)
   606   apply (erule_tac x = v in allE)
   607   txt {* second case *}
   608   apply (erule_tac x = "$ s a" in allE)
   609   apply (erule_tac x = s1 in allE)
   610   apply (erule_tac x = t1 in allE)
   611   apply (erule_tac x = n2 in allE)
   612   apply (erule_tac x = v in allE)
   613   apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
   614    apply (simp add: rotate_Ok o_def)
   615    apply (drule W_var_geD)
   616    apply (drule W_var_geD)
   617    apply (frule less_le_trans, assumption)
   618    apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
   619      free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
   620   apply simp
   621   apply (drule sym [THEN W_var_geD])
   622   apply (drule sym [THEN W_var_geD])
   623   apply (frule less_le_trans, assumption)
   624   apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
   625     thm "free_tv_subst_var" RS subsetD,
   626     thm "free_tv_app_subst_te" RS subsetD,
   627     thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
   628     addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
   629       -- {* builtin arithmetic in simpset messes things up *}
   630   done
   631 
   632 text {*
   633   \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
   634 *}
   635 
   636 lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
   637     (\<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))"
   638   apply (atomize (full))
   639   apply (induct e)
   640     txt {* case @{text "Var n"} *}
   641     apply (intro strip)
   642     apply (simp (no_asm) cong add: conj_cong)
   643     apply (erule has_type_casesE)
   644     apply (simp add: eq_sym_conv app_subst_list)
   645     apply (rule_tac x = s' in exI)
   646     apply simp
   647    txt {* case @{text "Abs e"} *}
   648    apply (intro strip)
   649    apply (erule has_type_casesE)
   650    apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
   651    apply (erule_tac x = "TVar n # a" in allE)
   652    apply (erule_tac x = t2 in allE)
   653    apply (erule_tac x = "Suc n" in allE)
   654    apply (fastsimp cong add: conj_cong split add: split_bind)
   655   txt {* case @{text "App e1 e2"} *}
   656   apply (intro strip)
   657   apply (erule has_type_casesE)
   658   apply (erule_tac x = s' in allE)
   659   apply (erule_tac x = a in allE)
   660   apply (erule_tac x = "t2 -> t'" in allE)
   661   apply (erule_tac x = n in allE)
   662   apply (tactic "safe_tac HOL_cs")
   663   apply (erule_tac x = r in allE)
   664   apply (erule_tac x = "$s a" in allE)
   665   apply (erule_tac x = t2 in allE)
   666   apply (erule_tac x = m in allE)
   667   apply simp
   668   apply (tactic "safe_tac HOL_cs")
   669    apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
   670      thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
   671   apply (subgoal_tac
   672     "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   673       else ra x)) ($ sa t) =
   674     $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   675       else ra x)) (ta -> (TVar ma))")
   676    apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
   677      else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
   678      s = "($ ra ta) -> t'" in ssubst)
   679     prefer 2
   680     apply (simp add: subst_comp_te)
   681     apply (rule eq_free_eq_subst_te)
   682     apply (intro strip)
   683     apply (subgoal_tac "na \<noteq> ma")
   684      prefer 2
   685      apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
   686     apply (case_tac "na \<in> free_tv sa")
   687      txt {* @{text "na \<notin> free_tv sa"} *}
   688      prefer 2
   689      apply (frule not_free_impl_id)
   690      apply simp
   691     txt {* @{text "na \<in> free_tv sa"} *}
   692     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   693     apply (drule_tac eq_subst_tel_eq_free)
   694      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   695     apply simp
   696     apply (case_tac "na \<in> dom sa")
   697      prefer 2
   698      txt {* @{text "na \<noteq> dom sa"} *}
   699      apply (simp add: dom_def)
   700     txt {* @{text "na \<in> dom sa"} *}
   701     apply (rule eq_free_eq_subst_te)
   702     apply (intro strip)
   703     apply (subgoal_tac "nb \<noteq> ma")
   704      prefer 2
   705      apply (frule new_tv_W, assumption)
   706      apply (erule conjE)
   707      apply (drule new_tv_subst_tel)
   708       apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   709      apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
   710     apply (fastsimp simp add: cod_def free_tv_subst)
   711    prefer 2
   712    apply (simp (no_asm))
   713    apply (rule eq_free_eq_subst_te)
   714    apply (intro strip)
   715    apply (subgoal_tac "na \<noteq> ma")
   716     prefer 2
   717     apply (frule new_tv_W, assumption)
   718     apply (erule conjE)
   719     apply (drule sym [THEN W_var_geD])
   720     apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
   721    apply (case_tac "na \<in> free_tv t - free_tv sa")
   722     prefer 2
   723     txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   724     apply simp
   725     defer
   726     txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   727     apply simp
   728     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   729     apply (drule eq_subst_tel_eq_free)
   730      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   731     apply (simp add: free_tv_subst dom_def)
   732    prefer 2 apply fast
   733   apply (simp (no_asm_simp) split add: split_bind)
   734   apply (tactic "safe_tac HOL_cs")
   735    apply (drule mgu_Ok)
   736    apply fastsimp
   737   apply (drule mgu_mg, assumption)
   738   apply (erule exE)
   739   apply (rule_tac x = rb in exI)
   740   apply (rule conjI)
   741    prefer 2
   742    apply (drule_tac x = ma in fun_cong)
   743    apply (simp add: eq_sym_conv)
   744   apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
   745   apply (rule subst_comp_tel [symmetric, THEN [2] trans])
   746   apply (simp add: o_def eq_sym_conv)
   747   apply (rule eq_free_eq_subst_tel)
   748   apply (tactic "safe_tac HOL_cs")
   749   apply (subgoal_tac "ma \<noteq> na")
   750    prefer 2
   751    apply (frule new_tv_W, assumption)
   752    apply (erule conjE)
   753    apply (drule new_tv_subst_tel)
   754     apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   755    apply (frule_tac n = m in new_tv_W, assumption)
   756    apply (erule conjE)
   757    apply (drule free_tv_app_subst_tel [THEN subsetD])
   758    apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
   759      thm "codD", thm "new_tv_not_free_tv"]) 1 *})
   760   apply (case_tac "na \<in> free_tv t - free_tv sa")
   761    prefer 2
   762    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   763    apply simp
   764    defer
   765    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   766    apply simp
   767    apply (drule free_tv_app_subst_tel [THEN subsetD])
   768    apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
   769      eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
   770   apply fast
   771   done
   772 
   773 lemma W_complete: "[] |- e :: t' ==>
   774     \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
   775   apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
   776     apply simp_all
   777   done
   778 
   779 
   780 section {* Equivalence of W and I *}
   781 
   782 text {*
   783   Recursive definition of type inference algorithm @{text \<I>} for
   784   Mini-ML.
   785 *}
   786 
   787 consts
   788   "\<I>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
   789 primrec
   790   "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
   791   "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
   792     Ok (s, TVar n -> t, m))"
   793   "\<I> (App e1 e2) a n s =
   794     ((s1, t1, m1) := \<I> e1 a n s;
   795     (s2, t2, m2) := \<I> e2 a m1 s1;
   796     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   797     Ok($u o s2, TVar m2, Suc m2))"
   798 
   799 text {* \medskip Correctness. *}
   800 
   801 lemma I_correct_wrt_W: "!!a m s s' t n.
   802     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
   803     \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
   804   apply (atomize (full))
   805   apply (induct e)
   806     txt {* case @{text "Var n"} *}
   807     apply (simp add: app_subst_list split: split_if)
   808    txt {* case @{text "Abs e"} *}
   809    apply (tactic {* asm_full_simp_tac
   810      (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
   811    apply (intro strip)
   812    apply (rule conjI)
   813     apply (intro strip)
   814     apply (erule allE)+
   815     apply (erule impE)
   816      prefer 2 apply (fastsimp simp add: new_tv_subst)
   817     apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   818       thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   819    apply (intro strip)
   820    apply (erule allE)+
   821    apply (erule impE)
   822     prefer 2 apply (fastsimp simp add: new_tv_subst)
   823    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   824      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   825   txt {* case @{text "App e1 e2"} *}
   826   apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
   827   apply (intro strip)
   828   apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   829   apply (rule conjI)
   830    apply fastsimp
   831   apply (intro strip)
   832   apply (rename_tac s1 t1' n1')
   833   apply (erule_tac x = a in allE)
   834   apply (erule_tac x = m in allE)
   835   apply (erule_tac x = s in allE)
   836   apply (erule_tac x = s1' in allE)
   837   apply (erule_tac x = t1 in allE)
   838   apply (erule_tac x = n1 in allE)
   839   apply (erule_tac x = a in allE)
   840   apply (erule_tac x = n1 in allE)
   841   apply (erule_tac x = s1' in allE)
   842   apply (erule_tac x = s2' in allE)
   843   apply (erule_tac x = t2 in allE)
   844   apply (erule_tac x = n2 in allE)
   845   apply (rule conjI)
   846    apply (intro strip)
   847    apply (rule notI)
   848    apply simp
   849    apply (erule impE)
   850     apply (frule new_tv_subst_tel, assumption)
   851     apply (drule_tac a = "$s a" in new_tv_W, assumption)
   852     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   853    apply (fastsimp simp add: subst_comp_tel)
   854   apply (intro strip)
   855   apply (rename_tac s2 t2' n2')
   856   apply (rule conjI)
   857    apply (intro strip)
   858    apply (rule notI)
   859    apply simp
   860    apply (erule impE)
   861    apply (frule new_tv_subst_tel, assumption)
   862    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   863     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   864    apply (fastsimp simp add: subst_comp_tel subst_comp_te)
   865   apply (intro strip)
   866   apply (erule (1) notE impE)
   867   apply (erule (1) notE impE)
   868   apply (erule exE)
   869   apply (erule conjE)
   870   apply (erule impE)
   871    apply (frule new_tv_subst_tel, assumption)
   872    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   873    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   874   apply (erule (1) notE impE)
   875   apply (erule exE conjE)+
   876   apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   877   apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
   878    apply (simp add: new_tv_subst)
   879   apply (frule new_tv_subst_tel, assumption)
   880   apply (drule_tac a = "$s a" in new_tv_W, assumption)
   881   apply (tactic "safe_tac HOL_cs")
   882     apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   883    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   884   apply (drule_tac e = e1 in sym [THEN W_var_geD])
   885   apply (drule new_tv_subst_tel, assumption)
   886   apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   887   apply (drule new_tv_subst_tel, assumption)
   888   apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
   889   done
   890 
   891 lemma I_complete_wrt_W: "!!a m s.
   892     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
   893   apply (atomize (full))
   894   apply (induct e)
   895     apply (simp add: app_subst_list)
   896    apply (simp (no_asm))
   897    apply (intro strip)
   898    apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
   899     apply (tactic {* asm_simp_tac (HOL_ss addsimps
   900       [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
   901     apply (erule conjE)
   902     apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
   903     apply (simp (no_asm_simp))
   904   apply (simp (no_asm_simp))
   905   apply (intro strip)
   906   apply (erule exE)+
   907   apply (erule conjE)+
   908   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   909    apply fast
   910   apply (erule exE)
   911   apply (erule conjE)
   912   apply hypsubst
   913   apply (simp (no_asm_simp))
   914   apply (erule disjE)
   915    apply (rule disjI1)
   916    apply (simp (no_asm_use) add: o_def subst_comp_tel)
   917    apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
   918      erule_tac [2] asm_rl, erule_tac [2] asm_rl)
   919    apply (rule conjI)
   920     apply (fast intro: W_var_ge [THEN new_tv_list_le])
   921    apply (rule new_tv_subst_comp_2)
   922     apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   923    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   924   apply (rule disjI2)
   925   apply (erule exE)+
   926   apply (erule conjE)
   927   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   928    apply (rule conjI)
   929    apply (fast intro: W_var_ge [THEN new_tv_list_le])
   930    apply (rule new_tv_subst_comp_1)
   931    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   932    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   933   apply (erule exE)
   934   apply (erule conjE)
   935   apply hypsubst
   936   apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
   937   done
   938 
   939 end