1(* Title: HOL/HOLCF/IOA/RefMappings.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Refinement Mappings in HOLCF/IOA\<close> 6 7theory RefMappings 8imports Traces 9begin 10 11default_sort type 12 13definition move :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<Rightarrow> 's \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool" 14 where "move ioa ex s a t \<longleftrightarrow> 15 is_exec_frag ioa (s, ex) \<and> Finite ex \<and> 16 laststate (s, ex) = t \<and> 17 mk_trace ioa \<cdot> ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)" 18 19definition is_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 20 where "is_ref_map f C A \<longleftrightarrow> 21 ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and> 22 (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> (\<exists>ex. move A ex (f s) a (f t))))" 23 24definition is_weak_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool" 25 where "is_weak_ref_map f C A \<longleftrightarrow> 26 ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and> 27 (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> 28 (if a \<in> ext C then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) else f s = f t)))" 29 30 31subsection \<open>Transitions and moves\<close> 32 33lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t \<Longrightarrow> \<exists>ex. move A ex s a t" 34 apply (rule_tac x = " (a, t) \<leadsto> nil" in exI) 35 apply (simp add: move_def) 36 done 37 38lemma nothing_is_ex: "a \<notin> ext A \<and> s = t \<Longrightarrow> \<exists>ex. move A ex s a t" 39 apply (rule_tac x = "nil" in exI) 40 apply (simp add: move_def) 41 done 42 43lemma ei_transitions_are_ex: 44 "s \<midarrow>a\<midarrow>A\<rightarrow> s' \<and> s' \<midarrow>a'\<midarrow>A\<rightarrow> s'' \<and> a' \<notin> ext A \<Longrightarrow> \<exists>ex. move A ex s a s''" 45 apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI) 46 apply (simp add: move_def) 47 done 48 49lemma eii_transitions_are_ex: 50 "s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2 \<and> s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3 \<and> s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4 \<and> a2 \<notin> ext A \<and> a3 \<notin> ext A \<Longrightarrow> 51 \<exists>ex. move A ex s1 a1 s4" 52 apply (rule_tac x = "(a1, s2) \<leadsto> (a2, s3) \<leadsto> (a3, s4) \<leadsto> nil" in exI) 53 apply (simp add: move_def) 54 done 55 56 57subsection \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close> 58 59lemma weak_ref_map2ref_map: "ext C = ext A \<Longrightarrow> is_weak_ref_map f C A \<Longrightarrow> is_ref_map f C A" 60 apply (unfold is_weak_ref_map_def is_ref_map_def) 61 apply auto 62 apply (case_tac "a \<in> ext A") 63 apply (auto intro: transition_is_ex nothing_is_ex) 64 done 65 66lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" 67 by blast 68 69declare if_split [split del] 70declare if_weak_cong [cong del] 71 72lemma rename_through_pmap: 73 "is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)" 74 apply (simp add: is_weak_ref_map_def) 75 apply (rule conjI) 76 text \<open>1: start states\<close> 77 apply (simp add: rename_def rename_set_def starts_of_def) 78 text \<open>1: start states\<close> 79 apply (rule allI)+ 80 apply (rule imp_conj_lemma) 81 apply (simp (no_asm) add: rename_def rename_set_def) 82 apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) 83 apply safe 84 apply (simplesubst if_split) 85 apply (rule conjI) 86 apply (rule impI) 87 apply (erule disjE) 88 apply (erule exE) 89 apply (erule conjE) 90 text \<open>\<open>x\<close> is input\<close> 91 apply (drule sym) 92 apply (drule sym) 93 apply simp 94 apply hypsubst+ 95 apply (frule reachable_rename) 96 apply simp 97 text \<open>\<open>x\<close> is output\<close> 98 apply (erule exE) 99 apply (erule conjE) 100 apply (drule sym) 101 apply (drule sym) 102 apply simp 103 apply hypsubst+ 104 apply (frule reachable_rename) 105 apply simp 106 text \<open>\<open>x\<close> is internal\<close> 107 apply (frule reachable_rename) 108 apply auto 109 done 110 111declare if_split [split] 112declare if_weak_cong [cong] 113 114end 115