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

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

File size:
652 bytes

Line  

1  

2  include "basics/logic.ma". 

3  

4  include "utilities/binary/positive.ma". 

5  include "common/Maps.ma". 

6  

7  definition label : Type[0] ≝ Pos. 

8  definition graph : Type[0] → Type[0] ≝ tree_t … PTree. 

9  definition graph_lookup : ∀T. graph T → label → option T ≝ 

10  λT,g,l. get … l g. 

11  

12  

13  definition 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  

17  record label_generation : Type[0] ≝ { label_next : label }. 

18  

19  definition 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.