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