src/HOL/W0/W0.thy
author wenzelm
Sun Apr 09 18:51:13 2006 +0200 (2006-04-09)
changeset 19380 b808efaa5828
parent 15236 f289e8ba2bb3
child 19736 d8d0f8f51d69
permissions -rw-r--r--
tuned syntax/abbreviations;
     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 constdefs
    15   bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60)
    16   "m \<bind> f \<equiv> 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 constdefs
    88   dom :: "subst \<Rightarrow> nat set"
    89   "dom s \<equiv> {n. s n \<noteq> TVar n}"
    90   -- {* domain of a substitution *}
    91 
    92   cod :: "subst \<Rightarrow> nat set"
    93   "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
    94   -- {* codomain of a substitutions: the introduced variables *}
    95 
    96 defs
    97   free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
    98 
    99 text {*
   100   @{text "new_tv s n"} checks whether @{text n} is a new type variable
   101   wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
   102   than any type variable occuring in the type structure.
   103 *}
   104 
   105 constdefs
   106   new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
   107   "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
   108 
   109 
   110 subsubsection {* Identity substitution *}
   111 
   112 constdefs
   113   id_subst :: subst
   114   "id_subst \<equiv> \<lambda>n. TVar n"
   115 
   116 lemma app_subst_id_te [simp]:
   117   "$id_subst = (\<lambda>t::typ. t)"
   118   -- {* application of @{text id_subst} does not change type expression *}
   119 proof
   120   fix t :: "typ"
   121   show "$id_subst t = t"
   122     by (induct t) (simp_all add: id_subst_def)
   123 qed
   124 
   125 lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)"
   126   -- {* application of @{text id_subst} does not change list of type expressions *}
   127 proof
   128   fix ts :: "typ list"
   129   show "$id_subst ts = ts"
   130     by (induct ts) (simp_all add: app_subst_list)
   131 qed
   132 
   133 lemma o_id_subst [simp]: "$s o id_subst = s"
   134   by (rule ext) (simp add: id_subst_def)
   135 
   136 lemma dom_id_subst [simp]: "dom id_subst = {}"
   137   by (simp add: dom_def id_subst_def)
   138 
   139 lemma cod_id_subst [simp]: "cod id_subst = {}"
   140   by (simp add: cod_def)
   141 
   142 lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
   143   by (simp add: free_tv_subst)
   144 
   145 
   146 lemma cod_app_subst [simp]:
   147   assumes free: "v \<in> free_tv (s n)"
   148     and neq: "v \<noteq> n"
   149   shows "v \<in> cod s"
   150 proof -
   151   have "s n \<noteq> TVar n"
   152   proof
   153     assume "s n = TVar n"
   154     with free have "v = n" by simp
   155     with neq show False ..
   156   qed
   157   with free show ?thesis
   158     by (auto simp add: dom_def cod_def)
   159 qed
   160 
   161 lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t"
   162   -- {* composition of substitutions *}
   163   by (induct t) simp_all
   164 
   165 lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts"
   166   by (induct ts) (simp_all add: app_subst_list subst_comp_te)
   167 
   168 
   169 lemma app_subst_Nil [simp]: "$s [] = []"
   170   by (simp add: app_subst_list)
   171 
   172 lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
   173   by (simp add: app_subst_list)
   174 
   175 lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
   176   by (simp add: new_tv_def)
   177 
   178 lemma new_tv_Fun [simp]:
   179   "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)"
   180   by (auto simp add: new_tv_def)
   181 
   182 lemma new_tv_Nil [simp]: "new_tv n []"
   183   by (simp add: new_tv_def)
   184 
   185 lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)"
   186   by (auto simp add: new_tv_def)
   187 
   188 lemma new_tv_id_subst [simp]: "new_tv n id_subst"
   189   by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
   190 
   191 lemma new_tv_subst:
   192   "new_tv n s =
   193     ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
   194      (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
   195   apply (unfold new_tv_def)
   196   apply (tactic "safe_tac HOL_cs")
   197   -- {* @{text \<Longrightarrow>} *}
   198     apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
   199       addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
   200    apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
   201     apply (tactic "safe_tac HOL_cs")
   202      apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
   203        addsimps [thm "free_tv_subst"])) 1 *})
   204     apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
   205     apply simp
   206    apply (tactic {* fast_tac (set_cs addss (simpset()
   207      addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   208   -- {* @{text \<Longleftarrow>} *}
   209   apply (unfold free_tv_subst cod_def dom_def)
   210   apply (tactic "safe_tac set_cs")
   211    apply (cut_tac m = m and n = n in less_linear)
   212    apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1")
   213   apply (cut_tac m = ma and n = n in less_linear)
   214   apply (fast intro!: less_or_eq_imp_le)
   215   done
   216 
   217 lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"
   218   by (induct x) simp_all
   219 
   220 lemma subst_te_new_tv [simp]:
   221   "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
   222   -- {* substitution affects only variables occurring freely *}
   223   by (induct t) simp_all
   224 
   225 lemma subst_tel_new_tv [simp]:
   226   "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
   227   by (induct ts) simp_all
   228 
   229 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
   230   -- {* all greater variables are also new *}
   231 proof (induct t)
   232   case (TVar n)
   233   thus ?case by (auto intro: less_le_trans)
   234 next
   235   case TFun
   236   thus ?case by simp
   237 qed
   238 
   239 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
   240   by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
   241 
   242 lemma new_tv_list_le:
   243   "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
   244 proof (induct ts)
   245   case Nil
   246   thus ?case by simp
   247 next
   248   case Cons
   249   thus ?case by (auto intro: new_tv_le)
   250 qed
   251 
   252 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
   253   by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
   254 
   255 lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s"
   256   apply (simp add: new_tv_subst)
   257   apply clarify
   258   apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
   259     apply clarify
   260     apply (simp_all add: new_tv_le)
   261   done
   262 
   263 lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)"
   264   by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
   265 
   266 lemma new_tv_subst_var:
   267     "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)"
   268   -- {* @{text new_tv} property remains if a substitution is applied *}
   269   by (simp add: new_tv_subst)
   270 
   271 lemma new_tv_subst_te [simp]:
   272     "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
   273   by (induct t) (auto simp add: new_tv_subst)
   274 
   275 lemma new_tv_subst_tel [simp]:
   276     "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)"
   277   by (induct ts) (fastsimp simp add: new_tv_subst)+
   278 
   279 lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
   280   -- {* auxilliary lemma *}
   281   by (simp add: new_tv_list)
   282 
   283 lemma new_tv_subst_comp_1 [simp]:
   284     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)"
   285   -- {* composition of substitutions preserves @{text new_tv} proposition *}
   286   by (simp add: new_tv_subst)
   287 
   288 lemma new_tv_subst_comp_2 [simp]:
   289     "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
   290   by (simp add: new_tv_subst)
   291 
   292 lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts"
   293   -- {* new type variables do not occur freely in a type structure *}
   294   by (auto simp add: new_tv_def)
   295 
   296 lemma ftv_mem_sub_ftv_list [simp]:
   297     "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts"
   298   by (induct ts) auto
   299 
   300 text {*
   301   If two substitutions yield the same result if applied to a type
   302   structure the substitutions coincide on the free type variables
   303   occurring in the type structure.
   304 *}
   305 
   306 lemma eq_subst_te_eq_free:
   307     "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
   308   by (induct t) auto
   309 
   310 lemma eq_free_eq_subst_te:
   311     "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
   312   by (induct t) auto
   313 
   314 lemma eq_subst_tel_eq_free:
   315     "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
   316   by (induct ts) (auto intro: eq_subst_te_eq_free)
   317 
   318 lemma eq_free_eq_subst_tel:
   319     "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
   320   by (induct ts) (auto intro: eq_free_eq_subst_te)
   321 
   322 text {*
   323   \medskip Some useful lemmas.
   324 *}
   325 
   326 lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
   327   by (simp add: free_tv_subst)
   328 
   329 lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
   330   by (simp add: free_tv_subst dom_def)
   331 
   332 lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
   333   by (unfold new_tv_def) fast
   334 
   335 lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
   336   by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
   337 
   338 lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t"
   339   by (induct t) (auto simp add: free_tv_subst_var)
   340 
   341 lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts"
   342   apply (induct ts)
   343    apply simp
   344   apply (cut_tac free_tv_app_subst_te)
   345   apply fastsimp
   346   done
   347 
   348 lemma free_tv_comp_subst:
   349     "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   350   apply (unfold free_tv_subst dom_def)
   351   apply (tactic {*
   352     fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
   353     thm "free_tv_subst_var" RS subsetD]
   354     addss (simpset() delsimps bex_simps
   355     addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   356   done
   357 
   358 
   359 subsection {* Most general unifiers *}
   360 
   361 consts
   362   mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe"
   363 axioms
   364   mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
   365   mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
   366   mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
   367   mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
   368 
   369 lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u"
   370   -- {* @{text mgu} does not introduce new type variables *}
   371   by (unfold new_tv_def) (blast dest: mgu_free)
   372 
   373 
   374 section {* Mini-ML with type inference rules *}
   375 
   376 datatype
   377   expr = Var nat | Abs expr | App expr expr
   378 
   379 
   380 text {* Type inference rules. *}
   381 
   382 consts
   383   has_type :: "(typ list \<times> expr \<times> typ) set"
   384 
   385 abbreviation
   386   has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   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 = e1 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