Theory FP
section‹Fixed Point of a Program›
theory FP imports UNITY begin
definition
FP_Orig :: "i⇒i" where
"FP_Orig(F) ≡ ⋃({A ∈ Pow(state). ∀B. F ∈ stable(A ∩ B)})"
definition
FP :: "i⇒i" where
"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))"
unfolding 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))"
unfolding st_set_def
apply (rule FP_type)
done
lemma stable_FP_Orig_Int: "F ∈ program ⟹ F ∈ stable(FP_Orig(F) ∩ 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 ∩ 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]
lemma stable_FP_Int: "F ∈ program ⟹ F ∈ stable (FP(F) ∩ B)"
apply (subgoal_tac "FP (F) ∩ B = (⋃x∈B. FP (F) ∩ {x}) ")
prefer 2 apply blast
apply (simp (no_asm_simp) add: Int_cons_right)
unfolding 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 ∩ 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) = (⋃act ∈ Acts(F). A - {s ∈ state. act``{s} ⊆ {s}})"
by (unfold FP_def stable_def constrains_def st_set_def, blast)
end