Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle proving theorem with translation

view this post on Zulip Email Gateway (Sep 01 2020 at 11:14):

From: Makarius <>
Your consts/syntax/translation setup looks odd: you need to understand how
inner syntax transformations work to make use of it. See the isar-ref manual
section 6.5.

The good news is that you don't need syntax translations in your example. You
can do it more directly via abbreviations within the abstract syntax:

theory A
imports ZF

abbreviation time :: i where "time ≡ int"
abbreviation sig :: "i ⇒ i" where "sig(A) ≡ int → A"

theorem sig_mono: "A ⊆ B ⟹ sig(A) ⊆ sig(B)"
apply (drule Pi_mono[of _ _ time])
apply assumption



Last updated: Jul 15 2022 at 23:21 UTC