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