# Theory FP

Up to index of Isabelle/ZF/UNITY

theory FP
imports UNITY
begin

    (*  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}})