1(*  Title:      HOL/UNITY/Comp/TimerArray.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5A trivial example of reasoning about an array of processes
6*)
7
8theory TimerArray imports "../UNITY_Main" begin
9
10type_synonym 'a state = "nat * 'a"   (*second component allows new variables*)
11
12definition count :: "'a state => nat"
13  where "count s = fst s"
14  
15definition decr  :: "('a state * 'a state) set"
16  where "decr = (UN n uu. {((Suc n, uu), (n,uu))})"
17  
18definition Timer :: "'a state program"
19  where "Timer = mk_total_program (UNIV, {decr}, UNIV)"
20
21
22declare Timer_def [THEN def_prg_Init, simp]
23
24declare count_def [simp] decr_def [simp]
25
26(*Demonstrates induction, but not used in the following proof*)
27lemma Timer_leadsTo_zero: "Timer \<in> UNIV leadsTo {s. count s = 0}"
28apply (rule_tac f = count in lessThan_induct, simp)
29apply (case_tac "m")
30 apply (force intro!: subset_imp_leadsTo)
31apply (unfold Timer_def, ensures_tac "decr")
32done
33
34lemma Timer_preserves_snd [iff]: "Timer \<in> preserves snd"
35apply (rule preservesI)
36apply (unfold Timer_def, safety)
37done
38
39
40declare PLam_stable [simp]
41
42lemma TimerArray_leadsTo_zero:
43     "finite I  
44      \<Longrightarrow> (plam i: I. Timer) \<in> UNIV leadsTo {(s,uu). \<forall>i\<in>I. s i = 0}"
45apply (erule_tac A'1 = "\<lambda>i. lift_set i ({0} \<times> UNIV)" 
46       in finite_stable_completion [THEN leadsTo_weaken])
47apply 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*)
52apply (rule_tac f = "sub i o fst" in lessThan_induct)
53apply (case_tac "m")
54(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
55apply (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])
59apply (rename_tac "n")
60apply (rule PLam_leadsTo_Basis)
61apply (auto simp add: lessThan_Suc [symmetric])
62apply (unfold Timer_def mk_total_program_def, safety) 
63apply (rule_tac act = decr in totalize_transientI, auto)
64done
65
66end
67