Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error



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













This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.