src/HOL/MiniML/W.thy
author kleing
Tue, 02 Mar 2004 01:32:23 +0100
changeset 14422 b8da5f258b04
parent 5184 9b8547a9496a
child 14424 9a415e68cc06
permissions -rw-r--r--
converted to Isar
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.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
     3
   Author:    Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     4
   Copyright  1996 TU Muenchen
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
     6
Correctness and completeness of type inference algorithm W
1300
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
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     9
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    10
theory W = MiniML:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    12
types result_W = "(subst * typ * nat)option"
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    13
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    14
-- "type inference algorithm W"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    15
consts W :: "[expr, ctxt, nat] => result_W"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 4502
diff changeset
    17
primrec
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    18
  "W (Var i) A n =  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    19
     (if i < length A then Some( id_subst,   
4502
337c073de95e nth -> !
nipkow
parents: 2525
diff changeset
    20
	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
337c073de95e nth -> !
nipkow
parents: 2525
diff changeset
    21
	                         n + (min_new_bound_tv (A!i)) )  
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    22
	              else None)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    23
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    24
  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    25
                     Some( S, (S n) -> t, m) )"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    26
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    27
  "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    28
                         (S2,t2,m2) := W e2 ($S1 A) m1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    29
                         U := mgu ($S2 t1) (t2 -> (TVar m2));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    30
                         Some( $U o $S2 o S1, U m2, Suc m2) )"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    31
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    32
  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    33
                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    34
                         Some( $S2 o S1, t2, m2) )"
