--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Jun 22 17:13:09 1998 +0200
@@ -18,7 +18,7 @@
(* ---------------------------------------------------------------- *)
-goal thy "corresp_ex_simC A R = (LAM ex. (%s. case ex of \
+Goal "corresp_ex_simC A R = (LAM 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' \
@@ -33,17 +33,17 @@
by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"corresp_ex_simC_unfold";
-goal thy "(corresp_ex_simC A R`UU) s=UU";
+Goal "(corresp_ex_simC A R`UU) s=UU";
by (stac corresp_ex_simC_unfold 1);
by (Simp_tac 1);
qed"corresp_ex_simC_UU";
-goal thy "(corresp_ex_simC A R`nil) s = nil";
+Goal "(corresp_ex_simC A R`nil) s = nil";
by (stac corresp_ex_simC_unfold 1);
by (Simp_tac 1);
qed"corresp_ex_simC_nil";
-goal thy "(corresp_ex_simC A R`((a,t)>>xs)) s = \
+Goal "(corresp_ex_simC A R`((a,t)>>xs)) s = \
\ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
\ in \
\ (@cex. move A cex s a T') \
@@ -68,7 +68,7 @@
Delsimps [Let_def];
-goalw thy [is_simulation_def]
+Goalw [is_simulation_def]
"!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
@@ -98,7 +98,7 @@
Addsimps [Let_def];
-goal thy
+Goal
"!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ is_exec_frag A (s',@x. move A x s' a T')";
@@ -107,7 +107,7 @@
by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
qed"move_subprop1_sim";
-goal thy
+Goal
"!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ Finite (@x. move A x s' a T')";
@@ -116,7 +116,7 @@
by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
qed"move_subprop2_sim";
-goal thy
+Goal
"!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ laststate (s',@x. move A x s' a T') = T'";
@@ -125,7 +125,7 @@
by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
qed"move_subprop3_sim";
-goal thy
+Goal
"!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ mk_trace A`((@x. move A x s' a T')) = \
@@ -135,7 +135,7 @@
by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
qed"move_subprop4_sim";
-goal thy
+Goal
"!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ (t,T'):R";
@@ -157,7 +157,7 @@
------------------------------------------------------- *)
Delsplits[split_if];
-goal thy
+Goal
"!!f.[|is_simulation R C A; ext C = ext A|] ==> \
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
\ mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
@@ -187,7 +187,7 @@
(* ----------------------------------------------------------- *)
-goal thy
+Goal
"!!f.[| is_simulation R C A |] ==>\
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R \
\ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')";
@@ -239,7 +239,7 @@
traces_coincide_sim, the second for the start state case.
S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *)
-goal thy
+Goal
"!!C. [| is_simulation R C A; s:starts_of C |] \
\ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
\ (s,S'):R & S':starts_of A";
@@ -258,7 +258,7 @@
bind_thm("sim_starts2",(rewrite_rule [Let_def] simulation_starts) RS conjunct2);
-goalw thy [traces_def]
+Goalw [traces_def]
"!!f. [| ext C = ext A; is_simulation R C A |] \
\ ==> traces C <= traces A";