source: src/utilities/bindLists.ma @ 2001

Last change on this file since 2001 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 1.3 KB
Line 
1include "utilities/bind_new.ma".
2
3definition bind_list ≝ λB,E.bind_new B (list E).
4
5coercion blist_from_list :
6  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.
7
8unification hint 0 ≔ B,E;
9Es ≟ list E
10(*--------------------------*)⊢
11bind_list B E ≡ bind_new B Es.
12
13definition bappend : ∀B,E.bind_list B E → bind_list B E →
14  bind_list B E ≝ λB,E. m_bin_op … (append ?).
15
16include "ASM/Vector.ma".
17interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).
18
19definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
20  λB,E,e,l.[e] @@ l.
21
22interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
23
24include "utilities/lists.ma".
25 
26theorem bcompile_append :
27  ∀U, R, E, fresh, bl1, bl2.
28  (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅
29  (
30  ! l1 ← bcompile … fresh bl1 ;
31  ! l2 ← bcompile … fresh bl2 ;
32  return (l1 @ l2)
33  ).
34  #U#R#E#fresh#bl1#bl2
35  #u >bcompile_bbind normalize @pair_elim
36  #u' #l' normalize @pair_elim
37  #u'' #l'' normalize >bcompile_bbind #EQ #EQ'
38  normalize >EQ normalize //
39qed.
40
41theorem bcompile_cons :
42  ∀U, R, E, fresh, e, bl2.
43  (bcompile U R (list E) fresh (e ::: bl2)) ≅
44    ! l ← bcompile … fresh bl2 ; return (e :: l).
45      #U#R#E#fresh#e#bl2 #u
46      >bcompile_append normalize //
47qed.
Note: See TracBrowser for help on using the repository browser.