Changeset 990


Ignore:
Timestamp:
Jun 17, 2011, 1:30:01 PM (8 years ago)
Author:
sacerdot
Message:

Do no longer use the daemon automatically :-)

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r985 r990  
    3030lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    3131 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    32  #n #hd #tl #abs @⊥ //
     32 #n #hd #tl #abs @⊥ destruct (abs)
    3333qed.
    3434
     
    3636 ∃hd.∃tl.v ≃ VCons bool n hd tl.
    3737 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    38  [ #abs @⊥ //
     38 [ #abs @⊥ destruct (abs)
    3939 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    4040qed.
  • src/ASM/BitVectorTrie.ma

    r985 r990  
    133133 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    134134  [ #w #_ %1 %[@w] %
    135   | #n #l #r #abs @⊥ //
     135  | #n #l #r #abs @⊥ destruct(abs)
    136136  | #n #EQ %2 >EQ %]
    137137qed.
     
    140140 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    141141 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    142   [ #m #abs @⊥ //
     142  [ #m #abs @⊥ destruct(abs)
    143143  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    144144  | #m #EQ %2 // ]
  • src/ASM/FoldStuff.ma

    r980 r990  
    7676    foldl_strong_internal A P l H [ ] l acc (refl …).
    7777
     78let rec foldr_strong_internal
     79 (A:Type[0])
     80 (P: list A → Type[0])
     81 (l: list A)
     82 (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl))
     83 (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝
     84  match suffix return λl'. l = prefix @ l' → P (l') with
     85   [ nil ⇒ λprf. acc
     86   | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ].
     87 applyS prf
     88qed.
     89
     90lemma foldr_strong:
     91 ∀A:Type[0].
     92  ∀P: list A → Type[0].
     93   ∀l: list A.
     94    ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl).
     95     ∀acc:P [ ]. P l
     96 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
     97
    7898lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
    7999 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
  • src/ASM/Status.ma

    r985 r990  
    532532  in
    533533    set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7).
    534  
    535 axiom not_implemented: False.
    536534 
    537535definition get_bit_addressable_sfr ≝
  • src/ASM/Util.ma

    r985 r990  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4
     5(* let's implement a daemon not used by automation *)
     6inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
     7axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
     8example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
     9example not_implemented: False. cases daemon qed.
    410 
    511lemma eq_rect_Type0_r :
Note: See TracChangeset for help on using the changeset viewer.