Re: [isabelle] Using case_tac with functions that have not been exhaustively defined

Hi Duncan,

> As far as I know, this behaviour only occurs with case expressions and
> functions defined using pattern matching, that don't provide an exhaustive
> list of matches, or functions that explicitly use the 'arbitrary' constant
> as a result. This behaviour allows me to generate Standard ML code that I
> think I have proved to be correct, but which actually results in a Match
> exception when run.

Note that code generation only guarantees partial correctness.  So, if
(!) under code generation a term t evaluates to t', "t = t'" is
derivable in the logic.  Raising a Match exception is still "correct"
and that sense though somehow unsatisfactory.

Hope this helps

fn:Florian Haftmann
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =

Attachment: signature.asc
Description: OpenPGP digital signature

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