equal
deleted
inserted
replaced
188 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
188 Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
189 |
189 |
190 Goal |
190 Goal |
191 "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s"; |
191 "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s"; |
192 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
192 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); |
193 by (rtac conjI 1); |
193 by (Clarify_tac 1); |
194 by (slow_tac (HOL_cs addIs [le_trans]) 1); |
|
195 by (safe_tac HOL_cs ); |
|
196 by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1); |
194 by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1); |
197 by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1); |
195 by (Clarify_tac 1); |
198 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) ); |
196 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) ); |
199 qed "new_tv_subst_le"; |
197 qed "new_tv_subst_le"; |
200 Addsimps [lessI RS less_imp_le RS new_tv_subst_le]; |
198 Addsimps [lessI RS less_imp_le RS new_tv_subst_le]; |
201 |
199 |
202 (* new_tv property remains if a substitution is applied *) |
200 (* new_tv property remains if a substitution is applied *) |