Isar proof of conjunction2019 Community Moderator ElectionWhat is a good way to define a finite multiplication table in Isar?When would you use `presume` in an Isar proof?Need proof for meta-logic conjunction elimination ruleTrying to understand fix/assume/show “Failure to refine goal”; Cmd to show proof info for schematic varsHow to submit an argument to keyword proof?Taming meta implication in Isar proofsExpressing a simple declarative proof about exponents in IsarProving properties of generated listsKnowing when an Isar-style proof is actually valid in IsabelleFunctor-like construction in Isabelle/Isar
How does a sound wave propagate?
Insult for someone who "doesn't know anything"
Is divide-by-zero a security vulnerability?
Why would /etc/passwd be used every time someone executes `ls -l` command?
Where is the License file location for Identity Server in Sitecore 9.1?
Who has more? Ireland or Iceland?
What is better: yes / no radio, or simple checkbox?
How to write a chaotic neutral protagonist and prevent my readers from thinking they are evil?
3.5% Interest Student Loan or use all of my savings on Tuition?
The (Easy) Road to Code
How to recover against Snake as a heavyweight character?
What do you call someone who likes to pick fights?
Use Mercury as quenching liquid for swords?
Is it a Cyclops number? "Nobody" knows!
Ultrafilters as a double dual
Short story about cities being connected by a conveyor belt
What can I do if someone tampers with my SSH public key?
How does learning spells work when leveling a multiclass character?
Generating a list with duplicate entries
Exempt portion of equation line from aligning?
What is the orbit and expected lifetime of Crew Dragon trunk?
Why aren't there more Gauls like Obelix?
A running toilet that stops itself
Should we avoid writing fiction about historical events without extensive research?
Isar proof of conjunction
2019 Community Moderator ElectionWhat is a good way to define a finite multiplication table in Isar?When would you use `presume` in an Isar proof?Need proof for meta-logic conjunction elimination ruleTrying to understand fix/assume/show “Failure to refine goal”; Cmd to show proof info for schematic varsHow to submit an argument to keyword proof?Taming meta implication in Isar proofsExpressing a simple declarative proof about exponents in IsarProving properties of generated listsKnowing when an Isar-style proof is actually valid in IsabelleFunctor-like construction in Isabelle/Isar
I'm trying to prove something using Isar; so far, I've gotten to a goal that looks like this:
(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R))
(here plmeets
is a function I've defined, where plmeets P l
is shorthand for "the point P lies on the line l" in an affine plane, but I don't think that's important to my question.)
This goal is a conjunction of three things. I've actually already proved lemmas that seem to me to be very close to each of these things. For instance, I have
lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"
which produces the output
theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l
which you can see is almost exactly the first of the three conjoined items. (I admit that my other lemmas aren't quite so exactly matched to the other two items, but I'll work on that).
I'd like to say "because of lemma four_points_a1, all we have left to prove is item2 ∧ item3
" and I'm pretty sure there's a way to do this. But looking at the "Programming and Proving" book doesn't suggest anything to me. In Isabelle, rather than Isar, I suppose I'd apply conjI
twice to split the one goal into three, and then resolve the first goal.
But I cannot see how to do this in Isar.
isabelle isar
add a comment |
I'm trying to prove something using Isar; so far, I've gotten to a goal that looks like this:
(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R))
(here plmeets
is a function I've defined, where plmeets P l
is shorthand for "the point P lies on the line l" in an affine plane, but I don't think that's important to my question.)
This goal is a conjunction of three things. I've actually already proved lemmas that seem to me to be very close to each of these things. For instance, I have
lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"
which produces the output
theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l
which you can see is almost exactly the first of the three conjoined items. (I admit that my other lemmas aren't quite so exactly matched to the other two items, but I'll work on that).
I'd like to say "because of lemma four_points_a1, all we have left to prove is item2 ∧ item3
" and I'm pretty sure there's a way to do this. But looking at the "Programming and Proving" book doesn't suggest anything to me. In Isabelle, rather than Isar, I suppose I'd apply conjI
twice to split the one goal into three, and then resolve the first goal.
But I cannot see how to do this in Isar.
isabelle isar
1
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof methodintro
instead of multiple applications ofrule conjI
, i.e. you can useapply(intro conjI)
to split the goal into 3 subgoals. Then you can usesubgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
– xanonec
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago
add a comment |
I'm trying to prove something using Isar; so far, I've gotten to a goal that looks like this:
(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R))
(here plmeets
is a function I've defined, where plmeets P l
is shorthand for "the point P lies on the line l" in an affine plane, but I don't think that's important to my question.)
This goal is a conjunction of three things. I've actually already proved lemmas that seem to me to be very close to each of these things. For instance, I have
lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"
which produces the output
theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l
which you can see is almost exactly the first of the three conjoined items. (I admit that my other lemmas aren't quite so exactly matched to the other two items, but I'll work on that).
I'd like to say "because of lemma four_points_a1, all we have left to prove is item2 ∧ item3
" and I'm pretty sure there's a way to do this. But looking at the "Programming and Proving" book doesn't suggest anything to me. In Isabelle, rather than Isar, I suppose I'd apply conjI
twice to split the one goal into three, and then resolve the first goal.
But I cannot see how to do this in Isar.
isabelle isar
I'm trying to prove something using Isar; so far, I've gotten to a goal that looks like this:
(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R))
(here plmeets
is a function I've defined, where plmeets P l
is shorthand for "the point P lies on the line l" in an affine plane, but I don't think that's important to my question.)
This goal is a conjunction of three things. I've actually already proved lemmas that seem to me to be very close to each of these things. For instance, I have
lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"
which produces the output
theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l
which you can see is almost exactly the first of the three conjoined items. (I admit that my other lemmas aren't quite so exactly matched to the other two items, but I'll work on that).
I'd like to say "because of lemma four_points_a1, all we have left to prove is item2 ∧ item3
" and I'm pretty sure there's a way to do this. But looking at the "Programming and Proving" book doesn't suggest anything to me. In Isabelle, rather than Isar, I suppose I'd apply conjI
twice to split the one goal into three, and then resolve the first goal.
But I cannot see how to do this in Isar.
isabelle isar
isabelle isar
edited yesterday
John
asked 2 days ago
JohnJohn
246214
246214
1
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof methodintro
instead of multiple applications ofrule conjI
, i.e. you can useapply(intro conjI)
to split the goal into 3 subgoals. Then you can usesubgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
– xanonec
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago
add a comment |
1
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof methodintro
instead of multiple applications ofrule conjI
, i.e. you can useapply(intro conjI)
to split the goal into 3 subgoals. Then you can usesubgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
– xanonec
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago
1
1
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof method
intro
instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.– xanonec
2 days ago
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof method
intro
instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.– xanonec
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago
add a comment |
1 Answer
1
active
oldest
votes
According to @xanonec:
I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal.
It is possible to do this within an Isar proof. However, it may be best to use the proof method intro instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
According to @John:
The syntax for this process that actually worked was this:
proposition four_points_sufficient: "affine_plane plmeets"
unfolding affine_plane_def
apply (intro conjI)
subgoal using four_points_a1 by blast
It's not clear to me how "It is possible to do this [i.e., apply conjI
twice] within an Isar proof," but perhaps I don't now need to know.
1
"It is possible to do this [i.e., applyconjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar andapply
scripts, e.glemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.
– xanonec
yesterday
1
Also, there is nothing that could prevent one from usingapply
style script inside aproof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).
– xanonec
yesterday
add a comment |
Your Answer
StackExchange.ifUsing("editor", function ()
StackExchange.using("externalEditor", function ()
StackExchange.using("snippets", function ()
StackExchange.snippets.init();
);
);
, "code-snippets");
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "1"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);
else
createEditor();
);
function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);
);
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55028088%2fisar-proof-of-conjunction%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
According to @xanonec:
I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal.
It is possible to do this within an Isar proof. However, it may be best to use the proof method intro instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
According to @John:
The syntax for this process that actually worked was this:
proposition four_points_sufficient: "affine_plane plmeets"
unfolding affine_plane_def
apply (intro conjI)
subgoal using four_points_a1 by blast
It's not clear to me how "It is possible to do this [i.e., apply conjI
twice] within an Isar proof," but perhaps I don't now need to know.
1
"It is possible to do this [i.e., applyconjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar andapply
scripts, e.glemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.
– xanonec
yesterday
1
Also, there is nothing that could prevent one from usingapply
style script inside aproof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).
– xanonec
yesterday
add a comment |
According to @xanonec:
I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal.
It is possible to do this within an Isar proof. However, it may be best to use the proof method intro instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
According to @John:
The syntax for this process that actually worked was this:
proposition four_points_sufficient: "affine_plane plmeets"
unfolding affine_plane_def
apply (intro conjI)
subgoal using four_points_a1 by blast
It's not clear to me how "It is possible to do this [i.e., apply conjI
twice] within an Isar proof," but perhaps I don't now need to know.
1
"It is possible to do this [i.e., applyconjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar andapply
scripts, e.glemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.
– xanonec
yesterday
1
Also, there is nothing that could prevent one from usingapply
style script inside aproof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).
– xanonec
yesterday
add a comment |
According to @xanonec:
I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal.
It is possible to do this within an Isar proof. However, it may be best to use the proof method intro instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
According to @John:
The syntax for this process that actually worked was this:
proposition four_points_sufficient: "affine_plane plmeets"
unfolding affine_plane_def
apply (intro conjI)
subgoal using four_points_a1 by blast
It's not clear to me how "It is possible to do this [i.e., apply conjI
twice] within an Isar proof," but perhaps I don't now need to know.
According to @xanonec:
I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal.
It is possible to do this within an Isar proof. However, it may be best to use the proof method intro instead of multiple applications of rule conjI
, i.e. you can use apply(intro conjI)
to split the goal into 3 subgoals. Then you can use subgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.
According to @John:
The syntax for this process that actually worked was this:
proposition four_points_sufficient: "affine_plane plmeets"
unfolding affine_plane_def
apply (intro conjI)
subgoal using four_points_a1 by blast
It's not clear to me how "It is possible to do this [i.e., apply conjI
twice] within an Isar proof," but perhaps I don't now need to know.
answered 2 days ago
community wiki
John
1
"It is possible to do this [i.e., applyconjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar andapply
scripts, e.glemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.
– xanonec
yesterday
1
Also, there is nothing that could prevent one from usingapply
style script inside aproof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).
– xanonec
yesterday
add a comment |
1
"It is possible to do this [i.e., applyconjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar andapply
scripts, e.glemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.
– xanonec
yesterday
1
Also, there is nothing that could prevent one from usingapply
style script inside aproof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).
– xanonec
yesterday
1
1
"It is possible to do this [i.e., apply
conjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar and apply
scripts, e.g lemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.– xanonec
yesterday
"It is possible to do this [i.e., apply
conjI
twice] within an Isar proof,". It is possible to use a comma-separated list of methods (sequential composition, also see 6.4 in the reference manual) both in Isar and apply
scripts, e.g lemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) ...
.– xanonec
yesterday
1
1
Also, there is nothing that could prevent one from using
apply
style script inside a proof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).– xanonec
yesterday
Also, there is nothing that could prevent one from using
apply
style script inside a proof
block. To the best of my knowledge, it is not considered to be a very good practice, but it is not considered to be a particularly bad practice either (see "Do not switch from apply into proof in the middle of a proof" in https://proofcraft.org/blog/isabelle-style.html).– xanonec
yesterday
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55028088%2fisar-proof-of-conjunction%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
" I suppose I'd apply conjI twice to split the one goal into three, and then resolve the first goal." It is possible to do this within an Isar proof. However, it may be best to use the proof method
intro
instead of multiple applications ofrule conjI
, i.e. you can useapply(intro conjI)
to split the goal into 3 subgoals. Then you can usesubgoal
to provide a proof for each subgoal individually. However, unless you provide your entire application, it will be difficult to say whether or not there exist better methods.– xanonec
2 days ago
Thanks. This appears to be the thing I needed to get me past this particular roadblock. I've posted it as a community-wiki answer so that I can "accept" it in a few days, leaving fewer unanswered questions lying around. (If you'd rather write it as an answer, I'll accept that one instead).
– John
2 days ago