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