1300
|
1 |
(* Title: HOL/MiniML/MiniML.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Dieter Nazareth and Tobias Nipkow
|
|
4 |
Copyright 1995 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
open MiniML;
|
|
8 |
|
|
9 |
Addsimps has_type.intrs;
|
|
10 |
Addsimps [Un_upper1,Un_upper2];
|
|
11 |
|
|
12 |
|
|
13 |
(* has_type is closed w.r.t. substitution *)
|
1743
|
14 |
goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
|
|
15 |
by (etac has_type.induct 1);
|
1300
|
16 |
(* case VarI *)
|
|
17 |
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
|
|
18 |
by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
|
2031
|
19 |
by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
|
1300
|
20 |
(* case AbsI *)
|
|
21 |
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
|
|
22 |
(* case AppI *)
|
|
23 |
by (Asm_full_simp_tac 1);
|
1743
|
24 |
qed "has_type_cl_sub";
|