Re: [isabelle] quickcheck and error constants



Hi John,

Here's a solution (with only one int argument - trust you can generalize ;-)

consts cerror :: "int => string => 'a"

consts_code
  "cerror" ("(fn i => (fn x => error(implode x)))")

definition f where "f i == if i < 0 then cerror i ''x'' else i"

lemma "f x = x"

The implode is required because HOL's strings are implemented as char lists.

However, there are two things that puzzle me, that the implementor might be able to comment on:

1. autoquickcheck does seem to kick in or its result is hidden...

2. If in the ML code for cerror I replace the i by _, I have a problem: the generatd ML does not type check...

Tobias

John Matthews schrieb:
Hello,

I am trying to provide a shallow embedding of the Cryptol primitive "cerror :: int => int => string => 'a". Logically this is an undefined value, but I'd like Isabelle's quickcheck command to compile the Cryptol expression "cerror a b str" into the SML expression "error str", so that quickcheck throws an exception if cerror s ever executed during a run. How do I define cerror appropriately?

Thanks,
-john








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