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 "!!a e t. a |- e :: t ==> $s a |- e :: $s t"; |
14 Goal "!!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); |