src/HOL/MiniML/MiniML.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2525 477c05586286
child 3008 0a887d5b6718
permissions -rw-r--r--
added AxClasses test;
     1 (* Title:     HOL/MiniML/MiniML.ML
     2    ID:        $Id$
     3    Author:    Dieter Nazareth and Tobias Nipkow
     4    Copyright  1995 TU Muenchen
     5 *)
     6 
     7 Addsimps has_type.intrs;
     8 Addsimps [Un_upper1,Un_upper2];
     9 
    10 Addsimps [is_bound_typ_instance_closed_subst];
    11 
    12 
    13 goal thy "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t";
    14 by (rtac typ_substitutions_only_on_free_variables 1);
    15 by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
    16 qed "s'_t_equals_s_t";
    17 
    18 Addsimps [s'_t_equals_s_t];
    19 
    20 goal thy "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A";
    21 by (rtac scheme_list_substitutions_only_on_free_variables 1);
    22 by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1);
    23 qed "s'_a_equals_s_a";
    24 
    25 Addsimps [s'_a_equals_s_a];
    26 
    27 goal thy "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ 
    28 \              $ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t) ==> \
    29 \             $S A |- e :: $S t";
    30 
    31 by (res_inst_tac [("P","%A. A |- e :: $S t")] ssubst 1);
    32 by (rtac (s'_a_equals_s_a RS sym) 1);
    33 by (res_inst_tac [("P","%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t")] ssubst 1);
    34 by (rtac (s'_t_equals_s_t RS sym) 1);
    35 by (Asm_full_simp_tac 1);
    36 qed "replace_s_by_s'";
    37 
    38 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A";
    39 by (rtac scheme_list_substitutions_only_on_free_variables 1);
    40 by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1);
    41 qed "alpha_A'";
    42 
    43 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A";
    44 by (rtac (alpha_A' RS ssubst) 1);
    45 by (Asm_full_simp_tac 1);
    46 qed "alpha_A";
    47 
    48 goal thy "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
    49 by (typ.induct_tac "t" 1);
    50 by (ALLGOALS (Asm_full_simp_tac));
    51 qed "S_o_alpha_typ";
    52 
    53 goal thy "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
    54 by (typ.induct_tac "t" 1);
    55 by (ALLGOALS (Asm_full_simp_tac));
    56 val S_o_alpha_typ' = result ();
    57 
    58 goal thy "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
    59 by (type_scheme.induct_tac "sch" 1);
    60 by (ALLGOALS (Asm_full_simp_tac));
    61 qed "S_o_alpha_type_scheme";
    62 
    63 goal thy "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
    64 by (list.induct_tac "A" 1);
    65 by (ALLGOALS (Asm_full_simp_tac));
    66 by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
    67 qed "S_o_alpha_type_scheme_list";
    68 
    69 goal thy "!!A::type_scheme list. \
    70 \              ($ (%n. if n : free_tv A Un free_tv t \
    71 \                      then S n else TVar n) \
    72 \                 A) = \
    73 \              ($ ((%x. if x : free_tv A Un free_tv t then S x \
    74 \                       else TVar x) o \
    75 \                  (%x. if x : free_tv A \
    76 \                       then x else n + x)) A)";
    77 by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1);
    78 by (rtac (alpha_A RS ssubst) 1);
    79 by (rtac refl 1);
    80 qed "S'_A_eq_S'_alpha_A";
    81 
    82 goalw thy [free_tv_subst,dom_def]
    83           "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
    84 \               free_tv A Un free_tv t";
    85 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    86 by (Fast_tac 1);
    87 qed "dom_S'";
    88 
    89 goalw thy [free_tv_subst,cod_def,subset_def]
    90           "!!(A::type_scheme list) (t::typ). \ 
    91 \              cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
    92 \              free_tv ($ S A) Un free_tv ($ S t)";
    93 by (rtac ballI 1);
    94 by (etac UN_E 1);
    95 by (dtac (dom_S' RS subsetD) 1);
    96 by (rotate_tac 1 1);
    97 by (Asm_full_simp_tac 1);
    98 by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
    99                       addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
   100 qed "cod_S'";
   101 
   102 goalw thy [free_tv_subst]
   103           "!!(A::type_scheme list) (t::typ). \
   104 \               free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
   105 \               free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
   106 by (fast_tac (!claset addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
   107 qed "free_tv_S'";
   108 
   109 goal thy "!!t1::typ. \
   110 \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
   111 \         {x. ? y. x = n + y}";
   112 by (typ.induct_tac "t1" 1);
   113 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   114 by (Fast_tac 1);
   115 by (Simp_tac 1);
   116 by (Fast_tac 1);
   117 qed "free_tv_alpha";
   118 
   119 goal thy "!!(k::nat). n <= n + k";
   120 by (res_inst_tac [("n","k")] nat_induct 1);
   121 by (Simp_tac 1);
   122 by (Asm_simp_tac 1);
   123 val aux_plus = result();
   124 
   125 Addsimps [aux_plus];
   126 
   127 goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
   128 by (step_tac (!claset) 1);
   129 by (cut_facts_tac [aux_plus] 1);
   130 by (dtac new_tv_le 1);
   131 ba 1;
   132 by (rotate_tac 1 1);
   133 by (dtac new_tv_not_free_tv 1);
   134 by (Fast_tac 1);
   135 val new_tv_Int_free_tv_empty_type = result ();
   136 
   137 goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
   138 by (step_tac (!claset) 1);
   139 by (cut_facts_tac [aux_plus] 1);
   140 by (dtac new_tv_le 1);
   141 ba 1;
   142 by (rotate_tac 1 1);
   143 by (dtac new_tv_not_free_tv 1);
   144 by (Fast_tac 1);
   145 val new_tv_Int_free_tv_empty_scheme = result ();
   146 
   147 goal thy "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
   148 by (rtac allI 1);
   149 by (list.induct_tac "A" 1);
   150 by (Simp_tac 1);
   151 by (Simp_tac 1);
   152 by (fast_tac (!claset addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
   153 val new_tv_Int_free_tv_empty_scheme_list = result ();
   154 
   155 goalw thy [le_type_scheme_def,is_bound_typ_instance] 
   156       "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
   157 by (strip_tac 1);
   158 by (etac exE 1);
   159 by (hyp_subst_tac 1);
   160 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
   161 by (typ.induct_tac "t" 1);
   162 by (Simp_tac 1);
   163 by (case_tac "nat : free_tv A" 1);
   164 by (Asm_simp_tac 1);
   165 by (subgoal_tac "n <= n + nat" 1);
   166 by (dtac new_tv_le 1);
   167 ba 1;
   168 by (dtac new_tv_not_free_tv 1);
   169 by (dtac new_tv_not_free_tv 1);
   170 by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
   171 by (Simp_tac 1);
   172 by (Asm_simp_tac 1);
   173 qed_spec_mp "gen_t_le_gen_alpha_t";
   174 
   175 AddSIs has_type.intrs;
   176 
   177 goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
   178 by(etac has_type.induct 1);
   179    by(simp_tac (!simpset addsimps [le_env_def]) 1);
   180    by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
   181   by(Asm_full_simp_tac 1);
   182  by(Fast_tac 1);
   183 by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
   184 qed_spec_mp "has_type_le_env";
   185 
   186 (* has_type is closed w.r.t. substitution *)
   187 goal thy "!!a. A |- e :: t ==> !S. $S A |- e :: $S t";
   188 by (etac has_type.induct 1);
   189 (* case VarI *)
   190    by (rtac allI 1);
   191    by (rtac has_type.VarI 1);
   192     by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
   193    by (asm_simp_tac (!simpset addsimps [app_subst_list]) 1);
   194   (* case AbsI *)
   195   by (rtac allI 1);
   196   by (Simp_tac 1);  
   197   by (rtac has_type.AbsI 1);
   198   by (Asm_full_simp_tac 1);
   199  (* case AppI *)
   200  by (rtac allI 1);
   201  by (rtac has_type.AppI 1);
   202   by (Asm_full_simp_tac 1);
   203   by (etac spec 1);
   204  by (etac spec 1);
   205 (* case LetI *)
   206 by (rtac allI 1);
   207 by (rtac replace_s_by_s' 1);
   208 by (cut_inst_tac [("A","$ S A"), 
   209                   ("A'","A"),
   210                   ("t","t"),
   211                   ("t'","$ S t")] 
   212                  ex_fresh_variable 1);
   213 by (etac exE 1);
   214 by (REPEAT (etac conjE 1));
   215 by (res_inst_tac [("t1.0","$((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
   216 \                            (%x. if x : free_tv A then x else n + x)) t1")] 
   217                  has_type.LETI 1);
   218  by (dres_inst_tac [("x","(%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
   219 \                         (%x. if x : free_tv A then x else n + x)")] spec 1);
   220  val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
   221  (fn _ => [rtac refl 1]);
   222  by (stac (S'_A_eq_S'_alpha_A) 1);
   223  ba 1;
   224 by (stac S_o_alpha_typ 1);
   225 by (stac gen_subst_commutes 1);
   226  by (rtac subset_antisym 1);
   227   by (rtac subsetI 1);
   228   by (etac IntE 1);
   229   by (dtac (free_tv_S' RS subsetD) 1);
   230   by (dtac (free_tv_alpha RS subsetD) 1);
   231   by (Asm_full_simp_tac 1);
   232   by (etac exE 1);
   233   by (hyp_subst_tac 1);
   234   by (subgoal_tac "new_tv (n + y) ($ S A)" 1);
   235    by (subgoal_tac "new_tv (n + y) ($ S t)" 1);
   236     by (subgoal_tac "new_tv (n + y) A" 1);
   237      by (subgoal_tac "new_tv (n + y) t" 1);
   238       by (REPEAT (dtac new_tv_not_free_tv 1));
   239       by (Fast_tac 1);
   240      by (REPEAT ((rtac new_tv_le 1) THEN (assume_tac 2) THEN (Simp_tac 1)));
   241  by (Fast_tac 1);
   242 by (rtac has_type_le_env 1);
   243  by (dtac spec 1);
   244  by (dtac spec 1);
   245  ba 1;
   246 by (rtac (app_subst_Cons RS subst) 1);
   247 by (rtac S_compatible_le_scheme_lists 1);
   248 by (Asm_simp_tac 1);
   249 qed "has_type_cl_sub";