Re: [isabelle] interpretations and lambda terms



Hi David,

> The term that appears is
> \<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})

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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.