src/HOL/UNITY/FP.thy
author nipkow
Fri, 27 Mar 2020 12:28:05 +0100
changeset 71593 71579bd59cd4
parent 69661 a03a63b81f44
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37936
1e4c5015a72e updated some headers;
wenzelm
parents: 35416
diff changeset
     1
(*  Title:      HOL/UNITY/FP.thy
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
From Misra, "A Logic for Concurrent Programming", 1994
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
63146
f1ecba0272f9 isabelle update_cartouches -c -t;
wenzelm
parents: 61952
diff changeset
     8
section\<open>Fixed Point of a Program\<close>
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13796
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15481
diff changeset
    10
theory FP imports UNITY begin
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 16417
diff changeset
    12
definition FP_Orig :: "'a program => 'a set" where
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    13
    "FP_Orig F == \<Union>{A. \<forall>B. F \<in> stable (A \<inter> B)}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 16417
diff changeset
    15
definition FP :: "'a program => 'a set" where
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    16
    "FP F == {s. F \<in> stable {s}}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    18
lemma stable_FP_Orig_Int: "F \<in> stable (FP_Orig F Int B)"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 13812
diff changeset
    19
apply (simp only: FP_Orig_def stable_def Int_Union2)
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    20
apply (blast intro: constrains_UN)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    21
done
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    22
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    23
lemma FP_Orig_weakest:
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    24
    "(\<And>B. F \<in> stable (A \<inter> B)) \<Longrightarrow> A <= FP_Orig F"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 13812
diff changeset
    25
by (simp add: FP_Orig_def stable_def, blast)
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    26
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    27
lemma stable_FP_Int: "F \<in> stable (FP F \<inter> B)"
69661
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    28
proof -
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    29
  have "F \<in> stable (\<Union>x\<in>B. FP F \<inter> {x})"
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    30
    apply (simp only: Int_insert_right FP_def stable_def)
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    31
    apply (rule constrains_UN)
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    32
    apply simp
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    33
    done
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    34
  also have "(\<Union>x\<in>B. FP F \<inter> {x}) = FP F \<inter> B"
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    35
    by simp
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    36
  finally show ?thesis .
a03a63b81f44 tuned proofs
haftmann
parents: 67613
diff changeset
    37
qed
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    38
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    39
lemma FP_equivalence: "FP F = FP_Orig F"
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    40
apply (rule equalityI) 
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    41
 apply (rule stable_FP_Int [THEN FP_Orig_weakest])
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 13812
diff changeset
    42
apply (simp add: FP_Orig_def FP_def, clarify)
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    43
apply (drule_tac x = "{x}" in spec)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    44
apply (simp add: Int_insert_right)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    45
done
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    46
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    47
lemma FP_weakest:
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63146
diff changeset
    48
    "(\<And>B. F \<in> stable (A Int B)) \<Longrightarrow> A <= FP F"
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    49
by (simp add: FP_equivalence FP_Orig_weakest)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    50
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    51
lemma Compl_FP: 
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    52
    "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    53
by (simp add: FP_def stable_def constrains_def, blast)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    54
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    55
lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    56
by (simp add: Diff_eq Compl_FP)
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 5648
diff changeset
    57
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    58
lemma totalize_FP [simp]: "FP (totalize F) = FP F"
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    59
by (simp add: FP_def)
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    60
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    61
end