# IRC log for #isabelle, 2014-09-23

All times shown according to UTC.

Time Nick Message
02:36 dmiles_afk joined #isabelle
05:13 dmiles_afk joined #isabelle
10:20 dmiles_afk joined #isabelle
13:25 redlizard joined #isabelle
13:27 redlizard How do I instantiate a sublocale declaration based on a term I know exists (by an \exists lemma) but can't define explicitly?
13:33 Jafet applybot: thm someI_ex
13:33 applybot ∃x. ?P x ⟹ ?P (SOME x. ?P x)
13:34 redlizard SOME?
13:34 * redlizard looks that up
13:36 Jafet If only one exists, consider using THE
13:36 Jafet applybot: thm theI'
13:36 applybot ∃! x. ?P x ⟹ ?P (THE x. ?P x)
13:43 redlizard Jafet: Do you know any documentation on how to use SOME-definitions in proofs?
13:43 redlizard That is, on how to prove things about terms defined with the SOME operator.
13:54 redlizard Jafet: For instance, any idea how I would prove "(SOME (f::nat ⇒ nat) . ∀n::nat. f n = n + n) 2 = 2 + 2" ?
14:00 Jafet someI_ex[of P] is everything that you can prove about (SOME x. P x)
14:01 Jafet applybot, lemma "(SOME (f::nat => nat). ALL n. f n = n + n) 2 = 2 + 2" by (force intro: someI_ex)
14:01 applybot Proving: 1. (SOME f. ∀n. f n = n + n) 2 = 2 + 2  \  *** Timed out  \  (During: 'by (force intro: someI_ex)')
14:04 Jafet Hmm
14:05 Jafet Oh, there's also someI, of course
14:08 redlizard Jafet: I tried this:
14:08 redlizard have "∃f::nat ⇒ nat. ∀n::nat. f n = n + n" by auto
14:08 redlizard then have "∀n::nat. (SOME (f::nat ⇒ nat) . ∀n::nat. f n = n + n) n = n + n" by (auto intro: someI_ex)
14:08 redlizard Which looks like it should work, but it doesn't.
14:10 redlizard Jafet: Ah, (rule someI_ex) does the job.
14:10 redlizard It's a bit more brute-force than I would like, but it works.
14:11 Jafet Eps is a useful construct but proving with it is a pain in general
14:11 redlizard Indeed.
14:11 redlizard But do you see any other way to do what I want?
14:12 redlizard That is, prove a sublocale proposition instantiated with a term I only know to \exist.
14:14 Jafet Probably not
14:15 redlizard Alright. I'll do it the hard way then.
14:15 redlizard Thanks for the help :)
14:15 Jafet I don't know about locales, but the same thing happens for class instantiations
14:16 redlizard Class instantiations are a special case of locales, so presumably similar rules apply.
17:05 dmiles_afk joined #isabelle
21:14 dmiles_afk joined #isabelle