src/HOL/UNITY/Comp/TimerArray.thy
author paulson
Tue Jan 03 15:43:54 2006 +0100 (2006-01-03)
changeset 18556 dc39832e9280
parent 16417 9bc16273c2d4
child 35416 d8d7d1b785af
permissions -rw-r--r--
added explicit paths to required theories
     1 (*  Title:      HOL/UNITY/TimerArray.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 A trivial example of reasoning about an array of processes
     7 *)
     8 
     9 theory TimerArray imports "../UNITY_Main" begin
    10 
    11 types 'a state = "nat * 'a"   (*second component allows new variables*)
    12 
    13 constdefs
    14   count  :: "'a state => nat"
    15     "count s == fst s"
    16   
    17   decr  :: "('a state * 'a state) set"
    18     "decr == UN n uu. {((Suc n, uu), (n,uu))}"
    19   
    20   Timer :: "'a state program"
    21     "Timer == mk_total_program (UNIV, {decr}, UNIV)"
    22 
    23 
    24 declare Timer_def [THEN def_prg_Init, simp]
    25 
    26 declare count_def [simp] decr_def [simp]
    27 
    28 (*Demonstrates induction, but not used in the following proof*)
    29 lemma Timer_leadsTo_zero: "Timer : UNIV leadsTo {s. count s = 0}"
    30 apply (rule_tac f = count in lessThan_induct, simp)
    31 apply (case_tac "m")
    32  apply (force intro!: subset_imp_leadsTo)
    33 apply (unfold Timer_def, ensures_tac "decr")
    34 done
    35 
    36 lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
    37 apply (rule preservesI)
    38 apply (unfold Timer_def, safety)
    39 done
    40 
    41 
    42 declare PLam_stable [simp]
    43 
    44 lemma TimerArray_leadsTo_zero:
    45      "finite I  
    46       ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
    47 apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" 
    48        in finite_stable_completion [THEN leadsTo_weaken])
    49 apply auto
    50 (*Safety property, already reduced to the single Timer case*)
    51  prefer 2
    52  apply (simp add: Timer_def, safety) 
    53 (*Progress property for the array of Timers*)
    54 apply (rule_tac f = "sub i o fst" in lessThan_induct)
    55 apply (case_tac "m")
    56 (*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
    57 apply (auto intro: subset_imp_leadsTo 
    58         simp add: insert_absorb 
    59                   lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] 
    60                Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
    61 apply (rename_tac "n")
    62 apply (rule PLam_leadsTo_Basis)
    63 apply (auto simp add: lessThan_Suc [symmetric])
    64 apply (unfold Timer_def mk_total_program_def, safety) 
    65 apply (rule_tac act = decr in totalize_transientI, auto)
    66 done
    67 
    68 end