new example HOL/UNITY/TimerArray
authorpaulson
Wed Sep 08 15:37:31 1999 +0200 (1999-09-08)
changeset 7513879ae27f5e6f
parent 7512 930e5947562d
child 7514 3235863a069a
new example HOL/UNITY/TimerArray
src/HOL/IsaMakefile
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/TimerArray.ML
src/HOL/UNITY/TimerArray.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 07 18:10:33 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 08 15:37:31 1999 +0200
     1.3 @@ -189,6 +189,7 @@
     1.4    UNITY/Guar.ML UNITY/Guar.thy\
     1.5    UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
     1.6    UNITY/Union.ML UNITY/Union.thy UNITY/Handshake.ML UNITY/Handshake.thy\
     1.7 +  UNITY/TimerArray.ML UNITY/TimerArray.thy\
     1.8    UNITY/Extend.ML UNITY/Extend.thy\
     1.9    UNITY/Follows.ML UNITY/Follows.thy\
    1.10    UNITY/GenPrefix.thy UNITY/GenPrefix.ML \
     2.1 --- a/src/HOL/UNITY/ROOT.ML	Tue Sep 07 18:10:33 1999 +0200
     2.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Sep 08 15:37:31 1999 +0200
     2.3 @@ -27,6 +27,7 @@
     2.4  time_use_thy "Client";
     2.5  time_use_thy "Extend";
     2.6  time_use_thy "PPROD";
     2.7 +time_use_thy "TimerArray";
     2.8  time_use_thy "Follows";
     2.9  
    2.10  add_path "../Auth";	(*to find Public.thy*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/TimerArray.ML	Wed Sep 08 15:37:31 1999 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      HOL/UNITY/TimerArray.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1998  University of Cambridge
     3.8 +
     3.9 +A trivial example of reasoning about an array of processes
    3.10 +*)
    3.11 +
    3.12 +Addsimps [Timer_def RS def_prg_Init];
    3.13 +program_defs_ref := [Timer_def];
    3.14 +
    3.15 +Goal "Timer : stable {0}";
    3.16 +by (constrains_tac 1);
    3.17 +qed "Timer_stable_zero";
    3.18 +Addsimps [Timer_stable_zero];
    3.19 +
    3.20 +(*Demonstrates induction, but not used in the following proof*)
    3.21 +Goal "Timer : UNIV leadsTo {0}";
    3.22 +by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
    3.23 +by (Simp_tac 1);
    3.24 +by (exhaust_tac "m" 1);
    3.25 +by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
    3.26 +by (ensures_tac "range (%n. (Suc n, n))" 1);
    3.27 +by (Blast_tac 1);
    3.28 +qed "Timer_leadsTo_zero";
    3.29 +
    3.30 +Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
    3.31 +by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
    3.32 +    (finite_stable_completion RS leadsTo_weaken) 1);
    3.33 +by Auto_tac;
    3.34 +by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
    3.35 +by (exhaust_tac "m" 1);
    3.36 +by (auto_tac (claset() addIs [subset_imp_leadsTo], 
    3.37 +	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
    3.38 +by (rename_tac "n" 1);
    3.39 +br PLam_leadsTo_Basis 1;
    3.40 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
    3.41 +by (constrains_tac 1);
    3.42 +by (res_inst_tac [("act", "range (%n. (Suc n, n))")] transient_mem 1);
    3.43 +by (auto_tac (claset(), simpset() addsimps [Timer_def]));
    3.44 +qed "TimerArray_leadsTo_zero";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/TimerArray.thy	Wed Sep 08 15:37:31 1999 +0200
     4.3 @@ -0,0 +1,15 @@
     4.4 +(*  Title:      HOL/UNITY/TimerArray.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1998  University of Cambridge
     4.8 +
     4.9 +A trivial example of reasoning about an array of processes
    4.10 +*)
    4.11 +
    4.12 +TimerArray = PPROD +
    4.13 +
    4.14 +constdefs
    4.15 +  Timer :: nat program
    4.16 +    "Timer == mk_program (UNIV, {range(%n. (Suc n, n))})"
    4.17 +
    4.18 +end