[isabelle] instantiating theorems




Hi,

I have a theorem

thm trunc_bl2bin ;
bintrunc (?m::nat) (bl_to_bin (?bl::bool list)) =
bl_to_bin (drop (length ?bl - ?m) ?bl)

Now I find that



lemmas trunc_bl2bin_len = trunc_bl2bin [where m = "size ?bl", simplified] ;

gives

lemma
  trunc_bl2bin_len:
    bintrunc (size (?bl::?'a::size)) (bl_to_bin (?bl::bool list)) =
    bl_to_bin (drop (length ?bl - size ?bl) ?bl)

ie the ?bl I enter is not recognized as being the same ?bl as in the theorem.

Whereas

(read_instantiate [("m", "size ?bl")] (thm "trunc_bl2bin")) ;
val it =
   "bintrunc (length (?bl::bool list)) (bl_to_bin ?bl) =
      bl_to_bin (drop (length ?bl - length ?bl) ?bl)" : Thm.thm

works fine.

Does anyone know why this might be?

Jeremy






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