(* Title: ZF/UNITY/FP.thy ID: $Id: FP.thy,v 1.6 2005/06/17 14:15:11 haftmann Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge From Misra, "A Logic for Concurrent Programming", 1994 Theory ported from HOL. *) header{*Fixed Point of a Program*} theory FP imports UNITY begin constdefs FP_Orig :: "i=>i" "FP_Orig(F) == Union({A ∈ Pow(state). ∀B. F ∈ stable(A Int B)})" FP :: "i=>i" "FP(F) == {s∈state. F ∈ stable({s})}" lemma FP_Orig_type: "FP_Orig(F) ⊆ state" by (unfold FP_Orig_def, blast) lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))" apply (unfold st_set_def) apply (rule FP_Orig_type) done lemma FP_type: "FP(F) ⊆ state" by (unfold FP_def, blast) lemma st_set_FP [iff]: "st_set(FP(F))" apply (unfold st_set_def) apply (rule FP_type) done lemma stable_FP_Orig_Int: "F ∈ program ==> F ∈ stable(FP_Orig(F) Int B)" apply (simp only: FP_Orig_def stable_def Int_Union2) apply (blast intro: constrains_UN) done lemma FP_Orig_weakest2: "[| ∀B. F ∈ stable (A Int B); st_set(A) |] ==> A ⊆ FP_Orig(F)" by (unfold FP_Orig_def stable_def st_set_def, blast) lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard] lemma stable_FP_Int: "F ∈ program ==> F ∈ stable (FP(F) Int B)" apply (subgoal_tac "FP (F) Int B = (\<Union>x∈B. FP (F) Int {x}) ") prefer 2 apply blast apply (simp (no_asm_simp) add: Int_cons_right) apply (unfold FP_def stable_def) apply (rule constrains_UN) apply (auto simp add: cons_absorb) done lemma FP_subset_FP_Orig: "F ∈ program ==> FP(F) ⊆ FP_Orig(F)" by (rule stable_FP_Int [THEN FP_Orig_weakest], auto) lemma FP_Orig_subset_FP: "F ∈ program ==> FP_Orig(F) ⊆ FP(F)" apply (unfold FP_Orig_def FP_def, clarify) apply (drule_tac x = "{x}" in spec) apply (simp add: Int_cons_right) apply (frule stableD2) apply (auto simp add: cons_absorb st_set_def) done lemma FP_equivalence: "F ∈ program ==> FP(F) = FP_Orig(F)" by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig) lemma FP_weakest [rule_format]: "[| ∀B. F ∈ stable(A Int B); F ∈ program; st_set(A) |] ==> A ⊆ FP(F)" by (simp add: FP_equivalence FP_Orig_weakest) lemma Diff_FP: "[| F ∈ program; st_set(A) |] ==> A-FP(F) = (\<Union>act ∈ Acts(F). A - {s ∈ state. act``{s} ⊆ {s}})" by (unfold FP_def stable_def constrains_def st_set_def, blast) ML {* val FP_Orig_type = thm "FP_Orig_type"; val st_set_FP_Orig = thm "st_set_FP_Orig"; val FP_type = thm "FP_type"; val st_set_FP = thm "st_set_FP"; val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; val FP_Orig_weakest2 = thm "FP_Orig_weakest2"; val stable_FP_Int = thm "stable_FP_Int"; val FP_subset_FP_Orig = thm "FP_subset_FP_Orig"; val FP_Orig_subset_FP = thm "FP_Orig_subset_FP"; val FP_equivalence = thm "FP_equivalence"; val FP_weakest = thm "FP_weakest"; val Diff_FP = thm "Diff_FP"; *} end
lemma FP_Orig_type:
FP_Orig(F) ⊆ state
lemma st_set_FP_Orig:
st_set(FP_Orig(F))
lemma FP_type:
FP(F) ⊆ state
lemma st_set_FP:
st_set(FP(F))
lemma stable_FP_Orig_Int:
F ∈ program ==> F ∈ stable(FP_Orig(F) ∩ B)
lemma FP_Orig_weakest2:
[| ∀B. F ∈ stable(A ∩ B); st_set(A) |] ==> A ⊆ FP_Orig(F)
lemmas FP_Orig_weakest:
[| !!B. F ∈ stable(A ∩ B); st_set(A) |] ==> A ⊆ FP_Orig(F)
lemmas FP_Orig_weakest:
[| !!B. F ∈ stable(A ∩ B); st_set(A) |] ==> A ⊆ FP_Orig(F)
lemma stable_FP_Int:
F ∈ program ==> F ∈ stable(FP(F) ∩ B)
lemma FP_subset_FP_Orig:
F ∈ program ==> FP(F) ⊆ FP_Orig(F)
lemma FP_Orig_subset_FP:
F ∈ program ==> FP_Orig(F) ⊆ FP(F)
lemma FP_equivalence:
F ∈ program ==> FP(F) = FP_Orig(F)
lemma FP_weakest:
[| !!B. F ∈ stable(A ∩ B); F ∈ program; st_set(A) |] ==> A ⊆ FP(F)
lemma Diff_FP:
[| F ∈ program; st_set(A) |] ==> A - FP(F) = (\<Union>act∈Acts(F). A - {s ∈ state . act `` {s} ⊆ {s}})