src/HOL/BCV/DFAandWTI.thy

+(*  Title:      HOL/BCV/DFAandWTI.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1999 TUM
+
+The relationship between dataflow analysis and a welltyped-insruction predicate.
+*)
+
+DFAandWTI = SemiLattice +
+
+types 's os = 's option list
+
+constdefs
+
+ stable :: (nat => 's => 's option) => (nat => nat list) => nat => 's os => bool
+"stable step succs p sos ==
+ !s. sos!p = Some s --> (? t. step p s = Some(t) &
+                              (!q:set(succs p). Some t <= sos!q))"
+
+ wti_is_fix_step ::
+   "(nat => 's => 's option)
+    => (nat => 's os => bool)
+    => (nat => nat list)
+    => nat => 's set => bool"
+"wti_is_fix_step step wti succs n L == !sos p.
+   sos : listsn n (option L) & p < n -->
+   wti p sos = stable step succs p sos"
+
+ welltyping :: (nat => 's os => bool) => 's os => bool
+"welltyping wti tos == !p<size(tos). wti p tos"
+
+ is_dfa ::  ('s os => bool)
+            => (nat => 's => 's option)
+            => (nat => nat list)
+            => nat => 's set => bool
+"is_dfa dfa step succs n L == !sos : listsn n (option L).
+   dfa sos =
+   (? tos : listsn n (option L).
+      sos <= tos & (!p < n. stable step succs p tos))"
+
+end