equal
deleted
inserted
replaced
157 |
157 |
158 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> |
158 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> |
159 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" |
159 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" |
160 unfolding Grp_def by rule auto |
160 unfolding Grp_def by rule auto |
161 |
161 |
|
162 lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)" |
|
163 by fastforce |
|
164 |
162 lemma if_if_True: |
165 lemma if_if_True: |
163 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = |
166 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) = |
164 (if b then x else if b' then x' else f y')" |
167 (if b then x else if b' then x' else f y')" |
165 by simp |
168 by simp |
166 |
169 |