src/HOL/MiniML/W.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6141 a6922171b396
child 6540 eaf90f6806df
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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
paulson@5348
     9
Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
nipkow@1300
    10
paulson@6141
    11
val has_type_casesE = 
paulson@6141
    12
    map has_type.mk_cases
paulson@6141
    13
	[" A |- Var n :: t",
paulson@6141
    14
	 " A |- Abs e :: t",
paulson@6141
    15
	 "A |- App e1 e2 ::t",
paulson@6141
    16
	 "A |- LET e1 e2 ::t" ];
nipkow@1300
    17
nipkow@1300
    18
(* the resulting type variable is always greater or equal than the given one *)
paulson@6141
    19
Goal "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
berghofe@5184
    20
by (induct_tac "e" 1);
nipkow@1300
    21
(* case Var(n) *)
nipkow@4686
    22
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@1300
    23
(* case Abs e *)
wenzelm@4089
    24
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@1300
    25
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
nipkow@1300
    26
(* case App e1 e2 *)
wenzelm@4089
    27
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
wenzelm@4423
    28
by (blast_tac (claset() addIs [le_SucI,le_trans]) 1);
nipkow@2525
    29
(* case LET e1 e2 *)
wenzelm@4089
    30
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
wenzelm@4423
    31
by (blast_tac (claset() addIs [le_trans]) 1);
nipkow@1486
    32
qed_spec_mp "W_var_ge";
nipkow@1300
    33
nipkow@1300
    34
Addsimps [W_var_ge];
nipkow@1300
    35
paulson@6141
    36
Goal "Some (S,t,m) = W e A n ==> n<=m";
wenzelm@4089
    37
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
nipkow@1300
    38
qed "W_var_geD";
nipkow@1300
    39
nipkow@5118
    40
Goal "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
nipkow@2525
    41
by (dtac W_var_geD 1);
nipkow@2525
    42
by (rtac new_scheme_list_le 1);
paulson@3018
    43
by (assume_tac 1);
paulson@3018
    44
by (assume_tac 1);
nipkow@2525
    45
qed "new_tv_compatible_W";
nipkow@1300
    46
nipkow@5118
    47
Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
berghofe@5184
    48
by (induct_tac "sch" 1);
nipkow@4727
    49
  by (Asm_full_simp_tac 1);
nipkow@4727
    50
 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
nipkow@2525
    51
by (strip_tac 1);
nipkow@2525
    52
by (Asm_full_simp_tac 1);
nipkow@2525
    53
by (etac conjE 1);
nipkow@2525
    54
by (rtac conjI 1);
nipkow@4727
    55
 by (rtac new_tv_le 1);
nipkow@4727
    56
  by (assume_tac 2);
nipkow@4727
    57
 by (rtac add_le_mono 1);
nipkow@4727
    58
  by (Simp_tac 1);
nipkow@4727
    59
 by (simp_tac (simpset() addsimps [max_def]) 1);
nipkow@2525
    60
by (rtac new_tv_le 1);
nipkow@4727
    61
 by (assume_tac 2);
nipkow@2525
    62
by (rtac add_le_mono 1);
nipkow@4727
    63
 by (Simp_tac 1);
nipkow@4686
    64
by (simp_tac (simpset() addsimps [max_def]) 1);
nipkow@2525
    65
qed_spec_mp "new_tv_bound_typ_inst_sch";
nipkow@2525
    66
nipkow@2525
    67
Addsimps [new_tv_bound_typ_inst_sch];
nipkow@1300
    68
nipkow@1300
    69
(* resulting type variable is new *)
paulson@6141
    70
Goal "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
nipkow@2525
    71
\                 new_tv m S & new_tv m t";
berghofe@5184
    72
by (induct_tac "e" 1);
nipkow@1300
    73
(* case Var n *)
nipkow@4686
    74
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@2525
    75
by (strip_tac 1);
nipkow@2525
    76
by (dtac new_tv_nth_nat_A 1);
paulson@3018
    77
by (assume_tac 1);
nipkow@4033
    78
by (Asm_simp_tac 1);
nipkow@1300
    79
(* case Abs e *)
wenzelm@4089
    80
