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