[isabelle] Trying to use "datatype" to restrict types of ... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Trying to use "datatype" to restrict types of ...

Email Gateway (Aug 19 2022 at 09:36):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,

I still did not quite get the meaning of the sT type. If I understand
you correctly, you use the values over which a variable ranges (what you
call "mapped to") also for the names of the variables.

Anyway, let's look at your issue with the value command. This command
use various evaluation strategies with Isabelle's code generator being
the default (and usually the fastest). Now, the definition of sFOLf1 for
Eq uses HOL equality on the right-hand side for the type sT:
"sFOLf1 E (Eq x y) = (E x = E y)"
However, you have not told Isabelle how to compute equality on type sT,
which is done as an instance of the type class equal.

The enum sort constraint comes from using the ! quantifier over sT in
"sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"
By default, ! is implemented to enumerate all values for v and test for
each whether the predicate holds. Again, Isabelle does not know how to
enumerate all values of type sT. You can do so by instantiating the type
class enum.

Best,
Andreas

Email Gateway (Aug 19 2022 at 09:36):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/21/2013 1:34 AM, Andreas Lochbihler wrote:

I still did not quite get the meaning of the sT type. If I understand
you correctly, you use the values over which a variable ranges (what
you call "mapped to") also for the names of the variables.
Andreas,

At this point, I stop trying to tell you "how things are" and only say
"some of what I think is happening". What you've given me so far has
satisfied my basic urge to try and do this. To finish it out will
require me to know more, and it may not be needed or even desirable to
implement.

There's a lot of magic that goes on with Isabelle, and to a certain
extent, I'm blindly laying down some of the foundation based on having
looked a little at HOL.thy, Set.thy, Larry's Isabelle/ZF and Obua's
HOLZF. Isabelle/HOL is magically proving standard theorems, and I'd say
"I'm probably getting lucky", but I think this is like playing the stock
market where "luck don't get you very far", and you're shut down fast if
what you're doing is completely based on guesswork.

I don't think that variables of type sT really take on values in the
normal sense. What takes on values is the predicate "inS" that they're
used in, which is of type bool, so the only real values I'm dealing with
are True and False, which ultimately come from my predicate of type "sT
=> sT => bool".

These five Isar statements set me up initially and demonstrate that
variables of type sT get their meaning from being used in the predicate
"inS".

--"The primitive type."
typedecl sT

--"The predicate 'is an element of'."
consts inS :: "sT => sT => bool"

--"HOL equal is defined."
axiomatization where
Ax_x: "!q.!p. ( !x. (inS x q) <-> (inS x p) ) <-> (p = q)"

--"The empty set constant."
consts emS :: "sT"

--"The empty set constant axiomatized."
axiomatization where
Ax_e: "!x.~(inS x emS)"

Having only crept along at a snail's pace, I've used 4 out of the 10
axioms I need, and Sledgehammer magically finds the right theorems to
prove other theorems, it times out when a "theorem" is false, and
Nitpick sometimes magically shows that a false "theorem" is false.

Several of the other 6 axioms have me worried, but it could all come to
a screeching halt today, and I'd still be impressed by the magic.

Anyway, let's look at your issue with the value command. This command
use various evaluation strategies with Isabelle's code generator being
the default (and usually the fastest). Now, the definition of sFOLf1
for Eq uses HOL equality on the right-hand side for the type sT:
"sFOLf1 E (Eq x y) = (E x = E y)"
However, you have not told Isabelle how to compute equality on type
sT, which is done as an instance of the type class equal.

Okay. I don't really compute equality, I define it as shown above by
axiom Ax_x. I stuck that axiom into the experimental fFOLdt theory and
it didn't get rid of the error.

Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive. So HOL
equal magically works for me in a basic way, because I've used it a
whole lot based on the properties I've attached to "=" with axiom Ax_x.

Thanks for the help. I need to make some more progress on getting the
first 9 axioms in. What will cause me logic problems is not necessarily
what I was trying to prevent by using my sFOLf function.

Regards,
GB

