src/HOL/MiniML/Instance.ML
author nipkow
Fri Jul 03 10:37:04 1998 +0200 (1998-07-03)
changeset 5118 6b995dad8a9d
parent 5069 3ea049f7979d
child 5184 9b8547a9496a
permissions -rw-r--r--
Removed leading !! in goals.
nipkow@2525
     1
(* Title:     HOL/MiniML/Instance.ML
nipkow@2525
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@2525
     5
*)
nipkow@2525
     6
nipkow@2525
     7
(* lemmatas for instatiation *)
nipkow@2525
     8
nipkow@2525
     9
nipkow@2525
    10
(* lemmatas for bound_typ_inst *)
nipkow@2525
    11
wenzelm@5069
    12
Goal "bound_typ_inst S (mk_scheme t) = t";
nipkow@2525
    13
by (typ.induct_tac "t" 1);
nipkow@2525
    14
by (ALLGOALS Asm_simp_tac);
nipkow@2525
    15
qed "bound_typ_inst_mk_scheme";
nipkow@2525
    16
nipkow@2525
    17
Addsimps [bound_typ_inst_mk_scheme];
narasche@2625
    18
nipkow@5118
    19
Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
nipkow@2525
    20
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
    21
by (ALLGOALS Asm_full_simp_tac);
nipkow@2525
    22
qed "bound_typ_inst_composed_subst";
nipkow@2525
    23
nipkow@2525
    24
Addsimps [bound_typ_inst_composed_subst];
nipkow@2525
    25
nipkow@5118
    26
Goal "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'";
nipkow@2525
    27
by (Asm_full_simp_tac 1);
nipkow@2525
    28
qed "bound_typ_inst_eq";
nipkow@2525
    29
nipkow@2525
    30
narasche@2625
    31
nipkow@2525
    32
(* lemmatas for bound_scheme_inst *)
nipkow@2525
    33
nipkow@5118
    34
Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
nipkow@2525
    35
by (typ.induct_tac "t" 1);
nipkow@2525
    36
by (Simp_tac 1);
nipkow@2525
    37
by (Asm_simp_tac 1);
nipkow@2525
    38
qed "bound_scheme_inst_mk_scheme";
nipkow@2525
    39
nipkow@2525
    40
Addsimps [bound_scheme_inst_mk_scheme];
nipkow@2525
    41
nipkow@5118
    42
Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
nipkow@2525
    43
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
    44
by (Simp_tac 1);
nipkow@2525
    45
by (Simp_tac 1);
nipkow@2525
    46
by (Asm_simp_tac 1);
nipkow@2525
    47
qed "substitution_lemma";
nipkow@2525
    48
wenzelm@5069
    49
Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
nipkow@2525
    50
\         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
nipkow@2525
    51
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
    52
by (Simp_tac 1);
paulson@4153
    53
by Safe_tac;
nipkow@2525
    54
by (rtac exI 1);
nipkow@2525
    55
by (rtac ballI 1);
nipkow@2525
    56
by (rtac sym 1);
nipkow@2525
    57
by (Asm_full_simp_tac 1);
nipkow@2525
    58
by (Asm_full_simp_tac 1);
nipkow@2525
    59
by (dtac mk_scheme_Fun 1);
nipkow@2525
    60
by (REPEAT (etac exE 1));
nipkow@2525
    61
by (etac conjE 1);
nipkow@2525
    62
by (dtac sym 1);
nipkow@2525
    63
by (dtac sym 1);
nipkow@2525
    64
by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
paulson@4153
    65
by Safe_tac;
nipkow@2525
    66
by (rename_tac "S1 S2" 1);
nipkow@2525
    67
by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
paulson@4153
    68
by Safe_tac;
nipkow@4686
    69
by (Asm_simp_tac 1);
nipkow@4686
    70
by (Asm_simp_tac 1);
nipkow@2525
    71
by (strip_tac 1);
nipkow@2525
    72
by (dres_inst_tac [("x","x")] bspec 1);
paulson@3018
    73
by (assume_tac 1);
nipkow@2525
    74
by (dres_inst_tac [("x","x")] bspec 1);
nipkow@2525
    75
by (Asm_simp_tac 1);
nipkow@2525
    76
by (Asm_full_simp_tac 1);
nipkow@2525
    77
