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