new_type_definition produces bad error messages

[mn200]

Reported by Rob Arthan

I think the section on new_type_definition in the HOL 4 reference manual should say that it fails if the theorem in the parameter has free variables. E.g.,

app load ["PairedLambda", "Q"]; open PairedLambda pairTheory;
val tyax1 = new_type_definition ("bad1", Q.prove(`?p.(\(x,y). ~(x /\ y /\ z)) p`,
Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));

correctly results in an error:

Exception-
   HOL_ERR
  {message =
  "at Thm.prim_type_definition:\nsubset predicate must be a closed term",
  origin_function = "new_type_definition", origin_structure = "Definition"}
   raised

In fact, this is the only error message I can provoke:

val tyax2 = new_type_definition ("bad1", Q.prove(`?p.FST p \/ SND p`,
Q.EXISTS_TAC `(T,T)` THEN REWRITE_TAC []));

results in the same exception even though what is wrong here is that the theorem doesn't have the form |= ?x.t x

[mn200]

Strictly, that error message is “sort of” legitimate: the existing code sees ?p. FST p \/ SND p and takes it apart to match a predicate applied to an argument, giving the predicate as ((\/) (FST p)) and the argument as SND p. The predicate is indeed of type α → bool for some α, but the predicate includes a free variable (p) and so you get the error you do.

Of course, this is not as helpful as it might be. I will shortly change the code to check that the argument is the bound variable of the existential before falling through to the free variable check.

[konrad-slind]

Hi Michael,

As the person who wrote that code some years ago, I thought I'd offer my
fix. See how it fits with your
view.

Thanks,
Konrad.

fun dest_type_def thm =
let val (x,M) = dest_exists (concl thm)
val (P,y) = dest_comb M
in if x=y then P
else raise ERR "" ""
end
handle HOL_ERR _
=> raise TYDEF_ERR "expected a theorem of the form "?x. P x"";

fun prim_type_definition (name as {Thy, Tyop}, thm) =
let val checked = check_null_hyp thm TYDEF_ERR
val P = dest_type_def thm
val Pty = type_of P
val (dom,rng) = Type.dom_rng Pty
val checked = assert_exn null (free_vars P)
(TYDEF_ERR "subset predicate must be a closed term")
val tyvars = Listsort.sort Type.compare (type_vars_in_term P)
val _ = Type.prim_new_type name (List.length tyvars)
val newty = Type.mk_thy_type{Tyop=Tyop,Thy=Thy,Args=tyvars}
val repty = newty --> dom
val rep = mk_primed_var("rep", repty)
val TYDEF = mk_thy_const{Thy="bool",
Name="TYPE_DEFINITION",
Ty = Pty --> (repty-->bool)}
in
mk_defn_thm(tag thm,
mk_exists(rep, list_mk_comb(TYDEF,[P,rep])))
end

On Sun, Aug 11, 2013 at 9:31 PM, Michael Norrish
[email protected]:

Strictly, that error message is “sort of” legitimate: the existing code
sees ?p. FST p / SND p and takes it apart to match a predicate applied
to an argument, giving the predicate as ((/) (FST p)) and the argument
as SND p. The predicate is indeed of type α → bool for some α, but the
predicate includes a free variable (p) and so you get the error you do.

Of course, this is not as helpful as it might be. I will shortly change
the code to check that the argument is the bound variable of the
existential before falling through to the free variable check.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/128#issuecomment-22469555
.

[mn200]

I've done something very similar, inlining to get

 val (bv,Body) = with_exn dest_exists (concl thm) TYDEF_FORM_ERR
 val (P,v)     = with_exn dest_comb Body TYDEF_FORM_ERR
 val _         = assert_exn (equal bv) v TYDEF_FORM_ERR

I’ll check this in shortly (just running the selftest build now).

[konrad-slind]

Looks good. --Konrad.

On Sun, Aug 11, 2013 at 10:11 PM, Michael Norrish
[email protected]:

I've done something very similar, inlining to get

val (bv,Body) = with_exn dest_exists (concl thm) TYDEF_FORM_ERR
val (P,v) = with_exn dest_comb Body TYDEF_FORM_ERR
val _ = assert_exn (equal bv) v TYDEF_FORM_ERR

I’ll check this in shortly (just running the selftest build now).

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/128#issuecomment-22470234
.