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.88 + apply (simp_all add: leadsTo_refl)
    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.100 +apply (rule leadsTo_UN [OF atLeast_leadsTo]) 
   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