by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
nipkow@4072
    81
    addsplits [split_option_bind]) 1);
nipkow@1300
    82
by (strip_tac 1);
nipkow@1300
    83
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@2525
    84
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
wenzelm@4089
    85
by (fast_tac (HOL_cs addss (simpset()
clasohm@1465
    86
              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
nipkow@1300
    87
(* case App e1 e2 *)
wenzelm@4089
    88
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@1300
    89
by (strip_tac 1);
nipkow@4033
    90
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
nipkow@1300
    91
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
    92
by (eres_inst_tac [("x","A")] allE 1);
nipkow@4033
    93
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@4033
    94
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
    95
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
    96
by (eres_inst_tac [("x","n1")] allE 1);
wenzelm@4089
    97
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv] delsimps all_simps) 1);
nipkow@4033
    98
by (eres_inst_tac [("x","$S1 A")] allE 1);
nipkow@4033
    99
by (eres_inst_tac [("x","S2")] allE 1);
nipkow@4033
   100
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@2525
   101
by (eres_inst_tac [("x","n2")] allE 1);
wenzelm@4089
   102
by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Some]) 1);
nipkow@1300
   103
by (rtac conjI 1);
nipkow@1300
   104
by (rtac new_tv_subst_comp_2 1);
nipkow@1300
   105
by (rtac new_tv_subst_comp_2 1);
nipkow@2525
   106
by (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
nipkow@2525
   107
by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 
wenzelm@4089
   108
by (asm_full_simp_tac (simpset() addsimps [rotate_Some]) 1);
nipkow@1300
   109
by (Asm_simp_tac 1);
nipkow@1300
   110
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   111
     [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le])
nipkow@1300
   112
    1);
clasohm@1465
   113
by (etac (sym RS mgu_new) 1);
nipkow@2525
   114
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
nipkow@2525
   115
   new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
nipkow@2525
   116
   new_tv_subst_le,new_tv_le]) 1);
nipkow@2525
   117
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   118
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 
wenzelm@4089
   119
        addss (simpset())) 1);
clasohm@1465
   120
by (rtac (lessI RS new_tv_subst_var) 1);
clasohm@1465
   121
by (etac (sym RS mgu_new) 1);
paulson@1925
   122
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
nipkow@2525
   123
   addDs [W_var_geD] addIs
nipkow@2525
   124
   [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS
wenzelm@4089
   125
   new_tv_subst_le,new_tv_le] addss simpset()) 1);
nipkow@2525
   126
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
nipkow@2525
   127
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
wenzelm@4089
   128
     addss (simpset())) 1);
nipkow@4033
   129
(* 41: case LET e1 e2 *)
wenzelm@4089
   130
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@2525
   131
by (strip_tac 1);
wenzelm@4423
   132
by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
nipkow@2525
   133
by (etac conjE 1);
wenzelm@4423
   134
by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
nipkow@4033
   135
         etac impE 1, mp_tac 2]);
nipkow@4033
   136
by (SELECT_GOAL(rewtac new_tv_def)1);
nipkow@4033
   137
by (Asm_simp_tac 1);
nipkow@4033
   138
by (REPEAT(dtac W_var_ge 1));
nipkow@4033
   139
by (rtac allI 1);
nipkow@4033
   140
by (strip_tac 1);
nipkow@4033
   141
by (SELECT_GOAL(rewtac free_tv_subst) 1);
nipkow@4033
   142
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
wenzelm@4089
   143
by (best_tac (claset() addEs [less_le_trans]) 1);
nipkow@2525
   144
by (etac conjE 1);
nipkow@2525
   145
by (rtac conjI 1);
nipkow@2525
   146
by (rtac new_tv_subst_comp_2 1);
nipkow@4033
   147
by (etac (W_var_ge RS new_tv_subst_le) 1);
paulson@3018
   148
by (assume_tac 1);
paulson@3018
   149
by (assume_tac 1);
paulson@3018
   150
by (assume_tac 1);
nipkow@1486
   151
qed_spec_mp "new_tv_W";
nipkow@1300
   152
nipkow@5118
   153
Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
berghofe@5184
   154
