src/HOL/Library/While_Combinator.thy
 changeset 11047 10c51288b00d parent 10997 e14029f92770 child 11284 981ea92a86dd
equal inserted replaced
11046:b5f5942781a0 11047:10c51288b00d
`   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)`