If I have
definition (in A) B where "B = t"
where A
is a locale, B
is a new constant, and t
is a term, then how do I later unfold the definition of B
in a proof?
I can't figure out the syntax.
I want to prove
theorem mythm: "X ==> B ==> C"
where X
is some assumption which is strong enough to let me prove the locale predicate for A
and let me unfold the definition of B.
But I don't declare (in locale A)
.
Do I have to use the "interpretation" keyword?
I want to prove
theorem nat_trans_assoc :
"nat_trans C D F1 F2 τ ⟹ nat_trans C D F2 F3 σ ⟹ nat_trans C D F3 F4 ρ ⟹
nat_trans_comp C D F1 F3 F4 (nat_trans_comp C D F1 F2 F3 τ σ) ρ =
nat_trans_comp C D F1 F2 F4 τ (nat_trans_comp C D F2 F3 F4 σ ρ)"
proof
Here, nat_trans_comp
is a definition which lives in a locale called nat_trans_comp_context
.
In order to unfold the definition of nat_trans_comp
, I assumed I would just have to prove
have p1: "nat_trans_comp_context C D F1 F2 F3 τ σ"
and then do something like
apply(simp add: p1 nat_trans_comp_context.nat_trans_comp_def)
or
using p1
unfolding nat_trans_comp_context.nat_trans_comp_def
but neither of these seem to give me what I want.
locale test =
fixes a :: nat
assumes X: "a = 3"
definition (in test) mycst where
‹mycst = a * a›
lemma (in test) a_squared: "a *a = 9"
using X by auto
lemma
fixes a :: nat
assumes "a = 3"
shows "a*a=9"
proof -
interpret test a
apply unfold_locales
apply (use assms in auto)
done
show ?thesis
by (rule a_squared)
qed
Mathias Fleury said:
locale test = fixes a :: nat assumes X: "a = 3" definition (in test) mycst where ‹mycst = a * a› lemma (in test) a_squared: "a *a = 9" using X by auto lemma fixes a :: nat assumes "a = 3" shows "a*a=9" proof - interpret test a apply unfold_locales apply (use assms in auto) done show ?thesis by (rule a_squared) qed
Thank you I think I have it now
.
Last updated: Jan 05 2025 at 20:18 UTC