Changeset 1882 for src/common/Graphs.ma


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r1635 r1882  
    5959  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
    6060
    61 axiom graph_num_nodes:
    62   ∀A: Type[0].
    63   ∀g: graph A.
    64     nat.
     61definition graph_num_nodes:
     62  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
     63 
     64lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
     65  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
     66#A#P#H#g
     67lapply (refl ? (|g|))
     68generalize in ⊢(???%→?);
     69#n lapply g -g
     70@(nat_elim1 … n)
     71#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
     72qed.
Note: See TracChangeset for help on using the changeset viewer.