|
(* Title: HOL/UNITY/Comp/Progress.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
David Meier's thesis
*)
section\<open>Progress Set Examples\<close>
theory Progress imports "../UNITY_Main" begin
subsection \<open>The Composition of Two Single-Assignment Programs\<close>
text\<open>Thesis Section 4.4.2\<close>
definition FF :: "int program" where
"FF = mk_total_program (UNIV, {range (\x. (x, x+1))}, UNIV)"
definition GG :: "int program" where
"GG = mk_total_program (UNIV, {range (\x. (x, 2*x))}, UNIV)"
subsubsection \<open>Calculating \<^term>\<open>wens_set FF (atLeast k)\<close>\<close>
lemma Domain_actFF: "Domain (range (\x::int. (x, x + 1))) = UNIV"
by force
lemma FF_eq:
"FF = mk_program (UNIV, {range (\x. (x, x+1))}, UNIV)"
by (simp add: FF_def mk_total_program_def totalize_def totalize_act_def
program_equalityI Domain_actFF)
lemma wp_actFF:
"wp (range (\x::int. (x, x + 1))) (atLeast k) = atLeast (k - 1)"
by (force simp add: wp_def)
lemma wens_FF: "wens FF (range (\x. (x, x+1))) (atLeast k) = atLeast (k - 1)"
by (force simp add: FF_eq wens_single_eq wp_actFF)
lemma single_valued_actFF: "single_valued (range (\x::int. (x, x + 1)))"
by (force simp add: single_valued_def)
lemma wens_single_finite_FF:
"wens_single_finite (range (\x. (x, x+1))) (atLeast k) n =
atLeast (k - int n)"
apply (induct n, simp)
apply (force simp add: wens_FF
def_wens_single_finite_Suc_eq_wens [OF FF_eq single_valued_actFF])
done
lemma wens_single_FF_eq_UNIV:
"wens_single (range (\x::int. (x, x + 1))) (atLeast k) = UNIV"
apply (auto simp add: wens_single_eq_Union)
apply (rule_tac x="nat (k-x)" in exI)
apply (simp add: wens_single_finite_FF)
done
lemma wens_set_FF:
"wens_set FF (atLeast k) = insert UNIV (atLeast ` atMost k)"
apply (auto simp add: wens_set_single_eq [OF FF_eq single_valued_actFF]
wens_single_FF_eq_UNIV wens_single_finite_FF)
apply (erule notE)
apply (rule_tac x="nat (k-xa)" in range_eqI)
apply (simp add: wens_single_finite_FF)
done
subsubsection \<open>Proving \<^term>\<open>FF \<in> UNIV leadsTo atLeast (k::int)\<close>\<close>
lemma atLeast_ensures: "FF \ atLeast (k - 1) ensures atLeast (k::int)"
apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
apply (simp add: wens_ensures FF_eq)
done
lemma atLeast_leadsTo: "FF \ atLeast (k - int n) leadsTo atLeast (k::int)"
apply (induct n)
apply (simp_all add: leadsTo_refl)
apply (rule_tac A = "atLeast (k - int n - 1)" in leadsTo_weaken_L)
apply (blast intro: leadsTo_Trans atLeast_ensures, force)
done
lemma UN_atLeast_UNIV: "(\n. atLeast (k - int n)) = UNIV"
apply auto
apply (rule_tac x = "nat (k - x)" in exI, simp)
done
lemma FF_leadsTo: "FF \ UNIV leadsTo atLeast (k::int)"
apply (subst UN_atLeast_UNIV [symmetric])
apply (rule leadsTo_UN [OF atLeast_leadsTo])
done
text\<open>Result (4.39): Applying the leadsTo-Join Theorem\<close>
theorem "FF\GG \ atLeast 0 leadsTo atLeast (k::int)"
apply (subgoal_tac "FF\GG \ (atLeast 0 \ atLeast 0) leadsTo atLeast k")
apply simp
apply (rule_tac T = "atLeast 0" in leadsTo_Join)
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
apply (simp add: awp_iff_constrains FF_def, safety)
apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
done
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
