equal
deleted
inserted
replaced
55 lemmas impl_ioas = sender_ioa_def receiver_ioa_def |
55 lemmas impl_ioas = sender_ioa_def receiver_ioa_def |
56 and impl_trans = sender_trans_def receiver_trans_def |
56 and impl_trans = sender_trans_def receiver_trans_def |
57 and impl_asigs = sender_asig_def receiver_asig_def |
57 and impl_asigs = sender_asig_def receiver_asig_def |
58 |
58 |
59 declare let_weak_cong [cong] |
59 declare let_weak_cong [cong] |
60 declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp] |
60 declare ioa_triple_proj [simp] starts_of_par [simp] |
61 |
61 |
62 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def |
62 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def |
63 lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas |
63 lemmas hom_ioas = |
|
64 env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp] |
|
65 asig_projections set_lemmas |
64 |
66 |
65 |
67 |
66 subsection {* lemmas about reduce *} |
68 subsection {* lemmas about reduce *} |
67 |
69 |
68 lemma l_iff_red_nil: "(reduce l = []) = (l = [])" |
70 lemma l_iff_red_nil: "(reduce l = []) = (l = [])" |
94 apply (rule conjI) |
96 apply (rule conjI) |
95 txt {* @{text "-->"} *} |
97 txt {* @{text "-->"} *} |
96 apply (induct_tac "l") |
98 apply (induct_tac "l") |
97 apply (simp (no_asm)) |
99 apply (simp (no_asm)) |
98 apply (case_tac "list=[]") |
100 apply (case_tac "list=[]") |
99 apply (simp add: reverse.simps) |
101 apply simp |
100 apply (rule impI) |
102 apply (rule impI) |
101 apply (simp (no_asm)) |
103 apply (simp (no_asm)) |
102 apply (cut_tac l = "list" in cons_not_nil) |
104 apply (cut_tac l = "list" in cons_not_nil) |
103 apply (simp del: reduce_Cons) |
105 apply (simp del: reduce_Cons) |
104 apply (erule exE)+ |
106 apply (erule exE)+ |