src/HOL/UNITY/Comp/Counterc.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 20625 1bb9a04f8c22
child 32960 69916a850301
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      HOL/UNITY/Counterc
     2     ID:         $Id$
     3     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4     Copyright   2001  University of Cambridge
     5 
     6 A family of similar counters, version with a full use of "compatibility "
     7 
     8 From Charpentier and Chandy,
     9 Examples of Program Composition Illustrating the Use of Universal Properties
    10    In J. Rolim (editor), Parallel and Distributed Processing,
    11    Spriner LNCS 1586 (1999), pages 1215-1227.
    12 *)
    13 
    14 header{*A Family of Similar Counters: Version with Compatibility*}
    15 
    16 theory Counterc imports "../UNITY_Main" begin
    17 
    18 typedecl state
    19 
    20 consts
    21   C :: "state=>int"
    22   c :: "state=>nat=>int"
    23 
    24 consts  
    25   sum  :: "[nat,state]=>int"
    26   sumj :: "[nat, nat, state]=>int"
    27 
    28 primrec (* sum I s = sigma_{i<I}. c s i *)
    29   "sum 0 s = 0"
    30   "sum (Suc i) s = (c s) i + sum i s"
    31 
    32 primrec
    33   "sumj 0 i s = 0"
    34   "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
    35   
    36 types command = "(state*state)set"
    37 
    38 constdefs
    39   a :: "nat=>command"
    40  "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
    41  
    42   Component :: "nat => state program"
    43   "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
    44 				   {a i},
    45  	                           \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
    46 
    47 
    48 declare Component_def [THEN def_prg_Init, simp]
    49 declare Component_def [THEN def_prg_AllowedActs, simp]
    50 declare a_def [THEN def_act_simp, simp]
    51 
    52 (* Theorems about sum and sumj *)
    53 lemma sum_sumj_eq1 [rule_format]: "\<forall>i. I<i--> (sum I s = sumj I i s)"
    54 by (induct_tac "I", auto)
    55 
    56 lemma sum_sumj_eq2 [rule_format]: "i<I --> sum I s  = c s i + sumj I i s"
    57 apply (induct_tac "I")
    58 apply (auto simp add: linorder_neq_iff sum_sumj_eq1)
    59 done
    60 
    61 lemma sum_ext [rule_format]:
    62      "(\<forall>i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)"
    63 by (induct_tac "I", auto)
    64 
    65 lemma sumj_ext [rule_format]:
    66      "(\<forall>j. j<I & j\<noteq>i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)"
    67 apply (induct_tac "I", safe)
    68 apply (auto intro!: sum_ext)
    69 done
    70 
    71 
    72 lemma sum0 [rule_format]: "(\<forall>i. i<I --> c s i = 0) -->  sum I s = 0"
    73 by (induct_tac "I", auto)
    74 
    75 
    76 (* Safety properties for Components *)
    77 
    78 lemma Component_ok_iff:
    79      "(Component i ok G) =  
    80       (G \<in> preserves (%s. c s i) & Component i \<in> Allowed G)"
    81 apply (auto simp add: ok_iff_Allowed Component_def [THEN def_total_prg_Allowed])
    82 done
    83 declare Component_ok_iff [iff]
    84 declare OK_iff_ok [iff]
    85 declare preserves_def [simp]
    86 
    87 
    88 lemma p2: "Component i \<in> stable {s. C s = (c s) i + k}"
    89 by (simp add: Component_def, safety)
    90 
    91 lemma p3:
    92      "[| OK I Component; i\<in>I |]   
    93       ==> Component i \<in> stable {s. \<forall>j\<in>I. j\<noteq>i --> c s j = c k j}"
    94 apply simp
    95 apply (unfold Component_def mk_total_program_def)
    96 apply (simp (no_asm_use) add: stable_def constrains_def)
    97 apply blast
    98 done
    99 
   100 
   101 lemma p2_p3_lemma1: 
   102      "[| OK {i. i<I} Component; i<I |] ==>  
   103       \<forall>k. Component i \<in> stable ({s. C s = c s i + sumj I i k} Int  
   104 	 	                {s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j})"
   105 by (blast intro: stable_Int [OF p2 p3])
   106 
   107 lemma p2_p3_lemma2:
   108      "(\<forall>k. F \<in> stable ({s. C s = (c s) i + sumj I i k} Int  
   109                         {s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j}))   
   110       ==> (F \<in> stable {s. C s = c s i + sumj I i s})"
   111 apply (simp add: constrains_def stable_def)
   112 apply (force intro!: sumj_ext)
   113 done
   114 
   115 
   116 lemma p2_p3:
   117      "[| OK {i. i<I} Component; i<I |]  
   118       ==> Component i \<in> stable {s. C s = c s i + sumj I i s}"
   119 by (blast intro: p2_p3_lemma1 [THEN p2_p3_lemma2])
   120 
   121 
   122 (* Compositional correctness *)
   123 lemma safety: 
   124      "[| 0<I; OK {i. i<I} Component |]   
   125       ==> (\<Squnion>i\<in>{i. i<I}. (Component i)) \<in> invariant {s. C s = sum I s}"
   126 apply (simp (no_asm) add: invariant_def JN_stable sum_sumj_eq2)
   127 apply (auto intro!: sum0 p2_p3)
   128 done
   129 
   130 end