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