Stream: Beginner Questions

Topic: Unfolding definitions in locale

Patrick Nicodemus (Nov 07 2023 at 23:22):

If I have
definition (in A) B where "B = t"
where Ais 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?

Patrick Nicodemus (Nov 07 2023 at 23:24):

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.

Mathias Fleury (Nov 08 2023 at 05:58):

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

Patrick Nicodemus (Nov 08 2023 at 12:56):

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

Patrick Nicodemus (Nov 08 2023 at 12:57):

.

Last updated: Apr 28 2024 at 04:17 UTC