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