Changeset 1256


Ignore:
Timestamp:
Sep 22, 2011, 6:03:03 PM (8 years ago)
Author:
mulligan
Message:

changes: added a mapi for graphs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1251 r1256  
    375375  ].
    376376
     377axiom Sm_leq_n_m_leq_n:
     378  ∀m, n: nat.
     379    S m ≤ n → m ≤ n.
     380
     381let rec mapi_aux
     382  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
     383    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
     384  match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
     385  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
     386    match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
     387    [ Leaf l ⇒ λprf. Leaf … (f accu l)
     388    | Stub s ⇒ λprf. Stub … s
     389    | Node n' l r ⇒ λabsrd. ⊥
     390    ] (refl … 0)
     391  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
     392    match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
     393    [ Leaf l ⇒ λabsrd. ⊥
     394    | Stub s ⇒ λprf. Stub … s
     395    | Node n'' l r ⇒ λprf.
     396      Node ? n'' ? ?
     397(*      (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
     398                 (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))*)
     399    ] (refl ? (S n'))
     400  ].
     401  [ 1,2: destruct(absrd)
     402  | 3  : destruct(prf)
     403         @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
     404         [ 1: @Sm_leq_n_m_leq_n
     405              assumption
     406         | 2: <minus_Sn_m
     407              [ 1: >minus_S_S %
     408              | 2: assumption
     409              ]
     410         ]
     411  | 4  : destruct(prf)
     412         @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
     413         [ 1: @Sm_leq_n_m_leq_n
     414              assumption
     415         | 2: <minus_Sn_m
     416              [ 1: >minus_S_S %
     417              | 2: assumption
     418              ]
     419         ]
     420  ]
     421qed.
     422 
     423check mapi_aux.
     424
    377425definition translate_internal ≝
    378426  λglobals.
    379427  λint_fun.
    380   let uses ≝ examine_internal globals int_fun in ?.
     428  let uses ≝ examine_internal globals int_fun in
     429  let
    381430
    382431definition translate_funct ≝
Note: See TracChangeset for help on using the changeset viewer.