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