by (induct_tac "sch" 1);
nipkow@2525
   155
by (Asm_full_simp_tac 1);
nipkow@2525
   156
by (Asm_full_simp_tac 1);
nipkow@2525
   157
by (strip_tac 1);
nipkow@2525
   158
by (rtac exI 1);
nipkow@2525
   159
by (rtac refl 1);
nipkow@2525
   160
by (Asm_full_simp_tac 1);
nipkow@2525
   161
qed_spec_mp "free_tv_bound_typ_inst1";
nipkow@2525
   162
nipkow@2525
   163
Addsimps [free_tv_bound_typ_inst1];
nipkow@1300
   164
paulson@6141
   165
Goal "!n A S t m v. W e A n = Some (S,t,m) -->            \
nipkow@2525
   166
\         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
berghofe@5184
   167
by (induct_tac "e" 1);
nipkow@1300
   168
(* case Var n *)
wenzelm@4089
   169
by (simp_tac (simpset() addsimps
nipkow@4686
   170
    [free_tv_subst] addsplits [split_option_bind]) 1);
nipkow@2525
   171
by (strip_tac 1);
nipkow@4502
   172
by (case_tac "v : free_tv (A!nat)" 1);
nipkow@2525
   173
by (Asm_full_simp_tac 1);
nipkow@2525
   174
by (dtac free_tv_bound_typ_inst1 1);
wenzelm@4089
   175
by (simp_tac (simpset() addsimps [o_def]) 1);
nipkow@2525
   176
by (etac exE 1);
nipkow@2525
   177
by (rotate_tac 3 1);
nipkow@2525
   178
by (Asm_full_simp_tac 1);
nipkow@1300
   179
(* case Abs e *)
wenzelm@4089
   180
by (asm_full_simp_tac (simpset() addsimps
nipkow@4072
   181
    [free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1);
nipkow@1300
   182
by (strip_tac 1);
nipkow@2525
   183
by (rename_tac "S t n1 S1 t1 m v" 1);
nipkow@1300
   184
by (eres_inst_tac [("x","Suc n")] allE 1);
nipkow@2525
   185
by (eres_inst_tac [("x","FVar n # A")] allE 1);
nipkow@2525
   186
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
   187
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
   188
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@1300
   189
by (eres_inst_tac [("x","v")] allE 1);
nipkow@2525
   190
by (best_tac (HOL_cs addIs [cod_app_subst]
wenzelm@4089
   191
                     addss (simpset() addsimps [less_Suc_eq])) 1);
nipkow@1300
   192
(* case App e1 e2 *)
wenzelm@4089
   193
by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
nipkow@1300
   194
by (strip_tac 1); 
nipkow@2525
   195
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
nipkow@1300
   196
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
   197
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   198
by (eres_inst_tac [("x","S")] allE 1);
nipkow@1300
   199
by (eres_inst_tac [("x","t")] allE 1);
nipkow@2525
   200
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@2525
   201
by (eres_inst_tac [("x","n1")] allE 1);
nipkow@1300
   202
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   203
(* second case *)
nipkow@2525
   204
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@2525
   205
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   206
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   207
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@1300
   208
by (eres_inst_tac [("x","v")] allE 1);
nipkow@1300
   209
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
wenzelm@4089
   210
by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
clasohm@1465
   211
by (dtac W_var_geD 1);
clasohm@1465
   212
by (dtac 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 [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
nipkow@2525
   215
    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
nipkow@1300
   216
    less_le_trans,less_not_refl2,subsetD]
nipkow@1300
   217
  addEs [UnE] 
wenzelm@4089
   218
  addss simpset()) 1);
nipkow@1300
   219
by (Asm_full_simp_tac 1); 
clasohm@1465
   220
by (dtac (sym RS W_var_geD) 1);
clasohm@1465
   221
by (dtac (sym RS W_var_geD) 1);
nipkow@1300
   222
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
nipkow@1300
   223
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
nipkow@2525
   224
    free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
nipkow@2525
   225
    less_le_trans,subsetD]
nipkow@2525
   226
  addEs [UnE]
