src/ZF/UNITY/FP.thy
 author wenzelm Wed, 27 Mar 2013 16:38:25 +0100 changeset 51553 63327f679cff parent 46823 57bf0cecb366 child 58871 c399ae4b836f permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
```
(*  Title:      ZF/UNITY/FP.thy
Author:     Sidi O Ehmety, Computer Laboratory

From Misra, "A Logic for Concurrent Programming", 1994

Theory ported from HOL.
*)

theory FP imports UNITY begin

definition
FP_Orig :: "i=>i"  where
"FP_Orig(F) == \<Union>({A \<in> Pow(state). \<forall>B. F \<in> stable(A \<inter> B)})"

definition
FP :: "i=>i"  where
"FP(F) == {s\<in>state. F \<in> stable({s})}"

lemma FP_Orig_type: "FP_Orig(F) \<subseteq> 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) \<subseteq> 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 \<in> program ==> F \<in> stable(FP_Orig(F) \<inter> B)"
apply (simp only: FP_Orig_def stable_def Int_Union2)
apply (blast intro: constrains_UN)
done

lemma FP_Orig_weakest2:
"[| \<forall>B. F \<in> stable (A \<inter> B); st_set(A) |]  ==> A \<subseteq> 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 \<in> program ==> F \<in> stable (FP(F) \<inter> B)"
apply (subgoal_tac "FP (F) \<inter> B = (\<Union>x\<in>B. FP (F) \<inter> {x}) ")
prefer 2 apply blast
apply (unfold FP_def stable_def)
apply (rule constrains_UN)
done

lemma FP_subset_FP_Orig: "F \<in> program ==> FP(F) \<subseteq> FP_Orig(F)"
by (rule stable_FP_Int [THEN FP_Orig_weakest], auto)

lemma FP_Orig_subset_FP: "F \<in> program ==> FP_Orig(F) \<subseteq> FP(F)"
apply (unfold FP_Orig_def FP_def, clarify)
apply (drule_tac x = "{x}" in spec)
apply (frule stableD2)
apply (auto simp add: cons_absorb st_set_def)
done

lemma FP_equivalence: "F \<in> program ==> FP(F) = FP_Orig(F)"
by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig)

lemma FP_weakest [rule_format]:
"[| \<forall>B. F \<in> stable(A \<inter> B); F \<in> program; st_set(A) |] ==> A \<subseteq> FP(F)"