src/HOL/TLA/Inc/Inc.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/ex/inc/Inc.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
Proofs for the "increment" example from SRC79.
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@3807
     9
val PsiInv_defs = [PsiInv_def,PsiInv1_def,PsiInv2_def,PsiInv3_def];
wenzelm@3807
    10
val Psi_defs = [Psi_def,InitPsi_def,N1_def,N2_def,alpha1_def,alpha2_def,
wenzelm@3807
    11
                beta1_def,beta2_def,gamma1_def,gamma2_def];
wenzelm@3807
    12
wenzelm@4089
    13
val Inc_css = (claset(), simpset());
wenzelm@3807
    14
wenzelm@3807
    15
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
wenzelm@3807
    16
wenzelm@3807
    17
qed_goal "PsiInv_Init" Inc.thy "InitPsi .-> PsiInv"
wenzelm@3807
    18
 (fn _ => [ auto_tac (Inc_css addsimps2 InitPsi_def::PsiInv_defs) ]);
wenzelm@3807
    19
wenzelm@3807
    20
qed_goal "PsiInv_alpha1" Inc.thy "alpha1 .& PsiInv .-> PsiInv`"
wenzelm@3807
    21
  (fn _ => [ auto_tac (Inc_css addsimps2 alpha1_def::PsiInv_defs) ]);
wenzelm@3807
    22
wenzelm@3807
    23
qed_goal "PsiInv_alpha2" Inc.thy "alpha2 .& PsiInv .-> PsiInv`"
wenzelm@3807
    24
  (fn _ => [ auto_tac (Inc_css addsimps2 alpha2_def::PsiInv_defs) ]);
wenzelm@3807
    25
wenzelm@3807
    26
qed_goal "PsiInv_beta1" Inc.thy "beta1 .& PsiInv .-> PsiInv`"
wenzelm@3807
    27
  (fn _ => [ auto_tac (Inc_css addsimps2 beta1_def::PsiInv_defs) ]);
wenzelm@3807
    28
wenzelm@3807
    29
qed_goal "PsiInv_beta2" Inc.thy "beta2 .& PsiInv .-> PsiInv`"
wenzelm@3807
    30
  (fn _ => [ auto_tac (Inc_css addsimps2 beta2_def::PsiInv_defs) ]);
wenzelm@3807
    31
wenzelm@3807
    32
qed_goal "PsiInv_gamma1" Inc.thy "gamma1 .& PsiInv .-> PsiInv`"
wenzelm@3807
    33
  (fn _ => [ auto_tac (Inc_css addsimps2 gamma1_def::PsiInv_defs) ]);
wenzelm@3807
    34
wenzelm@3807
    35
qed_goal "PsiInv_gamma2" Inc.thy "gamma2 .& PsiInv .-> PsiInv`"
wenzelm@3807
    36
  (fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]);
wenzelm@3807
    37
wenzelm@3807
    38
qed_goal "PsiInv_stutter" Inc.thy "unchanged <x,y,sem,pc1,pc2> .& PsiInv .-> PsiInv`"
wenzelm@3807
    39
  (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]);
wenzelm@3807
    40
wenzelm@3807
    41
qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv"
wenzelm@3807
    42
  (fn _ => [inv_tac (Inc_css addsimps2 [Psi_def]) 1,
wenzelm@3807
    43
	    SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init]
wenzelm@3807
    44
				           addsimps2 [Init_def])) 1,
wenzelm@3807
    45
	    auto_tac (Inc_css addSEs2 (map action_conjimpE
wenzelm@3807
    46
				           [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1,
wenzelm@3807
    47
					    PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2])
wenzelm@3807
    48
		              addIs2 [action_mp PsiInv_stutter]
wenzelm@3807
    49
                              addsimps2 [square_def,N1_def, N2_def])
wenzelm@3807
    50
	   ]);
wenzelm@3807
    51
wenzelm@3807
    52
wenzelm@3807
    53
wenzelm@3807
    54
(* Automatic proof works too, but it make take a while on a slow machine.
wenzelm@3807
    55
   More substantial examples require manual guidance anyway.
wenzelm@3807
    56
wenzelm@3807
    57
goal Inc.thy "Psi .-> []PsiInv";
wenzelm@4089
    58
by (auto_inv_tac (simpset() addsimps PsiInv_defs @ Psi_defs @ pcount.simps) 1);
wenzelm@3807
    59
wenzelm@3807
    60
*)
wenzelm@3807
    61
wenzelm@3807
    62
(**** Step simulation ****)
wenzelm@3807
    63
wenzelm@3807
    64
