| changeset 16417 | 9bc16273c2d4 |
| parent 15481 | fc075ae929e4 |
| child 24893 | b8ef7afe3a6b |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
8 Theory ported from HOL. |
8 Theory ported from HOL. |
9 *) |
9 *) |
10 |
10 |
11 header{*Fixed Point of a Program*} |
11 header{*Fixed Point of a Program*} |
12 |
12 |
13 theory FP = UNITY: |
13 theory FP imports UNITY begin |
14 |
14 |
15 constdefs |
15 constdefs |
16 FP_Orig :: "i=>i" |
16 FP_Orig :: "i=>i" |
17 "FP_Orig(F) == Union({A \<in> Pow(state). \<forall>B. F \<in> stable(A Int B)})" |
17 "FP_Orig(F) == Union({A \<in> Pow(state). \<forall>B. F \<in> stable(A Int B)})" |
18 |
18 |