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