Changeset 847


Ignore:
Timestamp:
May 26, 2011, 2:16:36 PM (8 years ago)
Author:
sacerdot
Message:

Several bugs fixed in Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r846 r847  
    99definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
    1010
    11 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
    12 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
     11coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
     12coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    1313
    1414axiom VOID: Type[0].
    1515axiom assert_false: VOID.
    16 definition bigbang: ∀A:Type[0].∀P:A → Prop. False → VOID → Σx:A.P x.
    17  #A #P #abs cases abs
    18 qed.
    19 
    20 (*coercion bigbang : ∀A.∀P:A → Prop.False → ∀v:VOID.Σx:A.P x ≝ bigbang on _v:VOID to Σx:?.?.*)
     16definition bigbang: ∀A:Type[0].False → VOID → A.
     17 #A #abs cases abs
     18qed.
     19
     20(*coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
    2121
    2222lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
     
    7171axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
    7272
     73(*
    7374definition build_maps' ≝
    7475  λpseudo_program.
     
    118119 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
    119120 |
    120      
    121 
    122 
     121*)     
    123122
    124123let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     
    130129      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
    131130  ].
    132 
    133 axiom sigma': pseudo_assembly_program → Word → Word.
    134131
    135132definition assembly_specification:
     
    198195           (p3_latch … ps)
    199196           (clock … ps)) ].
    200 (*
     197
    201198definition write_at_stack_pointer':
    202199 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
     
    218215          set_high_internal_ram ? s memory.
    219216  [ cases l0 %
    220   |2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *)
    221   ]
     217  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
    222218qed.
    223219
     
    254250 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
    255251 |
    256  | (*CSC: ??? *)
    257  | (*CSC: ??? *)
    258252 | %
    259253 ]
Note: See TracChangeset for help on using the changeset viewer.