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 SOMEdefinitions 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 bruteforce 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 