qed_goal "Init_sim" Inc.thy "Psi .-> Init(InitPhi)"
wenzelm@3807
    65
  (fn _ => [ auto_tac (Inc_css addsimps2 [InitPhi_def,Psi_def,InitPsi_def,Init_def]) ]);
wenzelm@3807
    66
wenzelm@3807
    67
qed_goal "Step_sim" Inc.thy "Psi .-> [][M1 .| M2]_<x,y>"
wenzelm@3807
    68
  (fn _ => [auto_tac (Inc_css addsimps2 [square_def,M1_def,M2_def] @ Psi_defs
wenzelm@3807
    69
                              addSEs2 [STL4E]) 
wenzelm@3807
    70
           ]);
wenzelm@3807
    71
wenzelm@3807
    72
(**** Proof of fairness ****)
wenzelm@3807
    73
wenzelm@3807
    74
(*
wenzelm@3807
    75
   The goal is to prove Fair_M1 far below, which asserts 
wenzelm@3807
    76
         Psi .-> WF(M1)_<x,y>   
wenzelm@3807
    77
   (the other fairness condition is symmetrical).
wenzelm@3807
    78
wenzelm@3807
    79
   The strategy is to use WF2 (with beta1 as the helpful action). Proving its
wenzelm@3807
    80
   temporal premise needs two auxiliary lemmas:
wenzelm@3807
    81
   1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1
wenzelm@3807
    82
   2. N1_live: the first component will eventually reach b
wenzelm@3807
    83
wenzelm@3807
    84
   Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness
wenzelm@3807
    85
   of the semaphore, and needs auxiliary lemmas that ensure that the second
wenzelm@3807
    86
   component will eventually release the semaphore. Most of the proofs of
wenzelm@3807
    87
   the auxiliary lemmas are very similar.
wenzelm@3807
    88
*)
wenzelm@3807
    89
wenzelm@3807
    90
qed_goal "Stuck_at_b" Inc.thy
wenzelm@3807
    91
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .-> stable($pc1 .= #b)"
wenzelm@3807
    92
  (fn _ => [rtac StableL 1,
wenzelm@3807
    93
	    auto_tac (Inc_css addsimps2 square_def::Psi_defs)
wenzelm@3807
    94
	   ]);
wenzelm@3807
    95
wenzelm@3807
    96
qed_goal "N1_enabled_at_g" Inc.thy
wenzelm@3807
    97
  "($pc1 .= #g) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))"
wenzelm@3807
    98
  (fn _ => [Action_simp_tac 1,
wenzelm@3807
    99
	    res_inst_tac [("F","gamma1")] enabled_mono 1,
wenzelm@3807
   100
	    enabled_tac Inc_base 1,
wenzelm@3807
   101
	    auto_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def])
wenzelm@3807
   102
	   ]);
wenzelm@3807
   103
wenzelm@3807
   104
qed_goal "g1_leadsto_a1" Inc.thy
wenzelm@3807
   105
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N1)_<x,y,sem,pc1,pc2> .& []#True \
wenzelm@3807
   106
\  .-> ($pc1 .= #g ~> $pc1 .= #a)"
wenzelm@3807
   107
  (fn _ => [rtac SF1 1,
wenzelm@3807
   108
	    (* the first two subgoals are simple action formulas and succumb to the
wenzelm@3807
   109
	       auto_tac; don't expand N1 in the third subgoal *)
wenzelm@3807
   110
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1,
wenzelm@3807
   111
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1,
wenzelm@3807
   112
	    (* reduce []A .-> <>Enabled B  to  A .-> Enabled B *)
wenzelm@3807
   113
	    auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N1_enabled_at_g]
wenzelm@3807
   114
		              addSDs2 [STL2bD]
wenzelm@3807
   115
		              addsimps2 [Init_def])
wenzelm@3807
   116
	   ]);
wenzelm@3807
   117
wenzelm@3807
   118
(* symmetrical for N2, and similar for beta2 *)
wenzelm@3807
   119
qed_goal "N2_enabled_at_g" Inc.thy
wenzelm@3807
   120
  "($pc2 .= #g) .-> $(Enabled (<N2>_<x,y,sem,pc1,pc2>))"
wenzelm@3807
   121
  (fn _ => [Action_simp_tac 1,
wenzelm@3807
   122
	    res_inst_tac [("F","gamma2")] enabled_mono 1,
wenzelm@3807
   123
	    enabled_tac Inc_base 1,
wenzelm@3807
   124
	    auto_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def])
wenzelm@3807
   125
	   ]);
wenzelm@3807
   126
wenzelm@3807
   127
