source: src/common/Graphs.ma @ 702

Last change on this file since 702 was 702, checked in by campbell, 9 years ago

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 652 bytes
Line 
1
2include "basics/logic.ma".
3
4include "utilities/binary/positive.ma".
5include "common/Maps.ma".
6
7definition label : Type[0] ≝ Pos.
8definition graph : Type[0] → Type[0] ≝ tree_t … PTree.
9definition graph_lookup : ∀T. graph T → label → option T ≝
10λT,g,l. get … l g.
11
12
13definition label_eq : ∀x,y:label. (x=y) + (x≠y).
14#x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
15[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
16
17record label_generation : Type[0] ≝ { label_next : label }.
18
19definition label_new : label_generation → label × label_generation ≝
20λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.
Note: See TracBrowser for help on using the repository browser.