Changeset 1256 for src/ERTL/ERTLToLTL.ma

Timestamp:

Sep 22, 2011, 6:03:03 PM (10 years ago)

Author:

mulligan

Message:

changes: added a mapi for graphs

File:

• src/ERTL/ERTLToLTL.ma (modified) (1 diff)

src/ERTL/ERTLToLTL.ma

@@ -375 +375 @@
   ].
 
+axiom Sm_leq_n_m_leq_n:
+  ∀m, n: nat.
+    S m ≤ n → m ≤ n.
+
+let rec mapi_aux
+  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
+    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
+  match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
+  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
+    match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
+    [ Leaf l ⇒ λprf. Leaf … (f accu l)
+    | Stub s ⇒ λprf. Stub … s
+    | Node n' l r ⇒ λabsrd. ⊥
+    ] (refl … 0)
+  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
+    match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
+    [ Leaf l ⇒ λabsrd. ⊥
+    | Stub s ⇒ λprf. Stub … s
+    | Node n'' l r ⇒ λprf.
+      Node ? n'' ? ?
+(*      (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
+                 (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))*)
+    ] (refl ? (S n'))
+  ].
+  [ 1,2: destruct(absrd)
+  | 3  : destruct(prf)
+         @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
+         [ 1: @Sm_leq_n_m_leq_n
+              assumption
+         | 2: <minus_Sn_m
+              [ 1: >minus_S_S %
+              | 2: assumption
+              ]
+         ]
+  | 4  : destruct(prf)
+         @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
+         [ 1: @Sm_leq_n_m_leq_n
+              assumption
+         | 2: <minus_Sn_m
+              [ 1: >minus_S_S %
+              | 2: assumption
+              ]
+         ]
+  ]
+qed.
+  
+check mapi_aux.
+
 definition translate_internal ≝
   λglobals.
   λint_fun.
-  let uses ≝ examine_internal globals int_fun in ?.
+  let uses ≝ examine_internal globals int_fun in
+  let 
 
 definition translate_funct ≝