*To*: Holden Lee <hl422 at cam.ac.uk>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Showing an "existence" axiom is satisfied.*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 23 Jul 2014 12:23:22 +0200*In-reply-to*: <CAKSvo_b9VwbAG2N3DzUjqm9YtGWBt5Yo9gFFAo-4riwZ78p7CQ@mail.gmail.com>*References*: <CAKSvo_b9VwbAG2N3DzUjqm9YtGWBt5Yo9gFFAo-4riwZ78p7CQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Hi Holden,

Hope this helps, Andreas On 23/07/14 12:17, Holden Lee wrote:

[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

**References**:**[isabelle] Showing an "existence" axiom is satisfied.***From:*Holden Lee

- Previous by Date: [isabelle] Showing an "existence" axiom is satisfied.
- Next by Date: [isabelle] Simplifying a nested if
- Previous by Thread: [isabelle] Showing an "existence" axiom is satisfied.
- Next by Thread: [isabelle] Simplifying a nested if
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list