equal
deleted
inserted
replaced
80 apply (rule monoI) |
80 apply (rule monoI) |
81 apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD) |
81 apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD) |
82 apply (rule up_chainI) |
82 apply (rule up_chainI) |
83 apply simp+ |
83 apply simp+ |
84 apply (drule Un_absorb1) |
84 apply (drule Un_absorb1) |
85 apply auto |
85 apply (auto simp add: nat_not_singleton) |
86 done |
86 done |
87 |
87 |
88 |
88 |
89 constdefs |
89 constdefs |
90 down_cont :: "('a set => 'a set) => bool" |
90 down_cont :: "('a set => 'a set) => bool" |
108 apply (rule monoI) |
108 apply (rule monoI) |
109 apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD) |
109 apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD) |
110 apply (rule down_chainI) |
110 apply (rule down_chainI) |
111 apply simp+ |
111 apply simp+ |
112 apply (drule Int_absorb1) |
112 apply (drule Int_absorb1) |
113 apply auto |
113 apply (auto simp add: nat_not_singleton) |
114 done |
114 done |
115 |
115 |
116 |
116 |
117 subsection "Iteration" |
117 subsection "Iteration" |
118 |
118 |