equal
deleted
inserted
replaced
113 by (auto intro!: lfp_lowerbound) |
113 by (auto intro!: lfp_lowerbound) |
114 thus ?case by (simp add: L.simps(5)) |
114 thus ?case by (simp add: L.simps(5)) |
115 qed auto |
115 qed auto |
116 |
116 |
117 text\<open>Make @{const L} executable by replacing @{const lfp} with the @{const |
117 text\<open>Make @{const L} executable by replacing @{const lfp} with the @{const |
118 while} combinator from theory @{theory While_Combinator}. The @{const while} |
118 while} combinator from theory @{theory "HOL-Library.While_Combinator"}. The @{const while} |
119 combinator obeys the recursion equation |
119 combinator obeys the recursion equation |
120 @{thm[display] While_Combinator.while_unfold[no_vars]} |
120 @{thm[display] While_Combinator.while_unfold[no_vars]} |
121 and is thus executable.\<close> |
121 and is thus executable.\<close> |
122 |
122 |
123 lemma L_While: fixes b c X |
123 lemma L_While: fixes b c X |