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