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