[isabelle] Anonymous functions, image, and inductive sets problem



Friends -
I'm stuck, so I'm asking for help.  I have a somewhat complex mutually inductive set definition, that I have carved down to a (nonsensical) minimum, and when I try to run the definitions I get the following mess when Isabelle is attempting to prove monotonicity.  I'm hoping that someone can point me in the right direction...

Note: I need to use an anonymous function here because (in the real version) I refer to other variables outside of the function.

The definitions follow:

theory test
imports Main
begin

typedecl "ExnMech"
datatype "PrimEff" = exception  "ExnMech"
type_synonym "Effects" = "(PrimEff set)"

inductive_set
  "mechanismshavetype" :: "(Effects * Effects) set" and
  "exnshavetype" :: "(Effects * Effects) set"
where
Exn_types: " 
  [| oepsilons = 
     (\<lambda> f . (if (epsilon_91, epsilon_93) \<in> mechanismshavetype
             then Some epsilon_91
             else None)) `
     epsilon_91 |]
  ==>
  (epsilon_91, {}) \<in> exnshavetype"

end


and the result from Isabelle is:

*** Proof failed.
*** mono (\<lambda>p b x1 x2.
***          \<exists>oepsilons epsilon_91 epsilon_93.
***             b \<and> x1 = epsilon_91 \<and>
***                 x2 = {} \<and>
***                 oepsilons = (\<lambda>f. if p False epsilon_91 epsilon_93 then Some epsilon_91 else None) ` epsilon_91)
***  1. \<And>x y xa xb xc oepsilons epsilon_91 epsilon_93.
***        x (?x14 x y xa xb xc oepsilons epsilon_91 epsilon_93) (?x15 x y xa xb xc oepsilons epsilon_91 epsilon_93)
***         (?x16 x y xa xb xc oepsilons epsilon_91 epsilon_93) \<longrightarrow>
***        y (?x14 x y xa xb xc oepsilons epsilon_91 epsilon_93) (?x15 x y xa xb xc oepsilons epsilon_91 epsilon_93)
***         (?x16 x y xa xb xc oepsilons epsilon_91 epsilon_93) \<Longrightarrow>
***        oepsilons = (\<lambda>f. if x False epsilon_91 epsilon_93 then Some epsilon_91 else None) ` epsilon_91 \<longrightarrow>
***        oepsilons = (\<lambda>f. if y False epsilon_91 epsilon_93 then Some epsilon_91 else None) ` epsilon_91
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** mono (\<lambda>p b x1 x2.
***          \<exists>oepsilons epsilon_91 epsilon_93.
***             b \<and> x1 = epsilon_91 \<and>
***                 x2 = {} \<and>
***                 oepsilons = (\<lambda>f. if p False epsilon_91 epsilon_93 then Some epsilon_91 else None) ` epsilon_91)
***  (line 9 of "/Users/ridgway/NewRIPLS/FICS2008/test.thy")
*** At command "inductive_set" (line 9 of "/Users/ridgway/NewRIPLS/FICS2008/test.thy")


Peace
- John






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