author | paulson |
Fri, 21 Nov 2008 13:17:43 +0100 | |
changeset 28869 | 191cbfac6c9a |
parent 28866 | 30cd9d89a0fb |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
28869
191cbfac6c9a
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
paulson
parents:
28866
diff
changeset
|
1 |
(* Title: HOL/UNITY/Progress |
13846 | 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 |
||
18556 | 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) |
28869
191cbfac6c9a
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
paulson
parents:
28866
diff
changeset
|
96 |
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
191cbfac6c9a
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
paulson
parents:
28866
diff
changeset
|
97 |
apply (simp add: awp_iff_constrains FF_def, safety) |
191cbfac6c9a
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
paulson
parents:
28866
diff
changeset
|
98 |
apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety) |
13846 | 99 |
done |
100 |
||
101 |
end |