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