# Re: [isabelle] Anonymous functions, image, and inductive sets problem

```Friends -
I did some more poking and simplified my definitions more, and still have trouble.  Here are the updated definitions and output from Isabelle.

Definitions:
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 =
(if (epsilon_91, epsilon_93) \<in> mechanismshavetype
then epsilon_91
else {}) |]
==>
(epsilon_91, {}) \<in> exnshavetype"
end

and the output from Isabelle:
*** Proof failed.
*** mono (\<lambda>p b x1 x2.
***          \<exists>oepsilons epsilon_91 epsilon_93.
***             b \<and> x1 = epsilon_91 \<and> x2 = {} \<and> oepsilons = (if p False epsilon_91 epsilon_93 then epsilon_91 else {}))
***  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 = (if x False epsilon_91 epsilon_93 then epsilon_91 else {}) \<longrightarrow>
***        oepsilons = (if y False epsilon_91 epsilon_93 then epsilon_91 else {})
*** 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 = (if p False epsilon_91 epsilon_93 then epsilon_91 else {}))
***  (line 9 of "/Users/ridgway/NewRIPLS/FICS2008/test.thy")
*** At command "inductive_set" (line 9 of "/Users/ridgway/NewRIPLS/FICS2008/test.thy")

Peace
- John

On Feb 5, 2012, at 8:36 PM, John Ridgway wrote:

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