14422
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    35
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    36
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    37
lemmas W_rules =
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    38
 le_env_Cons 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    39
 le_type_scheme_refl 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    40
 le_env_refl 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    41
 bound_typ_instance_BVar 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    42
 not_FVar_le_Fun 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    43
 not_BVar_le_Fun 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    44
 le_env_Cons 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    45
 le_type_scheme_refl 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    46
 le_env_refl 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    47
 bound_typ_instance_BVar 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    48
 not_FVar_le_Fun 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    49
 not_BVar_le_Fun
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    50
 has_type.intros
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    51
 equalityE
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    52
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    53
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    54
declare Suc_le_lessD [simp]
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    55
declare less_imp_le [simp del]  (*the combination loops*)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    56
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    57
inductive_cases has_type_casesE:
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    58
"A |- Var n :: t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    59
"A |- Abs e :: t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    60
"A |- App e1 e2 ::t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    61
"A |- LET e1 e2 ::t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    62
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    63
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    64
(* the resulting type variable is always greater or equal than the given one *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    65
lemma W_var_ge [rule_format (no_asm)]: "!A n S t m. W e A n  = Some (S,t,m) --> n<=m"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    66
apply (induct_tac "e")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    67
(* case Var(n) *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    68
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    69
(* case Abs e *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    70
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    71
apply (fast dest: Suc_leD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    72
(* case App e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    73
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    74
apply (blast intro: le_SucI le_trans)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    75
(* case LET e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    76
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    77
apply (blast intro: le_trans)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    78
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    79
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    80
declare W_var_ge [simp]
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    81
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    82
lemma W_var_geD: "Some (S,t,m) = W e A n ==> n<=m"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    83
apply (simp add: eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    84
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    85
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    86
lemma new_tv_compatible_W: "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    87
apply (drule W_var_geD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    88
apply (rule new_scheme_list_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    89
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    90
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    91
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    92
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    93
lemma new_tv_bound_typ_inst_sch [rule_format (no_asm)]: "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    94
apply (induct_tac "sch")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    95
  apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    96
 apply (simp add: add_commute)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    97
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    98
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
    99
apply (erule conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   100
apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   101
 apply (rule new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   102
  prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   103
 apply (rule add_le_mono)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   104
  apply (simp (no_asm))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   105
 apply (simp (no_asm) add: max_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   106
apply (rule new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   107
 prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   108
apply (rule add_le_mono)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   109
 apply (simp (no_asm))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   110
apply (simp (no_asm) add: max_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   111
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   112
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   113
declare new_tv_bound_typ_inst_sch [simp]
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   114
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   115
(* resulting type variable is new *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   116
lemma new_tv_W [rule_format (no_asm)]: "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->     
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   117
                  new_tv m S & new_tv m t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   118
apply (induct_tac "e")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   119
(* case Var n *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   120
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   121
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   122
apply (drule new_tv_nth_nat_A)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   123
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   124
apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   125
(* case Abs e *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   126
apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   127
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   128
apply (erule_tac x = "Suc n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   129
apply (erule_tac x = " (FVar n) #A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   130
apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   131
(* case App e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   132
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   133
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   134
apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   135
apply (erule_tac x = "n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   136
apply (erule_tac x = "A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   137
apply (erule_tac x = "S1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   138
apply (erule_tac x = "t1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   139
apply (erule_tac x = "n1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   140
apply (erule_tac x = "n1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   141
apply (simp add: eq_sym_conv del: all_simps)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   142
apply (erule_tac x = "$S1 A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   143
apply (erule_tac x = "S2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   144
apply (erule_tac x = "t2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   145
apply (erule_tac x = "n2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   146
apply ( simp add: o_def rotate_Some)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   147
apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   148
apply (rule new_tv_subst_comp_2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   149
apply (rule new_tv_subst_comp_2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   150
apply (rule lessI [THEN less_imp_le, THEN new_tv_le])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   151
apply (rule_tac n = "n1" in new_tv_subst_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   152
apply (simp add: rotate_Some)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   153
apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   154
apply (fast dest: W_var_geD intro: new_scheme_list_le new_tv_subst_scheme_list lessI [THEN less_imp_le [THEN new_tv_subst_le]])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   155
apply (erule sym [THEN mgu_new])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   156
apply (blast dest!: W_var_geD
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   157
             intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   158
                    new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   159
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   160
apply (erule impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   161
apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   162
apply clarsimp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   163
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   164
apply (rule lessI [THEN new_tv_subst_var])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   165
apply (erule sym [THEN mgu_new])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   166
apply (blast dest!: W_var_geD
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   167
             intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   168
                    new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   169
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   170
apply (erule impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   171
apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   172
apply clarsimp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   173
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   174
-- "41: case LET e1 e2"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   175
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   176
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   177
apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, assumption, erule impE, assumption) 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   178
apply (erule conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   179
apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   180
apply (simp only: new_tv_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   181
apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   182
apply (drule W_var_ge)+
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   183
apply (rule allI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   184
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   185
apply (simp only: free_tv_subst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   186
apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   187
apply (best elim: less_le_trans)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   188
apply (erule conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   189
apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   190
apply (simp only: o_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   191
apply (rule new_tv_subst_comp_2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   192
apply (erule W_var_ge [THEN new_tv_subst_le])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   193
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   194
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   195
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   196
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   197
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   198
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   199
lemma free_tv_bound_typ_inst1 [rule_format (no_asm)]: "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   200
apply (induct_tac "sch")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   201
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   202
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   203
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   204
apply (rule exI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   205
apply (rule refl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   206
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   207
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   208
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   209
declare free_tv_bound_typ_inst1 [simp]
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   210
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   211
lemma free_tv_W [rule_format (no_asm)]: "!n A S t m v. W e A n = Some (S,t,m) -->             
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   212
          (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   213
apply (induct_tac "e")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   214
(* case Var n *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   215
apply (simp (no_asm) add: free_tv_subst split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   216
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   217
apply (case_tac "v : free_tv (A!nat) ")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   218
 apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   219
apply (drule free_tv_bound_typ_inst1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   220
 apply (simp (no_asm) add: o_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   221
apply (erule exE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   222
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   223
(* case Abs e *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   224
apply (simp add: free_tv_subst split add: split_option_bind del: all_simps)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   225
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   226
apply (rename_tac S t n1 v)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   227
apply (erule_tac x = "Suc n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   228
apply (erule_tac x = "FVar n # A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   229
apply (erule_tac x = "S" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   230
apply (erule_tac x = "t" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   231
apply (erule_tac x = "n1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   232
apply (erule_tac x = "v" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   233
apply (bestsimp del: W_rules intro: cod_app_subst simp add: less_Suc_eq)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   234
(* case App e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   235
apply (simp (no_asm) split add: split_option_bind del: all_simps)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   236
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   237
apply (rename_tac S t n1 S1 t1 n2 S2 v)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   238
apply (erule_tac x = "n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   239
apply (erule_tac x = "A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   240
apply (erule_tac x = "S" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   241
apply (erule_tac x = "t" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   242
apply (erule_tac x = "n1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   243
apply (erule_tac x = "n1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   244
apply (erule_tac x = "v" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   245
(* second case *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   246
apply (erule_tac x = "$ S A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   247
apply (erule_tac x = "S1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   248
apply (erule_tac x = "t1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   249
apply (erule_tac x = "n2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   250
apply (erule_tac x = "v" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   251
apply (intro conjI impI | elim conjE)+
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   252
 apply (simp add: rotate_Some o_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   253
 apply (drule W_var_geD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   254
 apply (drule W_var_geD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   255
 apply ( (frule less_le_trans) , (assumption))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   256
 apply clarsimp 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   257
 apply (drule free_tv_comp_subst [THEN subsetD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   258
 apply (drule sym [THEN mgu_free])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   259
 apply clarsimp 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   260
 apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans less_not_refl2 subsetD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   261
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   262
apply (drule sym [THEN W_var_geD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   263
apply (drule sym [THEN W_var_geD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   264
apply ( (frule less_le_trans) , (assumption))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   265
apply clarsimp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   266
apply (drule mgu_free)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   267
apply (fastsimp dest: mgu_free codD free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans subsetD)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   268
(* LET e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   269
apply (simp (no_asm) split add: split_option_bind del: all_simps)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   270
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   271
apply (rename_tac S1 t1 n2 S2 t2 n3 v)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   272
apply (erule_tac x = "n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   273
apply (erule_tac x = "A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   274
apply (erule_tac x = "S1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   275
apply (erule_tac x = "t1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   276
apply (rotate_tac -1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   277
apply (erule_tac x = "n2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   278
apply (rotate_tac -1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   279
apply (erule_tac x = "v" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   280
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   281
apply (erule allE,erule allE,erule allE,erule allE,erule allE,erule_tac  x = "v" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   282
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   283
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   284
apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   285
apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] free_tv_o_subst [THEN subsetD] W_var_ge dest: less_le_trans)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   286
apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] W_var_ge dest: less_le_trans)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   287
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   288
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   289
lemma weaken_A_Int_B_eq_empty: "(!x. x : A --> x ~: B) ==> A Int B = {}"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   290
apply fast
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   291
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   292
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   293
lemma weaken_not_elem_A_minus_B: "x ~: A | x : B ==> x ~: A - B"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   294
apply fast
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   295
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   296
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   297
(* correctness of W with respect to has_type *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   298
lemma W_correct_lemma [rule_format (no_asm)]: "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   299
apply (induct_tac "e")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   300
(* case Var n *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   301
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   302
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   303
apply (rule has_type.VarI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   304
apply (simp (no_asm))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   305
apply (simp (no_asm) add: is_bound_typ_instance)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   306
apply (rule exI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   307
apply (rule refl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   308
(* case Abs e *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   309
apply (simp add: app_subst_list split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   310
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   311
apply (erule_tac x = " (mk_scheme (TVar n)) # A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   312
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   313
apply (rule has_type.AbsI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   314
apply (drule le_refl [THEN le_SucI, THEN new_scheme_list_le])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   315
apply (drule sym)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   316
apply (erule allE)+
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   317
apply (erule impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   318
apply (erule_tac [2] notE impE, tactic "assume_tac 2")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   319
apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   320
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   321
(* case App e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   322
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   323
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   324
apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   325
apply (rule_tac ?t2.0 = "$ S3 t2" in has_type.AppI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   326
apply (rule_tac S1 = "S3" in app_subst_TVar [THEN subst])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   327
apply (rule app_subst_Fun [THEN subst])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   328
apply (rule_tac t = "$S3 (t2 -> (TVar n2))" and s = "$S3 ($S2 t1) " in subst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   329
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   330
apply (simp only: subst_comp_scheme_list [symmetric] o_def) 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   331
apply ((rule has_type_cl_sub [THEN spec]) , (rule has_type_cl_sub [THEN spec]))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   332
apply (simp add: eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   333
apply (simp add: subst_comp_scheme_list [symmetric] o_def has_type_cl_sub eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   334
apply (rule has_type_cl_sub [THEN spec])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   335
apply (frule new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   336
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   337
apply (drule conjunct1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   338
apply (frule new_tv_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   339
apply (rule new_scheme_list_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   340
apply (rule W_var_ge)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   341
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   342
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   343
apply (erule thin_rl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   344
apply (erule allE)+
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   345
apply (drule sym)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   346
apply (drule sym)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   347
apply (erule thin_rl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   348
apply (erule thin_rl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   349
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   350
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   351
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   352
(* case Let e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   353
apply (simp (no_asm) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   354
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   355
(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   356
apply (rename_tac S1 t1 m1 S2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   357
apply (rule_tac ?t1.0 = "$ S2 t1" in has_type.LETI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   358
 apply (simp (no_asm) add: o_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   359
 apply (simp only: subst_comp_scheme_list [symmetric])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   360
 apply (rule has_type_cl_sub [THEN spec])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   361
 apply (drule_tac x = "A" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   362
 apply (drule_tac x = "S1" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   363
 apply (drule_tac x = "t1" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   364
 apply (drule_tac x = "m1" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   365
 apply (drule_tac x = "n" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   366
 apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   367
 apply (simp add: eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   368
apply (simp (no_asm) add: o_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   369
apply (simp only: subst_comp_scheme_list [symmetric])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   370
apply (rule gen_subst_commutes [symmetric, THEN subst])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   371
 apply (rule_tac [2] app_subst_Cons [THEN subst])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   372
 apply (erule_tac [2] thin_rl)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   373
 apply (drule_tac [2] x = "gen ($S1 A) t1 # $ S1 A" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   374
 apply (drule_tac [2] x = "S2" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   375
 apply (drule_tac [2] x = "t" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   376
 apply (drule_tac [2] x = "m" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   377
 apply (drule_tac [2] x = "m1" in spec)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   378
 apply (frule_tac [2] new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   379
  prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   380
 apply (drule_tac [2] conjunct1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   381
 apply (frule_tac [2] new_tv_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   382
  apply (rule_tac [2] new_scheme_list_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   383
   apply (rule_tac [2] W_var_ge)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   384
   prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   385
  prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   386
 apply (erule_tac [2] impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   387
  apply (rule_tac [2] A = "$ S1 A" in new_tv_only_depends_on_free_tv_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   388
   prefer 2 apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   389
   apply (fast)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   390
  prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   391
 prefer 2 apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   392
apply (rule weaken_A_Int_B_eq_empty)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   393
apply (rule allI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   394
apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   395
apply (rule weaken_not_elem_A_minus_B)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   396
apply (case_tac "x < m1")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   397
 apply (rule disjI2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   398
 apply (rule free_tv_gen_cons [THEN subst])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   399
 apply (rule free_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   400
   apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   401
  apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   402
 apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   403
apply (rule disjI1)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   404
apply (drule new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   405
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   406
apply (drule conjunct2)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   407
apply (rule new_tv_not_free_tv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   408
apply (rule new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   409
 prefer 2 apply (assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   410
apply (simp add: not_less_iff_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   411
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   412
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   413
(* Completeness of W w.r.t. has_type *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   414
lemma W_complete_lemma [rule_format (no_asm)]: 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   415
  "ALL S' A t' n. $S' A |- e :: t' --> new_tv n A -->      
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   416
               (EX S t. (EX m. W e A n = Some (S,t,m)) &   
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   417
                       (EX R. $S' A = $R ($S A) & t' = $R t))"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   418
apply (induct_tac "e")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   419
   (* case Var n *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   420
   apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   421
   apply (simp (no_asm) cong add: conj_cong)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   422
   apply (erule has_type_casesE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   423
   apply (simp add: is_bound_typ_instance)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   424
   apply (erule exE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   425
   apply (hypsubst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   426
   apply (rename_tac "S")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   427
   apply (rule_tac x = "%x. (if x < n then S' x else S (x - n))" in exI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   428
   apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   429
   apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   430
   apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   431
                             del: bound_typ_inst_composed_subst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   432
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   433
  (* case Abs e *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   434
  apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   435
  apply (erule has_type_casesE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   436
  apply (erule_tac x = "%x. if x=n then t1 else (S' x) " in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   437
  apply (erule_tac x = " (FVar n) #A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   438
  apply (erule_tac x = "t2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   439
  apply (erule_tac x = "Suc n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   440
  apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   441
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   442
 (* case App e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   443
 apply (intro strip)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   444
 apply (erule has_type_casesE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   445
 apply (erule_tac x = "S'" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   446
 apply (erule_tac x = "A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   447
 apply (erule_tac x = "t2 -> t'" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   448
 apply (erule_tac x = "n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   449
 apply safe
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   450
 apply (erule_tac x = "R" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   451
 apply (erule_tac x = "$ S A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   452
 apply (erule_tac x = "t2" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   453
 apply (erule_tac x = "m" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   454
 apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   455
 apply safe
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   456
  apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   457
 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   458
 (** LEVEL 33 **)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   459
apply (subgoal_tac "$ (%x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) = $ (%x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) (ta -> (TVar ma))")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   460
apply (rule_tac [2] t = "$ (%x. if x = ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) " and s = " ($ Ra ta) -> t'" in ssubst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   461
prefer 2 apply (simp (no_asm_simp) add: subst_comp_te) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   462
apply (rule_tac [2] eq_free_eq_subst_te)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   463
prefer 2 apply (intro strip) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   464
apply (subgoal_tac [2] "na ~=ma")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   465
 prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   466
apply (case_tac [2] "na:free_tv Sa")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   467
(* n1 ~: free_tv S1 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   468
apply (frule_tac [3] not_free_impl_id)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   469
 prefer 3 apply (simp)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   470
(* na : free_tv Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   471
apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   472
apply (drule_tac [2] eq_subst_scheme_list_eq_free)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   473
 prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   474
prefer 2 apply (simp (no_asm_simp)) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   475
apply (case_tac [2] "na:dom Sa")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   476
(* na ~: dom Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   477
 prefer 3 apply (simp add: dom_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   478
(* na : dom Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   479
apply (rule_tac [2] eq_free_eq_subst_te)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   480
prefer 2 apply (intro strip) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   481
apply (subgoal_tac [2] "nb ~= ma")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   482
apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   483
apply (erule_tac [3] conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   484
apply (drule_tac [3] new_tv_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   485
   prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   486
  prefer 3 apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   487
 prefer 2 apply (fastsimp simp add: cod_def free_tv_subst)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   488
prefer 2 apply (simp (no_asm)) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   489
apply (rule_tac [2] eq_free_eq_subst_te)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   490
prefer 2 apply (intro strip) prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   491
apply (subgoal_tac [2] "na ~= ma")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   492
apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   493
apply (erule_tac [3] conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   494
apply (drule_tac [3] sym [THEN W_var_geD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   495
 prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   496
apply (case_tac [2] "na: free_tv t - free_tv Sa")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   497
(* case na ~: free_tv t - free_tv Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   498
 prefer 3 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   499
 apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   500
 apply fast
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   501
(* case na : free_tv t - free_tv Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   502
prefer 2 apply simp prefer 2
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   503
apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   504
apply (drule_tac [2] eq_subst_scheme_list_eq_free)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   505
 prefer 2 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   506
 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   507
(** LEVEL 73 **)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   508
 prefer 2 apply (simp add: free_tv_subst dom_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   509
apply (simp (no_asm_simp) split add: split_option_bind)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   510
apply safe
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   511
apply (drule mgu_Some)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   512
 apply fastsimp  
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   513
(** LEVEL 78 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   514
apply (drule mgu_mg, assumption)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   515
apply (erule exE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   516
apply (rule_tac x = "Rb" in exI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   517
apply (rule conjI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   518
apply (drule_tac [2] x = "ma" in fun_cong)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   519
 prefer 2 apply (simp add: eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   520
apply (simp (no_asm) add: subst_comp_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   521
apply (simp (no_asm) add: subst_comp_scheme_list [symmetric])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   522
apply (rule_tac A2 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   523
apply (simp add: o_def eq_sym_conv)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   524
apply (drule_tac s = "Some ?X" in sym)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   525
apply (rule eq_free_eq_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   526
apply safe
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   527
apply (subgoal_tac "ma ~= na")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   528
apply (frule_tac [2] new_tv_W) prefer 2 apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   529
apply (erule_tac [2] conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   530
apply (drule_tac [2] new_tv_subst_scheme_list)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   531
 prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   532
apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   533
apply (erule_tac [2] conjE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   534
apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   535
 apply (tactic {* 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   536
   (fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_scheme_list_le", thm "codD",
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   537
   thm "new_tv_not_free_tv"]) 2) *})
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   538
apply (case_tac "na: free_tv t - free_tv Sa")
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   539
(* case na ~: free_tv t - free_tv Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   540
 prefer 2 apply simp apply blast
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   541
(* case na : free_tv t - free_tv Sa *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   542
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   543
apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   544
 apply (fastsimp dest: codD trans [OF _ subst_comp_scheme_list]
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   545
                       eq_subst_scheme_list_eq_free 
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   546
             simp add: free_tv_subst dom_def)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   547
(* case Let e1 e2 *)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   548
apply (erule has_type_casesE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   549
apply (erule_tac x = "S'" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   550
apply (erule_tac x = "A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   551
apply (erule_tac x = "t1" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   552
apply (erule_tac x = "n" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   553
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   554
apply (erule (1) notE impE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   555
apply safe  
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   556
apply (simp (no_asm_simp))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   557
apply (erule_tac x = "R" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   558
apply (erule_tac x = "gen ($ S A) t # $ S A" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   559
apply (erule_tac x = "t'" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   560
apply (erule_tac x = "m" in allE)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   561
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   562
apply (drule mp)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   563
apply (rule has_type_le_env)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   564
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   565
apply (simp (no_asm))
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   566
apply (rule gen_bound_typ_instance)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   567
apply (drule mp)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   568
apply (frule new_tv_compatible_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   569
apply (rule sym)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   570
apply assumption
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   571
apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   572
apply safe
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   573
apply simp
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   574
apply (rule_tac x = "Ra" in exI)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   575
apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric])
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   576
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   577
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   578
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   579
lemma W_complete: "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &   
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   580
                                  (? R. t' = $ R t))"
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   581
apply (cut_tac A = "[]" and S' = "id_subst" and e = "e" and t' = "t'" in W_complete_lemma)
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   582
apply simp_all
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   583
done
b8da5f258b04 converted to Isar
kleing
parents: 5184
diff changeset
   584
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   585
end