author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 16184 | 80617b8d33c5 |
child 18556 | dc39832e9280 |
permissions | -rw-r--r-- |
13846 | 1 |
(* Title: HOL/UNITY/Transformers |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2003 University of Cambridge |
|
5 |
||
6 |
David Meier's thesis |
|
7 |
*) |
|
8 |
||
9 |
header{*Progress Set Examples*} |
|
10 |
||
16417 | 11 |
theory Progress imports UNITY_Main begin |
13846 | 12 |
|
13 |
subsection {*The Composition of Two Single-Assignment Programs*} |
|
14 |
text{*Thesis Section 4.4.2*} |
|
15 |
||
16 |
constdefs |
|
17 |
FF :: "int program" |
|
18 |
"FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
|
19 |
||
20 |
GG :: "int program" |
|
21 |
"GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)" |
|
22 |
||
23 |
subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} |
|
24 |
||
25 |
lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV" |
|
26 |
by force |
|
27 |
||
28 |
lemma FF_eq: |
|
29 |
"FF = mk_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
|
30 |
by (simp add: FF_def mk_total_program_def totalize_def totalize_act_def |
|
31 |
program_equalityI Domain_actFF) |
|
32 |
||
33 |
lemma wp_actFF: |
|
34 |
"wp (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = atLeast (k - 1)" |
|
35 |
by (force simp add: wp_def) |
|
36 |
||
37 |
lemma wens_FF: "wens FF (range (\<lambda>x. (x, x+1))) (atLeast k) = atLeast (k - 1)" |
|
38 |
by (force simp add: FF_eq wens_single_eq wp_actFF) |
|
39 |
||
40 |
lemma single_valued_actFF: "single_valued (range (\<lambda>x::int. (x, x + 1)))" |
|
41 |
by (force simp add: single_valued_def) |
|
42 |
||
43 |
lemma wens_single_finite_FF: |
|
44 |
"wens_single_finite (range (\<lambda>x. (x, x+1))) (atLeast k) n = |
|
45 |
atLeast (k - int n)" |
|
46 |
apply (induct n, simp) |
|
47 |
apply (force simp add: wens_FF |
|
48 |
def_wens_single_finite_Suc_eq_wens [OF FF_eq single_valued_actFF]) |
|
49 |
done |
|
50 |
||
51 |
lemma wens_single_FF_eq_UNIV: |
|
52 |
"wens_single (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = UNIV" |
|
53 |
apply (auto simp add: wens_single_eq_Union) |
|
54 |
apply (rule_tac x="nat (k-x)" in exI) |
|
55 |
apply (simp add: wens_single_finite_FF) |
|
56 |
done |
|
57 |
||
58 |
lemma wens_set_FF: |
|
59 |
"wens_set FF (atLeast k) = insert UNIV (atLeast ` atMost k)" |
|
60 |
apply (auto simp add: wens_set_single_eq [OF FF_eq single_valued_actFF] |
|
61 |
wens_single_FF_eq_UNIV wens_single_finite_FF) |
|
62 |
apply (erule notE) |
|
63 |
apply (rule_tac x="nat (k-xa)" in range_eqI) |
|
64 |
apply (simp add: wens_single_finite_FF) |
|
65 |
done |
|
66 |
||
67 |
subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*} |
|
68 |
||
69 |
lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)" |
|
70 |
apply (simp add: Progress.wens_FF [symmetric] wens_ensures) |
|
71 |
apply (simp add: wens_ensures FF_eq) |
|
72 |
done |
|
73 |
||
74 |
lemma atLeast_leadsTo: "FF \<in> atLeast (k - int n) leadsTo atLeast (k::int)" |
|
75 |
apply (induct n) |
|
76 |
apply (simp_all add: leadsTo_refl) |
|
77 |
apply (rule_tac A = "atLeast (k - int n - 1)" in leadsTo_weaken_L) |
|
78 |
apply (blast intro: leadsTo_Trans atLeast_ensures, force) |
|
79 |
done |
|
80 |
||
81 |
lemma UN_atLeast_UNIV: "(\<Union>n. atLeast (k - int n)) = UNIV" |
|
82 |
apply auto |
|
83 |
apply (rule_tac x = "nat (k - x)" in exI, simp) |
|
84 |
done |
|
85 |
||
86 |
lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)" |
|
87 |
apply (subst UN_atLeast_UNIV [symmetric]) |
|
88 |
apply (rule leadsTo_UN [OF atLeast_leadsTo]) |
|
89 |
done |
|
90 |
||
13866 | 91 |
text{*Result (4.39): Applying the leadsTo-Join Theorem*} |
13846 | 92 |
theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)" |
93 |
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k") |
|
94 |
apply simp |
|
13866 | 95 |
apply (rule_tac T = "atLeast 0" in leadsTo_Join) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13866
diff
changeset
|
96 |
apply (simp add: awp_iff FF_def, safety) |
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
13866
diff
changeset
|
97 |
apply (simp add: awp_iff GG_def wens_set_FF, safety) |
13846 | 98 |
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
99 |
done |
|
100 |
||
101 |
end |