Ignore:
Timestamp:
Dec 19, 2011, 2:48:35 PM (9 years ago)
Author:
campbell
Message:

Show that the universe generated by Clight/fresh.ma is good.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1626 r1628  
    11include "basics/lists/list.ma".
     2
     3(* An alternative form of All that can be easier to use sometimes. *)
     4lemma All_alt : ∀A,P,l.
     5  (∀a,pre,post. l = pre@a::post → P a) →
     6  All A P l.
     7#A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?);
     8generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %);
     9[ #pre #E %
     10| #a #tl #IH #pre #E %
     11  [ @(H a pre tl E)
     12  | @(IH (pre@[a])) >associative_append @E
     13  ]
     14] qed.
    215
    316let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.