The enum sort constraint comes from using the ! quantifier over sT in
"sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"
By default, ! is implemented to enumerate all values for v and test
for each whether the predicate holds. Again, Isabelle does not know
how to enumerate all values of type sT. You can do so by instantiating
the type class enum.

Best,
Andreas

On 01/18/2013 06:50 PM, Gottfried Barrow wrote:

On 1/18/2013 1:28 AM, Andreas Lochbihler wrote:

you need to embed your formulas deeply in HOL, i.e., you cannot use
the standard HOL connectives &, |, !, etc. for your syntax. So you
must use your formula datatype also for the subexpressions of your
connectives:
Hope this helps,
Andreas,

It helped a lot. I wouldn't have gotten to this next step without a fix.

I'll answer a few questions and then show you the failure I'm at now.

I am not sure what sT is supposed to stand for. Is it the type for
variable names or the type of values that variables can take. In the
former case: what is the type of values?

Type "sT" is a primitive type that represents a set. By "can take", I
guess you mean "mapped to" as shown by your "env" below.

Semantically, I don't think a variable of type sT is mapped to another
value in the sense of a function.

I have a function:

consts seS :: "sT => (sT => bool) => sT"

I then use a function of that type, (seS q P), in an axiom describing a
property for every (q::sT) and (P::(sT => bool)), where P is a property
that holds for q. (Actually the (sT => bool) type function is what I'm
trying to tighten up with this sFOLf function.)

Variables of type sT are only used with the predicate \<in>, such as
(x::sT \<in> y::sT), or as a binder variable in \<exists> or \<forall>,
such as (!x. phi) or (? x. phi), where phi is a FOL formula built up
starting with the atomic formulas (x \<in> y) and (x = y).

Variables of type sT are used in HOL functions, but that's only because
that's how Isabelle makes me do it. The constant functions I define
represent sets, and axioms are used to state what is true about those
functions.

I could get more detailed, but I now get wellsortedness errors when
trying to use the function sFOLf in a "value" statement.

The command

value "sFOLf1 sID (In x y)"

gives the error

"Wellsortedness error... Type sT not of sort equal. No type arity sT ::
equal"

A similar error with "enum" in place of "equal" is after the third
"value" command. The "Eq" and the "Forall" mess things up.

I'm trying to keep this short, but I'm not all that clear on the
"environment" requirement. However, like I said, variables of type sT
aren't really mapped anywhere.

To use the "value" command, I just made my "env" function the identity
function.

The code is below, and I attached it as a THY.

Thanks for the help,
GB

theory sts__sFOLdt
imports Complex_Main
begin

typedecl sT

consts inS :: "sT => sT => bool"

datatype sFOLdt =
In sT sT
| Eq sT sT
| Forall sT sFOLdt

type_synonym env = "(sT => sT)"

definition sID :: "sT => sT" where
"sID s = s"

fun sFOLf :: "env => sFOLdt => bool" where
"sFOLf E (In x y) = inS x y"

value "sFOLf sID (In x y)"

fun sFOLf1 :: "env => sFOLdt => bool" where
"sFOLf1 E (In x y) = inS x y"
| "sFOLf1 E (Eq x y) = (E x = E y)"

value "sFOLf1 sID (In x y)"

fun sFOLf2 :: "env => sFOLdt => bool" where
"sFOLf2 E (In x y) = inS x y"
| "sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"

value "sFOLf2 sID (In x y)"

end

Email Gateway (Aug 19 2022 at 09:36):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,

--"HOL equal is defined."
axiomatization where
Ax_x: "!q.!p. ( !x. (inS x q) <-> (inS x p) ) <-> (p = q)"

Okay. I don't really compute equality, I define it as shown above by
axiom Ax_x. I stuck that axiom into the experimental fFOLdt theory and
it didn't get rid of the error.
The error remains because

you did not declare the axiom Ax_x as a code equation, and
it is not executable as the !x-quantifier ranges over sT for which
you have not provided an implementation.

