Changeset 2226 for src/common


Ignore:
Timestamp:
Jul 20, 2012, 6:36:34 PM (7 years ago)
Author:
campbell
Message:

Whole program proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2185 r2226  
    548548  ]
    549549] qed.
     550
     551(* lazy proof *)
     552lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P.
     553  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
     554  All ? (λx. P (\snd x)) (prog_funct ?? p) →
     555  P f.
     556#A #V #b #p #f #initV #P #FFP #ALL
     557cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
     558[ elim (prog_funct … p) in ALL ⊢ %;
     559  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
     560#ALL2
     561cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2)
     562#x * //
     563qed.
     564
    550565
    551566discriminator Prod.
Note: See TracChangeset for help on using the changeset viewer.