src/HOL/UNITY/Comp/Progress.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 18556 dc39832e9280
child 28866 30cd9d89a0fb
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      HOL/UNITY/Transformers
     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 
    11 theory Progress imports "../UNITY_Main" begin
    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 
    91 text{*Result (4.39): Applying the leadsTo-Join Theorem*}
    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
    95 apply (rule_tac T = "atLeast 0" in leadsTo_Join)
    96   apply (simp add: awp_iff FF_def, safety)
    97  apply (simp add: awp_iff GG_def wens_set_FF, safety)
    98 apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
    99 done
   100 
   101 end