Changeset 2226 for src/common

Timestamp:

Jul 20, 2012, 6:36:34 PM (9 years ago)

Author:

campbell

Message:

Whole program proof.

File:

• src/common/Globalenvs.ma (modified) (1 diff)

src/common/Globalenvs.ma

@@ -548 +548 @@
   ]
 ] qed.
+
+(* lazy proof *)
+lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P.
+  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
+  All ? (λx. P (\snd x)) (prog_funct ?? p) →
+  P f.
+#A #V #b #p #f #initV #P #FFP #ALL
+cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
+[ elim (prog_funct … p) in ALL ⊢ %;
+  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
+#ALL2
+cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2)
+#x * //
+qed.
+
 
 discriminator Prod.