equal
deleted
inserted
replaced
109 apply(simp (no_asm) add: L3_5v_lemma3) |
109 apply(simp (no_asm) add: L3_5v_lemma3) |
110 apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty) |
110 apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty) |
111 apply(rule conjI) |
111 apply(rule conjI) |
112 apply (blast dest: L3_5i) |
112 apply (blast dest: L3_5i) |
113 apply(simp add: SEM_def sem_def id_def) |
113 apply(simp add: SEM_def sem_def id_def) |
114 apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow) |
114 apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow) |
|
115 apply blast |
115 done |
116 done |
116 |
117 |
117 lemma atom_hoare_sound [rule_format]: |
118 lemma atom_hoare_sound [rule_format]: |
118 " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q" |
119 " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q" |
119 apply (unfold com_validity_def) |
120 apply (unfold com_validity_def) |