equal
deleted
inserted
replaced
106 (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) |
106 (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) |
107 THEN' asm_full_simp_tac (ss2 addsimps ths) |
107 THEN' asm_full_simp_tac (ss2 addsimps ths) |
108 in |
108 in |
109 Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) |
109 Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths))) |
110 end |
110 end |
111 *} "Lifts trivial vector statements to real arith statements" |
111 *} "lift trivial vector statements to real arith statements" |
112 |
112 |
113 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) |
113 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) |
114 lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) |
114 lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) |
115 |
115 |
116 lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector |
116 lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector |