equal
deleted
inserted
replaced
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"; |