qed_spec_mp "bound_scheme_inst_type";
nipkow@2525
    78
nipkow@2525
    79
nipkow@5118
    80
(* lemmas for subst_to_scheme *)
nipkow@2525
    81
nipkow@5118
    82
Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
nipkow@2525
    83
\                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
nipkow@2525
    84
by (type_scheme.induct_tac "sch" 1);
nipkow@4686
    85
by (simp_tac (simpset() addsimps [leD]) 1);
nipkow@4686
    86
by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
nipkow@2525
    87
by (Asm_simp_tac 1);
nipkow@2525
    88
qed_spec_mp "subst_to_scheme_inverse";
nipkow@2525
    89
nipkow@5118
    90
Goal "t = t' ==> \
nipkow@5118
    91
\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \
nipkow@5118
    92
\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'";
nipkow@2525
    93
by (Fast_tac 1);
nipkow@2525
    94
val aux = result ();
nipkow@2525
    95
wenzelm@5069
    96
Goal "new_tv n sch --> \
nipkow@5118
    97
\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
nipkow@5118
    98
\      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
nipkow@2525
    99
by (type_scheme.induct_tac "sch" 1);
nipkow@4686
   100
by (simp_tac (simpset() addsimps [leD]) 1);
nipkow@2525
   101
by (Asm_simp_tac 1);
nipkow@4686
   102
by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
nipkow@2525
   103
val aux2 = result () RS mp;
nipkow@2525
   104
nipkow@2525
   105
nipkow@2525
   106
(* lemmata for <= *)
nipkow@2525
   107
wenzelm@5069
   108
Goalw [le_type_scheme_def,is_bound_typ_instance]
nipkow@5118
   109
  "!!(sch::type_scheme) sch'. \
nipkow@5118
   110
\  (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
nipkow@2525
   111
by (rtac iffI 1);
nipkow@2525
   112
by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
nipkow@2525
   113
by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
nipkow@2525
   114
by (dtac make_one_new_out_of_two 1);
paulson@3018
   115
by (assume_tac 1);
nipkow@2525
   116
by (thin_tac "? n. new_tv n sch'" 1); 
nipkow@2525
   117
by (etac exE 1);
nipkow@2525
   118
by (etac allE 1);
nipkow@2525
   119
by (dtac mp 1);
nipkow@2525
   120
by (res_inst_tac [("x","(%k. TVar (k + n))")] exI 1);
nipkow@2525
   121
by (rtac refl 1);
nipkow@2525
   122
by (etac exE 1);
nipkow@2525
   123
by (REPEAT (etac conjE 1));
nipkow@2525
   124
by (dres_inst_tac [("n","n")] aux 1);
wenzelm@4089
   125
by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
nipkow@2525
   126
by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
wenzelm@4089
   127
by (asm_simp_tac (simpset() addsimps [aux2]) 1);
paulson@4153
   128
by Safe_tac;
nipkow@2525
   129
by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
nipkow@2525
   130
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   131
by (Simp_tac 1);
nipkow@2525
   132
by (Simp_tac 1);
nipkow@2525
   133
by (Asm_simp_tac 1);
nipkow@2525
   134
qed "le_type_scheme_def2";
nipkow@2525
   135
wenzelm@5069
   136
Goalw [is_bound_typ_instance] "(mk_scheme t) <= sch = t <| sch";
wenzelm@4089
   137
by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); 
nipkow@2525
   138
by (rtac iffI 1); 
nipkow@2525
   139
by (etac exE 1); 
nipkow@2525
   140
by (forward_tac [bound_scheme_inst_type] 1);
nipkow@2525
   141
by (etac exE 1);
nipkow@2525
   142
by (rtac exI 1);
nipkow@2525
   143
by (rtac mk_scheme_injective 1); 
nipkow@2525
   144
by (Asm_full_simp_tac 1);
nipkow@2525
   145
by (rotate_tac 1 1);
nipkow@2525
   146
by (rtac mp 1);
paulson@3018
   147
by (assume_tac 2);
nipkow@2525
   148
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   149
by (Simp_tac 1);
nipkow@2525
   150
by (Asm_full_simp_tac 1);
nipkow@2525
   151
by (Fast_tac 1);
nipkow@2525
   152
by (strip_tac 1);
nipkow@2525
   153
