1414 next |
1414 next |
1415 show "(f^^k) bot \<le> lfp f" |
1415 show "(f^^k) bot \<le> lfp f" |
1416 using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp |
1416 using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp |
1417 qed |
1417 qed |
1418 |
1418 |
|
1419 lemma mono_pow: |
|
1420 fixes f :: "'a \<Rightarrow> 'a::complete_lattice" |
|
1421 shows "mono f \<Longrightarrow> mono (f ^^ n)" |
|
1422 by (induction n) (auto simp: mono_def) |
|
1423 |
|
1424 lemma lfp_funpow: |
|
1425 assumes f: "mono f" shows "lfp (f ^^ Suc n) = lfp f" |
|
1426 proof (rule antisym) |
|
1427 show "lfp f \<le> lfp (f ^^ Suc n)" |
|
1428 proof (rule lfp_lowerbound) |
|
1429 have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))" |
|
1430 unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def) |
|
1431 then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)" |
|
1432 by (simp add: comp_def) |
|
1433 qed |
|
1434 have "(f^^n) (lfp f) = lfp f" for n |
|
1435 by (induction n) (auto intro: f lfp_unfold[symmetric]) |
|
1436 then show "lfp (f^^Suc n) \<le> lfp f" |
|
1437 by (intro lfp_lowerbound) (simp del: funpow.simps) |
|
1438 qed |
|
1439 |
|
1440 lemma gfp_funpow: |
|
1441 assumes f: "mono f" shows "gfp (f ^^ Suc n) = gfp f" |
|
1442 proof (rule antisym) |
|
1443 show "gfp f \<ge> gfp (f ^^ Suc n)" |
|
1444 proof (rule gfp_upperbound) |
|
1445 have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))" |
|
1446 unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def) |
|
1447 then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)" |
|
1448 by (simp add: comp_def) |
|
1449 qed |
|
1450 have "(f^^n) (gfp f) = gfp f" for n |
|
1451 by (induction n) (auto intro: f gfp_unfold[symmetric]) |
|
1452 then show "gfp (f^^Suc n) \<ge> gfp f" |
|
1453 by (intro gfp_upperbound) (simp del: funpow.simps) |
|
1454 qed |
1419 |
1455 |
1420 subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *} |
1456 subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *} |
1421 |
1457 |
1422 context semiring_1 |
1458 context semiring_1 |
1423 begin |
1459 begin |