61 by (mp_tac 1); |
61 by (mp_tac 1); |
62 by (mp_tac 1); |
62 by (mp_tac 1); |
63 by (etac exE 1); |
63 by (etac exE 1); |
64 by (etac conjE 1); |
64 by (etac conjE 1); |
65 by (etac impE 1); |
65 by (etac impE 1); |
66 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
66 by ((ftac new_tv_subst_tel 1) THEN (atac 1)); |
67 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
67 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
68 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
68 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
69 addss simpset()) 1); |
69 addss simpset()) 1); |
70 by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel])) 1); |
70 by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel])) 1); |
71 (** LEVEL 45 **) |
71 (** LEVEL 45 **) |
76 by (mp_tac 1); |
76 by (mp_tac 1); |
77 by (mp_tac 1); |
77 by (mp_tac 1); |
78 by (etac exE 1); |
78 by (etac exE 1); |
79 by (etac conjE 1); |
79 by (etac conjE 1); |
80 by (etac impE 1); |
80 by (etac impE 1); |
81 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
81 by ((ftac new_tv_subst_tel 1) THEN (atac 1)); |
82 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
82 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
83 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
83 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
84 addss simpset()) 1); |
84 addss simpset()) 1); |
85 by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel,subst_comp_te])) 1); |
85 by (fast_tac (HOL_cs addss (simpset() addsimps [subst_comp_tel,subst_comp_te])) 1); |
86 by (strip_tac 1); |
86 by (strip_tac 1); |
88 (** LEVEL 60 **) |
88 (** LEVEL 60 **) |
89 by (mp_tac 1); |
89 by (mp_tac 1); |
90 by (etac exE 1); |
90 by (etac exE 1); |
91 by (etac conjE 1); |
91 by (etac conjE 1); |
92 by (etac impE 1); |
92 by (etac impE 1); |
93 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
93 by ((ftac new_tv_subst_tel 1) THEN (atac 1)); |
94 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
94 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
95 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
95 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
96 addss simpset()) 1); |
96 addss simpset()) 1); |
97 by (mp_tac 1); |
97 by (mp_tac 1); |
98 by (REPEAT (eresolve_tac [exE,conjE] 1)); |
98 by (REPEAT (eresolve_tac [exE,conjE] 1)); |
100 [asm_full_simp_tac (simpset() addsimps [subst_comp_tel,subst_comp_te,o_def]), |
100 [asm_full_simp_tac (simpset() addsimps [subst_comp_tel,subst_comp_te,o_def]), |
101 REPEAT o etac conjE, hyp_subst_tac])); |
101 REPEAT o etac conjE, hyp_subst_tac])); |
102 (** LEVEL 70 **) |
102 (** LEVEL 70 **) |
103 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1); |
103 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1); |
104 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
104 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
105 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); |
105 by ((ftac new_tv_subst_tel 1) THEN (atac 1)); |
106 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
106 by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); |
107 by (safe_tac HOL_cs); |
107 by (safe_tac HOL_cs); |
108 by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
108 by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
109 addss simpset()) 1); |
109 addss simpset()) 1); |
110 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |
110 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] |