src/HOL/MiniML/MiniML.ML
changeset 1300 c7a8f374339b
child 1521 4ed3004ff75e
equal deleted inserted replaced
1299:e74f694ca1da 1300:c7a8f374339b
       
     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);