equal
deleted
inserted
replaced
112 |
112 |
113 theorem lfp_conv_while: |
113 theorem lfp_conv_while: |
114 "[| mono f; finite U; f U = U |] ==> |
114 "[| mono f; finite U; f U = U |] ==> |
115 lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))" |
115 lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))" |
116 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and |
116 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and |
117 r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter> |
117 r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter> |
118 inv_image finite_psubset (op - U o fst)" in while_rule) |
118 inv_image finite_psubset (op - U o fst)" in while_rule) |
119 apply (subst lfp_unfold) |
119 apply (subst lfp_unfold) |
120 apply assumption |
120 apply assumption |
121 apply (simp add: monoD) |
121 apply (simp add: monoD) |
122 apply (subst lfp_unfold) |
122 apply (subst lfp_unfold) |