nipkow@5655
   227
  addss (simpset() setSolver unsafe_solver)) 1);
nipkow@2525
   228
(* LET e1 e2 *)
wenzelm@4089
   229
by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
nipkow@2525
   230
by (strip_tac 1); 
nipkow@2525
   231
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
nipkow@2525
   232
by (eres_inst_tac [("x","nat")] allE 1);
nipkow@2525
   233
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   234
by (eres_inst_tac [("x","S1")] allE 1);
nipkow@2525
   235
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   236
by (rotate_tac 1 1);
nipkow@2525
   237
by (eres_inst_tac [("x","n2")] allE 1);
nipkow@2525
   238
by (rotate_tac 4 1);
nipkow@2525
   239
by (eres_inst_tac [("x","v")] allE 1);
nipkow@2525
   240
by (mp_tac 1);
nipkow@2525
   241
by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
nipkow@2525
   242
by (mp_tac 1);
nipkow@2525
   243
by (Asm_full_simp_tac 1);
nipkow@2525
   244
by (rtac conjI 1);
wenzelm@4089
   245
by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
nipkow@2525
   246
              addDs [less_le_trans]) 1);
wenzelm@4089
   247
by (fast_tac (claset() addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
nipkow@2525
   248
              addDs [less_le_trans]) 1);
nipkow@1486
   249
qed_spec_mp "free_tv_W"; 
nipkow@1300
   250
nipkow@5118
   251
Goal "(!x. x : A --> x ~: B) ==> A Int B = {}";
nipkow@2525
   252
by (Fast_tac 1);
narasche@2625
   253
val weaken_A_Int_B_eq_empty = result();
nipkow@2525
   254
nipkow@5118
   255
Goal "x ~: A | x : B ==> x ~: A - B";
nipkow@2525
   256
by (Fast_tac 1);
narasche@2625
   257
val weaken_not_elem_A_minus_B = result();
nipkow@2525
   258
nipkow@2525
   259
(* correctness of W with respect to has_type *)
paulson@6141
   260
Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
berghofe@5184
   261
by (induct_tac "e" 1);
nipkow@2525
   262
(* case Var n *)
nipkow@4686
   263
by (Asm_full_simp_tac 1);
nipkow@2525
   264
by (strip_tac 1);
nipkow@2525
   265
by (rtac has_type.VarI 1);
nipkow@2525
   266
by (Simp_tac 1);
wenzelm@4089
   267
by (simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
nipkow@2525
   268
by (rtac exI 1);
nipkow@2525
   269
by (rtac refl 1);
nipkow@2525
   270
(* case Abs e *)
wenzelm@4089
   271
by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
nipkow@4072
   272
                        addsplits [split_option_bind]) 1);
nipkow@2525
   273
by (strip_tac 1);
nipkow@2525
   274
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
nipkow@2525
   275
by (Asm_full_simp_tac 1);
nipkow@2525
   276
by (rtac has_type.AbsI 1);
nipkow@2525
   277
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
paulson@3018
   278
by (dtac sym 1);
nipkow@2525
   279
by (REPEAT (etac allE 1));
nipkow@2525
   280
by (etac impE 1);
nipkow@2525
   281
by (mp_tac 2);
nipkow@2525
   282
by (Asm_simp_tac 1);
paulson@3018
   283
by (assume_tac 1);
nipkow@2525
   284
(* case App e1 e2 *)
wenzelm@4089
   285
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@2525
   286
by (strip_tac 1);
nipkow@2525
   287
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
nipkow@2525
   288
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
nipkow@2525
   289
by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
nipkow@2525
   290
by (rtac (app_subst_Fun RS subst) 1);
nipkow@2525
   291
by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
nipkow@2525
   292
by (Asm_full_simp_tac 1);
nipkow@2525
   293
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   294
by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
wenzelm@4089
   295
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
wenzelm@4089
   296
by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
nipkow@2525
   297
by (rtac (has_type_cl_sub RS spec) 1);
nipkow@2525
   298
by (forward_tac [new_tv_W] 1);
paulson@3018
   299
by (assume_tac 1);
nipkow@2525
   300
