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