src/HOL/W0/W0.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14981 e73f8140af78
child 15236 f289e8ba2bb3
permissions -rw-r--r--
import -> imports
     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 syntax
   386   "_has_type" :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"
   387     ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
   388 translations
   389   "a |- e :: t" == "(a, e, t) \<in> has_type"
   390 
   391 inductive has_type
   392   intros
   393     Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
   394     Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
   395     App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
   396       \<Longrightarrow> a |- App e1 e2 :: t1"
   397 
   398 
   399 text {* Type assigment is closed wrt.\ substitution. *}
   400 
   401 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
   402 proof -
   403   assume "a |- e :: t"
   404   thus ?thesis (is "?P a e t")
   405   proof induct
   406     case (Var a n)
   407     hence "n < length (map ($ s) a)" by simp
   408     hence "map ($ s) a |- Var n :: map ($ s) a ! n"
   409       by (rule has_type.Var)
   410     also have "map ($ s) a ! n = $ s (a ! n)"
   411       by (rule nth_map)
   412     also have "map ($ s) a = $ s a"
   413       by (simp only: app_subst_list)
   414     finally show "?P a (Var n) (a ! n)" .
   415   next
   416     case (Abs a e t1 t2)
   417     hence "$ s t1 # map ($ s) a |- e :: $ s t2"
   418       by (simp add: app_subst_list)
   419     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
   420       by (rule has_type.Abs)
   421     thus "?P a (Abs e) (t1 -> t2)"
   422       by (simp add: app_subst_list)
   423   next
   424     case App
   425     thus ?case by (simp add: has_type.App)
   426   qed
   427 qed
   428 
   429 
   430 section {* Correctness and completeness of the type inference algorithm W *}
   431 
   432 consts
   433   W :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<W>")
   434 
   435 primrec
   436   "\<W> (Var i) a n =
   437     (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
   438   "\<W> (Abs e) a n =
   439     ((s, t, m) := \<W> e (TVar n # a) (Suc n);
   440      Ok (s, (s n) -> t, m))"
   441   "\<W> (App e1 e2) a n =
   442     ((s1, t1, m1) := \<W> e1 a n;
   443      (s2, t2, m2) := \<W> e2 ($s1 a) m1;
   444      u := mgu ($ s2 t1) (t2 -> TVar m2);
   445      Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
   446 
   447 theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
   448   (is "PROP ?P e")
   449 proof (induct e)
   450   fix a s t m n
   451   {
   452     fix i
   453     assume "Ok (s, t, m) = \<W> (Var i) a n"
   454     thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
   455   next
   456     fix e assume hyp: "PROP ?P e"
   457     assume "Ok (s, t, m) = \<W> (Abs e) a n"
   458     then obtain t' where "t = s n -> t'"
   459         and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
   460       by (auto split: bind_splits)
   461     with hyp show "$s a |- Abs e :: t"
   462       by (force intro: has_type.Abs)
   463   next
   464     fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
   465     assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
   466     then obtain s1 t1 n1 s2 t2 n2 u where
   467           s: "s = $u o $s2 o s1"
   468         and t: "t = u n2"
   469         and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
   470         and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
   471         and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
   472       by (auto split: bind_splits simp: that)
   473     show "$s a |- App e1 e2 :: t"
   474     proof (rule has_type.App)
   475       from s have s': "$u ($s2 ($s1 a)) = $s a"
   476         by (simp add: subst_comp_tel o_def)
   477       show "$s a |- e1 :: $u t2 -> t"
   478       proof -
   479         from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
   480         hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
   481           by (intro has_type_subst_closed)
   482         with s' t mgu_ok show ?thesis by simp
   483       qed
   484       show "$s a |- e2 :: $u t2"
   485       proof -
   486         from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
   487         hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
   488           by (rule has_type_subst_closed)
   489         with s' show ?thesis by simp
   490       qed
   491     qed
   492   }
   493 qed
   494 
   495 
   496 inductive_cases has_type_casesE:
   497   "s |- Var n :: t"
   498   "s |- Abs e :: t"
   499   "s |- App e1 e2 ::t"
   500 
   501 
   502 lemmas [simp] = Suc_le_lessD
   503   and [simp del] = less_imp_le ex_simps all_simps
   504 
   505 lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m"
   506   -- {* the resulting type variable is always greater or equal than the given one *}
   507   apply (atomize (full))
   508   apply (induct e)
   509     txt {* case @{text "Var n"} *}
   510     apply clarsimp
   511    txt {* case @{text "Abs e"} *}
   512    apply (simp split add: split_bind)
   513    apply (fast dest: Suc_leD)
   514   txt {* case @{text "App e1 e2"} *}
   515   apply (simp (no_asm) split add: split_bind)
   516   apply (intro strip)
   517   apply (rename_tac s t na sa ta nb sb)
   518   apply (erule_tac x = a in allE)
   519   apply (erule_tac x = n in allE)
   520   apply (erule_tac x = "$s a" in allE)
   521   apply (erule_tac x = s in allE)
   522   apply (erule_tac x = t in allE)
   523   apply (erule_tac x = na in allE)
   524   apply (erule_tac x = na in allE)
   525   apply (simp add: eq_sym_conv)
   526   done
   527 
   528 lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m"
   529   by (simp add: eq_sym_conv)
   530 
   531 lemma new_tv_W: "!!n a s t m.
   532   new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t"
   533   -- {* resulting type variable is new *}
   534   apply (atomize (full))
   535   apply (induct e)
   536     txt {* case @{text "Var n"} *}
   537     apply clarsimp
   538     apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
   539    txt {* case @{text "Abs e"} *}
   540    apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
   541    apply (intro strip)
   542    apply (erule_tac x = "Suc n" in allE)
   543    apply (erule_tac x = "TVar n # a" in allE)
   544    apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
   545   txt {* case @{text "App e1 e2"} *}
   546   apply (simp (no_asm) split add: split_bind)
   547   apply (intro strip)
   548   apply (rename_tac s t na sa ta nb sb)
   549   apply (erule_tac x = n in allE)
   550   apply (erule_tac x = a in allE)
   551   apply (erule_tac x = s in allE)
   552   apply (erule_tac x = t in allE)
   553   apply (erule_tac x = na in allE)
   554   apply (erule_tac x = na in allE)
   555   apply (simp add: eq_sym_conv)
   556   apply (erule_tac x = "$s a" in allE)
   557   apply (erule_tac x = sa in allE)
   558   apply (erule_tac x = ta in allE)
   559   apply (erule_tac x = nb in allE)
   560   apply (simp add: o_def rotate_Ok)
   561   apply (rule conjI)
   562    apply (rule new_tv_subst_comp_2)
   563     apply (rule new_tv_subst_comp_2)
   564      apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
   565      apply (rule_tac n = na in new_tv_subst_le)
   566       apply (simp add: rotate_Ok)
   567      apply (simp (no_asm_simp))
   568     apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   569       lessI [THEN less_imp_le, THEN new_tv_subst_le])
   570    apply (erule sym [THEN mgu_new])
   571     apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
   572       lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
   573       new_tv_le)
   574    apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   575      addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   576      addss (simpset())) 1 *})
   577   apply (rule lessI [THEN new_tv_subst_var])
   578   apply (erule sym [THEN mgu_new])
   579     apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
   580       dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
   581         lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   582   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
   583     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
   584     addss (simpset())) 1 *})
   585   done
   586 
   587 lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
   588     (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
   589   apply (atomize (full))
   590   apply (induct e)
   591     txt {* case @{text "Var n"} *}
   592     apply clarsimp
   593     apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   594    txt {* case @{text "Abs e"} *}
   595    apply (simp add: free_tv_subst split add: split_bind)
   596    apply (intro strip)
   597    apply (rename_tac s t n1 v)
   598    apply (erule_tac x = "Suc n" in allE)
   599    apply (erule_tac x = "TVar n # a" in allE)
   600    apply (erule_tac x = s in allE)
   601    apply (erule_tac x = t in allE)
   602    apply (erule_tac x = n1 in allE)
   603    apply (erule_tac x = v in allE)
   604    apply (force elim!: allE intro: cod_app_subst)
   605   txt {* case @{text "App e1 e2"} *}
   606   apply (simp (no_asm) split add: split_bind)
   607   apply (intro strip)
   608   apply (rename_tac s t n1 s1 t1 n2 s3 v)
   609   apply (erule_tac x = n in allE)
   610   apply (erule_tac x = a in allE)
   611   apply (erule_tac x = s in allE)
   612   apply (erule_tac x = t in allE)
   613   apply (erule_tac x = n1 in allE)
   614   apply (erule_tac x = n1 in allE)
   615   apply (erule_tac x = v in allE)
   616   txt {* second case *}
   617   apply (erule_tac x = "$ s a" in allE)
   618   apply (erule_tac x = s1 in allE)
   619   apply (erule_tac x = t1 in allE)
   620   apply (erule_tac x = n2 in allE)
   621   apply (erule_tac x = v in allE)
   622   apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
   623    apply (simp add: rotate_Ok o_def)
   624    apply (drule W_var_geD)
   625    apply (drule W_var_geD)
   626    apply (frule less_le_trans, assumption)
   627    apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
   628      free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
   629   apply simp
   630   apply (drule sym [THEN W_var_geD])
   631   apply (drule sym [THEN W_var_geD])
   632   apply (frule less_le_trans, assumption)
   633   apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
   634     thm "free_tv_subst_var" RS subsetD,
   635     thm "free_tv_app_subst_te" RS subsetD,
   636     thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD]
   637     addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
   638       -- {* builtin arithmetic in simpset messes things up *}
   639   done
   640 
   641 text {*
   642   \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}.
   643 *}
   644 
   645 lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
   646     (\<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))"
   647   apply (atomize (full))
   648   apply (induct e)
   649     txt {* case @{text "Var n"} *}
   650     apply (intro strip)
   651     apply (simp (no_asm) cong add: conj_cong)
   652     apply (erule has_type_casesE)
   653     apply (simp add: eq_sym_conv app_subst_list)
   654     apply (rule_tac x = s' in exI)
   655     apply simp
   656    txt {* case @{text "Abs e"} *}
   657    apply (intro strip)
   658    apply (erule has_type_casesE)
   659    apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE)
   660    apply (erule_tac x = "TVar n # a" in allE)
   661    apply (erule_tac x = t2 in allE)
   662    apply (erule_tac x = "Suc n" in allE)
   663    apply (fastsimp cong add: conj_cong split add: split_bind)
   664   txt {* case @{text "App e1 e2"} *}
   665   apply (intro strip)
   666   apply (erule has_type_casesE)
   667   apply (erule_tac x = s' in allE)
   668   apply (erule_tac x = a in allE)
   669   apply (erule_tac x = "t2 -> t'" in allE)
   670   apply (erule_tac x = n in allE)
   671   apply (tactic "safe_tac HOL_cs")
   672   apply (erule_tac x = r in allE)
   673   apply (erule_tac x = "$s a" in allE)
   674   apply (erule_tac x = t2 in allE)
   675   apply (erule_tac x = m in allE)
   676   apply simp
   677   apply (tactic "safe_tac HOL_cs")
   678    apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
   679      thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
   680   apply (subgoal_tac
   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)) ($ sa t) =
   683     $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
   684       else ra x)) (ta -> (TVar ma))")
   685    apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
   686      else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
   687      s = "($ ra ta) -> t'" in ssubst)
   688     prefer 2
   689     apply (simp add: subst_comp_te)
   690     apply (rule eq_free_eq_subst_te)
   691     apply (intro strip)
   692     apply (subgoal_tac "na \<noteq> ma")
   693      prefer 2
   694      apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
   695     apply (case_tac "na \<in> free_tv sa")
   696      txt {* @{text "na \<notin> free_tv sa"} *}
   697      prefer 2
   698      apply (frule not_free_impl_id)
   699      apply simp
   700     txt {* @{text "na \<in> free_tv sa"} *}
   701     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   702     apply (drule_tac eq_subst_tel_eq_free)
   703      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   704     apply simp
   705     apply (case_tac "na \<in> dom sa")
   706      prefer 2
   707      txt {* @{text "na \<noteq> dom sa"} *}
   708      apply (simp add: dom_def)
   709     txt {* @{text "na \<in> dom sa"} *}
   710     apply (rule eq_free_eq_subst_te)
   711     apply (intro strip)
   712     apply (subgoal_tac "nb \<noteq> ma")
   713      prefer 2
   714      apply (frule new_tv_W, assumption)
   715      apply (erule conjE)
   716      apply (drule new_tv_subst_tel)
   717       apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   718      apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
   719     apply (fastsimp simp add: cod_def free_tv_subst)
   720    prefer 2
   721    apply (simp (no_asm))
   722    apply (rule eq_free_eq_subst_te)
   723    apply (intro strip)
   724    apply (subgoal_tac "na \<noteq> ma")
   725     prefer 2
   726     apply (frule new_tv_W, assumption)
   727     apply (erule conjE)
   728     apply (drule sym [THEN W_var_geD])
   729     apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
   730    apply (case_tac "na \<in> free_tv t - free_tv sa")
   731     prefer 2
   732     txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   733     apply simp
   734     defer
   735     txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   736     apply simp
   737     apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   738     apply (drule eq_subst_tel_eq_free)
   739      apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   740     apply (simp add: free_tv_subst dom_def)
   741    prefer 2 apply fast
   742   apply (simp (no_asm_simp) split add: split_bind)
   743   apply (tactic "safe_tac HOL_cs")
   744    apply (drule mgu_Ok)
   745    apply fastsimp
   746   apply (drule mgu_mg, assumption)
   747   apply (erule exE)
   748   apply (rule_tac x = rb in exI)
   749   apply (rule conjI)
   750    prefer 2
   751    apply (drule_tac x = ma in fun_cong)
   752    apply (simp add: eq_sym_conv)
   753   apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
   754   apply (rule subst_comp_tel [symmetric, THEN [2] trans])
   755   apply (simp add: o_def eq_sym_conv)
   756   apply (rule eq_free_eq_subst_tel)
   757   apply (tactic "safe_tac HOL_cs")
   758   apply (subgoal_tac "ma \<noteq> na")
   759    prefer 2
   760    apply (frule new_tv_W, assumption)
   761    apply (erule conjE)
   762    apply (drule new_tv_subst_tel)
   763     apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
   764    apply (frule_tac n = m in new_tv_W, assumption)
   765    apply (erule conjE)
   766    apply (drule free_tv_app_subst_tel [THEN subsetD])
   767    apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
   768      thm "codD", thm "new_tv_not_free_tv"]) 1 *})
   769   apply (case_tac "na \<in> free_tv t - free_tv sa")
   770    prefer 2
   771    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
   772    apply simp
   773    defer
   774    txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   775    apply simp
   776    apply (drule free_tv_app_subst_tel [THEN subsetD])
   777    apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
   778      eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
   779   apply fast
   780   done
   781 
   782 lemma W_complete: "[] |- e :: t' ==>
   783     \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)"
   784   apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
   785     apply simp_all
   786   done
   787 
   788 
   789 section {* Equivalence of W and I *}
   790 
   791 text {*
   792   Recursive definition of type inference algorithm @{text \<I>} for
   793   Mini-ML.
   794 *}
   795 
   796 consts
   797   I :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"  ("\<I>")
   798 primrec
   799   "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
   800   "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
   801     Ok (s, TVar n -> t, m))"
   802   "\<I> (App e1 e2) a n s =
   803     ((s1, t1, m1) := \<I> e1 a n s;
   804     (s2, t2, m2) := \<I> e2 a m1 s1;
   805     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   806     Ok($u o s2, TVar m2, Suc m2))"
   807 
   808 text {* \medskip Correctness. *}
   809 
   810 lemma I_correct_wrt_W: "!!a m s s' t n.
   811     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
   812     \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)"
   813   apply (atomize (full))
   814   apply (induct e)
   815     txt {* case @{text "Var n"} *}
   816     apply (simp add: app_subst_list split: split_if)
   817    txt {* case @{text "Abs e"} *}
   818    apply (tactic {* asm_full_simp_tac
   819      (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
   820    apply (intro strip)
   821    apply (rule conjI)
   822     apply (intro strip)
   823     apply (erule allE)+
   824     apply (erule impE)
   825      prefer 2 apply (fastsimp simp add: new_tv_subst)
   826     apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   827       thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   828    apply (intro strip)
   829    apply (erule allE)+
   830    apply (erule impE)
   831     prefer 2 apply (fastsimp simp add: new_tv_subst)
   832    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
   833      thm "new_tv_subst_le", less_imp_le, lessI]) 1 *})
   834   txt {* case @{text "App e1 e2"} *}
   835   apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
   836   apply (intro strip)
   837   apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   838   apply (rule conjI)
   839    apply fastsimp
   840   apply (intro strip)
   841   apply (rename_tac s1 t1' n1')
   842   apply (erule_tac x = a in allE)
   843   apply (erule_tac x = m in allE)
   844   apply (erule_tac x = s in allE)
   845   apply (erule_tac x = s1' in allE)
   846   apply (erule_tac x = t1 in allE)
   847   apply (erule_tac x = n1 in allE)
   848   apply (erule_tac x = a in allE)
   849   apply (erule_tac x = n1 in allE)
   850   apply (erule_tac x = s1' in allE)
   851   apply (erule_tac x = s2' in allE)
   852   apply (erule_tac x = t2 in allE)
   853   apply (erule_tac x = n2 in allE)
   854   apply (rule conjI)
   855    apply (intro strip)
   856    apply (rule notI)
   857    apply simp
   858    apply (erule impE)
   859     apply (frule new_tv_subst_tel, assumption)
   860     apply (drule_tac a = "$s a" in new_tv_W, assumption)
   861     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   862    apply (fastsimp simp add: subst_comp_tel)
   863   apply (intro strip)
   864   apply (rename_tac s2 t2' n2')
   865   apply (rule conjI)
   866    apply (intro strip)
   867    apply (rule notI)
   868    apply simp
   869    apply (erule impE)
   870    apply (frule new_tv_subst_tel, assumption)
   871    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   872     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   873    apply (fastsimp simp add: subst_comp_tel subst_comp_te)
   874   apply (intro strip)
   875   apply (erule (1) notE impE)
   876   apply (erule (1) notE impE)
   877   apply (erule exE)
   878   apply (erule conjE)
   879   apply (erule impE)
   880    apply (frule new_tv_subst_tel, assumption)
   881    apply (drule_tac a = "$s a" in new_tv_W, assumption)
   882    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   883   apply (erule (1) notE impE)
   884   apply (erule exE conjE)+
   885   apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   886   apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
   887    apply (simp add: new_tv_subst)
   888   apply (frule new_tv_subst_tel, assumption)
   889   apply (drule_tac a = "$s a" in new_tv_W, assumption)
   890   apply (tactic "safe_tac HOL_cs")
   891     apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   892    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   893   apply (drule_tac e = expr1 in sym [THEN W_var_geD])
   894   apply (drule new_tv_subst_tel, assumption)
   895   apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   896   apply (drule new_tv_subst_tel, assumption)
   897   apply (bestsimp dest: new_tv_W simp add: subst_comp_tel)
   898   done
   899 
   900 lemma I_complete_wrt_W: "!!a m s.
   901     new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail"
   902   apply (atomize (full))
   903   apply (induct e)
   904     apply (simp add: app_subst_list)
   905    apply (simp (no_asm))
   906    apply (intro strip)
   907    apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)")
   908     apply (tactic {* asm_simp_tac (HOL_ss addsimps
   909       [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *})
   910     apply (erule conjE)
   911     apply (drule new_tv_not_free_tv [THEN not_free_impl_id])
   912     apply (simp (no_asm_simp))
   913   apply (simp (no_asm_simp))
   914   apply (intro strip)
   915   apply (erule exE)+
   916   apply (erule conjE)+
   917   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   918    apply fast
   919   apply (erule exE)
   920   apply (erule conjE)
   921   apply hypsubst
   922   apply (simp (no_asm_simp))
   923   apply (erule disjE)
   924    apply (rule disjI1)
   925    apply (simp (no_asm_use) add: o_def subst_comp_tel)
   926    apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE,
   927      erule_tac [2] asm_rl, erule_tac [2] asm_rl)
   928    apply (rule conjI)
   929     apply (fast intro: W_var_ge [THEN new_tv_list_le])
   930    apply (rule new_tv_subst_comp_2)
   931     apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   932    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   933   apply (rule disjI2)
   934   apply (erule exE)+
   935   apply (erule conjE)
   936   apply (drule I_correct_wrt_W [COMP swap_prems_rl])
   937    apply (rule conjI)
   938    apply (fast intro: W_var_ge [THEN new_tv_list_le])
   939    apply (rule new_tv_subst_comp_1)
   940    apply (fast intro: W_var_ge [THEN new_tv_subst_le])
   941    apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1])
   942   apply (erule exE)
   943   apply (erule conjE)
   944   apply hypsubst
   945   apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric])
   946   done
   947 
   948 end