equal
deleted
inserted
replaced
14 goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t"; |
14 goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t"; |
15 by (etac has_type.induct 1); |
15 by (etac has_type.induct 1); |
16 (* case VarI *) |
16 (* case VarI *) |
17 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
17 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
18 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 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); |
19 by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1); |
20 (* case AbsI *) |
20 (* case AbsI *) |
21 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
21 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
22 (* case AppI *) |
22 (* case AppI *) |
23 by (Asm_full_simp_tac 1); |
23 by (Asm_full_simp_tac 1); |
24 qed "has_type_cl_sub"; |
24 qed "has_type_cl_sub"; |