Answer to Q1
Because of M.Eberl's comment, I made a respectable effort to figure out how to get a witness without using obtain
. In the process, I answered my main question.
I got rid of the warning about introducing 'c
as a type variable by using b :: "'a => 'b option"
, instead of b
, as shown here:
lemma "dom (SOME b. dom b = A) = A"
proof-
obtain b :: "'a => 'b option" where "dom (b) = A"
by(metis (full_types) dom_const dom_restrict inf_top_left)
thus ?thesis
by(metis (lifting, full_types) exE_some)
qed
Answer to Q2
(Update 140119) I finally found Isar syntax for ...
, on page 6 of isar-ref.pdf.
term ...
-- the argument of the last explicitly stated result (for infix application this is the right-hand side)
The string ...
is not exactly a friendly search string. Finding the meaning was a result of starting to look through chapter 1. I now see that chapters 1, 2, and 6 of isar-ref.pdf
are key chapters for getting some help on how to use Isar to do proofs. (End update.)
Concerning an error due to using fix/assume
as an alternate to obtain
Now, I return back to M.Eberl telling me I shouldn't use obtain
, which happened to be beneficial. But it brings up that it's a major effort to try to figure out how to use the language to make the PIDE happy. The last source I show below is another example of what a hassle it is to learn how to make the PIDE happy. To a large extent, it's just using examples to try and figure out the right combination of syntax and commands.
P.Lammich says to use obtain
in his answer. I also looked up the use of obtain
in prog-prove.pdf page 42, which discusses it in connection with the use of a witness.
I read a few other things, and I thought it was all telling me that obtain
is crucial to fixing a variable or constant with certain properties.
Anyway, I used def
to create a witness, so I learned something new:
declare[[show_sorts,show_brackets]]
lemma "dom (SOME b. dom b = A) = A"
proof-
def w == "(SOME b::('a => 'b option). dom b = A)"
hence "dom w = A"
by(metis (lifting, mono_tags) dom_const dom_restrict inf_top_left someI_ex)
print_facts
thus ?thesis
by(metis (lifting, full_types) dom_option_map exE_some)
qed
But, I try to use a fix/assume
combination in place def
, where supposedly def
is an abbreviation, and I get that mysterious and greatly infuriating message, "Failed to refine any pending goal", which makes me wonder why I want to use this language.
declare[[show_sorts,show_brackets]]
lemma "dom (SOME b. dom b = A) = A"
proof-
fix w assume w_def: "w == (SOME b::('a => 'b option). dom b = A)"
hence "dom w = A"
by(metis (lifting, mono_tags) dom_const dom_restrict inf_top_left someI_ex)
print_facts
thus ?thesis
oops
For the two proofs, when the cursor is at the line before print_facts
, what I see in the output panel is exactly the same, other than the def
proof shows proof (state): step 4
, and the fix/assume
proofs shows proof (state): step 5
. The facts at print_facts
are also the same.
From searches, I know that "Failed to refine any pending goal" has been a source of great pain for many. In the past, I finally figured out the trick to get rid of it for what I was doing, but it doesn't make sense here, not that it made sense to me there either.
Update 140118_0054
L.Noschinski gives the subtle tip from IsaUserList 2012-11-13:
When you use "fix" or "def" to define a variable, they either get just generalized (i.e. turned into schematics) (fix) or replaced by their right hand side (definitions) when a block is closed / a show is performed.
So for the fix/assumes
form of the proof, I put part of it in brackets, and for some reason, it exports the fact in the way that's needed:
lemma "dom (SOME b. dom b = A) = A"
proof-
{
fix w assume "w == (SOME b::('a => 'b option). dom b = A)"
hence "dom w = A"
by(metis (lifting, mono_tags) dom_const dom_restrict inf_top_left someI_ex)
}
thus ?thesis
by(metis (lifting, full_types) dom_option_map exE_some)
qed
I go ahead and throw in a let
form of the proof. I wouldn't have known to use the schematic variable ?w
without having looked at M.Eberl's proofs.
lemma "dom (SOME b. dom b = A) = A"
proof-
let ?w = "(SOME b::('a => 'b option). dom b = A)"
have "dom ?w = A"
by(metis (lifting, mono_tags) dom_const dom_restrict inf_top_left someI_ex)
thus ?thesis
by(metis (lifting, full_types) dom_option_map exE_some)
qed