On 03/08/12 13:43, Bill Richter wrote:
> I don't know how to get rid of new_type using H and your 4-arg predicate. I
> tried this, and I got the error message # Exception: Failure "term after
> binary operator expected":
> parse_as_infix("===",(12, "right"));; let A1_DEF = new_definition `A1axiom T
> === <=> !a b. T a /\ T b ==> a,b === b,a`;;
> I can appreciate this error message. I want to say that T is a set and a
> belongs to T (or T a = True, or T a), but I don't see how I can do that
> without some typing. What do I even want the type of a, b & T to be here?
> This seems to be a question of how to implement sets in HOL Light.
You could do it by replacing your concrete type point with a type variable.
See
type_of `MAP`
for syntax. (In HOL4 and SML, you'd get (:'a->'b) -> 'a list -> 'b list, but I
have this feeling that HOL Light does things a little differently.)
But, first: the issue you have with your parameterised axioms and === is caused
by the fact that you need a way of "stripping" === of its special infix status.
So, I'd suggest:
`A1axiom T (===) <=> !a b. T a /\ T b ==> a,b === b,a`
Do this without pre-committing to any types at all and your definition will be
suitably polymorphic.
Ultimately, you'd have theorems of the form
TarskiModel T (===) ==> ...some conclusion...
From skimming your sources very superficially, it looks as if the Between
'constant' would need to be a parameter of TarskiModel too.
It also looks as if you could dispense with the T parameter, and just have
A1axiom (===) <=> !a b. a,b === b,a
Again, not defining any types in advance would give you something suitably
polymorphic.
As you noted, doing things this way is likely to be rather painful because you
will constantly have this annoying TarskiModel hypothesis hanging around.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
