[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.

    kind regards david streader
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.