--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Sep 02 17:23:59 2005 +0200
@@ -1,16 +1,17 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy
ID: $Id$
Author: Olaf Müller
-
-Correctness of Simulations in HOLCF/IOA.
*)
+header {* Correctness of Simulations in HOLCF/IOA *}
-SimCorrectness = Simulations +
-
+theory SimCorrectness
+imports Simulations
+begin
+
consts
- corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) =>
+ corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) =>
('a,'s1)execution => ('a,'s2)execution"
(* Note: s2 instead of s1 in last argument type !! *)
corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
@@ -18,21 +19,23 @@
defs
-
-corresp_ex_sim_def
+
+corresp_ex_sim_def:
"corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
- in
+ in
(S',(corresp_ex_simC A R$(snd ex)) S')"
-corresp_ex_simC_def
- "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of
+corresp_ex_simC_def:
+ "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of
nil => nil
| x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
- T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
+ T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
in
(@cex. move A cex s a T')
@@ ((h$xs) T'))
$x) )))"
-
-end
\ No newline at end of file
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end