by (dtac conjunct1 1);
nipkow@2525
   301
by (dtac conjunct1 1);
nipkow@2525
   302
by (forward_tac [new_tv_subst_scheme_list] 1);
nipkow@2525
   303
by (rtac new_scheme_list_le 1);
nipkow@2525
   304
by (rtac W_var_ge 1);
paulson@3018
   305
by (assume_tac 1);
paulson@3018
   306
by (assume_tac 1);
nipkow@2525
   307
by (etac thin_rl 1);
nipkow@2525
   308
by (REPEAT (etac allE 1));
paulson@3018
   309
by (dtac sym 1);
paulson@3018
   310
by (dtac sym 1);
nipkow@2525
   311
by (etac thin_rl 1);
nipkow@2525
   312
by (etac thin_rl 1);
nipkow@2525
   313
by (mp_tac 1);
nipkow@2525
   314
by (mp_tac 1);
paulson@3018
   315
by (assume_tac 1);
nipkow@2525
   316
(* case Let e1 e2 *)
wenzelm@4089
   317
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@2525
   318
by (strip_tac 1);
nipkow@2525
   319
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
nipkow@2525
   320
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
wenzelm@4089
   321
by (simp_tac (simpset() addsimps [o_def]) 1);
nipkow@2525
   322
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   323
by (rtac (has_type_cl_sub RS spec) 1);
nipkow@2525
   324
by (dres_inst_tac [("x","A")] spec 1);
nipkow@2525
   325
by (dres_inst_tac [("x","S1")] spec 1);
nipkow@2525
   326
by (dres_inst_tac [("x","t1")] spec 1);
nipkow@2525
   327
by (dres_inst_tac [("x","m2")] spec 1);
nipkow@2525
   328
by (rotate_tac 4 1);
nipkow@2525
   329
by (dres_inst_tac [("x","m1")] spec 1);
nipkow@2525
   330
by (mp_tac 1);
wenzelm@4089
   331
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
wenzelm@4089
   332
by (simp_tac (simpset() addsimps [o_def]) 1);
nipkow@2525
   333
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2525
   334
by (rtac (gen_subst_commutes RS sym RS subst) 1);
nipkow@2525
   335
by (rtac (app_subst_Cons RS subst) 2);
nipkow@2525
   336
by (etac thin_rl 2);
nipkow@2525
   337
by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
nipkow@2525
   338
by (dres_inst_tac [("x","S2")] spec 2);
nipkow@2525
   339
by (dres_inst_tac [("x","t")] spec 2);
nipkow@2525
   340
by (dres_inst_tac [("x","n2")] spec 2);
nipkow@2525
   341
by (dres_inst_tac [("x","m2")] spec 2);
nipkow@2525
   342
by (forward_tac [new_tv_W] 2);
paulson@3018
   343
by (assume_tac 2);
nipkow@2525
   344
by (dtac conjunct1 2);
nipkow@2525
   345
by (dtac conjunct1 2);
nipkow@2525
   346
by (forward_tac [new_tv_subst_scheme_list] 2);
nipkow@2525
   347
by (rtac new_scheme_list_le 2);
nipkow@2525
   348
by (rtac W_var_ge 2);
paulson@3018
   349
by (assume_tac 2);
paulson@3018
   350
by (assume_tac 2);
nipkow@2525
   351
by (etac impE 2);
nipkow@2525
   352
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
nipkow@2525
   353
by (Simp_tac 2);
nipkow@2525
   354
by (Fast_tac 2);
paulson@3018
   355
by (assume_tac 2);
nipkow@2525
   356
by (Asm_full_simp_tac 2);
nipkow@2525
   357
by (rtac weaken_A_Int_B_eq_empty 1);
nipkow@2525
   358
by (rtac allI 1);
nipkow@2525
   359
by (strip_tac 1);
nipkow@2525
   360
by (rtac weaken_not_elem_A_minus_B 1);
nipkow@2525
   361
by (case_tac "x < m2" 1);
nipkow@2525
   362
by (rtac disjI2 1);
nipkow@2525
   363
by (rtac (free_tv_gen_cons RS subst) 1);
nipkow@2525
   364
