src/HOL/UNITY/Comp/TimerArray.thy
author paulson
Mon Mar 05 15:32:54 2001 +0100 (2001-03-05)
changeset 11194 ea13ff5a26d1
child 13786 ab8f39f48a6f
permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
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@11194
     9
TimerArray = PPROD +
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@11194
    20
  Timer :: 'a state program
paulson@11194
    21
    "Timer == mk_program (UNIV, {decr}, UNIV)"
paulson@11194
    22
paulson@11194
    23
end