Hi Freek,
| Couldn't you set up things in a way that all the theorems
| would have the form "TarskiModel((===),Between) |- P"?
| I think I would find that more attractive.
Yes, I was wondering about that. Generally HOL inference rules will
happily propagate additional assumptions through them, and so the core
logical inferences should work smoothly, I think. So you'd give the
axioms too the form "TarskiModel((===),Between) |- P" by slightly
changing the line I gave, to:
let [A1;A2;A3;A4;A5;A6;A7;cong] =
CONJUNCTS(UNDISCH(fst(EQ_IMP_RULE(SPEC_ALL TarskiModel))));;
Then there is the question of how to force an initial environment of
variables into the beginning of a miz3 proof. Specifically, you'd like
to have "env" augmented with
let initial_env =
[`(===):point#point->point#point->bool`;
`(Between):point#point#point->bool`;
`(cong):point#point#point->point#point#point->bool`];;
I can probably figure this out for myself, but as the miz3 author I
will defer to you :-)
Perhaps if one can do both of the above, it would all work smoothly
and the proofs would look the same, but with the additional hypothesis
being automatically tacked on to any theorems that result. It would
certainly be interesting to try.
John.
------------------------------------------------------------------------------
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
