src/HOL/UNITY/Mutex.ML
author paulson
Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253 82a5ca6290aa
parent 5240 bbcd79ef7cf2
child 5277 e4297d03e5d2
permissions -rw-r--r--
New record type of programs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
     1
(*  Title:      HOL/UNITY/Mutex
4776
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
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
     9
(*split_all_tac causes a big blow-up*)
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    10
claset_ref() := claset() delSWrapper "split_all_tac";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    12
val cmd_defs = [Mprg_def, 
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    13
		cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    14
		cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    16
Goalw [Mprg_def] "id : Acts Mprg";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
by (Simp_tac 1);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    18
qed "id_in_Acts";
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    19
AddIffs [id_in_Acts];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    22
(*Simplification for records*)
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    23
val select_defs = thms"state.select_defs"
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    24
and update_defs = thms"state.update_defs"
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    25
and dest_defs   = thms"state.dest_defs";
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    26
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    27
Addsimps update_defs;
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    28
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    29
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    30
Addsimps [invariantU_def, invariantV_def];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    33
Goalw [Mprg_def] "invariant Mprg invariantU";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    34
by (rtac invariantI 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    35
by (constrains_tac cmd_defs 2);
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    36
by Auto_tac;
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    37
qed "invariantU";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    39
Goalw [Mprg_def] "invariant Mprg invariantV";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    40
by (rtac invariantI 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    41
by (constrains_tac cmd_defs 2);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    42
by Auto_tac;
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    43
qed "invariantV";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    45
val invariantUV = invariant_Int_rule [invariantU, invariantV];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    46
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    47
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    48
(*The safety property: mutual exclusion*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    49
Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    50
by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
qed "mutual_exclusion";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    53
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    54
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    55
(*The bad invariant FAILS in cmd1V*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    56
Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    57
by (constrains_tac cmd_defs 1);
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    58
by (REPEAT (trans_tac 1));
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
by (safe_tac (claset() addSEs [le_SucE]));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    60
by (Asm_full_simp_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    61
(*Resulting state: n=1, p=false, m=4, u=false.  
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    62
  Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    63
  violating the invariant!*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    64
(*Check that subgoals remain: proof failed.*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    65
getgoal 1;  
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    66
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    67
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    68
(*** Progress for U ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    69
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    70
Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    71
by (constrains_tac cmd_defs 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    72
qed "U_F0";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    73
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    74
Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    75
by (ensures_tac cmd_defs "cmd1U" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    76
qed "U_F1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    77
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    78
Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    79
by (cut_facts_tac [invariantUV] 1);
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    80
bw Mprg_def;
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    81
by (ensures_tac cmd_defs "cmd2U" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    82
qed "U_F2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    83
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    84
Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    85
by (rtac leadsTo_imp_LeadsTo 1); 
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    86
by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    87
by (ensures_tac cmd_defs "cmd4U" 2);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    88
by (ensures_tac cmd_defs "cmd3U" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    89
qed "U_F3";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    90
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    91
Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    92
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    93
	  MRS LeadsTo_Diff) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    94
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    95
by (auto_tac (claset() addSEs [less_SucE], simpset()));
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    96
val U_lemma2 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    97
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
    98
Goal "LeadsTo Mprg {s. MM s = 1} {s. PP s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
    99
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   100
by (Blast_tac 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   101
val U_lemma1 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   102
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   103
Goal "LeadsTo Mprg {s. 1 <= MM s & MM s <= 3} {s. PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   104
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   105
	                addcongs [rev_conj_cong]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   106
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   107
				  U_lemma1, U_lemma2, U_F3] ) 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   108
val U_lemma123 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   109
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   110
(*Misra's F4*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   111
Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   112
by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   113
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   114
qed "u_leadsto_p";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   115
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   116
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   117
(*** Progress for V ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   118
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   119
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   120
Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   121
by (constrains_tac cmd_defs 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   122
qed "V_F0";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   123
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   124
Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   125
by (ensures_tac cmd_defs "cmd1V" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   126
qed "V_F1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   127
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   128
Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   129
by (cut_facts_tac [invariantUV] 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   130
by (ensures_tac cmd_defs "cmd2V" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   131
qed "V_F2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   132
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   133
Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   134
by (rtac leadsTo_imp_LeadsTo 1); 
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
   135
by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   136
by (ensures_tac cmd_defs "cmd4V" 2);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   137
by (ensures_tac cmd_defs "cmd3V" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   138
qed "V_F3";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   139
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   140
Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   141
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   142
	  MRS LeadsTo_Diff) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   143
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   144
by (auto_tac (claset() addSEs [less_SucE], simpset()));
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   145
val V_lemma2 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   146
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   147
Goal "LeadsTo Mprg {s. NN s = 1} {s. ~ PP s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   148
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   149
by (Blast_tac 1);
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   150
val V_lemma1 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   151
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   152
Goal "LeadsTo Mprg {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   153
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   154
	                addcongs [rev_conj_cong]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   155
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   156
				  V_lemma1, V_lemma2, V_F3] ) 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   157
val V_lemma123 = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   158
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   159
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   160
(*Misra's F4*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   161
Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
5240
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents: 5232
diff changeset
   162
by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   163
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   164
qed "v_leadsto_not_p";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   165
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   166
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   167
(** Absence of starvation **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   168
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   169
(*Misra's F6*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   170
Goal "LeadsTo Mprg {s. MM s = 1} {s. MM s = 3}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   171
by (rtac LeadsTo_Un_duplicate 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   172
by (rtac LeadsTo_cancel2 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   173
by (rtac U_F2 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   174
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   175
by (stac Un_commute 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   176
by (rtac LeadsTo_Un_duplicate 1);
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
   177
by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   178
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   179
by (auto_tac (claset() addSEs [less_SucE], simpset()));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   180
qed "m1_leadsto_3";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   181
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   182
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   183
(*The same for V*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5240
diff changeset
   184
Goal "LeadsTo Mprg {s. NN s = 1} {s. NN s = 3}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   185
by (rtac LeadsTo_Un_duplicate 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   186
by (rtac LeadsTo_cancel2 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   187
by (rtac V_F2 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   188
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   189
by (stac Un_commute 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   190
by (rtac LeadsTo_Un_duplicate 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   191
by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   192
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   193
by (auto_tac (claset() addSEs [less_SucE], simpset()));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   194
qed "n1_leadsto_3";