by (rtac free_tv_W 1);
paulson@3018
   365
by (assume_tac 1);
nipkow@2525
   366
by (Asm_full_simp_tac 1);
paulson@3018
   367
by (assume_tac 1);
nipkow@2525
   368
by (rtac disjI1 1);
nipkow@2525
   369
by (dtac new_tv_W 1);
paulson@3018
   370
by (assume_tac 1);
nipkow@2525
   371
by (dtac conjunct2 1);
nipkow@2525
   372
by (dtac conjunct2 1);
nipkow@2525
   373
by (rtac new_tv_not_free_tv 1);
nipkow@2525
   374
by (rtac new_tv_le 1);
paulson@3018
   375
by (assume_tac 2);
wenzelm@4089
   376
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
nipkow@2525
   377
qed_spec_mp "W_correct_lemma";
nipkow@2525
   378
nipkow@1300
   379
(* Completeness of W w.r.t. has_type *)
paulson@6141
   380
Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
nipkow@2525
   381
\             (? S t. (? m. W e A n = Some (S,t,m)) &  \
nipkow@2525
   382
\                     (? R. $S' A = $R ($S A) & t' = $R t))";
berghofe@5184
   383
by (induct_tac "e" 1);
nipkow@1300
   384
(* case Var n *)
nipkow@1300
   385
by (strip_tac 1);
nipkow@4686
   386
by (simp_tac (simpset() addcongs [conj_cong]) 1);
nipkow@1300
   387
by (eresolve_tac has_type_casesE 1); 
wenzelm@4089
   388
by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
nipkow@2525
   389
by (etac exE 1);
nipkow@2525
   390
by (hyp_subst_tac 1);
nipkow@2525
   391
by (rename_tac "S" 1);
nipkow@2525
   392
by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
nipkow@2525
   393
by (rtac conjI 1);
nipkow@1300
   394
by (Asm_simp_tac 1);
wenzelm@4089
   395
by (asm_simp_tac (simpset() addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
nipkow@2525
   396
                           delsimps [bound_typ_inst_composed_subst]) 1);
paulson@2749
   397
(** LEVEL 12 **)
nipkow@1300
   398
(* case Abs e *)
nipkow@1300
   399
by (strip_tac 1);
nipkow@1300
   400
by (eresolve_tac has_type_casesE 1);
wenzelm@3842
   401
by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1);
nipkow@2525
   402
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
nipkow@1300
   403
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   404
by (eres_inst_tac [("x","Suc n")] allE 1);
paulson@2749
   405
by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
wenzelm@4089
   406
                  addss (simpset() addcongs [conj_cong] 
nipkow@4072
   407
                                addsplits [split_option_bind])) 1);
paulson@2749
   408
(** LEVEL 19 **)
nipkow@1300
   409
nipkow@1300
   410
(* case App e1 e2 *)
nipkow@1300
   411
by (strip_tac 1);
nipkow@1300
   412
by (eresolve_tac has_type_casesE 1);
nipkow@2525
   413
by (eres_inst_tac [("x","S'")] allE 1);
nipkow@2525
   414
by (eres_inst_tac [("x","A")] allE 1);
nipkow@1400
   415
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
nipkow@1300
   416
by (eres_inst_tac [("x","n")] allE 1);
nipkow@1300
   417
by (safe_tac HOL_cs);
paulson@2749
   418
(** LEVEL 26 **)
nipkow@2525
   419
by (eres_inst_tac [("x","R")] allE 1);
nipkow@2525
   420
by (eres_inst_tac [("x","$ S A")] allE 1);
nipkow@1300
   421
by (eres_inst_tac [("x","t2")] allE 1);
nipkow@1300
   422
by (eres_inst_tac [("x","m")] allE 1);
nipkow@1300
   423
by (Asm_full_simp_tac 1);
nipkow@1300
   424
by (safe_tac HOL_cs);
nipkow@1300
   425
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
nipkow@2525
   426
        conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
paulson@2779
   427
(** LEVEL 35 **)
nipkow@1300
   428
by (subgoal_tac
wenzelm@3842
   429
  "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
nipkow@2525
   430
\        else Ra x)) ($ Sa t) = \
wenzelm@3842
   431
