Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adds mrec and interp combinators to itreeTauTheory #1263

Draft
wants to merge 2 commits into
base: develop
Choose a base branch
from
Draft

Adds mrec and interp combinators to itreeTauTheory #1263

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d0bea38
Adds mrec and interp combinators
xdrr Jun 28, 2024
c127ea2
Merge branch 'HOL-Theorem-Prover:develop' into develop
xdrr Jul 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions src/coalgebras/itreeTauScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -740,6 +740,30 @@ Definition itree_loop_def:
(INR seed)
End

Definition interp_body_def:
interp_body rh (Ret r) = Ret (INR r) ∧
interp_body rh (Tau t) = Ret (INL t) ∧
interp_body rh (Vis e k) = itree_bind (rh e) (\a. Ret (INL (k a)))
End

Definition itree_interp_def:
itree_interp rh t = itree_iter (interp_body rh) t
End

Definition mrec_iter_body_def:
mrec_iter_body rh t =
case t of
| Ret r => Ret (INR r)
| Tau t => Ret (INL t)
| Vis (INL seed') k => Ret (INL (itree_bind (rh seed') k))
| Vis (INR e) k => Vis e (Ret o INL o k)
End

Definition itree_mrec_def:
itree_mrec rh seed =
itree_iter (mrec_iter_body rh) (rh seed)
End

(* weak termination-sensitive bisimulation *)

Inductive strip_tau:
Expand Down
Loading