src/HOL/MiniML/Instance.ML
changeset 5184 9b8547a9496a
parent 5118 6b995dad8a9d
child 5350 165b9c212caf
equal deleted inserted replaced
5183:89f162de39cf 5184:9b8547a9496a
     8 
     8 
     9 
     9 
    10 (* lemmatas for bound_typ_inst *)
    10 (* lemmatas for bound_typ_inst *)
    11 
    11 
    12 Goal "bound_typ_inst S (mk_scheme t) = t";
    12 Goal "bound_typ_inst S (mk_scheme t) = t";
    13 by (typ.induct_tac "t" 1);
    13 by (induct_tac "t" 1);
    14 by (ALLGOALS Asm_simp_tac);
    14 by (ALLGOALS Asm_simp_tac);
    15 qed "bound_typ_inst_mk_scheme";
    15 qed "bound_typ_inst_mk_scheme";
    16 
    16 
    17 Addsimps [bound_typ_inst_mk_scheme];
    17 Addsimps [bound_typ_inst_mk_scheme];
    18 
    18 
    19 Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
    19 Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
    20 by (type_scheme.induct_tac "sch" 1);
    20 by (induct_tac "sch" 1);
    21 by (ALLGOALS Asm_full_simp_tac);
    21 by (ALLGOALS Asm_full_simp_tac);
    22 qed "bound_typ_inst_composed_subst";
    22 qed "bound_typ_inst_composed_subst";
    23 
    23 
    24 Addsimps [bound_typ_inst_composed_subst];
    24 Addsimps [bound_typ_inst_composed_subst];
    25 
    25 
    30 
    30 
    31 
    31 
    32 (* lemmatas for bound_scheme_inst *)
    32 (* lemmatas for bound_scheme_inst *)
    33 
    33 
    34 Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
    34 Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
    35 by (typ.induct_tac "t" 1);
    35 by (induct_tac "t" 1);
    36 by (Simp_tac 1);
    36 by (Simp_tac 1);
    37 by (Asm_simp_tac 1);
    37 by (Asm_simp_tac 1);
    38 qed "bound_scheme_inst_mk_scheme";
    38 qed "bound_scheme_inst_mk_scheme";
    39 
    39 
    40 Addsimps [bound_scheme_inst_mk_scheme];
    40 Addsimps [bound_scheme_inst_mk_scheme];
    41 
    41 
    42 Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
    42 Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
    43 by (type_scheme.induct_tac "sch" 1);
    43 by (induct_tac "sch" 1);
    44 by (Simp_tac 1);
    44 by (Simp_tac 1);
    45 by (Simp_tac 1);
    45 by (Simp_tac 1);
    46 by (Asm_simp_tac 1);
    46 by (Asm_simp_tac 1);
    47 qed "substitution_lemma";
    47 qed "substitution_lemma";
    48 
    48 
    49 Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
    49 Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
    50 \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
    50 \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
    51 by (type_scheme.induct_tac "sch" 1);
    51 by (induct_tac "sch" 1);
    52 by (Simp_tac 1);
    52 by (Simp_tac 1);
    53 by Safe_tac;
    53 by Safe_tac;
    54 by (rtac exI 1);
    54 by (rtac exI 1);
    55 by (rtac ballI 1);
    55 by (rtac ballI 1);
    56 by (rtac sym 1);
    56 by (rtac sym 1);
    79 
    79 
    80 (* lemmas for subst_to_scheme *)
    80 (* lemmas for subst_to_scheme *)
    81 
    81 
    82 Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
    82 Goal "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";
    83 \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
    84 by (type_scheme.induct_tac "sch" 1);
    84 by (induct_tac "sch" 1);
    85 by (simp_tac (simpset() addsimps [leD]) 1);
    85 by (simp_tac (simpset() addsimps [leD]) 1);
    86 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
    86 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
    87 by (Asm_simp_tac 1);
    87 by (Asm_simp_tac 1);
    88 qed_spec_mp "subst_to_scheme_inverse";
    88 qed_spec_mp "subst_to_scheme_inverse";
    89 
    89 
    94 val aux = result ();
    94 val aux = result ();
    95 
    95 
    96 Goal "new_tv n sch --> \
    96 Goal "new_tv n sch --> \
    97 \     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
    97 \     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
    98 \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
    98 \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
    99 by (type_scheme.induct_tac "sch" 1);
    99 by (induct_tac "sch" 1);
   100 by (simp_tac (simpset() addsimps [leD]) 1);
   100 by (simp_tac (simpset() addsimps [leD]) 1);
   101 by (Asm_simp_tac 1);
   101 by (Asm_simp_tac 1);
   102 by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
   102 by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
   103 val aux2 = result () RS mp;
   103 val aux2 = result () RS mp;
   104 
   104 
   125 by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
   125 by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
   126 by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
   126 by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
   127 by (asm_simp_tac (simpset() addsimps [aux2]) 1);
   127 by (asm_simp_tac (simpset() addsimps [aux2]) 1);
   128 by Safe_tac;
   128 by Safe_tac;
   129 by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
   129 by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
   130 by (type_scheme.induct_tac "sch" 1);
   130 by (induct_tac "sch" 1);
   131 by (Simp_tac 1);
   131 by (Simp_tac 1);
   132 by (Simp_tac 1);
   132 by (Simp_tac 1);
   133 by (Asm_simp_tac 1);
   133 by (Asm_simp_tac 1);
   134 qed "le_type_scheme_def2";
   134 qed "le_type_scheme_def2";
   135 
   135 
   143 by (rtac mk_scheme_injective 1); 
   143 by (rtac mk_scheme_injective 1); 
   144 by (Asm_full_simp_tac 1);
   144 by (Asm_full_simp_tac 1);
   145 by (rotate_tac 1 1);
   145 by (rotate_tac 1 1);
   146 by (rtac mp 1);
   146 by (rtac mp 1);
   147 by (assume_tac 2);
   147 by (assume_tac 2);
   148 by (type_scheme.induct_tac "sch" 1);
   148 by (induct_tac "sch" 1);
   149 by (Simp_tac 1);
   149 by (Simp_tac 1);
   150 by (Asm_full_simp_tac 1);
   150 by (Asm_full_simp_tac 1);
   151 by (Fast_tac 1);
   151 by (Fast_tac 1);
   152 by (strip_tac 1);
   152 by (strip_tac 1);
   153 by (Asm_full_simp_tac 1);
   153 by (Asm_full_simp_tac 1);
   154 by (etac exE 1);
   154 by (etac exE 1);
   155 by (Asm_full_simp_tac 1);
   155 by (Asm_full_simp_tac 1);
   156 by (rtac exI 1);
   156 by (rtac exI 1);
   157 by (type_scheme.induct_tac "sch" 1);
   157 by (induct_tac "sch" 1);
   158 by (Simp_tac 1);
   158 by (Simp_tac 1);
   159 by (Simp_tac 1);
   159 by (Simp_tac 1);
   160 by (Asm_full_simp_tac 1);
   160 by (Asm_full_simp_tac 1);
   161 qed_spec_mp "le_type_eq_is_bound_typ_instance";
   161 qed_spec_mp "le_type_eq_is_bound_typ_instance";
   162 
   162 
   170  by (eres_inst_tac [("x","Suc i")] allE 1);
   170  by (eres_inst_tac [("x","Suc i")] allE 1);
   171  by (Asm_full_simp_tac 1);
   171  by (Asm_full_simp_tac 1);
   172 by (rtac conjI 1);
   172 by (rtac conjI 1);
   173  by (Fast_tac 1);
   173  by (Fast_tac 1);
   174 by (rtac allI 1);
   174 by (rtac allI 1);
   175 by (nat_ind_tac "i" 1);
   175 by (induct_tac "i" 1);
   176 by (ALLGOALS Asm_simp_tac);
   176 by (ALLGOALS Asm_simp_tac);
   177 qed "le_env_Cons";
   177 qed "le_env_Cons";
   178 AddIffs [le_env_Cons];
   178 AddIffs [le_env_Cons];
   179 
   179 
   180 Goalw [is_bound_typ_instance]"t <| sch ==> $S t <| $S sch";
   180 Goalw [is_bound_typ_instance]"t <| sch ==> $S t <| $S sch";
   219 qed "bound_typ_instance_BVar";
   219 qed "bound_typ_instance_BVar";
   220 AddIffs [bound_typ_instance_BVar];
   220 AddIffs [bound_typ_instance_BVar];
   221 
   221 
   222 Goalw [le_type_scheme_def,is_bound_typ_instance]
   222 Goalw [le_type_scheme_def,is_bound_typ_instance]
   223  "(sch <= FVar n) = (sch = FVar n)";
   223  "(sch <= FVar n) = (sch = FVar n)";
   224 by (type_scheme.induct_tac "sch" 1);
   224 by (induct_tac "sch" 1);
   225   by (Simp_tac 1);
   225   by (Simp_tac 1);
   226  by (Simp_tac 1);
   226  by (Simp_tac 1);
   227  by (Fast_tac 1);
   227  by (Fast_tac 1);
   228 by (Asm_full_simp_tac 1);
   228 by (Asm_full_simp_tac 1);
   229 by (Fast_tac 1);
   229 by (Fast_tac 1);
   247   "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
   247   "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
   248 by (fast_tac (claset() addss simpset()) 1);
   248 by (fast_tac (claset() addss simpset()) 1);
   249 qed "Fun_le_FunD";
   249 qed "Fun_le_FunD";
   250 
   250 
   251 Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
   251 Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
   252 by (type_scheme.induct_tac "sch'" 1);
   252 by (induct_tac "sch'" 1);
   253 by (Asm_simp_tac 1);
   253 by (Asm_simp_tac 1);
   254 by (Asm_simp_tac 1);
   254 by (Asm_simp_tac 1);
   255 by (Fast_tac 1);
   255 by (Fast_tac 1);
   256 qed_spec_mp "scheme_le_Fun";
   256 qed_spec_mp "scheme_le_Fun";
   257 
   257 
   258 Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
   258 Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
   259 by (type_scheme.induct_tac "sch" 1);
   259 by (induct_tac "sch" 1);
   260   by (rtac allI 1);
   260   by (rtac allI 1);
   261   by (type_scheme.induct_tac "sch'" 1);
   261   by (induct_tac "sch'" 1);
   262     by (Simp_tac 1);
   262     by (Simp_tac 1);
   263    by (Simp_tac 1);
   263    by (Simp_tac 1);
   264   by (Simp_tac 1);
   264   by (Simp_tac 1);
   265  by (rtac allI 1);
   265  by (rtac allI 1);
   266  by (type_scheme.induct_tac "sch'" 1);
   266  by (induct_tac "sch'" 1);
   267    by (Simp_tac 1);
   267    by (Simp_tac 1);
   268   by (Simp_tac 1);
   268   by (Simp_tac 1);
   269  by (Simp_tac 1);
   269  by (Simp_tac 1);
   270 by (rtac allI 1);
   270 by (rtac allI 1);
   271 by (type_scheme.induct_tac "sch'" 1);
   271 by (induct_tac "sch'" 1);
   272   by (Simp_tac 1);
   272   by (Simp_tac 1);
   273  by (Simp_tac 1);
   273  by (Simp_tac 1);
   274 by (Asm_full_simp_tac 1);
   274 by (Asm_full_simp_tac 1);
   275 by (strip_tac 1);
   275 by (strip_tac 1);
   276 by (dtac Fun_le_FunD 1);
   276 by (dtac Fun_le_FunD 1);
   277 by (Fast_tac 1);
   277 by (Fast_tac 1);
   278 qed_spec_mp "le_type_scheme_free_tv";
   278 qed_spec_mp "le_type_scheme_free_tv";
   279 
   279 
   280 Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
   280 Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
   281 by (list.induct_tac "B" 1);
   281 by (induct_tac "B" 1);
   282  by (Simp_tac 1);
   282  by (Simp_tac 1);
   283 by (rtac allI 1);
   283 by (rtac allI 1);
   284 by (list.induct_tac "A" 1);
   284 by (induct_tac "A" 1);
   285  by (simp_tac (simpset() addsimps [le_env_def]) 1);
   285  by (simp_tac (simpset() addsimps [le_env_def]) 1);
   286 by (Simp_tac 1);
   286 by (Simp_tac 1);
   287 by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
   287 by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
   288 qed_spec_mp "le_env_free_tv";
   288 qed_spec_mp "le_env_free_tv";