src/HOL/MiniML/W.ML
author nipkow
Mon Apr 22 15:42:20 1996 +0200 (1996-04-22)
changeset 1669 e56cdf711729
parent 1525 d127436567d0
child 1818 ffc20ff80190
permissions -rw-r--r--
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
nipkow@1300
     1
(* Title:     HOL/MiniML/W.ML
nipkow@1300
     2
   ID:        $Id$
nipkow@1300
     3
   Author:    Dieter Nazareth and Tobias Nipkow
nipkow@1300
     4
   Copyright  1995 TU Muenchen
nipkow@1300
     5
nipkow@1300
     6
Correctness and completeness of type inference algorithm W
nipkow@1300
     7
*)
nipkow@1300
     8
nipkow@1300
     9
open W;
nipkow@1300
    10
nipkow@1300
    11
nipkow@1300
    12
(* stronger version of Suc_leD *)
nipkow@1300
    13
goalw Nat.thy [le_def] 
clasohm@1465
    14
        "!!m. Suc m <= n ==> m < n";
nipkow@1669
    15
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
nipkow@1300
    16
by (cut_facts_tac [less_linear] 1);
nipkow@1300
    17
by (fast_tac HOL_cs 1);
nipkow@1300
    18
qed "Suc_le_lessD";
nipkow@1300
    19
Addsimps [Suc_le_lessD];
nipkow@1300
    20
nipkow@1300
    21
(* correctness of W with respect to has_type *)
nipkow@1525
    22
goal W.thy
nipkow@1525
    23
        "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
nipkow@1300
    24
by (expr.induct_tac "e" 1);
nipkow@1300
    25
(* case Var n *)
nipkow@1300
    26
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1300
    27
(* case Abs e *)
nipkow@1300
    28
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
nipkow@1300
    29
                        setloop (split_tac [expand_bind])) 1);
nipkow@1300
    30
by (strip_tac 1);
nipkow@1300
    31
by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
nipkow@1300
    32
by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
nipkow@1300
    33
(* case App e1 e2 *)
nipkow@1300
    34
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
nipkow@1300
    35
by (strip_tac 1);
nipkow@1300
    36
by( rename_tac "sa ta na sb tb nb sc" 1);
nipkow@1300
    37
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
nipkow@1300
    38
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
nipkow@1300
    39
by (rtac (app_subst_Fun RS subst) 1);
nipkow@1525
    40
by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
nipkow@1300
    41
by (Asm_full_simp_tac 1);
nipkow@1300
    42
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
nipkow@1300
    43
by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
nipkow@1300
    44
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1669
    45
by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
nipkow@1486
    46
qed_spec_mp "W_correct";
nipkow@1300
    47
nipkow@1300
    48
val has_type_casesE = map(has_type.mk_cases expr.simps)
clasohm@1465
    49
        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
nipkow@1300
    50
nipkow@1300
    51
nipkow@1300
    52
(* the resulting type variable is always greater or equal than the given one *)
nipkow@1300
    53
goal thy
clasohm@1465
    54
        "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
nipkow@1300
    55
by (expr.induct_tac "e" 1);
nipkow@1300
    56
(* case Var(n) *)
nipkow@1300
    57
by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
nipkow@1300
    58
(* case Abs e *)
nipkow@1300
    59
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
nipkow@1300
    60
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
nipkow@1300
    61
(* case App e1 e2 *)
nipkow@1300
    62
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
nipkow@1300
    63
by (strip_tac 1);
nipkow@1300
    64
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
nipkow@1300
    65
by (eres_inst_tac [("x","a")] allE 1);
nipkow@1300
    66
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
    67
by (eres_inst_tac [("x","$ s a")] allE 1);
nipkow@1300
    68
by (eres_inst_tac [("x","s")] allE 1);
nipkow@1300
    69
by (eres_inst_tac [("x","t")] allE 1);
nipkow@1300
    70
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
    71
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
    72
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
    73
by (etac conjE 1);
nipkow@1300
    74
by (eres_inst_tac [("x","sa")] allE 1);
nipkow@1300
    75
by (eres_inst_tac [("x","ta")] allE 1);
nipkow@1300
    76
by (eres_inst_tac [("x","nb")] allE 1);
nipkow@1300
    77
