1(* Title: HOL/HOLCF/IOA/Simulations.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Simulations in HOLCF/IOA\<close> 6 7theory Simulations 8imports RefCorrectness 9begin 10 11default_sort type 12 13definition is_simulation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 14 where "is_simulation R C A \<longleftrightarrow> 15 (\<forall>s \<in> starts_of C. R``{s} \<inter> starts_of A \<noteq> {}) \<and> 16 (\<forall>s s' t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (s, s') \<in> R 17 \<longrightarrow> (\<exists>t' ex. (t, t') \<in> R \<and> move A ex s' a t'))" 18 19definition is_backward_simulation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 20 where "is_backward_simulation R C A \<longleftrightarrow> 21 (\<forall>s \<in> starts_of C. R``{s} \<subseteq> starts_of A) \<and> 22 (\<forall>s t t' a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (t, t') \<in> R 23 \<longrightarrow> (\<exists>ex s'. (s,s') \<in> R \<and> move A ex s' a t'))" 24 25definition is_forw_back_simulation :: 26 "('s1 \<times> 's2 set) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 27 where "is_forw_back_simulation R C A \<longleftrightarrow> 28 (\<forall>s \<in> starts_of C. \<exists>S'. (s, S') \<in> R \<and> S' \<subseteq> starts_of A) \<and> 29 (\<forall>s S' t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (s, S') \<in> R 30 \<longrightarrow> (\<exists>T'. (t, T') \<in> R \<and> (\<forall>t' \<in> T'. \<exists>s' \<in> S'. \<exists>ex. move A ex s' a t')))" 31 32definition is_back_forw_simulation :: 33 "('s1 \<times> 's2 set) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 34 where "is_back_forw_simulation R C A \<longleftrightarrow> 35 ((\<forall>s \<in> starts_of C. \<forall>S'. (s, S') \<in> R \<longrightarrow> S' \<inter> starts_of A \<noteq> {}) \<and> 36 (\<forall>s t T' a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (t, T') \<in> R 37 \<longrightarrow> (\<exists>S'. (s, S') \<in> R \<and> (\<forall>s' \<in> S'. \<exists>t' \<in> T'. \<exists>ex. move A ex s' a t'))))" 38 39definition is_history_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 40 where "is_history_relation R C A \<longleftrightarrow> 41 is_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R\<inverse>)) A C" 42 43definition is_prophecy_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 44 where "is_prophecy_relation R C A \<longleftrightarrow> 45 is_backward_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R\<inverse>)) A C" 46 47 48lemma set_non_empty: "A \<noteq> {} \<longleftrightarrow> (\<exists>x. x \<in> A)" 49 by auto 50 51lemma Int_non_empty: "A \<inter> B \<noteq> {} \<longleftrightarrow> (\<exists>x. x \<in> A \<and> x \<in> B)" 52 by (simp add: set_non_empty) 53 54lemma Sim_start_convert [simp]: "R``{x} \<inter> S \<noteq> {} \<longleftrightarrow> (\<exists>y. (x, y) \<in> R \<and> y \<in> S)" 55 by (simp add: Image_def Int_non_empty) 56 57lemma ref_map_is_simulation: "is_ref_map f C A \<Longrightarrow> is_simulation {p. snd p = f (fst p)} C A" 58 by (simp add: is_ref_map_def is_simulation_def) 59 60end 61