The code generator will not work unless you provide a concrete
representation for the elements of sT.

Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive.
No, it is not HOL that proves these three properties, = on any type is
by axiom in HOL.thy reflexive, transitive and symmetric. As you use
axiomatization, it is your job to make sure that your specification is
consistent with HOL's axioms.

Regards,
Andreas

Email Gateway (Aug 19 2022 at 09:36):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/21/2013 8:55 AM, Andreas Lochbihler wrote:

The error remains because
1. you did not declare the axiom Ax_x as a code equation, and
2. it is not executable as the !x-quantifier ranges over sT for which
you have not provided an implementation.

The code generator will not work unless you provide a concrete
representation for the elements of sT.

Andreas,

"Satisfying the code generator" falls under what I had talked about
needing, which is "knowing more". The learning curve for "more" in
regards to the foundations of Isabelle is "huge", so I put that off for
now. I consider what I'm trying to do as something that should be done
by experts, but which the experts haven't taken time to do.

Still, the phrase "code generator" tells me what to search on to try and
finish the problem, so thanks for the tip.

Even after only having made the statement "typedecl sT", HOL will prove
that "=" for type "sT" is reflexive, symmetric, and transitive.
No, it is not HOL that proves these three properties, = on any type is
by axiom in HOL.thy reflexive, transitive and symmetric. As you use
axiomatization, it is your job to make sure that your specification is
consistent with HOL's axioms.

Being the argumentative type (GB::argumentative), I'm under the
impression that I can restate any axiom or theorem and "prove it again",
that with my reflexive, transitive, and symmetric proofs, I'm
effectively proving "A --> A" for previous axioms or theorems "A" in
HOL.thy. (I'm actually stating the 3 theorems after attaching additional
properties to "=" with my axiom).

I had looked previously at the axioms for "=" here in HOL.thy:

axiomatization where
refl: "t = (t::'a)" and
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
-- {*Extensionality is built into the meta-logic, and this rule
expresses
a related property. It is an eta-expanded version of the
traditional
rule, and similar to the ABS rule of HOL*} and

the_eq_trivial: "(THE x. x = a) = (a::'a)"

Number 1 is classic "reflexive", number 2 makes sense, but I quit at 3
and 4 at trying to understand why this gives us all the typical
properties of equality.

In the past, I had wondered whether HOL "=" has any special properties
that would result in inconsistencies once my axiom was attached to it
for type sT. Makarius said, paraphrasing, "HOL equal just has the
typical properties of equal." I decided, "Okay, then I'll consider that
until I attach additional properties to it for my type sT, that it's
simply reflexive, symmetric, and transitive." Consequently, I do proofs
for those 3 things regardless of what I read in HOL.thy or what you or
Makarius tell me.

I looked now a little further at this "equal is symmetric" theorem in
HOL.thy:

lemma sym: "s = t ==> t = s"
by (erule subst) (rule refl)

