src/HOL/MiniML/W.ML
author paulson
Thu, 09 Jan 1997 10:22:42 +0100
changeset 2498 7914881f47c0
parent 2083 b56425a385b9
child 2513 d708d8cdc8e8
permissions -rw-r--r--
New theorem add_leE
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/W.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
Correctness and completeness of type inference algorithm W
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
open W;
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
Addsimps [Suc_le_lessD];
1950
97f1c6bf3ace Miniscoping rules are deleted, as these brittle proofs
paulson
parents: 1925
diff changeset
    12
Delsimps (ex_simps @ all_simps);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    13
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
(* correctness of W with respect to has_type *)
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
    15
goal W.thy
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
    16
        "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    17
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    21
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    22
                        setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    23
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    24
by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
    25
by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    26
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    27
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    28
by (strip_tac 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
    29
by ( rename_tac "sa ta na sb tb nb sc" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    30
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    31
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    32
by (rtac (app_subst_Fun RS subst) 1);
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
    33
by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    34
by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    35
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    36
by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    37
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
    38
by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
    39
qed_spec_mp "W_correct";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    40
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    41
val has_type_casesE = map(has_type.mk_cases expr.simps)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
    42
        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    43
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    44
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    45
(* the resulting type variable is always greater or equal than the given one *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    46
goal thy
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
    47
        "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    48
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    49
(* case Var(n) *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    50
by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    51
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    52
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    53
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    54
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    55
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    56
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    57
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    58
by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    59
by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    60
by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    61
by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    62
by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    63
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    64
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    65
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    66
by (etac conjE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    67
by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    68
by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    69
by (eres_inst_tac [("x","nb")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    70
by (etac conjE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    71
by (res_inst_tac [("j","na")] le_trans 1); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    72
by (Asm_simp_tac 1);
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
    73
by (Asm_simp_tac 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
    74
qed_spec_mp "W_var_ge";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    75
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    76
Addsimps [W_var_ge];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    77
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    78
goal thy
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
    79
        "!! s. Ok (s,t,m) = W e a n ==> n<=m";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    80
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    81
qed "W_var_geD";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    82
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    83
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    84
(* auxiliary lemma *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    85
goal Maybe.thy "(y = Ok x) = (Ok x = y)";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
    86
by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    87
qed "rotate_Ok";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    88
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    89
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    90
(* resulting type variable is new *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    91
goal thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    92
     "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
    93
\                 new_tv m s & new_tv m t";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    94
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    95
(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    96
by (fast_tac (HOL_cs addss (!simpset 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
    97
        addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    98
        setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    99
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   100
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   101
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   102
    setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   103
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   104
by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   105
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   106
by (fast_tac (HOL_cs addss (!simpset
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   107
              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   108
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   109
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   110
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   111
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   112
by (rename_tac "s t na sa ta nb sb sc tb m" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   113
by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   114
by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   115
by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   116
by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   117
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   118
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   119
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   120
by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   121
by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   122
by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   123
by (eres_inst_tac [("x","nb")] allE 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   124
by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   125
by (rtac conjI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   126
by (rtac new_tv_subst_comp_2 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   127
by (rtac new_tv_subst_comp_2 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   128
by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   129
by (res_inst_tac [("n","na")] new_tv_subst_le 1); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   130
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   131
by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   132
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   133
     [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   134
    1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   135
by (etac (sym RS mgu_new) 1);
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   136
by (best_tac (HOL_cs addDs [W_var_geD] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   137
                     addIs [new_tv_subst_te,new_tv_list_le,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   138
                            new_tv_subst_tel,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   139
                            lessI RS less_imp_le RS new_tv_le,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   140
                            lessI RS less_imp_le RS new_tv_subst_le,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   141
                            new_tv_le]) 1);
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   142
by (fast_tac (HOL_cs addDs [W_var_geD] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   143
                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   144
                     addss (!simpset)) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   145
by (rtac (lessI RS new_tv_subst_var) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   146
by (etac (sym RS mgu_new) 1);
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   147
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   148
                     addDs [W_var_geD]
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   149
                     addIs [new_tv_list_le,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   150
                            new_tv_subst_tel,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   151
                            lessI RS less_imp_le RS new_tv_subst_le,
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   152
                            new_tv_le] 
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   153
                     addss !simpset) 1);
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   154
by (fast_tac (HOL_cs addDs [W_var_geD] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   155
                     addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le]
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   156
                     addss (!simpset)) 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   157
qed_spec_mp "new_tv_W";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   158
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   159
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   160
goal thy
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   161
     "!n a s t m v. W e a n = Ok (s,t,m) -->            \
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   162
\         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   163
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   164
(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   165
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   166
    addss (!simpset setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   167
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   168
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   169
by (asm_full_simp_tac (!simpset addsimps
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   170
    [free_tv_subst] setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   171
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   172
by (rename_tac "s t na sa ta m v" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   173
by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   174
by (eres_inst_tac [("x","TVar n # a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   175
by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   176
by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   177
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   178
by (eres_inst_tac [("x","v")] allE 1);
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
   179
by (fast_tac (HOL_cs addIs [cod_app_subst]
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
   180
                     addss (!simpset addsimps [less_Suc_eq])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   181
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   182
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   183
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   184
by (strip_tac 1); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   185
by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   186
by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   187
by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   188
by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   189
by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   190
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   191
by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   192
by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   193
(* second case *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   194
by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   195
by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   196
by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   197
by (eres_inst_tac [("x","nb")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   198
by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   199
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
   200
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   201
by (dtac W_var_geD 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   202
by (dtac W_var_geD 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   203
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   204
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   205
    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   206
    less_le_trans,less_not_refl2,subsetD]
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   207
  addEs [UnE] 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   208
  addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   209
by (Asm_full_simp_tac 1); 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   210
by (dtac (sym RS W_var_geD) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   211
by (dtac (sym RS W_var_geD) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   212
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   213
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   214
    free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   215
    less_le_trans,subsetD]
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   216
  addEs [UnE]
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   217
  addss !simpset) 1); 
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   218
qed_spec_mp "free_tv_W"; 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   219
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   220
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   221
(* Completeness of W w.r.t. has_type *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   222
goal thy
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   223
 "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   224
\             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   225
\                     (? r. $s' a = $r ($s a) & t' = $r t))";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   226
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   227
(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   228
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   229
by (simp_tac (!simpset addcongs [conj_cong] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   230
              setloop (split_tac [expand_if])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   231
by (eresolve_tac has_type_casesE 1); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   232
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   233
by (res_inst_tac [("x","id_subst")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   234
by (res_inst_tac [("x","nth nat a")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   235
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   236
by (res_inst_tac [("x","s'")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   237
by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   238
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   239
(** LEVEL 10 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   240
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   241
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   242
by (eresolve_tac has_type_casesE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   243
by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   244
by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   245
by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   246
by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   247
by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   248
                            setloop (split_tac [expand_bind]))) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   249
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   250
(** LEVEL 17 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   251
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   252
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   253
by (eresolve_tac has_type_casesE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   254
by (eres_inst_tac [("x","s'")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   255
by (eres_inst_tac [("x","a")] allE 1);
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   256
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   257
by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   258
by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   259
by (eres_inst_tac [("x","r")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   260
by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   261
by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   262
by (eres_inst_tac [("x","m")] allE 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   263
by (dtac asm_rl 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   264
by (dtac asm_rl 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   265
by (dtac asm_rl 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   266
by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   267
by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   268
by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   269
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   270
                            conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   271
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   272
(** LEVEL 35 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   273
by (subgoal_tac
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   274
  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   275
\        else ra x)) ($ sa t) = \
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   276
\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   277
\        else ra x)) (ta -> (TVar ma))" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   278
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   279
\   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   280
    ("s","($ ra ta) -> t'")] ssubst 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   281
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   282
by (rtac eq_free_eq_subst_te 2);  
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   283
by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   284
by (subgoal_tac "na ~=ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   285
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   286
                            new_tv_not_free_tv,new_tv_le]) 3);
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   287
(** LEVEL 42 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   288
by (case_tac "na:free_tv sa" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   289
(* na ~: free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   290
by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   291
                  setloop (split_tac [expand_if])) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   292
(* na : free_tv sa *)
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   293
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   294
by (dtac eq_subst_tel_eq_free 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   295
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   296
by (Asm_simp_tac 2); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   297
by (case_tac "na:dom sa" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   298
(* na ~: dom sa *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   299
by (asm_full_simp_tac (!simpset addsimps [dom_def] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   300
                       setloop (split_tac [expand_if])) 3);
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   301
(** LEVEL 50 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   302
(* na : dom sa *)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   303
by (rtac eq_free_eq_subst_te 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   304
by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   305
by (subgoal_tac "nb ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   306
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   307
by (etac conjE 3);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   308
by (dtac new_tv_subst_tel 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   309
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   310
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   311
              (!simpset addsimps [cod_def,free_tv_subst])) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   312
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   313
                            setloop (split_tac [expand_if]))) 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   314
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   315
by (Simp_tac 2);  
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   316
(** LEVEL 60 **)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   317
by (rtac eq_free_eq_subst_te 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   318
by (strip_tac 2 );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   319
by (subgoal_tac "na ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   320
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   321
by (etac conjE 3);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   322
by (dtac (sym RS W_var_geD) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   323
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   324
by (case_tac "na: free_tv t - free_tv sa" 2);
2058
ff04984186e9 Tidied up some proofs
paulson
parents: 2031
diff changeset
   325
(** LEVEL 68 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   326
(* case na ~: free_tv t - free_tv sa *)
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   327
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   328
(* case na : free_tv t - free_tv sa *)
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   329
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   330
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   331
by (dtac eq_subst_tel_eq_free 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   332
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   333
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   334
(** LEVEL 74 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   335
by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   336
by (safe_tac HOL_cs );
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   337
by (dtac mgu_Ok 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   338
by ( fast_tac (HOL_cs addss !simpset) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   339
by (REPEAT (resolve_tac [exI,conjI] 1));
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   340
by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   341
by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   342
by ((dtac mgu_mg 1) THEN (atac 1));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   343
by (etac exE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   344
by (res_inst_tac [("x","rb")] exI 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   345
by (rtac conjI 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   346
by (dres_inst_tac [("x","ma")] fun_cong 2);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   347
by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   348
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   349
by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   350
    (2,trans)) 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   351
by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   352
(** LEVEL 90 **)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   353
by (rtac eq_free_eq_subst_tel 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   354
by ( safe_tac HOL_cs );
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   355
by (subgoal_tac "ma ~= na" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   356
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   357
by (etac conjE 2);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   358
by (dtac new_tv_subst_tel 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   359
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   360
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   361
by (etac conjE 2);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   362
by (dtac (free_tv_app_subst_tel RS subsetD) 2);
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   363
(** LEVEL 100 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   364
by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   365
    new_tv_not_free_tv]) 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   366
by (case_tac "na: free_tv t - free_tv sa" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   367
(* case na ~: free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   368
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   369
(* case na : free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   370
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   371
by (dtac (free_tv_app_subst_tel RS subsetD) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   372
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   373
			    eq_subst_tel_eq_free] 
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   374
       addss ((!simpset addsimps [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   375
(** LEVEL 106 **)
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   376
by (Fast_tac 1);
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   377
qed_spec_mp "W_complete_lemma";
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   378
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   379
goal W.thy
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   380
 "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   381
\                                 (? r. t' = $r t))";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   382
by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   383
                W_complete_lemma 1);
2031
03a843f0f447 Ran expandshort
paulson
parents: 1950
diff changeset
   384
by (ALLGOALS Asm_full_simp_tac);
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   385
qed "W_complete";