by (etac conjE 1);
nipkow@1300
    78
by (res_inst_tac [("j","na")] le_trans 1); 
nipkow@1300
    79
by (Asm_simp_tac 1);
nipkow@1669
    80
by (Asm_simp_tac 1);
nipkow@1486
    81
qed_spec_mp "W_var_ge";
nipkow@1300
    82
nipkow@1300
    83
Addsimps [W_var_ge];
nipkow@1300
    84
nipkow@1300
    85
goal thy
clasohm@1465
    86
        "!! s. Ok (s,t,m) = W e a n ==> n<=m";
nipkow@1300
    87
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
    88
qed "W_var_geD";
nipkow@1300
    89
nipkow@1300
    90
nipkow@1300
    91
(* auxiliary lemma *)
nipkow@1300
    92
goal Maybe.thy "(y = Ok x) = (Ok x = y)";
nipkow@1300
    93
by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
    94
qed "rotate_Ok";
nipkow@1300
    95
nipkow@1300
    96
nipkow@1300
    97
(* resulting type variable is new *)
nipkow@1300
    98
goal thy
nipkow@1300
    99
     "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
nipkow@1525
   100
\                 new_tv m s & new_tv m t";
nipkow@1300
   101
by (expr.induct_tac "e" 1);
nipkow@1300
   102
(* case Var n *)
nipkow@1300
   103
by (fast_tac (HOL_cs addss (!simpset 
clasohm@1465
   104
        addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
nipkow@1300
   105
        setloop (split_tac [expand_if]))) 1);
nipkow@1300
   106
nipkow@1300
   107
(* case Abs e *)
nipkow@1300
   108
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
nipkow@1300
   109
    setloop (split_tac [expand_bind])) 1);
nipkow@1300
   110
by (strip_tac 1);
nipkow@1300
   111
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@1300
   112
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
nipkow@1300
   113
by (fast_tac (HOL_cs addss (!simpset
clasohm@1465
   114
              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
nipkow@1300
   115
nipkow@1300
   116
(* case App e1 e2 *)
nipkow@1300
   117
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
nipkow@1300
   118
by (strip_tac 1);
nipkow@1300
   119
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
nipkow@1300
   120
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
   121
by (eres_inst_tac [("x","a")] allE 1);
nipkow@1300
   122
by (eres_inst_tac [("x","s")] allE 1);
nipkow@1300
   123
by (eres_inst_tac [("x","t")] allE 1);
nipkow@1300
   124
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
   125
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
   126
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1300
   127
by (eres_inst_tac [("x","$ s a")] allE 1);
nipkow@1300
   128
by (eres_inst_tac [("x","sa")] allE 1);
nipkow@1300
   129
by (eres_inst_tac [("x","ta")] allE 1);
nipkow@1300
   130
by (eres_inst_tac [("x","nb")] allE 1);
nipkow@1669
   131
by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
nipkow@1300
   132
by (rtac conjI 1);
nipkow@1300
   133
by (rtac new_tv_subst_comp_2 1);
nipkow@1300
   134
by (rtac new_tv_subst_comp_2 1);
nipkow@1300
   135
by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
nipkow@1300
   136
by (res_inst_tac [("n","na")] new_tv_subst_le 1); 
nipkow@1300
   137
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
nipkow@1300
   138
by (Asm_simp_tac 1);
nipkow@1300
   139
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@1300
   140
     [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
nipkow@1300
   141
    1);
clasohm@1465
   142
by (etac (sym RS mgu_new) 1);
nipkow@1300
   143
by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,
nipkow@1300
   144
   new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
nipkow@1300
   145
   new_tv_subst_le,new_tv_le]) 1);
nipkow@1300
   146
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@1300
   147
     [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
clasohm@1465
   148
        addss (!simpset)) 1);
clasohm@1465
   149
by (rtac (lessI RS new_tv_subst_var) 1);
clasohm@1465
   150
by (etac (sym RS mgu_new) 1);
nipkow@1300
   151
by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
nipkow@1300
   152
   addDs [W_var_geD] addIs
nipkow@1300
   153
   [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS
nipkow@1300
   154
   new_tv_subst_le,new_tv_le] addss !simpset) 1);