by (Asm_full_simp_tac 1);
nipkow@2525
   154
by (etac exE 1);
nipkow@2525
   155
by (Asm_full_simp_tac 1);
nipkow@2525
   156
by (rtac exI 1);
nipkow@2525
   157
by (type_scheme.induct_tac "sch" 1);
nipkow@2525
   158
by (Simp_tac 1);
nipkow@2525
   159
by (Simp_tac 1);
nipkow@2525
   160
by (Asm_full_simp_tac 1);
nipkow@2525
   161
qed_spec_mp "le_type_eq_is_bound_typ_instance";
nipkow@2525
   162
wenzelm@5069
   163
Goalw [le_env_def]
nipkow@2525
   164
  "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
paulson@3018
   165
by (Simp_tac 1);
paulson@3018
   166
by (rtac iffI 1);
paulson@4153
   167
 by (SELECT_GOAL Safe_tac 1);
paulson@3018
   168
  by (eres_inst_tac [("x","0")] allE 1);
paulson@3018
   169
  by (Asm_full_simp_tac 1);
paulson@3018
   170
 by (eres_inst_tac [("x","Suc i")] allE 1);
paulson@3018
   171
 by (Asm_full_simp_tac 1);
paulson@3018
   172
by (rtac conjI 1);
paulson@3018
   173
 by (Fast_tac 1);
paulson@3018
   174
by (rtac allI 1);
paulson@3018
   175
by (nat_ind_tac "i" 1);
paulson@3018
   176
by (ALLGOALS Asm_simp_tac);
nipkow@2525
   177
qed "le_env_Cons";
nipkow@2525
   178
AddIffs [le_env_Cons];
nipkow@2525
   179
nipkow@5118
   180
Goalw [is_bound_typ_instance]"t <| sch ==> $S t <| $S sch";
nipkow@2525
   181
by (etac exE 1);
nipkow@2525
   182
by (rename_tac "SA" 1);
nipkow@2525
   183
by (hyp_subst_tac 1);
nipkow@2525
   184
by (res_inst_tac [("x","$S o SA")] exI 1);
nipkow@2525
   185
by (Simp_tac 1);
nipkow@2525
   186
qed "is_bound_typ_instance_closed_subst";
nipkow@2525
   187
wenzelm@5069
   188
Goal "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch";
wenzelm@4089
   189
by (asm_full_simp_tac (simpset() addsimps [le_type_scheme_def2]) 1);
nipkow@2525
   190
by (etac exE 1);
wenzelm@4089
   191
by (asm_full_simp_tac (simpset() addsimps [substitution_lemma]) 1);
nipkow@2525
   192
by (Fast_tac 1);
nipkow@2525
   193
qed "S_compatible_le_scheme";
nipkow@2525
   194
nipkow@5118
   195
Goalw [le_env_def,app_subst_list]
nipkow@5118
   196
 "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
wenzelm@4089
   197
by (simp_tac (simpset() addcongs [conj_cong]) 1);
wenzelm@4089
   198
by (fast_tac (claset() addSIs [S_compatible_le_scheme]) 1);
nipkow@2525
   199
qed "S_compatible_le_scheme_lists";
nipkow@2525
   200
nipkow@5118
   201
Goalw [le_type_scheme_def] "[| t <| sch; sch <= sch' |] ==> t <| sch'";
paulson@3018
   202
by (Fast_tac 1);
nipkow@2525
   203
qed "bound_typ_instance_trans";
nipkow@2525
   204
wenzelm@5069
   205
Goalw [le_type_scheme_def] "sch <= (sch::type_scheme)";
paulson@3018
   206
by (Fast_tac 1);
nipkow@2525
   207
qed "le_type_scheme_refl";
nipkow@2525
   208
AddIffs [le_type_scheme_refl];
nipkow@2525
   209
wenzelm@5069
   210
Goalw [le_env_def] "A <= (A::type_scheme list)";
paulson@3018
   211
by (Fast_tac 1);
nipkow@2525
   212
qed "le_env_refl";
nipkow@2525
   213
AddIffs [le_env_refl];
nipkow@2525
   214
wenzelm@5069
   215
