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