Changeset 852 for src

Timestamp:

May 27, 2011, 1:26:34 PM (10 years ago)

Author:

mulligan

Message:

foldl_strong outer definition

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -15 +15 @@
 *)
 
-let rec foldl_strong
+let rec foldl_strong_internal
   (A: Type[0]) (P: list A → Prop) (l: list A)
   (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
@@ -26 +26 @@
   [ > (append_nil ?)
     @ acc
-  | applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?)
+  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
     [ @ (H prefix hd tl prf acc)
     | applyS prf
@@ -32 +32 @@
   ]
 qed.
+
+definition foldl_strong ≝
+  λA: Type[0].
+  λP: list A → Prop.
+  λl: list A.
+  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
+  λsuffix: list A.
+  λacc: P [ ].
+    foldl_strong_internal A P l H [ ] suffix acc.
+
+definition bit_elim: ∀P: bool → bool. bool ≝
+  λP.
+    P true ∧ P false.
+
+definition bitvector_elim: ∀P: ∀n. BitVector n → bool. ∀n: nat. bool ≝
+  λP.
+  λn.
+    P n.
+  
+    
   
     (* > append_cons_commute