--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 02 17:23:59 2005 +0200
@@ -1,12 +1,8 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML
ID: $Id$
Author: Olaf Müller
-
-Correctness of Simulations in HOLCF/IOA.
*)
-
-
(* -------------------------------------------------------------------------------- *)
section "corresp_ex_sim";
@@ -45,7 +41,7 @@
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') \
+\ (@cex. move A cex s a T') \
\ @@ ((corresp_ex_simC A R$xs) T'))";
by (rtac trans 1);
by (stac corresp_ex_simC_unfold 1);
@@ -75,13 +71,13 @@
(* Does not perform conditional rewriting on assumptions automatically as
usual. Instantiate all variables per hand. Ask Tobias?? *)
by (subgoal_tac "? t' ex. (t,t'):R & move A ex s' a t'" 1);
-by (Asm_full_simp_tac 2);
+by (Asm_full_simp_tac 2);
by (etac conjE 2);
by (eres_inst_tac [("x","s")] allE 2);
by (eres_inst_tac [("x","s'")] allE 2);
by (eres_inst_tac [("x","t")] allE 2);
by (eres_inst_tac [("x","a")] allE 2);
-by (Asm_full_simp_tac 2);
+by (Asm_full_simp_tac 2);
(* Go on as usual *)
by (etac exE 1);
by (dres_inst_tac [("x","t'"),
@@ -152,30 +148,30 @@
(* ------------------------------------------------------
- Lemma 1 :Traces coincide
+ Lemma 1 :Traces coincide
------------------------------------------------------- *)
Delsplits[split_if];
-Goal
- "[|is_simulation R C A; ext C = ext A|] ==> \
+Goal
+ "[|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')";
by (pair_induct_tac "ex" [is_exec_frag_def] 1);
-(* cons case *)
-by (safe_tac set_cs);
+(* cons case *)
+by (safe_tac set_cs);
ren "ex a t s s'" 1;
by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
by (forward_tac [reachable.reachable_n] 1);
by (assume_tac 1);
by (eres_inst_tac [("x","t")] allE 1);
by (eres_inst_tac [("x",
- "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
+ "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
allE 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[rewrite_rule [Let_def] move_subprop5_sim,
- rewrite_rule [Let_def] move_subprop4_sim]
+ rewrite_rule [Let_def] move_subprop4_sim]
addsplits [split_if]) 1);
qed_spec_mp"traces_coincide_sim";
Addsplits[split_if];
@@ -186,10 +182,10 @@
(* ----------------------------------------------------------- *)
-Goal
+Goal
"[| 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')";
+\ --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')";
by (Asm_full_simp_tac 1);
by (pair_induct_tac "ex" [is_exec_frag_def] 1);
@@ -197,7 +193,7 @@
by (safe_tac set_cs);
ren "ex a t s s'" 1;
by (res_inst_tac [("t",
- "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
+ "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
lemma_2_1 1);
(* Finite *)
@@ -214,12 +210,12 @@
(* reachable_n looping, therefore apply it manually *)
by (eres_inst_tac [("x","t")] allE 1);
by (eres_inst_tac [("x",
- "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
+ "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
allE 1);
by (Asm_full_simp_tac 1);
by (forward_tac [reachable.reachable_n] 1);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[rewrite_rule [Let_def] move_subprop5_sim]) 1);
(* laststate *)
by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1);
@@ -234,11 +230,11 @@
(* -------------------------------------------------------------------------------- *)
(* generate condition (s,S'):R & S':starts_of A, the first being intereting
- for the induction cases concerning the two lemmas correpsim_is_execution and
- traces_coincide_sim, the second for the start state case.
+ for the induction cases concerning the two lemmas correpsim_is_execution and
+ 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
+Goal
"[| 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";
@@ -259,14 +255,14 @@
Goalw [traces_def]
"[| ext C = ext A; is_simulation R C A |] \
-\ ==> traces C <= traces A";
+\ ==> traces C <= traces A";
by (simp_tac(simpset() addsimps [has_trace_def2])1);
by (safe_tac set_cs);
(* give execution of abstract automata *)
by (res_inst_tac[("x","corresp_ex_sim A R ex")] bexI 1);
-
+
(* Traces coincide, Lemma 1 *)
by (pair_tac "ex" 1);
ren "s ex" 1;
@@ -275,13 +271,13 @@
by (REPEAT (atac 1));
by (asm_full_simp_tac (simpset() addsimps [executions_def,
reachable.reachable_0,sim_starts1]) 1);
-
+
(* corresp_ex_sim is execution, Lemma 2 *)
by (pair_tac "ex" 1);
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
ren "s ex" 1;
- (* start state *)
+ (* start state *)
by (rtac conjI 1);
by (asm_full_simp_tac (simpset() addsimps [sim_starts2,
corresp_ex_sim_def]) 1);
@@ -291,8 +287,4 @@
by (res_inst_tac [("s","s")] correspsim_is_execution 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
-qed"trace_inclusion_for_simulations";
-
-
-
-
+qed"trace_inclusion_for_simulations";