On 14/02/11 06:39, Lu Zhao wrote:
> val rel1_def =
> Define `rel1 (u:word32) v x y z = v x y z /\ x /\ y u /\ z`;
>
> val V_OK_def = Define `V_OK x y z = T`;
>
> Hol_reln `
> (!p c q. rel1 u V_OK p c q ==> rel2 u p c q) /\
> (!p c q. rel1 u (rel2 u) p c q ==> rel2 u p c q)`
This is a perfectly reasonable thing to want to do, however the definition
can't be made without knowing that the rel1 relation is monotone in its
treatment of that second argument.
Basically, whenever you make a "recursive call" to a relation, and the relation
doesn't just occur in the top-level position as an argument to a connective
like /\, you will need to prove that it's monotone in that position.
In your example, you need to add:
val rel1_mono = store_thm(
"rel1_mono",
``(!x y z. P x y z ==> Q x y z) ==> (rel1 u P x y z ==> rel1 u Q x y z)``,
SRW_TAC [][rel1_def]);
val _ = export_mono "rel1_mono"
Then the call to Hol_reln goes through.
We've already proved the monotonicity results for things like EVERY, but you'd
need to do the same sort of thing if you wanted to define a clause like
EVERY (myrel x) somelist ==> myrel x somearg
Michael
------------------------------------------------------------------------------
The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE:
Pinpoint memory and threading errors before they happen.
Find and fix more than 250 security defects in the development cycle.
Locate bottlenecks in serial and parallel code that limit performance.
http://p.sf.net/sfu/intel-dev2devfeb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
