48 by (simp_tac (simpset() addsplits [split_bind]) 1); |
48 by (simp_tac (simpset() addsplits [split_bind]) 1); |
49 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
49 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
50 (* case App e1 e2 *) |
50 (* case App e1 e2 *) |
51 by (simp_tac (simpset() addsplits [split_bind]) 1); |
51 by (simp_tac (simpset() addsplits [split_bind]) 1); |
52 by (strip_tac 1); |
52 by (strip_tac 1); |
53 by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
53 by (rename_tac "s t na sa ta nb sb" 1); |
54 by (eres_inst_tac [("x","a")] allE 1); |
54 by (eres_inst_tac [("x","a")] allE 1); |
55 by (eres_inst_tac [("x","n")] allE 1); |
55 by (eres_inst_tac [("x","n")] allE 1); |
56 by (eres_inst_tac [("x","$ s a")] allE 1); |
56 by (eres_inst_tac [("x","$ s a")] allE 1); |
57 by (eres_inst_tac [("x","s")] allE 1); |
57 by (eres_inst_tac [("x","s")] allE 1); |
58 by (eres_inst_tac [("x","t")] allE 1); |
58 by (eres_inst_tac [("x","t")] allE 1); |
59 by (eres_inst_tac [("x","na")] allE 1); |
59 by (eres_inst_tac [("x","na")] allE 1); |
60 by (eres_inst_tac [("x","na")] allE 1); |
60 by (eres_inst_tac [("x","na")] allE 1); |
61 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
61 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
62 by (etac conjE 1); |
|
63 by (eres_inst_tac [("x","sa")] allE 1); |
62 by (eres_inst_tac [("x","sa")] allE 1); |
64 by (eres_inst_tac [("x","ta")] allE 1); |
63 by (eres_inst_tac [("x","ta")] allE 1); |
65 by (eres_inst_tac [("x","nb")] allE 1); |
64 by (eres_inst_tac [("x","nb")] allE 1); |
66 by (Asm_full_simp_tac 1); |
65 by (Asm_full_simp_tac 1); |
67 qed_spec_mp "W_var_ge"; |
66 qed_spec_mp "W_var_ge"; |
97 addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
96 addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
98 |
97 |
99 (* case App e1 e2 *) |
98 (* case App e1 e2 *) |
100 by (simp_tac (simpset() addsplits [split_bind]) 1); |
99 by (simp_tac (simpset() addsplits [split_bind]) 1); |
101 by (strip_tac 1); |
100 by (strip_tac 1); |
102 by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
101 by (rename_tac "s t na sa ta nb sb" 1); |
103 by (eres_inst_tac [("x","n")] allE 1); |
102 by (eres_inst_tac [("x","n")] allE 1); |
104 by (eres_inst_tac [("x","a")] allE 1); |
103 by (eres_inst_tac [("x","a")] allE 1); |
105 by (eres_inst_tac [("x","s")] allE 1); |
104 by (eres_inst_tac [("x","s")] allE 1); |
106 by (eres_inst_tac [("x","t")] allE 1); |
105 by (eres_inst_tac [("x","t")] allE 1); |
107 by (eres_inst_tac [("x","na")] allE 1); |
106 by (eres_inst_tac [("x","na")] allE 1); |