equal
deleted
inserted
replaced
49 |
49 |
50 goalw thy [dom_def,cod_def,UNION_def,Bex_def] |
50 goalw thy [dom_def,cod_def,UNION_def,Bex_def] |
51 "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s"; |
51 "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s"; |
52 by (Simp_tac 1); |
52 by (Simp_tac 1); |
53 by (safe_tac (empty_cs addSIs [exI,conjI,notI])); |
53 by (safe_tac (empty_cs addSIs [exI,conjI,notI])); |
54 ba 2; |
54 by (assume_tac 2); |
55 by (rotate_tac 1 1); |
55 by (rotate_tac 1 1); |
56 by (Asm_full_simp_tac 1); |
56 by (Asm_full_simp_tac 1); |
57 qed "cod_app_subst"; |
57 qed "cod_app_subst"; |
58 Addsimps [cod_app_subst]; |
58 Addsimps [cod_app_subst]; |
59 |
59 |
133 by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
133 by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
134 qed "new_tv_subst"; |
134 qed "new_tv_subst"; |
135 |
135 |
136 goal thy |
136 goal thy |
137 "new_tv n = list_all (new_tv n)"; |
137 "new_tv n = list_all (new_tv n)"; |
138 br ext 1; |
138 by (rtac ext 1); |
139 by(list.induct_tac "x" 1); |
139 by(list.induct_tac "x" 1); |
140 by(ALLGOALS Asm_simp_tac); |
140 by(ALLGOALS Asm_simp_tac); |
141 qed "new_tv_list"; |
141 qed "new_tv_list"; |
142 |
142 |
143 (* substitution affects only variables occurring freely *) |
143 (* substitution affects only variables occurring freely *) |