Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Showing an "existence" axiom is satisfied.

Email Gateway (Aug 19 2022 at 15:01):

From: Holden Lee <hl422@cam.ac.uk>
[A] I'm trying to show a certain space of functions forms a vector space;
one of the necessary conditions is the existence of an additive inverse.

lemma (in vectorspace) coeff_space_is_vs:
fixes S
assumes h1: "finite S" and h2: "S⊆carrier V"
shows "vectorspace K (coeff_space S)"
proof -
have 0: "vectorspace K V"..
from 0 h1 h2 show ?thesis
apply (auto intro!: vs_criteria simp add: coeff_space_def)
apply (auto simp add: vectorspace_def)

The first goal is now

1. (!!v∷'c ⇒ 'a.
   finite S ⟹
   S ⊆ carrier V ⟹
   v ∈ S →⇩E carrier K ⟹
   module K V ⟹
   field K ⟹
   ∃neg_v∷'c ⇒ 'a∈S →⇩E carrier K.
   (λva∷'c∈S. v va ⊕⇘K⇙ neg_v va) = (λv∷'c∈S. 𝟬⇘K⇙)

The important part of this is the neg_v. I want to substitute a value to
neg_v so I try (tutorial p. 85)

apply (rule_tac x="restrict (λv'. ⊖⇘K⇙ (v v')) S" in exI)
(i.e. the additive inverse of a function just has every term negated) but
this doesn't work. What's the right way to write this?

Thanks,

Holden

Email Gateway (Aug 19 2022 at 15:01):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Holden,

The existential quantifier in your goal is bounded by the set "S ->_E carrier K", so you
have to use the introduction rule bexI for bounded existentials rather than exI for
unbounded existentials.

Hope this helps,
Andreas

Last updated: Apr 16 2024 at 08:18 UTC