Goalw [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
paulson@3018
   216
by (strip_tac 1);
wenzelm@3842
   217
by (res_inst_tac [("x","%a. t")]exI 1);
paulson@3018
   218
by (Simp_tac 1);
nipkow@2525
   219
qed "bound_typ_instance_BVar";
nipkow@2525
   220
AddIffs [bound_typ_instance_BVar];
nipkow@2525
   221
nipkow@5118
   222
Goalw [le_type_scheme_def,is_bound_typ_instance]
nipkow@5118
   223
 "(sch <= FVar n) = (sch = FVar n)";
paulson@3018
   224
by (type_scheme.induct_tac "sch" 1);
paulson@3018
   225
  by (Simp_tac 1);
paulson@3018
   226
 by (Simp_tac 1);
paulson@3018
   227
 by (Fast_tac 1);
paulson@3018
   228
by (Asm_full_simp_tac 1);
paulson@3018
   229
by (Fast_tac 1);
nipkow@2525
   230
qed "le_FVar";
nipkow@2525
   231
Addsimps [le_FVar];
nipkow@2525
   232
wenzelm@5069
   233
Goalw [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
paulson@3018
   234
by (Simp_tac 1);
nipkow@2525
   235
qed "not_FVar_le_Fun";
nipkow@2525
   236
AddIffs [not_FVar_le_Fun];
nipkow@2525
   237
wenzelm@5069
   238
Goalw [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
paulson@3018
   239
by (Simp_tac 1);
paulson@3018
   240
by (res_inst_tac [("x","TVar n")] exI 1);
paulson@3018
   241
by (Simp_tac 1);
paulson@3018
   242
by (Fast_tac 1);
nipkow@2525
   243
qed "not_BVar_le_Fun";
nipkow@2525
   244
AddIffs [not_BVar_le_Fun];
nipkow@2525
   245
wenzelm@5069
   246
Goalw [le_type_scheme_def,is_bound_typ_instance]
nipkow@5118
   247
  "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
wenzelm@4089
   248
by (fast_tac (claset() addss simpset()) 1);
nipkow@2525
   249
qed "Fun_le_FunD";
nipkow@2525
   250
wenzelm@5069
   251
Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
nipkow@2525
   252
by (type_scheme.induct_tac "sch'" 1);
nipkow@2525
   253
by (Asm_simp_tac 1);
nipkow@2525
   254
by (Asm_simp_tac 1);
nipkow@2525
   255
by (Fast_tac 1);
nipkow@2525
   256
qed_spec_mp "scheme_le_Fun";
nipkow@2525
   257
wenzelm@5069
   258
Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
paulson@3018
   259
by (type_scheme.induct_tac "sch" 1);
paulson@3018
   260
  by (rtac allI 1);
paulson@3018
   261
  by (type_scheme.induct_tac "sch'" 1);
paulson@3018
   262
    by (Simp_tac 1);
paulson@3018
   263
   by (Simp_tac 1);
paulson@3018
   264
  by (Simp_tac 1);
paulson@3018
   265
 by (rtac allI 1);
paulson@3018
   266
 by (type_scheme.induct_tac "sch'" 1);
paulson@3018
   267
   by (Simp_tac 1);
paulson@3018
   268
  by (Simp_tac 1);
paulson@3018
   269
 by (Simp_tac 1);
paulson@3018
   270
by (rtac allI 1);
paulson@3018
   271
by (type_scheme.induct_tac "sch'" 1);
paulson@3018
   272
  by (Simp_tac 1);
paulson@3018
   273
 by (Simp_tac 1);
paulson@3018
   274
by (Asm_full_simp_tac 1);
paulson@3018
   275
by (strip_tac 1);
paulson@3018
   276
by (dtac Fun_le_FunD 1);
paulson@3018
   277
by (Fast_tac 1);
nipkow@2525
   278
qed_spec_mp "le_type_scheme_free_tv";
nipkow@2525
   279
wenzelm@5069
   280
Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
paulson@3018
   281
by (list.induct_tac "B" 1);
paulson@3018
   282
 by (Simp_tac 1);
paulson@3018
   283
by (rtac allI 1);
paulson@3018
   284
by (list.induct_tac "A" 1);
wenzelm@4089
   285
 by (simp_tac (simpset() addsimps [le_env_def]) 1);
paulson@3018
   286
by (Simp_tac 1);
wenzelm@4089
   287
by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
nipkow@2525
   288
qed_spec_mp "le_env_free_tv";