Changeset 852


Ignore:
Timestamp:
May 27, 2011, 1:26:34 PM (8 years ago)
Author:
mulligan
Message:

foldl_strong outer definition

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r851 r852  
    1515*)
    1616
    17 let rec foldl_strong
     17let rec foldl_strong_internal
    1818  (A: Type[0]) (P: list A → Prop) (l: list A)
    1919  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
     
    2626  [ > (append_nil ?)
    2727    @ acc
    28   | applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?)
     28  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
    2929    [ @ (H prefix hd tl prf acc)
    3030    | applyS prf
     
    3232  ]
    3333qed.
     34
     35definition foldl_strong ≝
     36  λA: Type[0].
     37  λP: list A → Prop.
     38  λl: list A.
     39  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
     40  λsuffix: list A.
     41  λacc: P [ ].
     42    foldl_strong_internal A P l H [ ] suffix acc.
     43
     44definition bit_elim: ∀P: bool → bool. bool ≝
     45  λP.
     46    P true ∧ P false.
     47
     48definition bitvector_elim: ∀P: ∀n. BitVector n → bool. ∀n: nat. bool ≝
     49  λP.
     50  λn.
     51    P n.
     52 
     53   
    3454 
    3555    (* > append_cons_commute
Note: See TracChangeset for help on using the changeset viewer.