nipkow@1300
   155
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@1300
   156
     [new_tv_list_le,new_tv_subst_tel,new_tv_le]
nipkow@1300
   157
     addss (!simpset)) 1);
nipkow@1486
   158
qed_spec_mp "new_tv_W";
nipkow@1300
   159
nipkow@1300
   160
nipkow@1300
   161
goal thy
clasohm@1465
   162
     "!n a s t m v. W e a n = Ok (s,t,m) -->            \
nipkow@1300
   163
\         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
nipkow@1300
   164
by (expr.induct_tac "e" 1);
nipkow@1300
   165
(* case Var n *)
nipkow@1300
   166
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
nipkow@1300
   167
    addss (!simpset setloop (split_tac [expand_if]))) 1);
nipkow@1300
   168
nipkow@1300
   169
(* case Abs e *)
nipkow@1300
   170
by (asm_full_simp_tac (!simpset addsimps
nipkow@1300
   171
    [free_tv_subst] setloop (split_tac [expand_bind])) 1);
nipkow@1300
   172
by (strip_tac 1);
nipkow@1300
   173
by (rename_tac "s t na sa ta m v" 1);
nipkow@1300
   174
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@1300
   175
by (eres_inst_tac [("x","TVar n # a")] allE 1);
nipkow@1300
   176
by (eres_inst_tac [("x","s")] allE 1);
nipkow@1300
   177
by (eres_inst_tac [("x","t")] allE 1);
nipkow@1300
   178
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
   179
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1669
   180
by (fast_tac (HOL_cs addIs [cod_app_subst]
nipkow@1669
   181
                     addss (!simpset addsimps [less_Suc_eq])) 1);
nipkow@1300
   182
nipkow@1300
   183
(* case App e1 e2 *)
nipkow@1300
   184
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
nipkow@1300
   185
by (strip_tac 1); 
nipkow@1300
   186
by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
nipkow@1300
   187
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
   188
by (eres_inst_tac [("x","a")] allE 1);
nipkow@1300
   189
by (eres_inst_tac [("x","s")] allE 1);
nipkow@1300
   190
by (eres_inst_tac [("x","t")] allE 1);
nipkow@1300
   191
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
   192
by (eres_inst_tac [("x","na")] allE 1);
nipkow@1300
   193
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   194
(* second case *)
nipkow@1300
   195
by (eres_inst_tac [("x","$ s a")] allE 1);
nipkow@1300
   196
by (eres_inst_tac [("x","sa")] allE 1);
nipkow@1300
   197
by (eres_inst_tac [("x","ta")] allE 1);
nipkow@1300
   198
by (eres_inst_tac [("x","nb")] allE 1);
nipkow@1300
   199
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   200
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
nipkow@1669
   201
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
clasohm@1465
   202
by (dtac W_var_geD 1);
clasohm@1465
   203
by (dtac W_var_geD 1);
nipkow@1300
   204
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
nipkow@1300
   205
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
nipkow@1300
   206
    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
nipkow@1300
   207
    less_le_trans,less_not_refl2,subsetD]
nipkow@1300
   208
  addEs [UnE] 
nipkow@1300
   209
  addss !simpset) 1);
nipkow@1300
   210
by (Asm_full_simp_tac 1); 
clasohm@1465
   211
by (dtac (sym RS W_var_geD) 1);
clasohm@1465
   212
by (dtac (sym RS W_var_geD) 1);
nipkow@1300
   213
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
nipkow@1300
   214
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
nipkow@1300
   215
    free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
nipkow@1300
   216
    less_le_trans,subsetD]
nipkow@1300
   217
  addEs [UnE]
nipkow@1300
   218
  addss !simpset) 1); 
nipkow@1486
   219
qed_spec_mp "free_tv_W"; 
nipkow@1300
   220
nipkow@1300
   221
(* Completeness of W w.r.t. has_type *)
nipkow@1300
   222
goal thy
nipkow@1525
   223
 "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
nipkow@1525
   224
\             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
nipkow@1525
   225
\                     (? r. $s' a = $r ($s a) & t' = $r t))";
nipkow@1300
   226
by (expr.induct_tac "e" 1);
nipkow@1300
   227
(* case Var n *)
nipkow@1300
   228
by (strip_tac 1);
nipkow@1300
   229
