Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle proving theorem with translation

Email Gateway (Sep 01 2020 at 11:14):

From: Makarius <makarius@sketis.net>
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
begin

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
done

end

Makarius

Last updated: Jan 04 2025 at 20:18 UTC