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