Email Gateway (Aug 18 2022 at 12:40): Email Gateway (Aug 18 2022 at 12:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi David,
In such cases extensionality is the way to go: thm ext. Attached I have
two ways to employ it: either directly as (rule ext), which I recommend
in cases which require an Isar proof, or by means thm expand_fun_eq
which is handy for proofs which can be done automatically by simp (or
auto or clarsimp or ...).
Hope this helps
Florian
--
theory Hold
imports Main
begin
locale D_po =
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes D :: "'a set"
begin
abbreviation lle :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl
"\<sqsubseteq>" 100) where
"x \<sqsubseteq> y \<equiv> le x y"
definition downclosed where
"downclosed I \<longleftrightarrow> I \<subseteq> D \<and> (\<forall>x
y . (x \<in> I \<and> y \<in> D \<and> y \<sqsubseteq> x)
\<longrightarrow> y \<in> I)"
definition ub where
"ub S a \<longleftrightarrow> a \<in> D \<and> (\<forall>x\<in>S. x
\<sqsubseteq> a)"
definition lub where
"lub S d \<longleftrightarrow> ub S d \<and> (\<forall>a. ub S a
\<longrightarrow> d \<sqsubseteq> a)"
definition Directed where
"Directed S \<longleftrightarrow> S \<noteq> {} \<and> S \<subseteq> D
\<and> (\<forall>f g. (f \<in> S \<and> g \<in> S) \<longrightarrow>
(\<exists>l. ub {f, g} l \<and> l \<in> S))"
definition ideal where
"ideal I \<longleftrightarrow> Directed I \<and> downclosed I"
end
locale D_bpo = D_po +
fixes idall :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
and my_subset:: "('a \<Rightarrow> bool) \<Rightarrow> ('a
\<Rightarrow> bool) \<Rightarrow> bool"
defines Ideals: "idall \<equiv> {I:: ('a \<Rightarrow> bool) .
(D_po.ideal le D I)}"
defines relative: "my_subset x y \<equiv> x \<subseteq> y \<and> x
\<in> idall \<and> y \<in> idall"
locale D_cpo = D_bpo +
assumes compass: "\<forall>S. D_po.Directed le D S \<longrightarrow>
(\<exists> l. D_po.lub le D S l)"
locale bpo_ideal = D_bpo le D idall my_subset + D_cpo my_subset idall
idid ididsub
interpretation bpo_ideal \<subseteq> D_bpo .
interpretation D_bpo \<subseteq> bpo_ideal
proof -
show bopi: "bpo_ideal op \<sqsubseteq> D"
proof
show "\<forall>S. D_po.Directed (\<lambda>x y. x \<subseteq> y
\<and> x \<in> {I. D_po.ideal op \<sqsubseteq> D I} \<and> y \<in> {I.
D_po.ideal op \<sqsubseteq> D I})
{I. D_po.ideal op \<sqsubseteq> D I} S \<longrightarrow>
(\<exists>l. D_po.lub (\<lambda>x y. x \<subseteq> y \<and> x
\<in> {I. D_po.ideal op \<sqsubseteq> D I} \<and> y \<in> {I. D_po.ideal
op \<sqsubseteq> D I})
{I. D_po.ideal op \<sqsubseteq> D I} S l)" sorry
qed
-- {* Alt. 1: rule ext *}
have "my_subset = (\<lambda>x y. x \<subseteq> y \<and> x \<in> idall
\<and> y \<in> idall)"
proof (rule ext)+
fix x y
show "my_subset x y \<longleftrightarrow> x \<subseteq> y \<and> x
\<in> idall \<and> y \<in> idall"
by (simp add: relative)
qed
-- {* Alt. 2: expand_fun_eq *}
have "my_subset = (\<lambda>x y. x \<subseteq> y \<and> x \<in> idall
\<and> y \<in> idall)"
by (simp add: expand_fun_eq relative)
qed
--
Home:
http://wwwbroy.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Last updated: May 03 2024 at 04:19 UTC