Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] instantiating theorems

view this post on Zulip Email Gateway (Aug 18 2022 at 10:27):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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

Last updated: May 03 2024 at 08:18 UTC