Re: [isabelle] HOLogic.dest_string

Dear Matthias,

Indeed Const ("List.list.Cons", _) is the right implementation and not Const ("Cons", _). If you use the interactive mode and interpret e.g. ML{* @{term "Cons"} *} in a theory higher than List.thy, you will see that the output is indeed the first and not the second representation above. To convince yourself, you can try to certify a term built by just "Cons" e.g.
 ML{* cterm_of @{theory} (Const("Cons",@{typ "'a list"}))*}
and you will see that Isabelle refuses this term as valid.

Terms (datatype term) as pointed out by Florian, is very liberal and contains many "ill-formed" terms.

Hope this helps,

Matthias Berg wrote:

I just tried to use the function HOLogic.dest_string and it seems that
its pattern matching does not work. The function dest_list tries to
match terms like  (Const ("List.list.Cons", _) $ t $ u) but I think it
should be just (Const ("Cons", _) $ t $ u). The same problem occurs in
other functions as well. The following works for me:

fun dest_nibble t =
  let fun err () = raise TERM ("dest_nibble", [t]) in
    (case try (unprefix "Nibble" o fst o Term.dest_Const) t of
      NONE => err ()
    | SOME c =>
        if size c <> 1 then err ()
        else if "0" <= c andalso c <= "9" then ord c - ord "0"
        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
        else err ())
fun dest_char (Const ("Char", _) $ t $ u) =
      dest_nibble t * 16 + dest_nibble u
  | dest_char t = raise TERM ("dest_char", [t]);
fun dest_list (Const ("Nil", _)) = []
  | dest_list (Const ("Cons", _) $ t $ u) = t :: dest_list u
  | dest_list t = raise TERM ("dest_list", [t]);
val dest_string = implode o map (chr o dest_char) o dest_list;

Matthias Berg

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