# Theory TimerArray

theory TimerArray
imports UNITY_Main
```(*  Title:      HOL/UNITY/Comp/TimerArray.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

A trivial example of reasoning about an array of processes
*)

theory TimerArray imports "../UNITY_Main" begin

type_synonym 'a state = "nat * 'a"   (*second component allows new variables*)

definition count :: "'a state => nat"
where "count s = fst s"

definition decr  :: "('a state * 'a state) set"
where "decr = (UN n uu. {((Suc n, uu), (n,uu))})"

definition Timer :: "'a state program"
where "Timer = mk_total_program (UNIV, {decr}, UNIV)"

declare Timer_def [THEN def_prg_Init, simp]

declare count_def [simp] decr_def [simp]

(*Demonstrates induction, but not used in the following proof*)
apply (rule_tac f = count in lessThan_induct, simp)
apply (case_tac "m")
apply (unfold Timer_def, ensures_tac "decr")
done

lemma Timer_preserves_snd [iff]: "Timer ∈ preserves snd"
apply (rule preservesI)
apply (unfold Timer_def, safety)
done

declare PLam_stable [simp]

"finite I
⟹ (plam i: I. Timer) ∈ UNIV leadsTo {(s,uu). ∀i∈I. s i = 0}"
apply (erule_tac A'1 = "λi. lift_set i ({0} × UNIV)"
apply auto
(*Safety property, already reduced to the single Timer case*)
prefer 2
(*Progress property for the array of Timers*)
apply (rule_tac f = "sub i o fst" in lessThan_induct)
apply (case_tac "m")
(*Annoying need to massage the conditions to have the form (... × UNIV)*)