src/HOL/UNITY/Comp/Progress.thy
 changeset 13846 b2c494d76012 child 13851 f6923453953a
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/UNITY/Comp/Progress.thy	Wed Mar 05 16:03:33 2003 +0100
1.3 @@ -0,0 +1,110 @@
1.4 +(*  Title:      HOL/UNITY/Transformers
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   2003  University of Cambridge
1.8 +
1.9 +David Meier's thesis
1.10 +*)
1.11 +
1.12 +header{*Progress Set Examples*}
1.13 +
1.14 +theory Progress = UNITY_Main:
1.15 +
1.16 +
1.17 +
1.18 +(*????????????????Int*)
1.19 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
1.20 +by simp
1.21 +
1.22 +
1.23 +
1.24 +
1.25 +subsection {*The Composition of Two Single-Assignment Programs*}
1.26 +text{*Thesis Section 4.4.2*}
1.27 +
1.28 +constdefs
1.29 +  FF :: "int program"
1.30 +    "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
1.31 +
1.32 +  GG :: "int program"
1.33 +    "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
1.34 +
1.35 +subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
1.36 +
1.37 +lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
1.38 +by force
1.39 +
1.40 +lemma FF_eq:
1.41 +      "FF = mk_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
1.42 +by (simp add: FF_def mk_total_program_def totalize_def totalize_act_def
1.43 +              program_equalityI Domain_actFF)
1.44 +
1.45 +lemma wp_actFF:
1.46 +     "wp (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = atLeast (k - 1)"
1.47 +by (force simp add: wp_def)
1.48 +
1.49 +lemma wens_FF: "wens FF (range (\<lambda>x. (x, x+1))) (atLeast k) = atLeast (k - 1)"
1.50 +by (force simp add: FF_eq wens_single_eq wp_actFF)
1.51 +
1.52 +lemma single_valued_actFF: "single_valued (range (\<lambda>x::int. (x, x + 1)))"
1.53 +by (force simp add: single_valued_def)
1.54 +
1.55 +lemma wens_single_finite_FF:
1.56 +     "wens_single_finite (range (\<lambda>x. (x, x+1))) (atLeast k) n =
1.57 +      atLeast (k - int n)"
1.58 +apply (induct n, simp)
1.59 +apply (force simp add: wens_FF
1.60 +            def_wens_single_finite_Suc_eq_wens [OF FF_eq single_valued_actFF])
1.61 +done
1.62 +
1.63 +lemma wens_single_FF_eq_UNIV:
1.64 +     "wens_single (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = UNIV"
1.65 +apply (auto simp add: wens_single_eq_Union)
1.66 +apply (rule_tac x="nat (k-x)" in exI)
1.67 +apply (simp add: wens_single_finite_FF)
1.68 +done
1.69 +
1.70 +lemma wens_set_FF:
1.71 +     "wens_set FF (atLeast k) = insert UNIV (atLeast ` atMost k)"
1.72 +apply (auto simp add: wens_set_single_eq [OF FF_eq single_valued_actFF]
1.73 +                      wens_single_FF_eq_UNIV wens_single_finite_FF)
1.74 +apply (erule notE)
1.75 +apply (rule_tac x="nat (k-xa)" in range_eqI)
1.76 +apply (simp add: wens_single_finite_FF)
1.77 +done
1.78 +
1.79 +subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
1.80 +
1.81 +lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
1.82 +apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
1.83 +apply (simp add: wens_ensures FF_eq)
1.84 +done
1.85 +
1.86 +lemma atLeast_leadsTo: "FF \<in> atLeast (k - int n) leadsTo atLeast (k::int)"
1.87 +apply (induct n)
1.89 +apply (rule_tac A = "atLeast (k - int n - 1)" in leadsTo_weaken_L)
1.90 + apply (blast intro: leadsTo_Trans atLeast_ensures, force)
1.91 +done
1.92 +
1.93 +lemma UN_atLeast_UNIV: "(\<Union>n. atLeast (k - int n)) = UNIV"
1.94 +apply auto
1.95 +apply (rule_tac x = "nat (k - x)" in exI, simp)
1.96 +done
1.97 +
1.98 +lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)"
1.99 +apply (subst UN_atLeast_UNIV [symmetric])
1.101 +done
1.102 +
1.103 +text{*Result (4.39): Applying the Union Theorem*}
1.104 +theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
1.105 +apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
1.106 + apply simp
1.107 +apply (rule_tac T = "atLeast 0" in leadsTo_Union)
1.108 +  apply (simp add: awp_iff FF_def, constrains)
1.109 + apply (simp add: awp_iff GG_def wens_set_FF, constrains)
1.110 +apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
1.111 +done
1.112 +
1.113 +end
```