\  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
nipkow@2525
   432
\        else Ra x)) (ta -> (TVar ma))" 1);
nipkow@1300
   433
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
nipkow@2525
   434
\   (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
nipkow@2525
   435
    ("s","($ Ra ta) -> t'")] ssubst 2);
wenzelm@4089
   436
by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2);
clasohm@1465
   437
by (rtac eq_free_eq_subst_te 2);  
nipkow@1300
   438
by (strip_tac 2);
nipkow@1300
   439
by (subgoal_tac "na ~=ma" 2);
paulson@2749
   440
by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
nipkow@2525
   441
    new_tv_not_free_tv,new_tv_le]) 3);
nipkow@2525
   442
by (case_tac "na:free_tv Sa" 2);
nipkow@2525
   443
(* n1 ~: free_tv S1 *)
nipkow@2525
   444
by (forward_tac [not_free_impl_id] 3);
nipkow@4686
   445
by (Asm_simp_tac 3);
nipkow@2525
   446
(* na : free_tv Sa *)
nipkow@2525
   447
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
nipkow@2525
   448
by (dtac eq_subst_scheme_list_eq_free 2);
nipkow@1300
   449
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@1300
   450
by (Asm_simp_tac 2); 
nipkow@2525
   451
by (case_tac "na:dom Sa" 2);
nipkow@2525
   452
(* na ~: dom Sa *)
nipkow@4686
   453
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
nipkow@2525
   454
(* na : dom Sa *)
clasohm@1465
   455
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   456
by (strip_tac 2);
nipkow@1300
   457
by (subgoal_tac "nb ~= ma" 2);
nipkow@1300
   458
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   459
by (etac conjE 3);
nipkow@2525
   460
by (dtac new_tv_subst_scheme_list 3);
nipkow@2525
   461
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
nipkow@1300
   462
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
wenzelm@4089
   463
    (simpset() addsimps [cod_def,free_tv_subst])) 3);
nipkow@4686
   464
by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
nipkow@1300
   465
by (Simp_tac 2);  
clasohm@1465
   466
by (rtac eq_free_eq_subst_te 2);
nipkow@1300
   467
by (strip_tac 2 );
nipkow@1300
   468
by (subgoal_tac "na ~= ma" 2);
nipkow@1300
   469
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
clasohm@1465
   470
by (etac conjE 3);
clasohm@1465
   471
by (dtac (sym RS W_var_geD) 3);
nipkow@2525
   472
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
nipkow@2525
   473
by (case_tac "na: free_tv t - free_tv Sa" 2);
nipkow@2525
   474
(* case na ~: free_tv t - free_tv Sa *)
nipkow@4686
   475
by (Asm_full_simp_tac 3);
nipkow@2793
   476
by (Fast_tac 3);
nipkow@2525
   477
(* case na : free_tv t - free_tv Sa *)
nipkow@4686
   478
by (Asm_full_simp_tac 2);
nipkow@2525
   479
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
nipkow@2525
   480
by (dtac eq_subst_scheme_list_eq_free 2);
nipkow@1300
   481
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
nipkow@2793
   482
(** LEVEL 75 **)
wenzelm@4089
   483
by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2);
wenzelm@4089
   484
by (asm_simp_tac (simpset() addsplits [split_option_bind]) 1); 
nipkow@1300
   485
by (safe_tac HOL_cs );
nipkow@2525
   486
by (dtac mgu_Some 1);
wenzelm@4089
   487
by ( fast_tac (HOL_cs addss simpset()) 1);
nipkow@2793
   488
(** LEVEL 80 *)
nipkow@1300
   489
by ((dtac mgu_mg 1) THEN (atac 1));
clasohm@1465
   490
by (etac exE 1);
nipkow@2525
   491
by (res_inst_tac [("x","Rb")] exI 1);
clasohm@1465
   492
by (rtac conjI 1);
nipkow@1300
   493
by (dres_inst_tac [("x","ma")] fun_cong 2);
wenzelm@4089
   494
by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2);
wenzelm@4089
   495
