equal
deleted
inserted
replaced
78 by simp |
78 by simp |
79 |
79 |
80 lemma ch2ch_Pair [simp]: "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))" |
80 lemma ch2ch_Pair [simp]: "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))" |
81 by (rule chainI, simp add: chainE) |
81 by (rule chainI, simp add: chainE) |
82 |
82 |
83 text \<open>@{term fst} and @{term snd} are monotone\<close> |
83 text \<open>\<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> are monotone\<close> |
84 |
84 |
85 lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y" |
85 lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y" |
86 by (simp add: below_prod_def) |
86 by (simp add: below_prod_def) |
87 |
87 |
88 lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y" |
88 lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y" |