equal
deleted
inserted
replaced
27 by (list.induct_tac "ts" 1); |
27 by (list.induct_tac "ts" 1); |
28 by (ALLGOALS Asm_simp_tac); |
28 by (ALLGOALS Asm_simp_tac); |
29 qed "app_subst_id_tel"; |
29 qed "app_subst_id_tel"; |
30 Addsimps [app_subst_id_tel]; |
30 Addsimps [app_subst_id_tel]; |
31 |
31 |
|
32 goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s"; |
|
33 br ext 1; |
|
34 by(Simp_tac 1); |
|
35 qed "o_id_subst"; |
|
36 Addsimps[o_id_subst]; |
|
37 |
32 goalw thy [dom_def,id_subst_def,empty_def] |
38 goalw thy [dom_def,id_subst_def,empty_def] |
33 "dom id_subst = {}"; |
39 "dom id_subst = {}"; |
34 by (Simp_tac 1); |
40 by (Simp_tac 1); |
35 qed "dom_id_subst"; |
41 qed "dom_id_subst"; |
36 Addsimps [dom_id_subst]; |
42 Addsimps [dom_id_subst]; |
109 by (fast_tac (HOL_cs addss !simpset) 1); |
115 by (fast_tac (HOL_cs addss !simpset) 1); |
110 qed "new_tv_Cons"; |
116 qed "new_tv_Cons"; |
111 |
117 |
112 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
118 Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
113 |
119 |
|
120 goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
|
121 "new_tv n id_subst"; |
|
122 by(Simp_tac 1); |
|
123 qed "new_tv_id_subst"; |
|
124 Addsimps[new_tv_id_subst]; |
114 |
125 |
115 goalw thy [new_tv_def] |
126 goalw thy [new_tv_def] |
116 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
127 "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
117 \ (! l. l < n --> new_tv n (s l) ))"; |
128 \ (! l. l < n --> new_tv n (s l) ))"; |
118 by( safe_tac HOL_cs ); |
129 by( safe_tac HOL_cs ); |