src/HOL/UNITY/Comp/Counter.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/UNITY/Comp/Counter.thy
     2     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3     Copyright   2001  University of Cambridge
     4 
     5 From Charpentier and Chandy,
     6 Examples of Program Composition Illustrating the Use of Universal Properties
     7    In J. Rolim (editor), Parallel and Distributed Processing,
     8    Springer LNCS 1586 (1999), pages 1215-1227.
     9 *)
    10 
    11 header{*A Family of Similar Counters: Original Version*}
    12 
    13 theory Counter imports "../UNITY_Main" begin
    14 
    15 (* Variables are names *)
    16 datatype name = C | c nat
    17 type_synonym state = "name=>int"
    18 
    19 primrec sum  :: "[nat,state]=>int" where
    20   (* sum I s = sigma_{i<I}. s (c i) *)
    21   "sum 0 s = 0"
    22 | "sum (Suc i) s = s (c i) + sum i s"
    23 
    24 primrec sumj :: "[nat, nat, state]=>int" where
    25   "sumj 0 i s = 0"
    26 | "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
    27   
    28 type_synonym command = "(state*state)set"
    29 
    30 definition a :: "nat=>command" where
    31  "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
    32 
    33 definition Component :: "nat => state program" where
    34   "Component i =
    35     mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
    36                      \<Union>G \<in> preserves (%s. s (c i)). Acts G)"
    37 
    38 
    39 
    40 declare Component_def [THEN def_prg_Init, simp]
    41 declare a_def [THEN def_act_simp, simp]
    42 
    43 (* Theorems about sum and sumj *)
    44 lemma sum_upd_gt: "I<n ==> sum I (s(c n := x)) = sum I s"
    45   by (induct I) auto
    46 
    47 
    48 lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
    49   by (induct I) (auto simp add: sum_upd_gt [unfolded fun_upd_def])
    50 
    51 lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
    52   by (induct I) auto
    53 
    54 lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
    55   by (induct I) (auto simp add: sum_upd_eq [unfolded fun_upd_def])
    56 
    57 lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
    58   by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])
    59 
    60 lemma sumj_sum_gt: "I<i ==> sumj I i s = sum I s"
    61   by (induct I) auto
    62 
    63 lemma sumj_sum_eq: "(sumj I I s = sum I s)"
    64   by (induct I) (auto simp add: sumj_sum_gt)
    65 
    66 lemma sum_sumj: "i<I ==> sum I s = s (c i) +  sumj I i s"
    67   by (induct I) (auto simp add: linorder_neq_iff sumj_sum_eq)
    68 
    69 (* Correctness proofs for Components *)
    70 (* p2 and p3 proofs *)
    71 lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}"
    72 by (simp add: Component_def, safety)
    73 
    74 lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"
    75 by (simp add: Component_def, safety)
    76 
    77 
    78 lemma p2_p3_lemma1: 
    79 "(\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k}  
    80                    \<inter> {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}))  
    81    = (Component i \<in> stable {s. s C = s (c i) + sumj I i s})"
    82 apply (simp add: Component_def mk_total_program_def)
    83 apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci)
    84 done
    85 
    86 lemma p2_p3_lemma2: 
    87 "\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} Int  
    88                             {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v})"
    89 by (blast intro: stable_Int [OF p2 p3])
    90 
    91 lemma p2_p3: "Component i \<in> stable {s.  s C = s (c i) + sumj I i s}"
    92 by (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric])
    93 
    94 (* Compositional Proof *)
    95 
    96 lemma sum_0': "(\<And>i. i < I ==> s (c i) = 0) ==> sum I s = 0"
    97   by (induct I) auto
    98 
    99 (* I cannot be empty *)
   100 lemma safety:
   101      "0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}"
   102 apply (simp (no_asm) add: invariant_def JN_stable sum_sumj)
   103 apply (force intro: p2_p3 sum_0')
   104 done
   105 
   106 end