new example HOL/UNITY/TimerArray

--- a/src/HOL/IsaMakefile	Tue Sep 07 18:10:33 1999 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 08 15:37:31 1999 +0200
@@ -189,6 +189,7 @@
   UNITY/Guar.ML UNITY/Guar.thy\
   UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
   UNITY/Union.ML UNITY/Union.thy UNITY/Handshake.ML UNITY/Handshake.thy\
+  UNITY/TimerArray.ML UNITY/TimerArray.thy\
   UNITY/Extend.ML UNITY/Extend.thy\
   UNITY/Follows.ML UNITY/Follows.thy\
   UNITY/GenPrefix.thy UNITY/GenPrefix.ML \

--- a/src/HOL/UNITY/ROOT.ML	Tue Sep 07 18:10:33 1999 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Wed Sep 08 15:37:31 1999 +0200
@@ -27,6 +27,7 @@
 time_use_thy "Client";
 time_use_thy "Extend";
 time_use_thy "PPROD";
+time_use_thy "TimerArray";
 time_use_thy "Follows";
 
 add_path "../Auth";	(*to find Public.thy*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/TimerArray.ML	Wed Sep 08 15:37:31 1999 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/UNITY/TimerArray.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+A trivial example of reasoning about an array of processes
+*)
+
+Addsimps [Timer_def RS def_prg_Init];
+program_defs_ref := [Timer_def];
+
+Goal "Timer : stable {0}";
+by (constrains_tac 1);
+qed "Timer_stable_zero";
+Addsimps [Timer_stable_zero];
+
+(*Demonstrates induction, but not used in the following proof*)
+Goal "Timer : UNIV leadsTo {0}";
+by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
+by (Simp_tac 1);
+by (exhaust_tac "m" 1);
+by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
+by (ensures_tac "range (%n. (Suc n, n))" 1);
+by (Blast_tac 1);
+qed "Timer_leadsTo_zero";
+
+Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
+by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
+    (finite_stable_completion RS leadsTo_weaken) 1);
+by Auto_tac;
+by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
+by (exhaust_tac "m" 1);
+by (auto_tac (claset() addIs [subset_imp_leadsTo], 
+	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
+by (rename_tac "n" 1);
+br PLam_leadsTo_Basis 1;
+by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
+by (constrains_tac 1);
+by (res_inst_tac [("act", "range (%n. (Suc n, n))")] transient_mem 1);
+by (auto_tac (claset(), simpset() addsimps [Timer_def]));
+qed "TimerArray_leadsTo_zero";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/TimerArray.thy	Wed Sep 08 15:37:31 1999 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/UNITY/TimerArray.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+A trivial example of reasoning about an array of processes
+*)
+
+TimerArray = PPROD +
+
+constdefs
+  Timer :: nat program
+    "Timer == mk_program (UNIV, {range(%n. (Suc n, n))})"
+
+end