qed_goal "g2_leadsto_a2" Inc.thy
wenzelm@3807
   128
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \
wenzelm@3807
   129
\  .-> ($pc2 .= #g ~> $pc2 .= #a)"
wenzelm@3807
   130
  (fn _ => [rtac SF1 1,
wenzelm@3807
   131
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1,
wenzelm@3807
   132
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1,
wenzelm@3807
   133
	    auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_g]
wenzelm@3807
   134
		              addSDs2 [STL2bD]
wenzelm@3807
   135
		              addsimps2 [Init_def])
wenzelm@3807
   136
	   ]);
wenzelm@3807
   137
wenzelm@3807
   138
qed_goal "N2_enabled_at_b" Inc.thy
wenzelm@3807
   139
  "($pc2 .= #b) .-> $(Enabled (<N2>_<x,y,sem,pc1,pc2>))"
wenzelm@3807
   140
  (fn _ => [Action_simp_tac 1,
wenzelm@3807
   141
	    res_inst_tac [("F","beta2")] enabled_mono 1,
wenzelm@3807
   142
	    enabled_tac Inc_base 1,
wenzelm@3807
   143
	    auto_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def])
wenzelm@3807
   144
	   ]);
wenzelm@3807
   145
wenzelm@3807
   146
qed_goal "b2_leadsto_g2" Inc.thy
wenzelm@3807
   147
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \
wenzelm@3807
   148
\  .-> ($pc2 .= #b ~> $pc2 .= #g)"
wenzelm@3807
   149
  (fn _ => [rtac SF1 1,
wenzelm@3807
   150
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1,
wenzelm@3807
   151
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1,
wenzelm@3807
   152
	    auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_b]
wenzelm@3807
   153
		              addSDs2 [STL2bD]
wenzelm@3807
   154
		              addsimps2 [Init_def])
wenzelm@3807
   155
	   ]);
wenzelm@3807
   156
wenzelm@3807
   157
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
wenzelm@3807
   158
qed_goal "N2_leadsto_a" Inc.thy
wenzelm@3807
   159
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \
wenzelm@3807
   160
\  .-> (($pc2 .= #a .| $pc2 .= #b .| $pc2 .= #g) ~> $pc2 .= #a)"
wenzelm@3807
   161
  (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]),
wenzelm@3807
   162
	    rtac (LatticeReflexivity RS tempD) 1,
wenzelm@3807
   163
	    rtac LatticeTransitivity 1,
wenzelm@3807
   164
	    auto_tac (Inc_css addSIs2 (map temp_mp [b2_leadsto_g2,g2_leadsto_a2]))
wenzelm@3807
   165
	   ]);
wenzelm@3807
   166
wenzelm@3807
   167
(* A variant that gets rid of the disjunction, thanks to induction over data types *)
wenzelm@3807
   168
qed_goal "N2_live" Inc.thy
wenzelm@3807
   169
  "[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> \
wenzelm@3807
   170
\  .-> <>($pc2 .= #a)"
wenzelm@3807
   171
  (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
wenzelm@3807
   172
	    rewrite_goals_tac (Init_def::action_rews),
wenzelm@3807
   173
	    pcount.induct_tac "pc2 (fst_st sigma)" 1,
paulson@4477
   174
	    Auto_tac
wenzelm@3807
   175
	   ]);
wenzelm@3807
   176
wenzelm@3807
   177
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
wenzelm@3807
   178
wenzelm@3807
   179
qed_goal "N1_enabled_at_both_a" Inc.thy
wenzelm@3807
   180
  "$pc2 .= #a .& (PsiInv .& $pc1 .= #a) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))"
wenzelm@3807
   181
  (fn _ => [Action_simp_tac 1,
wenzelm@3807
   182
	    res_inst_tac [("F","alpha1")] enabled_mono 1,
wenzelm@3807
   183
	    enabled_tac Inc_base 1,
wenzelm@3807
   184
	    auto_tac (Inc_css addIs2 [sym]
wenzelm@3807
   185
		              addsimps2 [angle_def,alpha1_def,N1_def] @ PsiInv_defs)
wenzelm@3807
   186
	   ]);
wenzelm@3807
   187
wenzelm@3807
   188
qed_goal "a1_leadsto_b1" Inc.thy
wenzelm@3807
   189
  "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>)              \
wenzelm@3807
   190
\            .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2>  \
wenzelm@3807
   191
\  .-> ($pc1 .= #a ~> $pc1 .= #b)"
wenzelm@3807
   192
  (fn _ => [rtac SF1 1,
wenzelm@3807
   193
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1,
wenzelm@3807
   194
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1,
wenzelm@3807
   195
	    auto_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_mp DmdImpl)]),
