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


14 
goal MiniML.thy


15 
"!a e t. (a  e :: t) > ($ s a  e :: $ s t)";


16 
by (rtac has_type.mutual_induct 1);


17 
(* case VarI *)


18 
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);


19 
by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);


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


21 
(* case AbsI *)


22 
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);


23 
(* case AppI *)


24 
by (Asm_full_simp_tac 1);


25 
bind_thm ("has_type_cl_sub", result() RS spec RS spec RS spec RS mp);
