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