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);


19 
by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);


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";