by (simp_tac (!simpset addcongs [conj_cong] 
nipkow@1300
   230
    setloop (split_tac [expand_if])) 1);
nipkow@1300
   231
by (eresolve_tac has_type_casesE 1); 
nipkow@1300
   232
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
nipkow@1300
   233
by (res_inst_tac [("x","id_subst")] exI 1);
nipkow@1300
   234
by (res_inst_tac [("x","nth nat a")] exI 1);
nipkow@1300
   235
by (Simp_tac 1);
nipkow@1300
   236
by (res_inst_tac [("x","s'")] exI 1);
nipkow@1300
   237
by (Asm_simp_tac 1);
nipkow@1300
   238
nipkow@1300
   239
(* case Abs e *)
nipkow@1300
   240
by (strip_tac 1);
nipkow@1300
   241
by (eresolve_tac has_type_casesE 1);
nipkow@1300
   242
by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
nipkow@1300
   243
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
nipkow@1300
   244
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   245
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@1300
   246
by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
nipkow@1300
   247
    setloop (split_tac [expand_bind]))) 1);
nipkow@1300
   248
nipkow@1300
   249
(* case App e1 e2 *)
nipkow@1300
   250
by (strip_tac 1);
nipkow@1300
   251
by (eresolve_tac has_type_casesE 1);
nipkow@1300
   252
by (eres_inst_tac [("x","s'")] allE 1);
nipkow@1300
   253
by (eres_inst_tac [("x","a")] allE 1);
nipkow@1400
   254
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
nipkow@1300
   255
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
   256
by (safe_tac HOL_cs);
nipkow@1300
   257
by (eres_inst_tac [("x","r")] allE 1);
nipkow@1300
   258
by (eres_inst_tac [("x","$ s a")] allE 1);
nipkow@1300
   259
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   260
by (eres_inst_tac [("x","m")] allE 1);
clasohm@1465
   261
by (dtac asm_rl 1);
clasohm@1465
   262
by (dtac asm_rl 1);
clasohm@1465
   263
by (dtac asm_rl 1);
nipkow@1300
   264
by (Asm_full_simp_tac 1);
nipkow@1300
   265
by (safe_tac HOL_cs);
nipkow@1300
   266
by (fast_tac HOL_cs 1);
nipkow@1300
   267
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
clasohm@1465
   268
        conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
nipkow@1300
   269
nipkow@1300
   270
by (subgoal_tac
nipkow@1300
   271
  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
nipkow@1300
   272
\        else ra x)) ($ sa t) = \
nipkow@1300
   273
\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
nipkow@1400
   274
\        else ra x)) (ta -> (TVar ma))" 1);
nipkow@1300
   275
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
nipkow@1300
   276
\   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
nipkow@1400
   277
    ("s","($ ra ta) -> t'")] ssubst 2);
nipkow@1300
   278
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
clasohm@1465
   279
by (rtac eq_free_eq_subst_te 2);  
nipkow@1300
   280
by (strip_tac 2);
nipkow@1300
   281
by (subgoal_tac "na ~=ma" 2);
nipkow@1300
   282
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
nipkow@1300
   283
    new_tv_not_free_tv,new_tv_le]) 3);
nipkow@1300
   284
by (case_tac "na:free_tv sa" 2);
nipkow@1300
   285
(* na ~: free_tv sa *)
nipkow@1300
   286
by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
nipkow@1300
   287
    setloop (split_tac [expand_if])) 3);
nipkow@1300
   288
(* na : free_tv sa *)
nipkow@1400
   289
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
clasohm@1465
   290
by (dtac eq_subst_tel_eq_free 2);
nipkow@1300
   291
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@1300
   292
by (Asm_simp_tac 2); 
nipkow@1300
   293
by (case_tac "na:dom sa" 2);
nipkow@1300
   294
(* na ~: dom sa *)
nipkow@1300
   295
by (asm_full_simp_tac (!simpset addsimps [dom_def] 
nipkow@1300
   296
    setloop (split_tac [expand_if])) 3);
nipkow@1300
   297
(* na : dom sa *)
clasohm@1465
   298
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   299
by (strip_tac 2);
nipkow@1300
   300