by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1);
wenzelm@4089
   496
by (simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym]) 1);
nipkow@2793
   497
by (res_inst_tac [("A2","($ Sa ($ S A))")]
nipkow@2793
   498
       ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
wenzelm@4089
   499
by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1);
nipkow@2525
   500
by (rtac eq_free_eq_subst_scheme_list 1);
paulson@3018
   501
by ( safe_tac HOL_cs );
nipkow@1300
   502
by (subgoal_tac "ma ~= na" 1);
nipkow@1300
   503
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
clasohm@1465
   504
by (etac conjE 2);
nipkow@2525
   505
by (dtac new_tv_subst_scheme_list 2);
nipkow@2525
   506
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
nipkow@2793
   507
by (forw_inst_tac [("n","m")] new_tv_W 2  THEN  atac 2);
clasohm@1465
   508
by (etac conjE 2);
nipkow@2525
   509
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
nipkow@2793
   510
by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD,
nipkow@1300
   511
    new_tv_not_free_tv]) 2);
nipkow@2525
   512
by (case_tac "na: free_tv t - free_tv Sa" 1);
nipkow@2525
   513
(* case na ~: free_tv t - free_tv Sa *)
nipkow@4686
   514
by (Asm_full_simp_tac 2);
nipkow@2525
   515
(* case na : free_tv t - free_tv Sa *)
nipkow@4686
   516
by (Asm_full_simp_tac 1);
nipkow@2525
   517
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
nipkow@2525
   518
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
wenzelm@4089
   519
    eq_subst_scheme_list_eq_free] addss ((simpset() addsimps 
nipkow@2525
   520
    [free_tv_subst,dom_def]))) 1);
paulson@2083
   521
by (Fast_tac 1);
nipkow@2525
   522
(* case Let e1 e2 *)
nipkow@2525
   523
by (eresolve_tac has_type_casesE 1);
nipkow@2525
   524
by (eres_inst_tac [("x","S'")] allE 1);
nipkow@2525
   525
by (eres_inst_tac [("x","A")] allE 1);
nipkow@2525
   526
by (eres_inst_tac [("x","t1")] allE 1);
nipkow@2525
   527
by (eres_inst_tac [("x","n")] allE 1);
nipkow@2525
   528
by (mp_tac 1);
nipkow@2525
   529
by (mp_tac 1);
nipkow@2525
   530
by (safe_tac HOL_cs);
nipkow@2525
   531
by (Asm_simp_tac 1); 
nipkow@2525
   532
by (eres_inst_tac [("x","R")] allE 1);
nipkow@2525
   533
by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
nipkow@2525
   534
by (eres_inst_tac [("x","t'")] allE 1);
nipkow@2525
   535
by (eres_inst_tac [("x","m")] allE 1);
nipkow@2525
   536
by (Asm_full_simp_tac 1);
nipkow@2525
   537
by (dtac mp 1);
nipkow@2525
   538
by (rtac has_type_le_env 1);
paulson@3018
   539
by (assume_tac 1);
nipkow@2525
   540
by (Simp_tac 1);
nipkow@2525
   541
by (rtac gen_bound_typ_instance 1);
nipkow@2525
   542
by (dtac mp 1);
nipkow@2525
   543
by (forward_tac [new_tv_compatible_W] 1);
nipkow@2525
   544
by (rtac sym 1);
paulson@3018
   545
by (assume_tac 1);
wenzelm@4089
   546
by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
nipkow@2525
   547
by (safe_tac HOL_cs);
nipkow@2525
   548
by (Asm_full_simp_tac 1);
nipkow@2525
   549
by (res_inst_tac [("x","Ra")] exI 1);
wenzelm@4089
   550
by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
nipkow@1525
   551
qed_spec_mp "W_complete_lemma";
nipkow@1525
   552
paulson@6141
   553
Goal "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
nipkow@2525
   554
\                                 (? R. t' = $ R t))";
paulson@3018
   555
by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
nipkow@1525
   556
                W_complete_lemma 1);
paulson@3018
   557
by (ALLGOALS Asm_full_simp_tac);
nipkow@1525
   558
qed "W_complete";