# HG changeset patch
# User mueller
# Date 884697981 -3600
# Node ID ea467ce150405756d4c9b9dd7d033fb7b8facb21
# Parent  dc45cf21dbd21a26b9e99c0d71f9aa8d66d04073
added forward simulation correectness;

diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/IOA.thy
--- a/src/HOLCF/IOA/meta_theory/IOA.thy	Tue Jan 13 10:40:38 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Tue Jan 13 14:26:21 1998 +0100
@@ -8,6 +8,6 @@
 
  
 	       
-IOA = RefCorrectness + Compositionality + Deadlock
+IOA = SimCorrectness + RefCorrectness + Compositionality + Deadlock
 
 
diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- /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"; 
+
+
+
+
diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 13 14:26:21 1998 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1997  TU Muenchen
+
+Correctness of Simulations in HOLCF/IOA
+*)
+
+
+SimCorrectness = Simulations + 
+       
+consts
+
+  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
+                   -> ('s2 => ('a,'s2)pairs)"
+
+
+defs
+           
+corresp_ex_sim_def
+  "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
+                            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 
+      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')
+                                 @@ ((h`xs) T'))
+                        `x) )))"
+ 
+end
\ No newline at end of file
diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/Simulations.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 13 14:26:21 1998 +0100
@@ -0,0 +1,39 @@
+(*  Title:      HOLCF/IOA/meta_theory/Simulations.ML
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1997  TU Muenchen
+
+Simulations in HOLCF/IOA
+*)
+
+
+
+goal thy "(A~={}) = (? x. x:A)";
+by (safe_tac set_cs);
+auto();
+qed"set_non_empty";
+
+goal thy "(A Int B ~= {}) = (? x. x: A & x:B)";
+by (simp_tac (simpset() addsimps [set_non_empty]) 1);
+qed"Int_non_empty";
+
+
+goalw thy [Image_def]
+"(R^^{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
+by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
+qed"Sim_start_convert";
+
+Addsimps [Sim_start_convert];
+
+
+goalw thy [is_ref_map_def,is_simulation_def]
+"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A";
+(* start states *)
+by (Asm_full_simp_tac 1);
+(* main case *)
+by (Blast_tac 1);
+qed"ref_map_is_simulation";
+
+
+
+
diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/Simulations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 13 14:26:21 1998 +0100
@@ -0,0 +1,64 @@
+(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1997  TU Muenchen
+
+Simulations in HOLCF/IOA
+*)
+
+Simulations = RefCorrectness  +
+
+default term
+
+consts
+
+  is_simulation            ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+  is_backward_simulation   ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+  is_forw_back_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+  is_back_forw_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+  is_history_relation      ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+  is_prophecy_relation     ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
+
+defs
+
+is_simulation_def
+  "is_simulation R C A ==                          
+   (!s:starts_of C. R^^{s} Int starts_of A ~= {}) &        
+   (!s s' t a. reachable C s &                      
+               s -a--C-> t   &
+               (s,s') : R              
+               --> (? t' ex. (t,t'):R & move A ex s' a t'))"
+
+is_backward_simulation_def
+  "is_backward_simulation R C A ==                          
+   (!s:starts_of C. R^^{s} <= starts_of A) &        
+   (!s t t' a. reachable C s &                      
+               s -a--C-> t   &
+               (t,t') : R              
+               --> (? ex s'. (s,s'):R & move A ex s' a t'))"
+
+is_forw_back_simulation_def
+  "is_forw_back_simulation R C A ==                          
+   (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &        
+   (!s S' t a. reachable C s &                      
+               s -a--C-> t   &
+               (s,S') : R              
+               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"
+
+is_back_forw_simulation_def
+  "is_back_forw_simulation R C A ==                          
+   (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &        
+   (!s t T' a. reachable C s &                      
+               s -a--C-> t   &
+               (t,T') : R              
+               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"
+
+is_history_relation_def
+  "is_history_relation R C A == is_simulation R C A & 
+                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
+
+is_prophecy_relation_def
+  "is_prophecy_relation R C A == is_backward_simulation R C A & 
+                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
+                      
+end
diff -r dc45cf21dbd2 -r ea467ce15040 src/HOLCF/IOA/meta_theory/TrivEx2.ML
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Tue Jan 13 10:40:38 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Tue Jan 13 14:26:21 1998 +0100
@@ -64,3 +64,9 @@
 qed"TrivEx2_abstraction";
 
 
+(*
+goal thy "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) 
+IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
+
+*)
+