src/HOL/UNITY/Comp/Counter.ML
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@11194
     1
(*  Title:      HOL/UNITY/Counter
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 close to the original. 
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@13812
    14
Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
paulson@11194
    15
paulson@11194
    16
(* Theorems about sum and sumj *)
paulson@13812
    17
Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s";
paulson@11194
    18
by (induct_tac "I" 1);
paulson@11194
    19
by Auto_tac;
paulson@11194
    20
qed_spec_mp "sum_upd_gt";
paulson@11194
    21
paulson@11194
    22
paulson@11194
    23
Goal "sum I (s(c I := x)) = sum I s";
paulson@11194
    24
by (induct_tac "I" 1);
paulson@11194
    25
by Auto_tac;
paulson@11194
    26
by (simp_tac (simpset() 
paulson@11194
    27
    addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
paulson@11194
    28
qed "sum_upd_eq";
paulson@11194
    29
paulson@11194
    30
Goal "sum I (s(C := x)) = sum I s";
paulson@11194
    31
by (induct_tac "I" 1);
paulson@11194
    32
by Auto_tac;
paulson@11194
    33
qed "sum_upd_C";
paulson@11194
    34
paulson@11194
    35
Goal "sumj I i (s(c i := x)) = sumj I i s";
paulson@11194
    36
by (induct_tac "I" 1);
paulson@11194
    37
by Auto_tac;
paulson@11194
    38
by (simp_tac (simpset() addsimps 
paulson@11194
    39
    [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
paulson@11194
    40
qed "sumj_upd_ci";
paulson@11194
    41
paulson@11194
    42
Goal "sumj I i (s(C := x)) = sumj I i s";
paulson@11194
    43
by (induct_tac "I" 1);
paulson@11194
    44
by Auto_tac;
paulson@11194
    45
by (simp_tac (simpset() 
paulson@11194
    46
    addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
paulson@11194
    47
qed "sumj_upd_C";
paulson@11194
    48
paulson@13812
    49
Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)";
paulson@11194
    50
by (induct_tac "I" 1);
paulson@11194
    51
by Auto_tac;
paulson@11194
    52
qed_spec_mp  "sumj_sum_gt";
paulson@11194
    53
paulson@11194
    54
Goal "(sumj I I s = sum I s)";
paulson@11194
    55
by (induct_tac "I" 1);
paulson@11194
    56
by Auto_tac;
paulson@11194
    57
by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
paulson@11194
    58
qed "sumj_sum_eq";
paulson@11194
    59
paulson@13812
    60
Goal "\\<forall>i. i<I-->(sum I s = s (c i) +  sumj I i s)";
paulson@11194
    61
by (induct_tac "I" 1);
paulson@11194
    62
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));  
paulson@11194
    63
qed_spec_mp "sum_sumj";
paulson@11194
    64
paulson@11194
    65
(* Correctness proofs for Components *)
paulson@11194
    66
(* p2 and p3 proofs *)
paulson@13812
    67
Goal "Component i \\<in> stable {s. s C = s (c i) + k}";
paulson@13797
    68
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
paulson@11194
    69
by (constrains_tac 1);
paulson@11194
    70
qed "p2";
paulson@11194
    71
paulson@13812
    72
Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}";
paulson@13797
    73
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
paulson@11194
    74
by (constrains_tac 1);
paulson@11194
    75
qed "p3";
paulson@11194
    76
paulson@11194
    77
paulson@11194
    78
Goal 
paulson@13812
    79
"(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \
paulson@13812
    80
\                  \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \
paulson@13812
    81
\  = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})";
paulson@13812
    82
by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1);
paulson@11194
    83
by (auto_tac (claset(), simpset() 
paulson@13812
    84
     addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci]));
paulson@11194
    85
qed "p2_p3_lemma1";
paulson@11194
    86
paulson@11194
    87
Goal 
paulson@13812
    88
"\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \
paulson@13812
    89
\                             {s. \\<forall>v. v~=c i & v~=C --> s v = k v})";
paulson@11194
    90
by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
paulson@11194
    91
qed "p2_p3_lemma2";
paulson@11194
    92
paulson@11194
    93
paulson@11194
    94
Goal 
paulson@13812
    95
"Component i \\<in> stable {s.  s C = s (c i) + sumj I i s}";
paulson@11194
    96
by (auto_tac (claset() addSIs [p2_p3_lemma2],
paulson@11194
    97
              simpset() addsimps [p2_p3_lemma1 RS sym]));
paulson@11194
    98
qed "p2_p3";
paulson@11194
    99
paulson@11194
   100
(* Compositional Proof *)
paulson@11194
   101
paulson@13812
   102
Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0";
paulson@11194
   103
by (induct_tac "I" 1);
paulson@11194
   104
by Auto_tac;
paulson@11194
   105
qed "sum_0'";
paulson@11194
   106
val sum0_lemma =  (sum_0' RS mp) RS sym;
paulson@11194
   107
paulson@11194
   108
(* I could'nt be empty *)
paulson@11194
   109
Goalw [invariant_def] 
paulson@13812
   110
"!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}";
paulson@13812
   111
by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1);
paulson@11194
   112
by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
paulson@11194
   113
qed "safety";