# [isabelle] interpretations and lambda terms

```Hi
```
I have been using locales very happily for some months but Have a problem that I can not see a way around.
```
```
One of the parameters "my_subset" in a locale expression appears as a lambda term when trying to prove an interpretation but I fail to see why or how I can reason about it.
```
definition ideal  where "ideal I = (Directed I \<and> downclosed I)"
```
defines relative: "my_subset x y \<equiv> x \<subseteq> y \<and> x\<in>idall \<and> y\<in> idall"
```
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})
```
I am at a loss how to proceed?

A cut down theory file is attached.

```
```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 = (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 =  ((a\<in> D)\<and> (\<forall> x\<in> S. x  \<sqsubseteq> a))"
definition lub where "lub  S d =  (ub S d \<and> (\<forall> a. ub S a \<longrightarrow> d \<sqsubseteq> a))"
definition Directed where "Directed S = (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 = (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
from    my_subset_def have  "my_subset = (\<lambda>x y. x \<subseteq> y \<and> x \<in> idall \<and> y \<in> idall)"
sorry ```

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