Changeset 2286 for src/utilities


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r1593 r2286  
    108108@(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.
    109109
     110lemma distributive_times_plus_fast : distributive ? times plus.
     111#n elim n [ #m #p % ]
     112#n' #IH #m #p normalize
     113>IH
     114>associative_plus in ⊢ (???%);
     115<(associative_plus ? p) in ⊢ (???%);
     116>(commutative_plus_faster ? p) in ⊢ (???%);
     117>(associative_plus p)
     118@associative_plus
     119qed.
     120
     121lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m.
     122#n elim n -n
     123[ #m % ]
     124#n #IH #m normalize <IH
     125<associative_plus >(commutative_plus_faster n)
     126>associative_plus >IH %
     127qed.
     128
     129lemma commutative_times_fast : commutative ? times.
     130#n elim n -n
     131[ #m <times_n_O % ]
     132#n #IH #m normalize <times_n_Sm_fast >IH %
     133qed.
     134
Note: See TracChangeset for help on using the changeset viewer.