--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Tue Jan 13 14:26:21 1998 +0100
@@ -0,0 +1,297 @@
+(* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Correctness of Simulations in HOLCF/IOA
+*)
+
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "corresp_ex_sim";
+
+
+(* ---------------------------------------------------------------- *)
+(* corresp_ex_simC *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "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' \
+\ in \
+\ (@cex. move A cex s a T') \
+\ @@ ((corresp_ex_simC A R `xs) T')) \
+\ `x) ))";
+by (rtac trans 1);
+br fix_eq2 1;
+br corresp_ex_simC_def 1;
+br beta_cfun 1;
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
+qed"corresp_ex_simC_unfold";
+
+goal thy "(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";
+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 = \
+\ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
+\ in \
+\ (@cex. move A cex s a T') \
+\ @@ ((corresp_ex_simC A R`xs) T'))";
+br trans 1;
+by (stac corresp_ex_simC_unfold 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
+by (Simp_tac 1);
+qed"corresp_ex_simC_cons";
+
+
+Addsimps [corresp_ex_simC_UU,corresp_ex_simC_nil,corresp_ex_simC_cons];
+
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata describe the definition *)
+(* of move in more detail *)
+(* ------------------------------------------------------------------ *)
+
+section"properties of move";
+
+Delsimps [Let_def];
+
+goalw thy [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'";
+
+(* 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 (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);
+(* Go on as usual *)
+be exE 1;
+by (dres_inst_tac [("x","t'"),
+ ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
+be exE 1;
+be conjE 1;
+by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
+by (res_inst_tac [("x","ex")] selectI 1);
+be conjE 1;
+ba 1;
+qed"move_is_move_sim";
+
+
+Addsimps [Let_def];
+
+goal thy
+ "!!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')";
+by (cut_inst_tac [] move_is_move_sim 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
+qed"move_subprop1_sim";
+
+goal thy
+ "!!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')";
+by (cut_inst_tac [] move_is_move_sim 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
+qed"move_subprop2_sim";
+
+goal thy
+ "!!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'";
+by (cut_inst_tac [] move_is_move_sim 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
+qed"move_subprop3_sim";
+
+goal thy
+ "!!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')) = \
+\ (if a:ext A then a>>nil else nil)";
+by (cut_inst_tac [] move_is_move_sim 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
+qed"move_subprop4_sim";
+
+goal thy
+ "!!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";
+by (cut_inst_tac [] move_is_move_sim 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [move_def,Let_def]) 1);
+qed"move_subprop5_sim";
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata contribute to *)
+(* TRACE INCLUSION Part 1: Traces coincide *)
+(* ------------------------------------------------------------------ *)
+
+section "Lemmata for <==";
+
+
+(* ------------------------------------------------------
+ Lemma 1 :Traces coincide
+ ------------------------------------------------------- *)
+
+goal thy
+ "!!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')";
+
+by (pair_induct_tac "ex" [is_exec_frag_def] 1);
+(* 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);
+ba 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'")]
+ allE 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [rewrite_rule [Let_def] move_subprop5_sim,
+ rewrite_rule [Let_def] move_subprop4_sim]
+ setloop split_tac [expand_if] ) 1);
+qed_spec_mp"traces_coincide_sim";
+
+
+(* ----------------------------------------------------------- *)
+(* Lemma 2 : corresp_ex_sim is execution *)
+(* ----------------------------------------------------------- *)
+
+
+goal thy
+ "!!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')";
+
+by (Asm_full_simp_tac 1);
+by (pair_induct_tac "ex" [is_exec_frag_def] 1);
+(* main case *)
+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'")]
+ lemma_2_1 1);
+
+(* Finite *)
+be (rewrite_rule [Let_def] move_subprop2_sim) 1;
+by (REPEAT (atac 1));
+by (rtac conjI 1);
+
+(* is_exec_frag *)
+be (rewrite_rule [Let_def] move_subprop1_sim) 1;
+by (REPEAT (atac 1));
+by (rtac conjI 1);
+
+(* Induction hypothesis *)
+(* 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'")]
+ allE 1);
+by (Asm_full_simp_tac 1);
+by (forward_tac [reachable.reachable_n] 1);
+ba 1;
+by (asm_full_simp_tac (simpset() addsimps
+ [rewrite_rule [Let_def] move_subprop5_sim]) 1);
+(* laststate *)
+be ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1;
+by (REPEAT (atac 1));
+qed_spec_mp"correspsim_is_execution";
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "Main Theorem: T R A C E - I N C L U S I O N";
+
+(* -------------------------------------------------------------------------------- *)
+
+ (* 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.
+ S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *)
+
+goal thy
+"!!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";
+ by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
+ corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
+ by (REPEAT (etac conjE 1));
+ be ballE 1;
+ by (Blast_tac 2);
+ be exE 1;
+ br selectI2 1;
+ ba 1;
+ by (Blast_tac 1);
+qed"simulation_starts";
+
+bind_thm("sim_starts1",(rewrite_rule [Let_def] simulation_starts) RS conjunct1);
+bind_thm("sim_starts2",(rewrite_rule [Let_def] simulation_starts) RS conjunct2);
+
+
+goalw thy [traces_def]
+ "!!f. [| ext C = ext A; is_simulation R C 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;
+ by (simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
+ by (res_inst_tac [("s","s")] traces_coincide_sim 1);
+ 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 *)
+ by (rtac conjI 1);
+ by (asm_full_simp_tac (simpset() addsimps [sim_starts2,
+ corresp_ex_sim_def]) 1);
+
+ (* is-execution-fragment *)
+ by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
+ by (res_inst_tac [("s","s")] correspsim_is_execution 1);
+ ba 1;
+ by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
+qed"trace_inclusion_for_simulations";
+
+
+
+