src/HOL/UNITY/Common.ML
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5648 fe887910e32e
child 6012 1894bfc4aee9
permissions -rw-r--r--
Drule.rev_triv_goal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Common
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Common Meeting Time example from Misra (1994)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
The state is identified with the one variable in existence.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
(*Misra's property CMT4: t exceeds no common meeting time*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    14
Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    15
\     ==> F : Stable (atMost n)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    16
by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
by (asm_full_simp_tac
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    18
    (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    19
			 le_max_iff_disj]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    20
by (etac Constrains_weaken_R 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    21
by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
qed "common_stable";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5608
diff changeset
    24
Goal "[| Init F <= atMost n;  \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    25
\        ALL m. F : Constrains {m} (maxfg m); n: common |] \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    26
\     ==> F : Invariant (atMost n)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    27
by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    28
qed "common_Invariant";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    29
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    30
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
(*** Some programs that implement the safety property above ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    33
Goal "SKIP : constrains {m} (maxfg m)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    35
				  fasc]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    36
result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    37
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    38
(*This one is  t := ftime t || t := gtime t*)
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    39
Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    40
\      : constrains {m} (maxfg m)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    41
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    42
				  le_max_iff_disj, fasc]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    46
(*This one is  t := max (ftime t) (gtime t)*)
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    47
Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    48
\      : constrains {m} (maxfg m)";
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    49
by (simp_tac 
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    50
    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    53
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    54
(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    55
Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    56
\      : constrains {m} (maxfg m)";
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    57
by (simp_tac 
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    58
    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
by (blast_tac (claset() addIs [Suc_leI]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    60
result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    61
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    62
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    63
(*It remans to prove that they satisfy CMT3': t does not decrease,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    64
  and that CMT3' implies that t stops changing once common(t) holds.*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    65
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    66
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    67
(*** Progress under weak fairness ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    68
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    69
Addsimps [atMost_Int_atLeast];
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    70
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    71
Goal "[| ALL m. F : Constrains {m} (maxfg m); \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    72
\               ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5490
diff changeset
    73
\               n: common |]  \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    74
\     ==> F : LeadsTo (atMost n) common";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    75
by (rtac LeadsTo_weaken_R 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    76
by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    77
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    78
by (rtac subset_refl 2);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    79
by (blast_tac (claset() addDs [PSP_stable2] 
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    80
                        addIs [common_stable, LeadsTo_weaken_R]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    81
val lemma = result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    82
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5313
diff changeset
    83
(*The "ALL m: -common" form echoes CMT6.*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    84
Goal "[| ALL m. F : Constrains {m} (maxfg m); \
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    85
\               ALL m: -common. F : LeadsTo {m} (greaterThan m); \
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5490
diff changeset
    86
\               n: common |]  \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    87
\            ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    88
by (rtac lemma 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    89
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    90
by (etac LeastI 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    91
by (blast_tac (claset() addSDs [not_less_Least]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    92
qed "leadsTo_common";