src/HOL/MiniML/Generalize.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5522 982c710450c6
child 7036 895c7c1e56ba
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* Title:     HOL/MiniML/Generalize.ML
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 *)
     6 
     7 AddSEs [equalityE];
     8 
     9 Goal "free_tv A = free_tv B ==> gen A t = gen B t";
    10 by (induct_tac "t" 1);
    11 by (ALLGOALS Asm_simp_tac);
    12 qed "gen_eq_on_free_tv";
    13 
    14 Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
    15 by (induct_tac "t" 1);
    16 by (Asm_simp_tac 1);
    17 by (Simp_tac 1);
    18 by (Fast_tac 1);
    19 qed_spec_mp "gen_without_effect";
    20 
    21 Addsimps [gen_without_effect];
    22 
    23 Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
    24 by (induct_tac "t" 1);
    25 by (Simp_tac 1);
    26 by (case_tac "nat : free_tv ($ S A)" 1);
    27 by (Asm_simp_tac 1);
    28 by (Fast_tac 1);
    29 by (Asm_simp_tac 1);
    30 by (Fast_tac 1);
    31 by (Asm_full_simp_tac 1);
    32 by (Fast_tac 1);
    33 qed "free_tv_gen";
    34 
    35 Addsimps [free_tv_gen];
    36 
    37 Goal "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
    38 by (Simp_tac 1);
    39 by (Fast_tac 1);
    40 qed "free_tv_gen_cons";
    41 
    42 Addsimps [free_tv_gen_cons];
    43 
    44 Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
    45 by (induct_tac "t1" 1);
    46 by (Simp_tac 1);
    47 by (case_tac "nat : free_tv A" 1);
    48 by (Asm_simp_tac 1);
    49 by (Asm_simp_tac 1);
    50 by (Fast_tac 1);
    51 by (Asm_simp_tac 1);
    52 by (Fast_tac 1);
    53 qed "bound_tv_gen";
    54 
    55 Addsimps [bound_tv_gen];
    56 
    57 Goal "new_tv n t --> new_tv n (gen A t)";
    58 by (induct_tac "t" 1);
    59 by (Simp_tac 1);
    60 by (case_tac "nat : free_tv A" 1);
    61 by (Asm_simp_tac 1);
    62 by (Asm_simp_tac 1);
    63 qed_spec_mp "new_tv_compatible_gen";
    64 
    65 Goalw [gen_ML_def] "gen A t = gen_ML A t";
    66 by (induct_tac "t" 1);
    67  by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
    68 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
    69 qed "gen_eq_gen_ML";
    70 
    71 Goal "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
    72 \     --> gen ($ S A) ($ S t) = $ S (gen A t)";
    73 by (induct_tac "t" 1);
    74  by (strip_tac 1);
    75  by (case_tac "nat:(free_tv A)" 1);
    76   by (Asm_simp_tac 1);
    77  by (Asm_full_simp_tac 1);
    78  by (subgoal_tac "nat ~: free_tv S" 1);
    79   by (Fast_tac 2);
    80  by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1);
    81  by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
    82  by (Fast_tac 1);
    83 by (Asm_simp_tac 1);
    84 by (Blast_tac 1);
    85 qed_spec_mp "gen_subst_commutes";
    86 
    87 Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
    88 by (induct_tac "t" 1);
    89 by (ALLGOALS Asm_simp_tac);
    90 by (Fast_tac 1);
    91 qed_spec_mp "bound_typ_inst_gen";
    92 Addsimps [bound_typ_inst_gen];
    93 
    94 Goalw [le_type_scheme_def,is_bound_typ_instance]
    95   "gen ($ S A) ($ S t) <= $ S (gen A t)";
    96 by Safe_tac;
    97 by (rename_tac "R" 1);
    98 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
    99 by (induct_tac "t" 1);
   100  by (Simp_tac 1);
   101 by (Asm_simp_tac 1);
   102 qed "gen_bound_typ_instance";
   103 
   104 Goalw [le_type_scheme_def,is_bound_typ_instance]
   105   "free_tv B <= free_tv A ==> gen A t <= gen B t";
   106 by Safe_tac;
   107 by (rename_tac "S" 1);
   108 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
   109 by (induct_tac "t" 1);
   110  by (Asm_simp_tac 1);
   111  by (Fast_tac 1);
   112 by (Asm_simp_tac 1);
   113 qed "free_tv_subset_gen_le";
   114 
   115 Goalw [le_type_scheme_def,is_bound_typ_instance] 
   116   "new_tv n A --> \
   117 \  gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
   118 by (strip_tac 1);
   119 by (etac exE 1);
   120 by (hyp_subst_tac 1);
   121 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
   122 by (induct_tac "t" 1);
   123 by (Simp_tac 1);
   124 by (case_tac "nat : free_tv A" 1);
   125 by (Asm_simp_tac 1);
   126 by (Asm_simp_tac 1);
   127 by (subgoal_tac "n <= n + nat" 1);
   128 by (forw_inst_tac [("t","A")] new_tv_le 1);
   129 by (assume_tac 1);
   130 by (dtac new_tv_not_free_tv 1);
   131 by (dtac new_tv_not_free_tv 1);
   132 by (asm_simp_tac (simpset() addsimps [diff_add_inverse]) 1);
   133 by (simp_tac (simpset() addsimps [le_add1]) 1);
   134 by (Asm_simp_tac 1);
   135 qed_spec_mp "gen_t_le_gen_alpha_t";
   136 
   137 Addsimps [gen_t_le_gen_alpha_t];