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



Inductive definitions must be monotone. The standard way of ensuring
this is to stick to the standard format: all conclusions are of the form
"term : ind_set" and all premises are of the same form or are side
conditions, i.e. do not mention ind_pred. This format can be liberalised
a little by allowing quantifiers and implications of a certain format.
However, your definition is rather arbitrary and does not follow any
format. In fact, it could easily be non-monotone: "if term : ind_set
..." hides a negated "term : ind_set", which is the mother of all
non-montonicities: think about "~ x : S ==> x : S".

In a nutshell: rewrite your definition to meet the standard format.

Regards
Tobias

Am 06/02/2012 02:54, schrieb John Ridgway:
> 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.