equal
deleted
inserted
replaced
134 |
134 |
135 lemma transfer_if [transfer_intro]: |
135 lemma transfer_if [transfer_intro]: |
136 "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> |
136 "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> |
137 \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)" |
137 \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)" |
138 apply (rule eq_reflection) |
138 apply (rule eq_reflection) |
139 apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1) |
139 apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_mono) |
140 done |
140 done |
141 |
141 |
142 lemma transfer_fun_eq [transfer_intro]: |
142 lemma transfer_fun_eq [transfer_intro]: |
143 "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) |
143 "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) |
144 \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk> |
144 \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk> |