src/HOL/UNITY/Comp/Progress.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01 ago)
changeset 35416 d8d7d1b785af
parent 28869 191cbfac6c9a
child 37936 1e4c5015a72e
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     1 (*  Title:      HOL/UNITY/Progress
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2003  University of Cambridge
     4 
     5 David Meier's thesis
     6 *)
     7 
     8 header{*Progress Set Examples*}
     9 
    10 theory Progress imports "../UNITY_Main" begin
    11 
    12 subsection {*The Composition of Two Single-Assignment Programs*}
    13 text{*Thesis Section 4.4.2*}
    14 
    15 definition FF :: "int program" where
    16     "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
    17 
    18 definition GG :: "int program" where
    19     "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
    20 
    21 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
    22 
    23 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
    24 by force
    25 
    26 lemma FF_eq:
    27       "FF = mk_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
    28 by (simp add: FF_def mk_total_program_def totalize_def totalize_act_def
    29               program_equalityI Domain_actFF)
    30 
    31 lemma wp_actFF:
    32      "wp (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = atLeast (k - 1)"
    33 by (force simp add: wp_def)
    34 
    35 lemma wens_FF: "wens FF (range (\<lambda>x. (x, x+1))) (atLeast k) = atLeast (k - 1)"
    36 by (force simp add: FF_eq wens_single_eq wp_actFF)
    37 
    38 lemma single_valued_actFF: "single_valued (range (\<lambda>x::int. (x, x + 1)))"
    39 by (force simp add: single_valued_def)
    40 
    41 lemma wens_single_finite_FF:
    42      "wens_single_finite (range (\<lambda>x. (x, x+1))) (atLeast k) n =
    43       atLeast (k - int n)"
    44 apply (induct n, simp)
    45 apply (force simp add: wens_FF
    46             def_wens_single_finite_Suc_eq_wens [OF FF_eq single_valued_actFF])
    47 done
    48 
    49 lemma wens_single_FF_eq_UNIV:
    50      "wens_single (range (\<lambda>x::int. (x, x + 1))) (atLeast k) = UNIV"
    51 apply (auto simp add: wens_single_eq_Union)
    52 apply (rule_tac x="nat (k-x)" in exI)
    53 apply (simp add: wens_single_finite_FF)
    54 done
    55 
    56 lemma wens_set_FF:
    57      "wens_set FF (atLeast k) = insert UNIV (atLeast ` atMost k)"
    58 apply (auto simp add: wens_set_single_eq [OF FF_eq single_valued_actFF]
    59                       wens_single_FF_eq_UNIV wens_single_finite_FF)
    60 apply (erule notE)
    61 apply (rule_tac x="nat (k-xa)" in range_eqI)
    62 apply (simp add: wens_single_finite_FF)
    63 done
    64 
    65 subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
    66 
    67 lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
    68 apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
    69 apply (simp add: wens_ensures FF_eq)
    70 done
    71 
    72 lemma atLeast_leadsTo: "FF \<in> atLeast (k - int n) leadsTo atLeast (k::int)"
    73 apply (induct n)
    74  apply (simp_all add: leadsTo_refl)
    75 apply (rule_tac A = "atLeast (k - int n - 1)" in leadsTo_weaken_L)
    76  apply (blast intro: leadsTo_Trans atLeast_ensures, force) 
    77 done
    78 
    79 lemma UN_atLeast_UNIV: "(\<Union>n. atLeast (k - int n)) = UNIV"
    80 apply auto 
    81 apply (rule_tac x = "nat (k - x)" in exI, simp) 
    82 done
    83 
    84 lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)"
    85 apply (subst UN_atLeast_UNIV [symmetric]) 
    86 apply (rule leadsTo_UN [OF atLeast_leadsTo]) 
    87 done
    88 
    89 text{*Result (4.39): Applying the leadsTo-Join Theorem*}
    90 theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
    91 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
    92  apply simp
    93 apply (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)
    96 apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
    97 done
    98 
    99 end