1(* Title: HOL/HOLCF/IOA/Compositionality.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Compositionality of I/O automata\<close> 6theory Compositionality 7imports CompoTraces 8begin 9 10lemma compatibility_consequence3: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eA \<or> eB) \<longrightarrow> A = eA" 11 by auto 12 13lemma Filter_actAisFilter_extA: 14 "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext A \<or> a \<in> ext B) tr \<Longrightarrow> 15 Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr" 16 apply (rule ForallPFilterQR) 17 text \<open>i.e.: \<open>(\<forall>x. P x \<longrightarrow> (Q x = R x)) \<Longrightarrow> Forall P tr \<Longrightarrow> Filter Q \<cdot> tr = Filter R \<cdot> tr\<close>\<close> 18 prefer 2 apply assumption 19 apply (rule compatibility_consequence3) 20 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1) 21 done 22 23 24text \<open> 25 The next two theorems are only necessary, as there is no theorem 26 \<open>ext (A \<parallel> B) = ext (B \<parallel> A)\<close> 27\<close> 28 29lemma compatibility_consequence4: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eB \<or> eA) \<longrightarrow> A = eA" 30 by auto 31 32lemma Filter_actAisFilter_extA2: 33 "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext B \<or> a \<in> ext A) tr \<Longrightarrow> 34 Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr" 35 apply (rule ForallPFilterQR) 36 prefer 2 apply (assumption) 37 apply (rule compatibility_consequence4) 38 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1) 39 done 40 41 42subsection \<open>Main Compositionality Theorem\<close> 43 44lemma compositionality: 45 assumes "is_trans_of A1" and "is_trans_of A2" 46 and "is_trans_of B1" and "is_trans_of B2" 47 and "is_asig_of A1" and "is_asig_of A2" 48 and "is_asig_of B1" and "is_asig_of B2" 49 and "compatible A1 B1" and "compatible A2 B2" 50 and "A1 =<| A2" and "B1 =<| B2" 51 shows "(A1 \<parallel> B1) =<| (A2 \<parallel> B2)" 52 apply (insert assms) 53 apply (simp add: is_asig_of_def) 54 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1]) 55 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1]) 56 apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par) 57 apply auto 58 apply (simp add: compositionality_tr) 59 apply (subgoal_tac "ext A1 = ext A2 \<and> ext B1 = ext B2") 60 prefer 2 61 apply (simp add: externals_def) 62 apply (erule conjE)+ 63 text \<open>rewrite with proven subgoal\<close> 64 apply (simp add: externals_of_par) 65 apply auto 66 text \<open>2 goals, the 3rd has been solved automatically\<close> 67 text \<open>1: \<open>Filter A2 x \<in> traces A2\<close>\<close> 68 apply (drule_tac A = "traces A1" in subsetD) 69 apply assumption 70 apply (simp add: Filter_actAisFilter_extA) 71 text \<open>2: \<open>Filter B2 x \<in> traces B2\<close>\<close> 72 apply (drule_tac A = "traces B1" in subsetD) 73 apply assumption 74 apply (simp add: Filter_actAisFilter_extA2) 75 done 76 77end 78