wenzelm@3807
   196
	    auto_tac (Inc_css addSIs2 [temp_mp BoxDmdT2, temp_mp N2_live]
wenzelm@3807
   197
		              addsimps2 split_box_conj::more_temp_simps)
wenzelm@3807
   198
	   ]);
wenzelm@3807
   199
wenzelm@3807
   200
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
wenzelm@3807
   201
wenzelm@3807
   202
qed_goal "N1_leadsto_b" Inc.thy
wenzelm@3807
   203
  "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>)              \
wenzelm@3807
   204
\            .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2>  \
wenzelm@3807
   205
\  .-> (($pc1 .= #b .| $pc1 .= #g .| $pc1 .= #a) ~> $pc1 .= #b)"
wenzelm@3807
   206
  (fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]),
wenzelm@3807
   207
	    rtac (LatticeReflexivity RS tempD) 1,
wenzelm@3807
   208
	    rtac LatticeTransitivity 1,
wenzelm@3807
   209
	    auto_tac (Inc_css addSIs2 (map temp_mp [a1_leadsto_b1,g1_leadsto_a1])
wenzelm@3807
   210
		              addsimps2 [split_box_conj])
wenzelm@3807
   211
	   ]);
wenzelm@3807
   212
wenzelm@3807
   213
qed_goal "N1_live" Inc.thy
wenzelm@3807
   214
  "[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>)              \
wenzelm@3807
   215
\            .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2>  \
wenzelm@3807
   216
\  .-> <>($pc1 .= #b)"
wenzelm@3807
   217
  (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
wenzelm@3807
   218
	    rewrite_goals_tac (Init_def::action_rews),
wenzelm@3807
   219
	    pcount.induct_tac "pc1 (fst_st sigma)" 1,
paulson@4477
   220
	    Auto_tac
wenzelm@3807
   221
	   ]);
wenzelm@3807
   222
wenzelm@3807
   223
qed_goal "N1_enabled_at_b" Inc.thy
wenzelm@3807
   224
  "($pc1 .= #b) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))"
wenzelm@3807
   225
  (fn _ => [Action_simp_tac 1,
wenzelm@3807
   226
	    res_inst_tac [("F","beta1")] enabled_mono 1,
wenzelm@3807
   227
	    enabled_tac Inc_base 1,
wenzelm@3807
   228
	    auto_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def])
wenzelm@3807
   229
	   ]);
wenzelm@3807
   230
wenzelm@3807
   231
(* Now assemble the bits and pieces to prove that Psi is fair. *)
wenzelm@3807
   232
wenzelm@3807
   233
qed_goal "Fair_M1_lemma" Inc.thy
wenzelm@3807
   234
  "[](PsiInv .& [(N1 .| N2)]_<x,y,sem,pc1,pc2>)              \
wenzelm@3807
   235
\            .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2>  \
wenzelm@3807
   236
\  .-> SF(M1)_<x,y>"
wenzelm@3807
   237
  (fn _ => [res_inst_tac [("B","beta1"),("P","$pc1 .= #b")] SF2 1,
wenzelm@3807
   238
	    (* the action premises are simple *)
wenzelm@3807
   239
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def])) 1,
wenzelm@3807
   240
	    SELECT_GOAL (auto_tac (Inc_css addsimps2 angle_def::Psi_defs)) 1,
wenzelm@3807
   241
	    SELECT_GOAL (auto_tac (Inc_css addSEs2 [action_mp N1_enabled_at_b])) 1,
wenzelm@3807
   242
	    (* temporal premise: use previous lemmas and simple TL *)
wenzelm@3807
   243
	    auto_tac (Inc_css addSIs2 DmdStable::(map temp_mp [N1_live,Stuck_at_b]) 
wenzelm@3807
   244
                              addEs2 [STL4E]
wenzelm@3807
   245
		              addsimps2 [square_def])
wenzelm@3807
   246
	   ]);
wenzelm@3807
   247
wenzelm@3807
   248
qed_goal "Fair_M1" Inc.thy "Psi .-> WF(M1)_<x,y>"
wenzelm@3807
   249
  (fn _ => [auto_tac (Inc_css addSIs2 SFImplWF::(map temp_mp [Fair_M1_lemma, PsiInv])
wenzelm@3807
   250
		              addsimps2 [split_box_conj]),
wenzelm@3807
   251
	    auto_tac (Inc_css addsimps2 Psi_def::more_temp_simps)
wenzelm@3807
   252
	   ]);
wenzelm@3807
   253