src/HOL/MiniML/Instance.ML
author wenzelm
Fri, 10 Oct 1997 19:02:28 +0200
changeset 3842 b55686a7b22c
parent 3018 e65b60b28341
child 3919 c036caebfc75
permissions -rw-r--r--
fixed dots;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Instance.ML
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     2
   ID:        $Id$
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     4
   Copyright  1996 TU Muenchen
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     5
*)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     6
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     7
(* lemmatas for instatiation *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     8
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     9
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    10
(* lemmatas for bound_typ_inst *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    11
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    12
goal thy "bound_typ_inst S (mk_scheme t) = t";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    13
by (typ.induct_tac "t" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    14
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    15
qed "bound_typ_inst_mk_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    16
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    17
Addsimps [bound_typ_inst_mk_scheme];
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    18
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    19
goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    20
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    21
by (ALLGOALS Asm_full_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    22
qed "bound_typ_inst_composed_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    23
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    24
Addsimps [bound_typ_inst_composed_subst];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    25
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    26
goal thy "!!S. S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    27
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    28
qed "bound_typ_inst_eq";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    29
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    30
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    31
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    32
(* lemmatas for bound_scheme_inst *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    33
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    34
goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    35
by (typ.induct_tac "t" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    36
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    37
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    38
qed "bound_scheme_inst_mk_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    39
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    40
Addsimps [bound_scheme_inst_mk_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    41
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    42
goal thy "!!S. $S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    43
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    44
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    45
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    46
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    47
qed "substitution_lemma";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    48
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    49
goal thy "!t. mk_scheme t = bound_scheme_inst B sch --> \
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    50
\         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    51
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    52
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    53
by (safe_tac (!claset));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    54
by (rtac exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    55
by (rtac ballI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    56
by (rtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    57
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    58
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    59
by (dtac mk_scheme_Fun 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    60
by (REPEAT (etac exE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    61
by (etac conjE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    62
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    63
by (dtac sym 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    64
by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    65
by (safe_tac (!claset));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    66
by (rename_tac "S1 S2" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    67
by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    68
by (safe_tac (!claset));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    69
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    70
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    71
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    72
by (dres_inst_tac [("x","x")] bspec 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
    73
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    74
by (dres_inst_tac [("x","x")] bspec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    75
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    76
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    77
qed_spec_mp "bound_scheme_inst_type";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    78
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    79
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    80
(* lemmatas for subst_to_scheme *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    81
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    82
goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    83
\                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    84
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    85
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    86
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    87
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    88
qed_spec_mp "subst_to_scheme_inverse";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    89
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    90
goal thy "!!t t'. t = t' ==> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    91
\                            subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    92
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    93
val aux = result ();
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    94
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    95
goal thy "new_tv n sch --> \
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    96
\        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    97
\                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    98
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    99
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   100
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   101
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   102
val aux2 = result () RS mp;
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   103
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   104
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   105
(* lemmata for <= *)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   106
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   107
goalw thy [le_type_scheme_def,is_bound_typ_instance]
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   108
      "!!(sch::type_scheme) sch'. (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   109
by (rtac iffI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   110
by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   111
by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   112
by (dtac make_one_new_out_of_two 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   113
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   114
by (thin_tac "? n. new_tv n sch'" 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   115
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   116
by (etac allE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   117
by (dtac mp 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   118
by (res_inst_tac [("x","(%k. TVar (k + n))")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   119
by (rtac refl 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   120
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   121
by (REPEAT (etac conjE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   122
by (dres_inst_tac [("n","n")] aux 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   123
by (asm_full_simp_tac (!simpset addsimps [subst_to_scheme_inverse]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   124
by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   125
by (asm_simp_tac (!simpset addsimps [aux2]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   126
by (safe_tac (!claset));
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   127
by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   128
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   129
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   130
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   131
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   132
qed "le_type_scheme_def2";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   133
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   134
goalw thy [is_bound_typ_instance] "(mk_scheme t) <= sch = t <| sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   135
by (simp_tac (!simpset addsimps [le_type_scheme_def2]) 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   136
by (rtac iffI 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   137
by (etac exE 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   138
by (forward_tac [bound_scheme_inst_type] 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   139
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   140
by (rtac exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   141
by (rtac mk_scheme_injective 1); 
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   142
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   143
by (rotate_tac 1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   144
by (rtac mp 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   145
by (assume_tac 2);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   146
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   147
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   148
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   149
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   150
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   151
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   152
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   153
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   154
by (rtac exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   155
by (type_scheme.induct_tac "sch" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   156
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   157
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   158
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   159
qed_spec_mp "le_type_eq_is_bound_typ_instance";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   160
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   161
goalw thy [le_env_def]
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   162
  "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   163
by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   164
by (rtac iffI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   165
 by (SELECT_GOAL(safe_tac (!claset))1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   166
  by (eres_inst_tac [("x","0")] allE 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   167
  by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   168
 by (eres_inst_tac [("x","Suc i")] allE 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   169
 by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   170
by (rtac conjI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   171
 by (Fast_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   172
by (rtac allI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   173
by (nat_ind_tac "i" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   174
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   175
qed "le_env_Cons";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   176
AddIffs [le_env_Cons];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   177
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   178
goalw thy [is_bound_typ_instance]"!!t. t <| sch ==> $S t <| $S sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   179
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   180
by (rename_tac "SA" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   181
by (hyp_subst_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   182
by (res_inst_tac [("x","$S o SA")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   183
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   184
qed "is_bound_typ_instance_closed_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   185
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   186
goal thy "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   187
by (asm_full_simp_tac (!simpset addsimps [le_type_scheme_def2]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   188
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   189
by (asm_full_simp_tac (!simpset addsimps [substitution_lemma]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   190
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   191
qed "S_compatible_le_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   192
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   193
goalw thy [le_env_def,app_subst_list] "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   194
by (simp_tac (!simpset addcongs [conj_cong]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   195
by (fast_tac (!claset addSIs [S_compatible_le_scheme]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   196
qed "S_compatible_le_scheme_lists";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   197
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   198
goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   199
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   200
qed "bound_typ_instance_trans";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   201
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   202
goalw thy [le_type_scheme_def] "sch <= (sch::type_scheme)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   203
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   204
qed "le_type_scheme_refl";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   205
AddIffs [le_type_scheme_refl];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   206
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   207
goalw thy [le_env_def] "A <= (A::type_scheme list)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   208
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   209
qed "le_env_refl";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   210
AddIffs [le_env_refl];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   211
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   212
goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   213
by (strip_tac 1);
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3018
diff changeset
   214
by (res_inst_tac [("x","%a. t")]exI 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   215
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   216
qed "bound_typ_instance_BVar";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   217
AddIffs [bound_typ_instance_BVar];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   218
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   219
goalw thy [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   220
by (type_scheme.induct_tac "sch" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   221
  by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   222
 by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   223
 by (SELECT_GOAL(safe_tac(!claset))1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   224
 by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   225
 by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   226
 by (Fast_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   227
by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   228
by (rtac iffI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   229
 by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   230
 by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   231
 by (Fast_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   232
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   233
qed "le_FVar";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   234
Addsimps [le_FVar];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   235
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   236
goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   237
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   238
qed "not_FVar_le_Fun";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   239
AddIffs [not_FVar_le_Fun];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   240
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   241
goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   242
by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   243
by (res_inst_tac [("x","TVar n")] exI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   244
by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   245
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   246
qed "not_BVar_le_Fun";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   247
AddIffs [not_BVar_le_Fun];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   248
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   249
goalw thy [le_type_scheme_def,is_bound_typ_instance]
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   250
  "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   251
by (fast_tac (!claset addss !simpset) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   252
qed "Fun_le_FunD";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   253
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   254
goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   255
by (type_scheme.induct_tac "sch'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   256
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   257
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   258
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   259
qed_spec_mp "scheme_le_Fun";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   260
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   261
goal thy "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   262
by (type_scheme.induct_tac "sch" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   263
  by (rtac allI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   264
  by (type_scheme.induct_tac "sch'" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   265
    by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   266
   by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   267
  by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   268
 by (rtac allI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   269
 by (type_scheme.induct_tac "sch'" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   270
   by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   271
  by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   272
 by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   273
by (rtac allI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   274
by (type_scheme.induct_tac "sch'" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   275
  by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   276
 by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   277
by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   278
by (strip_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   279
by (dtac Fun_le_FunD 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   280
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   281
qed_spec_mp "le_type_scheme_free_tv";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   282
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   283
goal thy "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
3018
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   284
by (list.induct_tac "B" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   285
 by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   286
by (rtac allI 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   287
by (list.induct_tac "A" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   288
 by (simp_tac (!simpset addsimps [le_env_def]) 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   289
by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2625
diff changeset
   290
by (fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   291
qed_spec_mp "le_env_free_tv";