src/HOL/MiniML/W.ML
author paulson
Mon, 10 Mar 1997 10:32:32 +0100
changeset 2779 9c42ae57b5f4
parent 2749 2f477a0e690d
child 2793 b30c41754c86
permissions -rw-r--r--
The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac does not recognize eta-equality. But making it do so is costly
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
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    11
Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    13
val has_type_casesE = map(has_type.mk_cases expr.simps)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    14
        [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
(* 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
    17
goal thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    18
        "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
(* case Var(n) *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    21
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    22
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    23
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    24
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    25
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    26
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    27
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    28
by (Asm_full_simp_tac 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    29
(* case Abs e *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    30
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    31
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    32
(* case App e1 e2 *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    33
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    34
by (strip_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    35
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    36
by (eres_inst_tac [("x","A")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    37
by (eres_inst_tac [("x","n")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    38
by (eres_inst_tac [("x","$ S A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    39
by (eres_inst_tac [("x","S")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    40
by (eres_inst_tac [("x","t")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    41
by (eres_inst_tac [("x","n1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    42
by (eres_inst_tac [("x","n1")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    43
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    44
by (etac conjE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    45
by (eres_inst_tac [("x","S1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    46
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    47
by (eres_inst_tac [("x","n2")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    48
by (etac conjE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    49
by (res_inst_tac [("j","n1")] le_trans 1); 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    50
by (Asm_simp_tac 1);
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
    51
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    52
(* case LET e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    53
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    54
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    55
by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    56
by (REPEAT (etac conjE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    57
by (REPEAT (etac allE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    58
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    59
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    60
by (best_tac (!claset addEs [le_trans]) 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
    61
qed_spec_mp "W_var_ge";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    62
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    63
Addsimps [W_var_ge];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    64
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    65
goal thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    66
        "!! s. Some (S,t,m) = W e A n ==> n<=m";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    67
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    68
qed "W_var_geD";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    69
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    70
goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    71
by (dtac W_var_geD 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    72
by (rtac new_scheme_list_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    73
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    74
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    75
qed "new_tv_compatible_W";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    76
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    77
goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    78
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    79
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    80
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    81
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    82
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    83
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    84
by (rtac conjI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    85
by (rtac new_tv_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    86
by (mp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    87
by (mp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    88
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    89
by (rtac add_le_mono 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    90
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    91
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    92
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    93
by (rtac new_tv_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    94
by (mp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    95
by (mp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    96
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    97
by (rtac add_le_mono 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    98
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    99
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   100
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   101
by (dtac not_leE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   102
by (rtac less_or_eq_imp_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   103
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   104
qed_spec_mp "new_tv_bound_typ_inst_sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   105
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   106
Addsimps [new_tv_bound_typ_inst_sch];
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   107
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   108
(* resulting type variable is new *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   109
goal thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   110
     "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   111
\                 new_tv m S & new_tv m t";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   112
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   113
(* case Var n *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   114
by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   115
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   116
by (REPEAT (etac conjE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   117
by (rtac conjI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   118
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   119
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   120
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   121
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   122
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   123
by (dtac new_tv_nth_nat_A 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   124
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   125
by (Asm_full_simp_tac 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   126
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   127
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   128
    setloop (split_tac [expand_option_bind])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   129
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   130
by (eres_inst_tac [("x","Suc n")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   131
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   132
by (fast_tac (HOL_cs addss (!simpset
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   133
              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   134
(* case App e1 e2 *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   135
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   136
by (strip_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   137
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   138
by (eres_inst_tac [("x","n")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   139
by (eres_inst_tac [("x","A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   140
by (eres_inst_tac [("x","S")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   141
by (eres_inst_tac [("x","t")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   142
by (eres_inst_tac [("x","n1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   143
by (eres_inst_tac [("x","n1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   144
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   145
by (eres_inst_tac [("x","$ S A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   146
by (eres_inst_tac [("x","S1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   147
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   148
by (eres_inst_tac [("x","n2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   149
by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   150
by (rtac conjI 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   151
by (rtac new_tv_subst_comp_2 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   152
by (rtac new_tv_subst_comp_2 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   153
by (rtac (lessI RS less_imp_le RS new_tv_le) 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   154
by (res_inst_tac [("n","n1")] new_tv_subst_le 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   155
by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   156
by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   157
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   158
     [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le])
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   159
    1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   160
by (etac (sym RS mgu_new) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   161
by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   162
   new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   163
   new_tv_subst_le,new_tv_le]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   164
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   165
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le] 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   166
        addss (!simpset)) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   167
by (rtac (lessI RS new_tv_subst_var) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   168
by (etac (sym RS mgu_new) 1);
1925
1150f128c7fe Some tidying. This brittle proof depends upon
paulson
parents: 1910
diff changeset
   169
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   170
   addDs [W_var_geD] addIs
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   171
   [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   172
   new_tv_subst_le,new_tv_le] addss !simpset) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   173
by (fast_tac (HOL_cs addDs [W_var_geD] addIs
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   174
     [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   175
     addss (!simpset)) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   176
(* case LET e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   177
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   178
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   179
by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   180
by (REPEAT (etac conjE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   181
by (eres_inst_tac [("x","n1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   182
by (eres_inst_tac [("x","A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   183
by (eres_inst_tac [("x","S1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   184
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   185
by (rotate_tac 1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   186
by (eres_inst_tac [("x","n2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   187
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   188
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   189
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   190
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   191
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   192
by (eres_inst_tac [("x","n2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   193
by (eres_inst_tac [("x","gen ($ S1 A) t1 # $ S1 A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   194
by (eres_inst_tac [("x","S2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   195
by (eres_inst_tac [("x","t2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   196
by (eres_inst_tac [("x","m2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   197
by (subgoal_tac "new_tv n2 (gen ($ S1 A) t1 # $ S1 A)" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   198
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   199
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   200
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   201
by (rtac conjI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   202
by (simp_tac (!simpset addsimps [o_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   203
by (rtac new_tv_subst_comp_2 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   204
by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   205
by (etac W_var_ge 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   206
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   207
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   208
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   209
by (rewrite_goals_tac [new_tv_def]);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   210
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   211
by (dtac W_var_ge 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   212
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   213
by (rename_tac "p" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   214
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   215
by (rewrite_goals_tac [free_tv_subst]);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   216
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   217
fun restrict_prems is tacf =
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   218
  METAHYPS(fn prems =>
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   219
    let val iprems = map (fn i => nth_elem(i,prems)) is
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   220
    in cut_facts_tac iprems 1 THEN tacf 1 end);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   221
by (restrict_prems [0,4,8,9] (best_tac (!claset addEs [less_le_trans])) 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   222
qed_spec_mp "new_tv_W";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   223
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   224
goal thy "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   225
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   226
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   227
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   228
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   229
by (rtac exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   230
by (rtac refl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   231
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   232
qed_spec_mp "free_tv_bound_typ_inst1";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   233
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   234
Addsimps [free_tv_bound_typ_inst1];
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   235
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   236
goal thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   237
     "!n A S t m v. W e A n = Some (S,t,m) -->            \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   238
\         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   239
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   240
(* case Var n *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   241
by (simp_tac (!simpset addsimps
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   242
    [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   243
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   244
by (REPEAT (etac conjE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   245
by (hyp_subst_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   246
by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   247
by (case_tac "v : free_tv (nth nat A)" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   248
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   249
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   250
by (dtac free_tv_bound_typ_inst1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   251
by (simp_tac (!simpset addsimps [o_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   252
by (rotate_tac 3 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   253
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   254
by (rotate_tac 3 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   255
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   256
by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   257
by (dtac add_lessD1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   258
by (fast_tac (!claset addIs [less_irrefl]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   259
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   260
by (asm_full_simp_tac (!simpset addsimps
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   261
    [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   262
by (strip_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   263
by (rename_tac "S t n1 S1 t1 m v" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   264
by (eres_inst_tac [("x","Suc n")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   265
by (eres_inst_tac [("x","FVar n # A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   266
by (eres_inst_tac [("x","S")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   267
by (eres_inst_tac [("x","t")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   268
by (eres_inst_tac [("x","n1")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   269
by (eres_inst_tac [("x","v")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   270
by (best_tac (HOL_cs addIs [cod_app_subst]
1669
e56cdf711729 inserted Suc_less_eq explictly in a few proofs.
nipkow
parents: 1525
diff changeset
   271
                     addss (!simpset addsimps [less_Suc_eq])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   272
(* case App e1 e2 *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   273
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   274
by (strip_tac 1); 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   275
by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   276
by (eres_inst_tac [("x","n")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   277
by (eres_inst_tac [("x","A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   278
by (eres_inst_tac [("x","S")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   279
by (eres_inst_tac [("x","t")] allE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   280
by (eres_inst_tac [("x","n1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   281
by (eres_inst_tac [("x","n1")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   282
by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   283
(* second case *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   284
by (eres_inst_tac [("x","$ S A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   285
by (eres_inst_tac [("x","S1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   286
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   287
by (eres_inst_tac [("x","n2")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   288
by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   289
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   290
by (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   291
by (dtac W_var_geD 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   292
by (dtac W_var_geD 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   293
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   294
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   295
    codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   296
    less_le_trans,less_not_refl2,subsetD]
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   297
  addEs [UnE] 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   298
  addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   299
by (Asm_full_simp_tac 1); 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   300
by (dtac (sym RS W_var_geD) 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   301
by (dtac (sym RS W_var_geD) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   302
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   303
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   304
    free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   305
    less_le_trans,subsetD]
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   306
  addEs [UnE]
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   307
  addss !simpset) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   308
(* LET e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   309
by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   310
by (strip_tac 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   311
by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   312
by (eres_inst_tac [("x","nat")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   313
by (eres_inst_tac [("x","A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   314
by (eres_inst_tac [("x","S1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   315
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   316
by (rotate_tac 1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   317
by (eres_inst_tac [("x","n2")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   318
by (rotate_tac 4 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   319
by (eres_inst_tac [("x","v")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   320
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   321
by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   322
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   323
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   324
by (rtac conjI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   325
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge] 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   326
              addDs [less_le_trans]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   327
by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge] 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   328
              addDs [less_le_trans]) 1);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   329
qed_spec_mp "free_tv_W"; 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   330
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   331
goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   332
by (Fast_tac 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   333
val weaken_A_Int_B_eq_empty = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   334
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   335
goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   336
by (Fast_tac 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   337
val weaken_not_elem_A_minus_B = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   338
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   339
(* correctness of W with respect to has_type *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   340
goal W.thy
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   341
        "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   342
by (expr.induct_tac "e" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   343
(* case Var n *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   344
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   345
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   346
by (rtac has_type.VarI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   347
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   348
by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   349
by (rtac exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   350
by (rtac refl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   351
(* case Abs e *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   352
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   353
                        setloop (split_tac [expand_option_bind])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   354
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   355
by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   356
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   357
by (rtac has_type.AbsI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   358
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   359
bd sym 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   360
by (REPEAT (etac allE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   361
by (etac impE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   362
by (mp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   363
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   364
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   365
(* case App e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   366
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   367
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   368
by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   369
by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   370
by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   371
by (rtac (app_subst_Fun RS subst) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   372
by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   373
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   374
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   375
by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   376
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   377
by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   378
by (rtac (has_type_cl_sub RS spec) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   379
by (forward_tac [new_tv_W] 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   380
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   381
by (dtac conjunct1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   382
by (dtac conjunct1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   383
by (forward_tac [new_tv_subst_scheme_list] 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   384
by (rtac new_scheme_list_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   385
by (rtac W_var_ge 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   386
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   387
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   388
by (etac thin_rl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   389
by (REPEAT (etac allE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   390
bd sym 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   391
bd sym 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   392
by (etac thin_rl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   393
by (etac thin_rl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   394
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   395
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   396
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   397
(* case Let e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   398
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   399
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   400
by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   401
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   402
by (simp_tac (!simpset addsimps [o_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   403
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   404
by (rtac (has_type_cl_sub RS spec) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   405
by (dres_inst_tac [("x","A")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   406
by (dres_inst_tac [("x","S1")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   407
by (dres_inst_tac [("x","t1")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   408
by (dres_inst_tac [("x","m2")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   409
by (rotate_tac 4 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   410
by (dres_inst_tac [("x","m1")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   411
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   412
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   413
by (simp_tac (!simpset addsimps [o_def]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   414
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   415
by (rtac (gen_subst_commutes RS sym RS subst) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   416
by (rtac (app_subst_Cons RS subst) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   417
by (etac thin_rl 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   418
by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   419
by (dres_inst_tac [("x","S2")] spec 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   420
by (dres_inst_tac [("x","t")] spec 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   421
by (dres_inst_tac [("x","n2")] spec 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   422
by (dres_inst_tac [("x","m2")] spec 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   423
by (forward_tac [new_tv_W] 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   424
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   425
by (dtac conjunct1 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   426
by (dtac conjunct1 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   427
by (forward_tac [new_tv_subst_scheme_list] 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   428
by (rtac new_scheme_list_le 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   429
by (rtac W_var_ge 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   430
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   431
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   432
by (etac impE 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   433
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   434
by (Simp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   435
by (Fast_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   436
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   437
by (Asm_full_simp_tac 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   438
by (rtac weaken_A_Int_B_eq_empty 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   439
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   440
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   441
by (rtac weaken_not_elem_A_minus_B 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   442
by (case_tac "x < m2" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   443
by (rtac disjI2 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   444
by (rtac (free_tv_gen_cons RS subst) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   445
by (rtac free_tv_W 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   446
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   447
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   448
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   449
by (rtac disjI1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   450
by (dtac new_tv_W 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   451
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   452
by (dtac conjunct2 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   453
by (dtac conjunct2 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   454
by (rtac new_tv_not_free_tv 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   455
by (rtac new_tv_le 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   456
ba 2;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   457
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   458
qed_spec_mp "W_correct_lemma";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   459
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   460
goal Arith.thy "!!n::nat. ~ k+n < n";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   461
by (nat_ind_tac "k" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   462
by(ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   463
by(trans_tac 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   464
val not_add_less1 = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   465
Addsimps [not_add_less1];
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   466
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   467
(* Completeness of W w.r.t. has_type *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   468
goal thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   469
 "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   470
\             (? S t. (? m. W e A n = Some (S,t,m)) &  \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   471
\                     (? R. $S' A = $R ($S A) & t' = $R t))";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   472
by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   473
(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   474
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   475
by (simp_tac (!simpset addcongs [conj_cong] 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   476
    setloop (split_tac [expand_if])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   477
by (eresolve_tac has_type_casesE 1); 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   478
by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   479
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   480
by (hyp_subst_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   481
by (rename_tac "S" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   482
by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   483
by (rtac conjI 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   484
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   485
by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst] 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   486
                           delsimps [bound_typ_inst_composed_subst]) 1);
2749
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   487
(** LEVEL 12 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   488
(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   489
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   490
by (eresolve_tac has_type_casesE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   491
by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   492
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   493
by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   494
by (eres_inst_tac [("x","Suc n")] allE 1);
2749
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   495
by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   496
                  unsafe_addss (!simpset addcongs [conj_cong] 
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   497
				setloop (split_tac [expand_option_bind]))) 1);
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   498
(** LEVEL 19 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   499
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   500
(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   501
by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   502
by (eresolve_tac has_type_casesE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   503
by (eres_inst_tac [("x","S'")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   504
by (eres_inst_tac [("x","A")] allE 1);
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1300
diff changeset
   505
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   506
by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   507
by (safe_tac HOL_cs);
2749
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   508
(** LEVEL 26 **)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   509
by (eres_inst_tac [("x","R")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   510
by (eres_inst_tac [("x","$ S A")] allE 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   511
by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   512
by (eres_inst_tac [("x","m")] allE 1);
2749
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   513
by (rotate_tac ~3 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   514
by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   515
by (safe_tac HOL_cs);
2779
9c42ae57b5f4 The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
paulson
parents: 2749
diff changeset
   516
by (contr_tac 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   517
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   518
        conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
2779
9c42ae57b5f4 The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac
paulson
parents: 2749
diff changeset
   519
(** LEVEL 35 **)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   520
by (subgoal_tac
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   521
  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   522
\        else Ra x)) ($ Sa t) = \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   523
\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   524
\        else Ra x)) (ta -> (TVar ma))" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   525
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   526
\   (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   527
    ("s","($ Ra ta) -> t'")] ssubst 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   528
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   529
by (rtac eq_free_eq_subst_te 2);  
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   530
by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   531
by (subgoal_tac "na ~=ma" 2);
2749
2f477a0e690d Deleted steps made redundant by the stronger eq_assume_tac
paulson
parents: 2637
diff changeset
   532
by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   533
    new_tv_not_free_tv,new_tv_le]) 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   534
by (case_tac "na:free_tv Sa" 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   535
(* n1 ~: free_tv S1 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   536
by (forward_tac [not_free_impl_id] 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   537
by (asm_simp_tac (!simpset 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   538
    setloop (split_tac [expand_if])) 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   539
(* na : free_tv Sa *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   540
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   541
by (dtac eq_subst_scheme_list_eq_free 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   542
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
   543
by (Asm_simp_tac 2); 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   544
by (case_tac "na:dom Sa" 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   545
(* na ~: dom Sa *)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   546
by (asm_full_simp_tac (!simpset addsimps [dom_def] 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   547
    setloop (split_tac [expand_if])) 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   548
(* na : dom Sa *)
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   549
by (rtac eq_free_eq_subst_te 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   550
by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   551
by (subgoal_tac "nb ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   552
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   553
by (etac conjE 3);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   554
by (dtac new_tv_subst_scheme_list 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   555
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   556
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   557
    (!simpset addsimps [cod_def,free_tv_subst])) 3);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   558
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   559
    setloop (split_tac [expand_if]))) 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   560
by (Simp_tac 2);  
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   561
by (rtac eq_free_eq_subst_te 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   562
by (strip_tac 2 );
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   563
by (subgoal_tac "na ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   564
by ((forward_tac [new_tv_W] 3) THEN (atac 3));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   565
by (etac conjE 3);
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   566
by (dtac (sym RS W_var_geD) 3);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   567
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   568
by (case_tac "na: free_tv t - free_tv Sa" 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   569
(* case na ~: free_tv t - free_tv Sa *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   570
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   571
(* case na : free_tv t - free_tv Sa *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   572
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   573
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   574
by (dtac eq_subst_scheme_list_eq_free 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   575
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   576
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   577
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   578
by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   579
by (safe_tac HOL_cs );
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   580
by (dtac mgu_Some 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   581
by( fast_tac (HOL_cs addss !simpset) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   582
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   583
by ((dtac mgu_mg 1) THEN (atac 1));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   584
by (etac exE 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   585
by (res_inst_tac [("x","Rb")] exI 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   586
by (rtac conjI 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   587
by (dres_inst_tac [("x","ma")] fun_cong 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   588
by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   589
by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   590
by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   591
by (res_inst_tac [("A2","($ Sa ($ S A))")] ((subst_comp_scheme_list RS sym) RSN 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   592
    (2,trans)) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   593
by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   594
by (rtac eq_free_eq_subst_scheme_list 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   595
by( safe_tac HOL_cs );
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   596
by (subgoal_tac "ma ~= na" 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   597
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   598
by (etac conjE 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   599
by (dtac new_tv_subst_scheme_list 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   600
by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1465
diff changeset
   601
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
   602
by (etac conjE 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   603
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   604
by (fast_tac (set_cs addDs [W_var_geD,new_scheme_list_le,codD,
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   605
    new_tv_not_free_tv]) 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   606
by (case_tac "na: free_tv t - free_tv Sa" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   607
(* case na ~: free_tv t - free_tv Sa *)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   608
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   609
(* case na : free_tv t - free_tv Sa *)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   610
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   611
by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   612
by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   613
    eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   614
    [free_tv_subst,dom_def]))) 1);
2083
b56425a385b9 Tidied some proofs: changed needed for de Morgan laws
paulson
parents: 2058
diff changeset
   615
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   616
(* case Let e1 e2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   617
by (eresolve_tac has_type_casesE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   618
by (eres_inst_tac [("x","S'")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   619
by (eres_inst_tac [("x","A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   620
by (eres_inst_tac [("x","t1")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   621
by (eres_inst_tac [("x","n")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   622
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   623
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   624
by (safe_tac HOL_cs);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   625
by (Asm_simp_tac 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   626
by (eres_inst_tac [("x","R")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   627
by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   628
by (eres_inst_tac [("x","t'")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   629
by (eres_inst_tac [("x","m")] allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   630
by (rotate_tac 4 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   631
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   632
by (dtac mp 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   633
by (rtac has_type_le_env 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   634
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   635
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   636
by (rtac gen_bound_typ_instance 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   637
by (dtac mp 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   638
by (forward_tac [new_tv_compatible_W] 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   639
by (rtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   640
ba 1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   641
by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   642
by (safe_tac HOL_cs);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   643
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   644
by (res_inst_tac [("x","Ra")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   645
by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   646
qed_spec_mp "W_complete_lemma";
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   647
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   648
goal W.thy
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   649
 "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   650
\                                 (? R. t' = $ R t))";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   651
by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   652
                W_complete_lemma 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   653
by(ALLGOALS Asm_full_simp_tac);
1525
d127436567d0 modified priorities in syntax
nipkow
parents: 1486
diff changeset
   654
qed "W_complete";