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 |
|
|
11 |
theory Progress = UNITY_Main:
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
(*????????????????Int*)
|
|
16 |
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
|
|
17 |
by simp
|
|
18 |
|
|
19 |
|
|
20 |
|
|
21 |
|
|
22 |
subsection {*The Composition of Two Single-Assignment Programs*}
|
|
23 |
text{*Thesis Section 4.4.2*}
|
|
24 |
|
|
25 |
constdefs
|
|
26 |
FF :: "int program"
|
|
27 |
"FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
|
|
28 |
|
|
29 |
GG :: "int program"
|
|
30 |
"GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
|
|
31 |
|
|
32 |
subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
|
|
33 |
|
|
34 |
lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
|
|
35 |
by force
|
|
36 |
|
|
37 |
lemma FF_eq:
|
|
38 |
"FF = mk_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
|
|
39 |
by (simp add: FF_def mk_total_program_def totalize_def totalize_act_def
|
|
40 |
program_equalityI Domain_actFF)
|
|
41 |
|
|
42 |
lemma wp_actFF:
|
|
43 |
"wp (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = atLeast (k - 1)"
|
|
44 |
by (force simp add: wp_def)
|
|
45 |
|
|
46 |
lemma wens_FF: "wens FF (range (\<lambda>x. (x, x+1))) (atLeast k) = atLeast (k - 1)"
|
|
47 |
by (force simp add: FF_eq wens_single_eq wp_actFF)
|
|
48 |
|
|
49 |
lemma single_valued_actFF: "single_valued (range (\<lambda>x::int. (x, x + 1)))"
|
|
50 |
by (force simp add: single_valued_def)
|
|
51 |
|
|
52 |
lemma wens_single_finite_FF:
|
|
53 |
"wens_single_finite (range (\<lambda>x. (x, x+1))) (atLeast k) n =
|
|
54 |
atLeast (k - int n)"
|
|
55 |
apply (induct n, simp)
|
|
56 |
apply (force simp add: wens_FF
|
|
57 |
def_wens_single_finite_Suc_eq_wens [OF FF_eq single_valued_actFF])
|
|
58 |
done
|
|
59 |
|
|
60 |
lemma wens_single_FF_eq_UNIV:
|
|
61 |
"wens_single (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = UNIV"
|
|
62 |
apply (auto simp add: wens_single_eq_Union)
|
|
63 |
apply (rule_tac x="nat (k-x)" in exI)
|
|
64 |
apply (simp add: wens_single_finite_FF)
|
|
65 |
done
|
|
66 |
|
|
67 |
lemma wens_set_FF:
|
|
68 |
"wens_set FF (atLeast k) = insert UNIV (atLeast ` atMost k)"
|
|
69 |
apply (auto simp add: wens_set_single_eq [OF FF_eq single_valued_actFF]
|
|
70 |
wens_single_FF_eq_UNIV wens_single_finite_FF)
|
|
71 |
apply (erule notE)
|
|
72 |
apply (rule_tac x="nat (k-xa)" in range_eqI)
|
|
73 |
apply (simp add: wens_single_finite_FF)
|
|
74 |
done
|
|
75 |
|
|
76 |
subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
|
|
77 |
|
|
78 |
lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
|
|
79 |
apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
|
|
80 |
apply (simp add: wens_ensures FF_eq)
|
|
81 |
done
|
|
82 |
|
|
83 |
lemma atLeast_leadsTo: "FF \<in> atLeast (k - int n) leadsTo atLeast (k::int)"
|
|
84 |
apply (induct n)
|
|
85 |
apply (simp_all add: leadsTo_refl)
|
|
86 |
apply (rule_tac A = "atLeast (k - int n - 1)" in leadsTo_weaken_L)
|
|
87 |
apply (blast intro: leadsTo_Trans atLeast_ensures, force)
|
|
88 |
done
|
|
89 |
|
|
90 |
lemma UN_atLeast_UNIV: "(\<Union>n. atLeast (k - int n)) = UNIV"
|
|
91 |
apply auto
|
|
92 |
apply (rule_tac x = "nat (k - x)" in exI, simp)
|
|
93 |
done
|
|
94 |
|
|
95 |
lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)"
|
|
96 |
apply (subst UN_atLeast_UNIV [symmetric])
|
|
97 |
apply (rule leadsTo_UN [OF atLeast_leadsTo])
|
|
98 |
done
|
|
99 |
|
|
100 |
text{*Result (4.39): Applying the Union Theorem*}
|
|
101 |
theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
|
|
102 |
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
|
|
103 |
apply simp
|
|
104 |
apply (rule_tac T = "atLeast 0" in leadsTo_Union)
|
|
105 |
apply (simp add: awp_iff FF_def, constrains)
|
|
106 |
apply (simp add: awp_iff GG_def wens_set_FF, constrains)
|
|
107 |
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
|
|
108 |
done
|
|
109 |
|
|
110 |
end
|