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);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/FP.thy
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
From Misra, "A Logic for Concurrent Programming", 1994
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
Theory ported from HOL.
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     8
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     9
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    10
header{*Fixed Point of a Program*}
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    11
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15481
diff changeset
    12
theory FP imports UNITY begin
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition   
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
  FP_Orig :: "i=>i"  where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    16
    "FP_Orig(F) == \<Union>({A \<in> Pow(state). \<forall>B. F \<in> stable(A \<inter> B)})"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    17
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    18
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    19
  FP :: "i=>i"  where
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    20
    "FP(F) == {s\<in>state. F \<in> stable({s})}"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    21
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    22
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    23
lemma FP_Orig_type: "FP_Orig(F) \<subseteq> state"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    24
by (unfold FP_Orig_def, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    25
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    26
lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    27
apply (unfold st_set_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    28
apply (rule FP_Orig_type)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    29
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    30
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    31
lemma FP_type: "FP(F) \<subseteq> state"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    32
by (unfold FP_def, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    33
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    34
lemma st_set_FP [iff]: "st_set(FP(F))"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    35
apply (unfold st_set_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    36
apply (rule FP_type)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    37
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    38
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    39
lemma stable_FP_Orig_Int: "F \<in> program ==> F \<in> stable(FP_Orig(F) \<inter> B)"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14092
diff changeset
    40
apply (simp only: FP_Orig_def stable_def Int_Union2)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    41
apply (blast intro: constrains_UN)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    42
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    43
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    44
lemma FP_Orig_weakest2: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    45
    "[| \<forall>B. F \<in> stable (A \<inter> B); st_set(A) |]  ==> A \<subseteq> FP_Orig(F)"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14092
diff changeset
    46
by (unfold FP_Orig_def stable_def st_set_def, blast)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    47
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    48
lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2]
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    49
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    50
lemma stable_FP_Int: "F \<in> program ==> F \<in> stable (FP(F) \<inter> B)"
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    51
apply (subgoal_tac "FP (F) \<inter> B = (\<Union>x\<in>B. FP (F) \<inter> {x}) ")
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    52
 prefer 2 apply blast
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    53
apply (simp (no_asm_simp) add: Int_cons_right)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    54
apply (unfold FP_def stable_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    55
apply (rule constrains_UN)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    56
apply (auto simp add: cons_absorb)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    57
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    58
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    59
lemma FP_subset_FP_Orig: "F \<in> program ==> FP(F) \<subseteq> FP_Orig(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    60
by (rule stable_FP_Int [THEN FP_Orig_weakest], auto)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    61
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    62
lemma FP_Orig_subset_FP: "F \<in> program ==> FP_Orig(F) \<subseteq> FP(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    63
apply (unfold FP_Orig_def FP_def, clarify)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    64
apply (drule_tac x = "{x}" in spec)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    65
apply (simp add: Int_cons_right)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    66
apply (frule stableD2)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    67
apply (auto simp add: cons_absorb st_set_def)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    68
done
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    69
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    70
lemma FP_equivalence: "F \<in> program ==> FP(F) = FP_Orig(F)"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    71
by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    72
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    73
lemma FP_weakest [rule_format]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    74
     "[| \<forall>B. F \<in> stable(A \<inter> B); F \<in> program; st_set(A) |] ==> A \<subseteq> FP(F)"
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    75
by (simp add: FP_equivalence FP_Orig_weakest)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    76
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    77
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    78
lemma Diff_FP: 
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    79
     "[| F \<in> program;  st_set(A) |] 
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    80
      ==> A-FP(F) = (\<Union>act \<in> Acts(F). A - {s \<in> state. act``{s} \<subseteq> {s}})"
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    81
by (unfold FP_def stable_def constrains_def st_set_def, blast)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 12195
diff changeset
    82
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    83
end