equal
deleted
inserted
replaced
25 show "f \<sqsubseteq> f" |
25 show "f \<sqsubseteq> f" |
26 by (simp add: below_fun_def) |
26 by (simp add: below_fun_def) |
27 next |
27 next |
28 fix f g :: "'a \<Rightarrow> 'b" |
28 fix f g :: "'a \<Rightarrow> 'b" |
29 assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g" |
29 assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g" |
30 by (simp add: below_fun_def ext_iff below_antisym) |
30 by (simp add: below_fun_def fun_eq_iff below_antisym) |
31 next |
31 next |
32 fix f g h :: "'a \<Rightarrow> 'b" |
32 fix f g h :: "'a \<Rightarrow> 'b" |
33 assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h" |
33 assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h" |
34 unfolding below_fun_def by (fast elim: below_trans) |
34 unfolding below_fun_def by (fast elim: below_trans) |
35 qed |
35 qed |
101 |
101 |
102 instance "fun" :: (type, discrete_cpo) discrete_cpo |
102 instance "fun" :: (type, discrete_cpo) discrete_cpo |
103 proof |
103 proof |
104 fix f g :: "'a \<Rightarrow> 'b" |
104 fix f g :: "'a \<Rightarrow> 'b" |
105 show "f \<sqsubseteq> g \<longleftrightarrow> f = g" |
105 show "f \<sqsubseteq> g \<longleftrightarrow> f = g" |
106 unfolding expand_fun_below ext_iff |
106 unfolding expand_fun_below fun_eq_iff |
107 by simp |
107 by simp |
108 qed |
108 qed |
109 |
109 |
110 text {* chain-finite function spaces *} |
110 text {* chain-finite function spaces *} |
111 |
111 |
112 lemma maxinch2maxinch_lambda: |
112 lemma maxinch2maxinch_lambda: |
113 "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" |
113 "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" |
114 unfolding max_in_chain_def ext_iff by simp |
114 unfolding max_in_chain_def fun_eq_iff by simp |
115 |
115 |
116 lemma maxinch_mono: |
116 lemma maxinch_mono: |
117 "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y" |
117 "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y" |
118 unfolding max_in_chain_def |
118 unfolding max_in_chain_def |
119 proof (intro allI impI) |
119 proof (intro allI impI) |