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.