src/HOL/MiniML/MiniML.ML
changeset 1743 f7feaacd33d3
parent 1525 d127436567d0
child 2031 03a843f0f447
equal deleted inserted replaced
1742:328fb06a1648 1743:f7feaacd33d3
     9 Addsimps has_type.intrs;
     9 Addsimps has_type.intrs;
    10 Addsimps [Un_upper1,Un_upper2];
    10 Addsimps [Un_upper1,Un_upper2];
    11 
    11 
    12 
    12 
    13 (* has_type is closed w.r.t. substitution *)
    13 (* has_type is closed w.r.t. substitution *)
    14 goal MiniML.thy
    14 goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
    15      "!a e t. a |- e :: t --> $s a |- e :: $s t";
    15 by (etac has_type.induct 1);
    16 by (rtac has_type.mutual_induct 1);
       
    17 (* case VarI *)
    16 (* case VarI *)
    18 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
    17 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
    19 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
    18 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);
    19 by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
    21 (* case AbsI *)
    20 (* case AbsI *)
    22 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
    21 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
    23 (* case AppI *)
    22 (* case AppI *)
    24 by (Asm_full_simp_tac 1);
    23 by (Asm_full_simp_tac 1);
    25 qed_spec_mp "has_type_cl_sub";
    24 qed "has_type_cl_sub";