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



On 1/21/2013 10:40 AM, Andreas Lochbihler wrote:
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,

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







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