Still, my three theorems aren't exact restatements of anything in HOL.
(I didn't actually look much past "lemma sym", so they could be.) If
they are restatements, it doesn't hurt to prove them again after I add
my own "equality" axiom.

If you say, "You're restating the obvious", I would say, "But in
Isabelle, with automatic proof methods, it's so easy to restate and
prove the obvious. So I do it to be explicit, and to show what I can't
know or haven't taken time to know based on "imports Complex_Main".

As you use axiomatization, it is your job to make sure that your
specification is consistent with HOL's axioms.

And that is a major concern of mine, and my fFOLdt and fFOLf idea was an
attempt to deal with unknowns that might cause my logic to be inconsistent.

Thanks,
GB

Email Gateway (Aug 19 2022 at 09:36):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Gottfried,

If you want to prove that your notion of equality of sT is really
reflexive, transitive and symmetric, then you might do the following:

definition eq :: "sT => sT => bool" where
"eq p q = (!x. inS x q <--> inS x p)"

lemma "eq x x" <proof>
lemma "eq x y = eq y x" <proof>
lemma "eq x y ==> eq y z ==> eq x z" <proof>

By using your own predicate eq instead of =, you avoid that the
automated proof methods use any of HOL's predefined properties.

Andreas

Email Gateway (Aug 19 2022 at 09:37):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Andreas,

Alright, I get this last part for free. I haven't tried it out yet, but
there's enough temporary good news with my sFOLf that I go ahead and
send this email off, since I now need to experiment with both what
you've just given me and with the sFOLf, which might take a few days.

Before talking about sFOLf, in the past, I had tried to create my own
primitive "=" like this,

consts eqS :: "sT = > sT => bool",

and then use it in its undefined form in my axiom which defines set
equality.

Well, I don't just state trivial theorems to prove them, I also state
them to run Nitpick on them, so I ran Nitpick on this theorem,

theorem "!x. !y. (eqS x y) <-> (x = y)",

and Nitpick found a counterexample, though the theorem was also proved
"by auto" or something simple like that.

The scary part is that all the theorems I had proved still worked using
my primitive eqS.

As to my sFOLf, I looked at Larry's ZF.thy, when I was searching for
"code generator", and I saw this:

typedecl i
arities i :: "term"

After some trial and error, and seeing "arity", "equal", and "enum" in
the error messages, I put in some "arities" like this:

typedecl sT
arities sT :: equal
arities sT :: enum

That got rid of the errors in the simplified code I include below. As to
it being legitimate, I guess I'll find out, but what I have learned is
this: "arities, it's an Isar command that is used periodically". That
could be a very important lesson.

Thanks for the "eq" to help me try and isolate my equal from the HOL equal.

Regards,
GB

theory sTs__sFOLdt_130121b
imports Complex_Main
begin
typedecl sT
arities sT :: equal
arities sT :: enum

consts inS :: "sT => sT => bool"

datatype sFOLdt =
In sT sT
| Eq sT sT
| Forall sT sFOLdt

type_synonym env = "(sT => sT)"

definition sID :: "sT => sT" where
"sID s = s"

fun sFOLf :: "env => sFOLdt => bool" where
"sFOLf E (In x y) = inS x y"
| "sFOLf E (Eq x y) = (E x = E y)"
| "sFOLf E (Forall x f) = (!v. sFOLf (E(x := v)) f)"

value "sFOLf sID (In x y)"
value "sFOLf sID (Eq x y)"
value "sFOLf sID (Forall x (Eq x x) )"
end

Email Gateway (Aug 19 2022 at 09:38):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,

arities declares that a type belongs to the given type class, but leaves
the parameters of the type class uninterpreted and the assumptions
unproven. Thus, it is like axiomatisation: you can use it to introduce
inconsistencies. Here's an example:

class false = assumes FalseI: "x = x ==> False"

typedecl my_type
arities my_type :: false

lemma "False"
apply(rule FalseI)
apply(rule refl)
done

Without the arities command, I could not finish the proof of the lemma,
because Isabelle does not know whether the type class "false" can be
instantiated at all. With the arities command, I declare that my_type
satisfies the axiom FalseI for all x of type my_type.

Hence, arities (like axiomatization) belongs to the group of commands
for an axiomatic approach to formalisations. As most people nowadays
prefer a definitional approach, I would not call arities frequently used.

Have said all this, it is obvious that the arities declarations make the
error messages for the values command go away. But not for the code
generator, it will continue to complain about missing code equations for
the type class parameters. The second evaluation strategy (normalisation
by evaluation) works.

Andreas

Email Gateway (Aug 19 2022 at 09:38):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/22/2013 1:19 AM, Andreas Lochbihler wrote:

arities declares that a type belongs to the given type class, but
leaves the parameters of the type class uninterpreted and the
assumptions unproven. Thus, it is like axiomatisation: you can use it
to introduce inconsistencies. Here's an example:

Andreas,

So what we can say is that Isar commands that are axiomatic are
excellent commands for getting rid of error messages.

It looks like I have three options:

(1) Learn about arities and see if I can or can't assign my type sT to
type class "enum".
(2) Learn about code generation and figure out how to make my type sT
computable.
(3) Never use "datatype" and "fun" in such a way that it requires me to
have a concrete representation of type sT.

It appears that option (3) is working for me, at least for the simple
stuff I'm doing now. I think (3) would require that I be able to do
induction and recursion without "datatype". That I will be able do that,
I don't know. Ideally I would want to, if it's practical enough.

It finally sunk in that "value" is computing values, as you said, and so
I need a concrete representation.

Actually, that last sentence doesn't "represent the situation". Isabelle
can magically deal with a whole lot of things that haven't been
completely defined. So, what I really know is that in this particular
situation, with how I tried to use "value", it finally got to where it
needed a more concrete representation.

Trial and error, with some informative error messages, and a little help
interpreting them, can help teach a person the abstract limits of Isabelle.

I renamed sFOLdt and sFOLf to "sD" and "sF", completely implemented the
9 FOL formulas, and then proved a few basic theorems.

It turns out that "sD" and "sF" is a heavy weight solution. Theorems
that Sledgehammer can easily prove without this layer of heavy
recursion, it can't do with it in.

It also messes up the value of metis proofs. Most of the facts that
metis is now using for proofs aren't informative at all. I have big
plans for metis proofs, even in detailed proofs. I provide a step, I
apply Sledgehammer to it, it finds the theorems that justifies the step,
I don't have to, up front, memorize hundreds of theorem names, and the
facts in the metis proof can teach a person something, that is, if
they're not facts like "sF.simps(9)", like I'm getting now.

However, this recursive restriction of the HOL functions that can be
used is possibly a "fallback" solution, or a "parallel" solution.

What I did got extra, in trying to make type sT computable, is the
beginnings of a recursive definition of what a set is (possibly a bogus
definition), which is basically an attempt to implement the idea that
every set is built from the empty set.

I was going to try and prove something about it, like, "Okay, let's see
if I got lucky, and see if Sledgehammer can prove that my recursive
function sTf satisfies the properties of the ordered pair axiom". But
then, I haven't defined what membership means for it yet.

But first running a combination of Sledgehammer and Nitpick on a theorem
is always a winner. Nitpick can sometimes tells me in a few seconds what
a loser idea I've come up with.

In regards to the "eq" function that you gave me. That's basically my
"equality axiom", which I suppose you know. It would make proving
reflexive, etc less messy, but I already know that the "equality axiom"
is reflexive, symmetric, and transitive, so that wasn't what got me
motivated. What motivated me was the idea of using it in a trick to
define my own "=" and not use the HOL "=".

However, there is a cardinal rule I now live by, based on nothing any
expert has told me. But it is this:

"Never, ever, leave HOL equal undefined for a type, and then add axioms
for that type."

So, if I have to define HOL equal for my type sT, then I might as well
use HOL equal as my only equal, with whatever luggage it already comes
with, which I assume is nothing bad for my type sT, even with the
additional axioms, or we'd all probably be in trouble.

You say:

The second evaluation strategy (normalisation by evaluation) works.

I think you're saying here that the non-arities approach, that is,
making my type sT concrete and computable (to "satisfy the code
generator"), would work, if I could do it.

Thanks for the "arities" example of inconsistency.

The theory below shows my simple use of the recursive "sD" and "sF" in a
way described in item (3) above. I have two versions of the axioms and
two versions of a theorem. One version with outermost universal
quantifiers, and one version without them, to try and make it easier for
the theorem to be proved. Knowing, because of a previous thread, that
the meta-logic will take care of outermost quantification for me, is
very valuable information.

At the very bottom is my infant, experimentation of defining a recursive
set.

Also, thanks to Alfio for some points on recursion and the need for the
environment.

Regards,
GB

theory sTs__sF_130122_01
imports Complex_Main
begin

typedecl sT

consts inS :: "sT => sT => bool"

type_synonym env = "(sT => sT)"

definition sID :: "sT => sT" where
"sID s = s"

--"THE AXIOM OF EXTENSION: SET EQUALITY."
axiomatization where
Ax_x: "sF sID
(Forall p
(Forall q
(Iff (Eq p q) (Forall x (Iff (In x p) (In x q))))
)
)" and
Ax_x2: "sF sID
(Iff (Eq p q) (Forall x (Iff (In x p) (In x q))))"

theorem "(sF sID (In x y)) <-> (inS x y)"
by(simp)

theorem "(sF sID (Eq x y)) <-> (x = y)"
by (metis sF.simps(2) sID_def)

--"THE AXIOM OF EXISTENCE: THE EMPTY SET EXISTS."
consts emS :: "sT"

axiomatization where
Ax_e: "sF sID (Forall x (Not (In x emS)))" and
Ax_e2: "sF sID (Not (In x emS))"

--"NO X EXISTS IN THE EMPTY SET."
theorem "sF sID (Not (Exists x (In x emS)) )"
by (metis Ax_e sF.simps(3) sF.simps(8) sF.simps(9))

--"THE EMPTY SET IS UNIQUE."
theorem "sF sID
(Forall q
(Iff
(Forall x (Not (In x q)))
(Eq q emS)
)
)"
oops

theorem "sF sID
(Iff
(Forall x (Not (In x q)))
(Eq q emS)
)"
--"Sledgehammer found a proof, but it takes longer to execute than I'm
willing to wait."
--"by (metis Ax_e2 Ax_x2 sF.simps(1) sF.simps(3) sF.simps(7) sF.simps(8))"
oops

--"THE RECURSIVE SET TYPE: Everything is built from emS."

--"The unordered pair set."
consts upS :: "sT => sT => sT"

--"The separation set, 'all x in q such that P x'."
consts seS :: "sT => (sT => bool) => sT"

datatype sTd =
emSd
| upSd sTd sTd
| seSd sTd "sT => bool"

fun sTf :: "sTd => sT" where
"sTf emSd = emS"
| "sTf (upSd p q) = upS (sTf p) (sTf q)"
| "sTf (seSd q P) = seS (sTf q) P"

value "sTf emSd"
value "sTf ( upSd emSd emSd )"
value "sTf ( seSd q (%x. inS x emS) )"
value "sTf ( seSd emSd (%x. inS x emS) )"
value "sTf ( seSd emSd (%x. P) )"

end

Email Gateway (Aug 19 2022 at 09:57):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,

I'm trying to set up this formula,

!q. !P. ?u. (!x. x \<in> u <-> (x \<in> q & P x)),

so that P is only a FOL formula with a free variable x. I'm getting an
error when I get to the part that uses quantification.

Currently P is of type (sT => bool), but I want to restrict it according
to the following recursive definition:

Let x and y be variables, and let f and g be formulas, then
x \<in> y is a formula,
x = y is a formula,
~(f) is a formula,
(f & g) is a formula,
(f | g) is a formula,
(f --> g) is a formula,
(f <-> g) is formula,
(!x. f) is a formula,
(?x. f) is a formula, and
nothing else is a formula.

Really, all I want to do is restrict the syntax that can be used, but P
has to have a type, P has to be based on recursion, and I have to use
pattern matching, so I guess I have to use "datatype".

Here is what I have, where the last line causes an error, with the error
shown below.

typedecl sT

consts inS :: "sT => sT => bool" (infixl "inS" 55)

OUTPUT WINDOW ERROR:
Additional type variable(s) in specification of "sFOLf_graph": 'a
Specification depends on extra type variables: "'a"
The error(s) above occurred in "sTs.sFOLf_sumC_def"
The error(s) above occurred in definition "sFOLf_sumC_def":
"(sFOLf_sumC ≡ (%(x::sFOLdt). (THE_default undefined (%(y::bool).
(sFOLf_graph TYPE('a) x y)))))"

I've attached a 33KB screen capture which shows the same thing. I
switched the screen capture from JPG to PNG and it went from 244KB to
33KB, using http://lightscreen.sourceforge.net/

Thanks,
GB
function error.1.png

Email Gateway (Aug 19 2022 at 09:57):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Please change "function" to "fun".

It still works out the same. Without the "Forall" lines in my "datatype"
and "fun", my sFOLf function terminates correctly with the message
"Found termination order: "{}"".

Thanks,
GB

Email Gateway (Aug 19 2022 at 09:57):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
People can ignore what I was talking about, unless someone wants to give
me a complete "datatype" and "fun/primrec" solution based on the
informal, recursive definition I gave. Or a solution of another form
would be okay.

Trying to figure out how recursion works, I have this experimental code:

typedecl sT
consts inS :: "sT => sT => bool" (infixl "inS" 55)

datatype sFOLdt =
In sT sT
|And bool bool
|Rec bool

primrec sFOLf :: "sFOLdt => bool" where
"sFOLf (In u1 u2) = (u1 inS u2)" |
"sFOLf (And f1 f2) = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" |
"sFOLf (Rec f) = True"

which gives the error: Extra variables on rhs: "(sFOLf::(sFOLdt => bool))"

All that to say, trial and error has shown me I haven't understood
certain basic things, but trial and error can be an excellent learning
aid sometimes.

Regards,
GB

Email Gateway (Aug 19 2022 at 09:58):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
John,

No, you're on the mark. Thanks for the tip. That gets rid of that
particular error, but there are some major problems still. I'm not doing
any real recursion. Like for this statement,

"sFOLf (And f1 f2) = (f1 & f2)",

I would need to recurse on f1 and f2, but I'm not even close; that's all
messed up. I get an error from trying

value "sFOLf (And True True)"

Alfio pointed out section 2.5.6 of the tutorial, page 19:

http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/tutorial.pdf

Thanks,
GB

Email Gateway (Aug 19 2022 at 09:58):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Gottfried,

you need to embed your formulas deeply in HOL, i.e., you cannot use the
standard HOL connectives &, |, !, etc. for your syntax. So you must use
your formula datatype also for the subexpressions of your connectives:

I am not sure what sT is supposed to stand for. Is it the type for
variable names or the type of values that variables can take. In the
former case: what is the type of values? In the latter case: this would
be a very unusual setup, to mix values of variables (like in Eq and In)
with name binding (like in Forall); in that case, replace sT with some
type of variable names, e.g., string.

Your sFOLf function would then interpret such formulae in terms of HOL.
However, you need to deal with variables (sT) that occur freely in your
formula. They must be bound by some environment (I use val for the type
of values that variables can take).

type_synonym env = (sT => val)

Then, your sFOLf function should look like this:

fun sFOLf :: "env => sFOLdt => bool"
where
"sFOLf E (In x y) = inS x y"
| "sFOLf E (Eq x y) = (E x = E y)
| "sFOLf E (Not f) = \<not> (sFOLf E f)"
| "sFOLf E (And f g) = (sFOLf E f & sFOLf E g)"
| "sFOLf E (Forall x f) = (!v. sFOLf (E(x := v)) f)"
| ,.. (* remaining cases *)

Hope this helps,
Andreas

Email Gateway (Aug 19 2022 at 09:58):

From: Lars Noschinski <noschinl@in.tum.de>
This definition is not primitive recursive and hence rejected by primrec
(recursive calls my only make the arguments structurally smaller, so
"sFOLf (Rec f1)" is not valid on the rhs.

-- Lars

Email Gateway (Aug 19 2022 at 09:59):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Lars,

That was my experimental effort to force some termination; from that
and some other ideas, I figured out I was too far off to stumble on to
something that would make it all work.

However, it's not obvious to me why "sFOLf (Rec f1)" is not smaller. No
matter what "f1" is, it looks like I should get ""sFOLf (Rec f1) = True"
on the second call of sFOLf.

On the other hand, "((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" starts out as
"bool & bool", and it ends up as "bool & bool", even with the recursive
calls, so I guess that wouldn't be considered "structurally smaller". It
would help if I had a more precise understanding of "structurally
smaller", but I don't worry about that right now.

Thanks,
GB

Email Gateway (Aug 19 2022 at 09:59):

From: Tjark Weber <webertj@in.tum.de>
You know that, but the primrec command doesn't. Quoting from Section
10.3 of the Isabelle/Isar reference manual
(http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2012/doc/isar-ref.pdf):

Each equation needs to be of the form:
f x1 ... xm (C y1 ... yk) z1 ... zn = rhs
such that C is a datatype constructor, rhs contains only the free
variables on the left-hand side (or from the context), and all
recursive occurrences of f in rhs are of the form f ... yi ...
for some i.

Best regards,
Tjark

Email Gateway (Aug 19 2022 at 09:59):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/18/2013 1:28 AM, Andreas Lochbihler wrote:

you need to embed your formulas deeply in HOL, i.e., you cannot use
the standard HOL connectives &, |, !, etc. for your syntax. So you
must use your formula datatype also for the subexpressions of your
connectives:
Hope this helps,
Andreas,

It helped a lot. I wouldn't have gotten to this next step without a fix.

I'll answer a few questions and then show you the failure I'm at now.

I am not sure what sT is supposed to stand for. Is it the type for
variable names or the type of values that variables can take. In the
former case: what is the type of values?

Type "sT" is a primitive type that represents a set. By "can take", I
guess you mean "mapped to" as shown by your "env" below.

Semantically, I don't think a variable of type sT is mapped to another
value in the sense of a function.

I have a function:

consts seS :: "sT => (sT => bool) => sT"

I then use a function of that type, (seS q P), in an axiom describing a
property for every (q::sT) and (P::(sT => bool)), where P is a property
that holds for q. (Actually the (sT => bool) type function is what I'm
trying to tighten up with this sFOLf function.)

Variables of type sT are only used with the predicate \<in>, such as
(x::sT \<in> y::sT), or as a binder variable in \<exists> or \<forall>,
such as (!x. phi) or (? x. phi), where phi is a FOL formula built up
starting with the atomic formulas (x \<in> y) and (x = y).

Variables of type sT are used in HOL functions, but that's only because
that's how Isabelle makes me do it. The constant functions I define
represent sets, and axioms are used to state what is true about those
functions.

I could get more detailed, but I now get wellsortedness errors when
trying to use the function sFOLf in a "value" statement.

The command

value "sFOLf1 sID (In x y)"

gives the error

"Wellsortedness error... Type sT not of sort equal. No type arity sT ::
equal"

A similar error with "enum" in place of "equal" is after the third
"value" command. The "Eq" and the "Forall" mess things up.

I'm trying to keep this short, but I'm not all that clear on the
"environment" requirement. However, like I said, variables of type sT
aren't really mapped anywhere.

To use the "value" command, I just made my "env" function the identity
function.

The code is below, and I attached it as a THY.

Thanks for the help,
GB

theory sts__sFOLdt
imports Complex_Main
begin

typedecl sT

consts inS :: "sT => sT => bool"

datatype sFOLdt =
In sT sT
| Eq sT sT
| Forall sT sFOLdt

type_synonym env = "(sT => sT)"

definition sID :: "sT => sT" where
"sID s = s"

fun sFOLf :: "env => sFOLdt => bool" where
"sFOLf E (In x y) = inS x y"

value "sFOLf sID (In x y)"

fun sFOLf1 :: "env => sFOLdt => bool" where
"sFOLf1 E (In x y) = inS x y"
| "sFOLf1 E (Eq x y) = (E x = E y)"

value "sFOLf1 sID (In x y)"

fun sFOLf2 :: "env => sFOLdt => bool" where
"sFOLf2 E (In x y) = inS x y"
| "sFOLf2 E (Forall x f) = (!v. sFOLf2 (E(x := v)) f)"

value "sFOLf2 sID (In x y)"

end
sTs__sFOLdt.thy

Email Gateway (Aug 19 2022 at 09:59):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
I was actually looking at that last night, but with all the dots and
with other information overload, I didn't sort much of it out, so thanks
for the clarification.

I was mainly looking for examples to use as plug 'n play templates,
which can get me some progress sometimes.

Thanks to John Wickerson also for a clarification on the same subject.

Regards,
GB

Last updated: Apr 27 2024 at 01:05 UTC