equal
deleted
inserted
replaced
122 lemma norm_Rep [simp]: "norm (Rep x) = Rep x" |
122 lemma norm_Rep [simp]: "norm (Rep x) = Rep x" |
123 by (auto simp: eq_norm' intro: td_th) |
123 by (auto simp: eq_norm' intro: td_th) |
124 |
124 |
125 lemmas td = td_thm |
125 lemmas td = td_thm |
126 |
126 |
127 lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w" |
127 lemma set_iff_norm: "w \<in> A \<longleftrightarrow> w = norm w" |
128 by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
128 by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
129 |
129 |
130 lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
130 lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
131 apply (rule iffI) |
131 apply (rule iffI) |
132 apply (clarsimp simp add: eq_norm) |
132 apply (clarsimp simp add: eq_norm) |