Changeset 992


Ignore:
Timestamp:
Jun 17, 2011, 6:05:05 PM (8 years ago)
Author:
mulligan
Message:

a few more axioms closed

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r991 r992  
    7878qed.
    7979
    80 axiom vector_associative_append:
    81   ∀A: Type[0].
    82   ∀n, m, o:  nat.
    83   ∀v: Vector A n.
    84   ∀q: Vector A m.
    85   ∀r: Vector A o.
    86     ((v @@ q) @@ r)
    87     ≃
    88     (v @@ (q @@ r)).
    89        
     80lemma super_rewrite2:
     81 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
     82  ∀P: ∀m. Vector A m → Prop.
     83   n=m → v1 ≃ v2 → P n v1 → P m v2.
     84 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
     85qed.
     86
    9087lemma vector_cons_append:
    9188  ∀A: Type[0].
     
    103100qed.
    104101
    105 lemma super_rewrite2:
    106  ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
    107   ∀P: ∀m. Vector A m → Prop.
    108    n=m → v1 ≃ v2 → P n v1 → P m v2.
    109  #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
     102lemma vector_cons_append2:
     103  ∀A: Type[0].
     104  ∀n, m: nat.
     105  ∀v: Vector A n.
     106  ∀q: Vector A m.
     107  ∀hd: A.
     108    hd:::(v@@q) = (hd:::v)@@q.
     109  #A #n #m #v #q
     110  elim v
     111  [ #hd %
     112  | #n' #hd' #tl' #ih #hd' <ih %
     113  ]
     114qed.
     115
     116lemma jmeq_cons_vector_monotone:
     117  ∀A: Type[0].
     118  ∀m, n: nat.
     119  ∀v: Vector A m.
     120  ∀q: Vector A n.
     121  ∀prf: m = n.
     122  ∀hd: A.
     123    v ≃ q → hd:::v ≃ hd:::q.
     124  #A #m #n #v #q #prf #hd #E
     125  @(super_rewrite2 A … E)
     126  [ assumption | @jmrefl ]
     127qed.
     128
     129lemma vector_associative_append:
     130  ∀A: Type[0].
     131  ∀n, m, o:  nat.
     132  ∀v: Vector A n.
     133  ∀q: Vector A m.
     134  ∀r: Vector A o.
     135    ((v @@ q) @@ r)
     136    ≃
     137    (v @@ (q @@ r)).
     138  #A #n #m #o #v #q #r
     139  elim v
     140  [ %
     141  | #n' #hd #tl #ih
     142    <(vector_cons_append2 A … hd)
     143    @jmeq_cons_vector_monotone
     144    //
     145  ]
    110146qed.
    111147
  • src/ASM/CPP2011/cpp-2011.tex

    r986 r992  
    3636
    3737\title{On the correctness of an assembler for the Intel MCS-51 microprocessor}
    38 \author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
     38\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    3939\institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna}
    4040
Note: See TracChangeset for help on using the changeset viewer.