by (subgoal_tac "nb ~= ma" 2);
nipkow@1300
   301
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   302
by (etac conjE 3);
clasohm@1465
   303
by (dtac new_tv_subst_tel 3);
nipkow@1300
   304
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
nipkow@1300
   305
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
nipkow@1300
   306
    (!simpset addsimps [cod_def,free_tv_subst])) 3);
nipkow@1300
   307
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
nipkow@1300
   308
    setloop (split_tac [expand_if]))) 2);
nipkow@1300
   309
nipkow@1300
   310
by (Simp_tac 2);  
clasohm@1465
   311
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   312
by (strip_tac 2 );
nipkow@1300
   313
by (subgoal_tac "na ~= ma" 2);
nipkow@1300
   314
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   315
by (etac conjE 3);
clasohm@1465
   316
by (dtac (sym RS W_var_geD) 3);
nipkow@1300
   317
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
nipkow@1300
   318
by (case_tac "na: free_tv t - free_tv sa" 2);
nipkow@1300
   319
(* case na ~: free_tv t - free_tv sa *)
nipkow@1300
   320
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
nipkow@1300
   321
(* case na : free_tv t - free_tv sa *)
nipkow@1300
   322
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
nipkow@1400
   323
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
clasohm@1465
   324
by (dtac eq_subst_tel_eq_free 2);
nipkow@1300
   325
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@1486
   326
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
nipkow@1300
   327
nipkow@1300
   328
by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
nipkow@1300
   329
by (safe_tac HOL_cs );
clasohm@1465
   330
by (dtac mgu_Ok 1);
nipkow@1300
   331
by( fast_tac (HOL_cs addss !simpset) 1);
nipkow@1300
   332
by (REPEAT (resolve_tac [exI,conjI] 1));
nipkow@1300
   333
by (fast_tac HOL_cs 1);
nipkow@1300
   334
by (fast_tac HOL_cs 1);
nipkow@1300
   335
by ((dtac mgu_mg 1) THEN (atac 1));
clasohm@1465
   336
by (etac exE 1);
nipkow@1300
   337
by (res_inst_tac [("x","rb")] exI 1);
clasohm@1465
   338
by (rtac conjI 1);
nipkow@1300
   339
by (dres_inst_tac [("x","ma")] fun_cong 2);
nipkow@1300
   340
by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
nipkow@1300
   341
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
nipkow@1400
   342
by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
nipkow@1300
   343
    (2,trans)) 1);
nipkow@1300
   344
by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
clasohm@1465
   345
by (rtac eq_free_eq_subst_tel 1);
nipkow@1300
   346
by( safe_tac HOL_cs );
nipkow@1300
   347
by (subgoal_tac "ma ~= na" 1);
nipkow@1300
   348
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
clasohm@1465
   349
by (etac conjE 2);
clasohm@1465
   350
by (dtac new_tv_subst_tel 2);
nipkow@1300
   351
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
nipkow@1486
   352
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
clasohm@1465
   353
by (etac conjE 2);
clasohm@1465
   354
by (dtac (free_tv_app_subst_tel RS subsetD) 2);
nipkow@1300
   355
by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
nipkow@1300
   356
    new_tv_not_free_tv]) 2);
nipkow@1300
   357
by (case_tac "na: free_tv t - free_tv sa" 1);
nipkow@1300
   358
(* case na ~: free_tv t - free_tv sa *)
nipkow@1300
   359
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
nipkow@1300
   360
(* case na : free_tv t - free_tv sa *)
nipkow@1300
   361
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
clasohm@1465
   362
by (dtac (free_tv_app_subst_tel RS subsetD) 1);
nipkow@1300
   363
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
nipkow@1300
   364
    eq_subst_tel_eq_free] addss ((!simpset addsimps 
nipkow@1486
   365
    [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
nipkow@1525
   366
qed_spec_mp "W_complete_lemma";
nipkow@1525
   367
nipkow@1525
   368
goal W.thy
nipkow@1525
   369
 "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
nipkow@1525
   370
\                                 (? r. t' = $r t))";
nipkow@1525
   371
by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
nipkow@1525
   372
                W_complete_lemma 1);
nipkow@1525
   373
by(ALLGOALS Asm_full_simp_tac);
nipkow@1525
   374
qed "W_complete";