Finite runs on a transition system
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 '18 at 11:37
JavierJavier
653723
add a comment |
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 '18 at 11:37
JavierJavier
653723
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 '18 at 12:04
add a comment |
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 '18 at 11:37
JavierJavier
653723
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
isabelle
asked Nov 22 '18 at 11:37
JavierJavier
653723
asked Nov 22 '18 at 11:37
JavierJavier
653723
edited Nov 23 '18 at 10:50
Javier
asked Nov 22 '18 at 11:37
JavierJavier
653723
asked Nov 22 '18 at 11:37
JavierJavier
653723
asked Nov 22 '18 at 11:37
JavierJavier
653723
653723
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 '18 at 12:04
add a comment |
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 '18 at 12:04
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 '18 at 12:04
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 '18 at 12:04
add a comment |
2 Answers
2
active
oldest
votes
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 '18 at 11:34
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
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%2f53430148%2ffinite-runs-on-a-transition-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 '18 at 11:34
add a comment |
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 '18 at 11:34
add a comment |
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
answered Nov 22 '18 at 12:05
Manuel EberlManuel Eberl
4,674520
4,674520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 '18 at 11:34
add a comment |
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 '18 at 11:34
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 '18 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.
{(y,x) | (x,y) ∈ R}).– Manuel Eberl
Nov 23 '18 at 11:34
Without checking: No, I think it's simply the converse of the relation (i.e.
{(y,x) | (x,y) ∈ R}).– Manuel Eberl
Nov 23 '18 at 11:34
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
answered Nov 22 '18 at 11:57
René ThiemannRené Thiemann
96142
96142
add a comment |
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%2f53430148%2ffinite-runs-on-a-transition-system%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
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 '18 at 12:04