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

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:


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.


theory sTs__sF_130122_01
imports Complex_Main

typedecl sT

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

datatype sD =
  In sT sT
| Eq sT sT
| Not sD
| And sD sD
| Or sD sD
| Imp sD sD
| Iff sD sD
| Forall sT sD
| Exists sT sD

type_synonym env = "(sT => sT)"

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

primrec sF :: "env => sD => bool"
  "sF E (In x y) = inS x y"
| "sF E (Eq x y) = (E x = E y)"
| "sF E (Not f) = (¬(sF E f))"
| "sF E (And f g) = (sF E f & sF E g)"
| "sF E (Or f g) = (sF E f | sF E g)"
| "sF E (Imp f g) = (sF E f --> sF E g)"
| "sF E (Iff f g) = (sF E f <-> sF E g)"
| "sF E (Forall x f) = (!v. sF (E(x := v)) f)"
| "sF E (Exists x f) = (? v. sF (E(x := v)) f)"

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)"

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

consts emS :: "sT"

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

theorem "sF sID (Not (Exists x (In x emS)) )"
  by (metis Ax_e sF.simps(3) sF.simps(8) sF.simps(9))

theorem "sF sID
(Forall q
    (Forall x (Not (In x q)))
    (Eq q emS)

theorem "sF sID
    (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))"

--"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 =
| 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) )"


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