Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Anonymous functions, image, and inductive sets...

view this post on Zulip Email Gateway (Aug 18 2022 at 19:13):

From: John Ridgway <john@jacelridge.com>
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

Last updated: Nov 21 2024 at 12:39 UTC