--- a/src/HOL/UNITY/Constrains.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Wed Aug 19 10:34:31 1998 +0200
@@ -9,6 +9,10 @@
(*** Constrains ***)
+(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*)
+Blast.overloaded ("Constrains.Constrains",
+ HOLogic.dest_setT o domain_type o range_type);
+
(*constrains (Acts prg) B B'
==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
bind_thm ("constrains_reachable_Int",
@@ -80,7 +84,8 @@
"[| ALL i:I. Constrains prg (A i) (A' i) |] \
\ ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
by (dtac ball_constrains_INT 1);
-by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
+by (dtac constrains_reachable_Int 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "ball_Constrains_INT";
Goalw [Constrains_def]
--- a/src/HOL/UNITY/Handshake.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Wed Aug 19 10:34:31 1998 +0200
@@ -32,13 +32,14 @@
by (constrains_tac [prgF_def,cmdF_def] 1);
qed "invFG";
-Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
+Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
+\ ({s. NF s = k} Int {s. BB s})";
by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
by (constrains_tac [prgF_def,cmdF_def] 1);
qed "lemma2_1";
-Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
+Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac [prgG_def,cmdG_def] 2);
by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
@@ -55,6 +56,6 @@
by (rtac lemma2_2 2);
by (rtac LeadsTo_Trans 1);
by (rtac lemma2_2 2);
-by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
+by (rtac (lemma2_1) 1);
by Auto_tac;
qed "progress";
--- a/src/HOL/UNITY/Lift.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Wed Aug 19 10:34:31 1998 +0200
@@ -6,6 +6,13 @@
The Lift-Control Example
*)
+(*ARITH.ML??*)
+Goal "m-1 < n ==> m <= n";
+by (exhaust_tac "m" 1);
+by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
+qed "pred_less_imp_le";
+
+
val always_defs = [above_def, below_def, queueing_def,
goingup_def, goingdown_def, ready_def];
@@ -13,8 +20,6 @@
request_act_def, open_act_def, close_act_def,
req_up_act_def, req_down_act_def, move_up_def, move_down_def];
-AddIffs [min_le_max];
-
Goalw [Lprg_def] "id : Acts Lprg";
by (Simp_tac 1);
qed "id_in_Acts";
@@ -32,9 +37,8 @@
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
moving_up_def, moving_down_def];
+AddIffs [min_le_max];
-val nat_exhaust_less_pred =
- read_instantiate_sg (sign_of thy) [("P", "?m < ?y-1")] nat.exhaust;
val nat_exhaust_le_pred =
read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
@@ -47,6 +51,11 @@
by Auto_tac;
qed "le_pred_eq";
+Goal "0 < n ==> (m-1 < n) = (m<=n)";
+by (exhaust_tac "m" 1);
+by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
+qed "less_pred_eq";
+
Goal "m < n ==> m <= n-1";
by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
qed "less_imp_le_pred";
@@ -107,34 +116,303 @@
val abbrev_defs = [moving_def, stopped_def,
- opened_def, closed_def, atFloor_def];
+ opened_def, closed_def, atFloor_def, Req_def];
val defs = cmd_defs@always_defs@abbrev_defs;
-(***
+
+(** The HUG'93 paper mistakenly omits the Req n from these! **)
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
by (ensures_tac defs "open_act" 1);
-qed "U_F1";
+qed "E_thm01";
+
+Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
+\ (Req n Int opened - atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
+by (ensures_tac defs "open_act" 1);
+qed "E_thm02";
+
+Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
+\ (Req n Int closed - (atFloor n - queueing))";
+by (ensures_tac defs "close_act" 1);
+qed "E_thm03";
+
+Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
+\ (opened Int atFloor n)";
+by (ensures_tac defs "open_act" 1);
+qed "E_thm04";
+
+
+(** Theorem 5. Statements of thm05a and thm05b were wrong! **)
+
+Open_locale "floor";
+
+AddIffs [thm "min_le_n", thm "n_le_max"];
+
+(*NOT an ensures property, but a mere inclusion*)
+Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+\ ((closed Int goingup Int Req n) Un \
+\ (closed Int goingdown Int Req n))";
+br subset_imp_LeadsTo 1;
+by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
+qed "E_thm05c";
+
+Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+\ (moving Int Req n)";
+br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
+by (ensures_tac defs "req_down_act" 2);
+by (ensures_tac defs "req_up_act" 1);
+qed "lift_2";
+
+
+
+val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
+and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
+(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
+
+val [lift_3] =
+goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
+br LeadsTo_Trans 1;
+br (E_thm04 RS LeadsTo_Un) 2;
+br LeadsTo_Un_post' 2;
+br (E_thm01 RS LeadsTo_Trans_Un') 2;
+br (lift_3 RS LeadsTo_Trans_Un') 2;
+br (lift_2 RS LeadsTo_Trans_Un') 2;
+br (E_thm03 RS LeadsTo_Trans_Un') 2;
+br E_thm02 2;
+br (open_move RS Invariant_LeadsToI) 1;
+br (open_stop RS Invariant_LeadsToI) 1;
+br subset_imp_LeadsTo 1;
+by (rtac id_in_Acts 2);
+bws defs;
+by (Clarify_tac 1);
+ (*stops simplification from looping*)
+by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
+by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
+qed "lift_1";
+
-Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
-by (cut_facts_tac [invariantUV] 1);
-by (rewtac Lprg_def);
-by (ensures_tac defs "cmd2U" 1);
-qed "U_F2";
+val rev_mp' = read_instantiate_sg (sign_of thy)
+ [("P", "0 < metric ?n ?s")] rev_mp;
+
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_up_act" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+by (auto_tac (claset() addIs [diff_Suc_less_diff],
+ simpset() addsimps [arith1, arith2, metric_def]));
+qed "E_thm16a";
+
+
+(*arith1 comes from
+ 1. !!s i.
+ [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
+ i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
+ ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
+ Suc (floor s) < n; 0 < floor s - min |]
+ ==> n - Suc (floor s) < floor s - min + (n - min)
+*)
+
+(*arith2 comes from
+ 2. !!s i.
+ [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
+ i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
+ ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
+ Suc (floor s) < n; min < n |]
+ ==> n - Suc (floor s) < floor s - min + (n - min)
+*)
+
+
+xxxxxxxxxxxxxxxx;
+
+Goal "j<=i ==> i - j < Suc i - j";
+by (REPEAT (etac rev_mp 1));
+by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
+by Auto_tac;
+qed "diff_less_Suc_diff";
+
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_down_act" 1);
+be rev_mp 2;
+be rev_mp 1;
+by (dtac less_eq_Suc_add 2);
+by (Clarify_tac 2);
+by (Asm_full_simp_tac 2);
+by (dtac less_eq_Suc_add 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+
+by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
+by (REPEAT (Safe_step_tac 1));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
+by (REPEAT (Safe_step_tac 1));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
+by (REPEAT (Safe_step_tac 1));
+
+
+
+
+
+
+
+Goal "[| i + k < n; Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
+by (REPEAT (etac rev_mp 1));
+by (arith_oracle_tac 1);
+
-Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
-by (rtac leadsTo_imp_LeadsTo 1);
-by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
-by (ensures_tac defs "cmd4U" 2);
-by (ensures_tac defs "cmd3U" 1);
-qed "U_F3";
+by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(blast_tac (claset() addEs [less_asym]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+
+
+by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
+
+
+by (REPEAT (Safe_step_tac 2));
+by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
+
+by (auto_tac (claset() addIs [diff_Suc_less_diff],
+ simpset() addsimps [metric_def]));
+qed "E_thm16b";
+
+
+
+Goal "[| m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
+
+
+not_less_iff_le
+
+Goal "[| ~ m < n; m - 1 < n |] ==> n = m";
+by (cut_facts_tac [less_linear] 1);
+by (blast_tac (claset() addSEs [less_irrefl]) 1);
+ by (REPEAT (etac rev_mp 1));
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (arith_oracle_tac 1);
+
+
+
+
+
+
+
+(**in the postscript file, but too horrible**)
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_down_act" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+
+by (dtac less_eq_Suc_add 2);
+by (Clarify_tac 2);
+by (Asm_full_simp_tac 2);
+by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
+
+
+yyyyyyyyyyyyyyyy;
+
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by(blast_tac (claset() addDs [le_anti_sym]
+ addSDs [leI, pred_less_imp_le]) 2);
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+
-Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
- MRS LeadsTo_Diff) 1);
-by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
-val U_lemma2 = result();
+by(Blast_tac 3);
+
+
+
+
+
+
+
+Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
+fe rev_mp;
+by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
+ by (ALLGOALS Asm_simp_tac);
+
+by (arith_oracle_tac 1);
+
+
+Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
+by (REPEAT (etac rev_mp 1));
+by (arith_oracle_tac 1);
+
+
+
+
+
+
+
+infixr TRANS;
+fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
+
+E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
+
+
+
+[E_thm02,
+ E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
+
-***)
+val sact = "open_act";
+val sact = "move_up_act";
+
+val (main_def::CDEFS) = defs;
+
+by (REPEAT (Invariant_Int_tac 1));
+
+by (etac Invariant_LeadsTo_Basis 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1));
+
+by (res_inst_tac [("act", sact)] transient_mem 2);
+by (simp_tac (simpset() addsimps (Domain_partial_func::CDEFS)) 3);
+by (force_tac (claset(), simpset() addsimps [main_def]) 2);
+by (constrains_tac (main_def::CDEFS) 1);
+by (rewrite_goals_tac CDEFS);
+by (ALLGOALS Clarify_tac);
+by (Auto_tac);
+
+by(Force_tac 2);
+
+
+
+yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
+
+
+
+Goalw [transient_def]
+ "transient acts A = (EX act:acts. A <= act^-1 ^^ (Compl A))";
+by Safe_tac;
+by (ALLGOALS (rtac bexI));
+by (TRYALL assume_tac);
+by (Blast_tac 1);
+br conjI 1;
+by (Blast_tac 1);
+(*remains to show
+ [| act : acts; A <= act^-1 ^^ Compl A |] ==> act ^^ A <= Compl A
+*)
+
--- a/src/HOL/UNITY/Lift.thy Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Wed Aug 19 10:34:31 1998 +0200
@@ -4,6 +4,8 @@
Copyright 1998 University of Cambridge
The Lift-Control Example
+
+
*)
Lift = SubstAx +
@@ -17,11 +19,15 @@
move :: bool (*whether moving takes precedence over opening*)
consts
- min, max :: nat (*least and greatest floors*)
+ min, max :: nat (*least and greatest floors*)
rules
min_le_max "min <= max"
+ (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
+ arith1 "m < fl ==> n - Suc fl < fl - m + (n - m)"
+ arith2 "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
+
constdefs
@@ -37,7 +43,7 @@
"queueing == above Un below"
goingup :: state set
- "goingup == above Int ({s. up s} Un Compl below)"
+ "goingup == above Int ({s. up s} Un Compl below)"
goingdown :: state set
"goingdown == below Int ({s. ~ up s} Un Compl above)"
@@ -52,17 +58,20 @@
"moving == {s. ~ stop s & ~ open s}"
stopped :: state set
- "stopped == {s. stop s & ~ open s & move s}"
+ "stopped == {s. stop s & ~ open s & ~ move s}"
opened :: state set
"opened == {s. stop s & open s & move s}"
- closed :: state set
+ closed :: state set (*but this is the same as ready!!*)
"closed == {s. stop s & ~ open s & move s}"
atFloor :: nat => state set
"atFloor n == {s. floor s = n}"
+ Req :: nat => state set
+ "Req n == {s. n : req s}"
+
(** The program **)
@@ -125,7 +134,7 @@
"open_move == {s. open s --> move s}"
stop_floor :: state set
- "stop_floor == {s. open s & ~ move s --> floor s : req s}"
+ "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
moving_up :: state set
"moving_up == {s. ~ stop s & up s -->
@@ -135,8 +144,19 @@
"moving_down == {s. ~ stop s & ~ up s -->
(EX f. min <= f & f <= floor s & f : req s)}"
- (*intersection of all invariants: NECESSARY??*)
- valid :: state set
- "valid == bounded Int open_stop Int open_move"
+ metric :: [nat,state] => nat
+ "metric n s == if up s & floor s < n then n - floor s
+ else if ~ up s & n < floor s then floor s - n
+ else if up s & n < floor s then (max - floor s) + (max-n)
+ else if ~ up s & floor s < n then (floor s - min) + (n-min)
+ else 0"
+
+locale floor =
+ fixes
+ n :: nat
+ assumes
+ min_le_n "min <= n"
+ n_le_max "n <= max"
+ defines
end
--- a/src/HOL/UNITY/Mutex.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Wed Aug 19 10:34:31 1998 +0200
@@ -76,7 +76,7 @@
qed "U_F1";
Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
-by (cut_facts_tac [invariantUV] 1);
+by (cut_facts_tac [invariantU] 1);
by (rewtac Mprg_def);
by (ensures_tac cmd_defs "cmd2U" 1);
qed "U_F2";
@@ -88,7 +88,7 @@
qed "U_F3";
Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
@@ -125,7 +125,7 @@
qed "V_F1";
Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
-by (cut_facts_tac [invariantUV] 1);
+by (cut_facts_tac [invariantV] 1);
by (ensures_tac cmd_defs "cmd2V" 1);
qed "V_F2";
@@ -136,7 +136,7 @@
qed "V_F3";
Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
--- a/src/HOL/UNITY/SubstAx.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Wed Aug 19 10:34:31 1998 +0200
@@ -6,6 +6,9 @@
LeadsTo relation, restricted to the set of reachable states.
*)
+(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*)
+Blast.overloaded ("SubstAx.LeadsTo",
+ HOLogic.dest_setT o domain_type o range_type);
(*** Specialized laws for handling invariants ***)
@@ -42,7 +45,7 @@
by (Simp_tac 1);
by (stac Int_Union 1);
by (blast_tac (claset() addIs [leadsTo_UN,
- simplify (simpset()) prem]) 1);
+ simplify (simpset()) prem]) 1);
qed "LeadsTo_Union";
@@ -88,15 +91,36 @@
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
qed_spec_mp "LeadsTo_weaken_R";
-
Goal "[| LeadsTo prg A A'; B <= A; id: Acts prg |] \
\ ==> LeadsTo prg B A'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
qed_spec_mp "LeadsTo_weaken_L";
+Goal "[| LeadsTo prg A A'; id: Acts prg; \
+\ B <= A; A' <= B' |] \
+\ ==> LeadsTo prg B B'";
+(*PROOF FAILED unless the Trans rule is last*)
+by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
+ LeadsTo_Trans]) 1);
+qed "LeadsTo_weaken";
-(*Distributes over binary unions*)
+
+(** Two theorems for "proof lattices" **)
+
+Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
+qed "LeadsTo_Un_post";
+
+Goal "[| id: Acts prg; LeadsTo prg A B; LeadsTo prg B C |] \
+\ ==> LeadsTo prg (A Un B) C";
+by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
+ LeadsTo_weaken_L, LeadsTo_Trans]) 1);
+qed "LeadsTo_Trans_Un";
+
+
+(** Distributive laws **)
+
Goal "id: Acts prg ==> \
\ LeadsTo prg (A Un B) C = \
\ (LeadsTo prg A C & LeadsTo prg B C)";
@@ -116,15 +140,6 @@
qed "LeadsTo_Union_distrib";
-Goal "[| LeadsTo prg A A'; id: Acts prg; \
-\ B <= A; A' <= B' |] \
-\ ==> LeadsTo prg B B'";
-(*PROOF FAILED*)
-by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
- LeadsTo_weaken_L]) 1);
-qed "LeadsTo_weaken";
-
-
(** More rules using the premise "Invariant prg" **)
Goalw [LeadsTo_def, Constrains_def]
@@ -160,12 +175,18 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: Acts prg |] \
+Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
\ ==> LeadsTo prg A C";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
+by (stac (Un_Diff_Int RS sym) 1 THEN rtac LeadsTo_Un 1);
+by (REPEAT (assume_tac 1));
+(*One step, but PROOF FAILED...
+ by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
+*)
qed "LeadsTo_Diff";
+
+
val prems =
Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
\ ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
@@ -405,8 +426,10 @@
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
res_inst_tac [("act", sact)] transient_mem 2,
+ (*simplify the command's domain*)
simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
- simp_tac (simpset() addsimps [main_def]) 2,
+ (*INSIST that the command belongs to the program*)
+ force_tac (claset(), simpset() addsimps [main_def]) 2,
constrains_tac (main_def::cmd_defs) 1,
rewrite_goals_tac cmd_defs,
ALLGOALS Clarify_tac,
--- a/src/HOL/UNITY/UNITY.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Wed Aug 19 10:34:31 1998 +0200
@@ -14,6 +14,14 @@
(*** constrains ***)
+(*Map the type (anything => ('a set => anything) to just 'a*)
+fun overload_2nd_set s =
+ Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
+
+overload_2nd_set "UNITY.constrains";
+overload_2nd_set "UNITY.stable";
+overload_2nd_set "UNITY.unless";
+
val prems = Goalw [constrains_def]
"(!!act s s'. [| act: acts; (s,s') : act; s: A |] ==> s': A') \
\ ==> constrains acts A A'";
--- a/src/HOL/UNITY/WFair.ML Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Wed Aug 19 10:34:31 1998 +0200
@@ -9,6 +9,14 @@
*)
+(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*)
+Blast.overloaded ("WFair.leadsto",
+ #1 o HOLogic.dest_prodT o
+ HOLogic.dest_setT o HOLogic.dest_setT o domain_type);
+
+overload_2nd_set "WFair.transient";
+overload_2nd_set "WFair.ensures";
+
(*** transient ***)
Goalw [stable_def, constrains_def, transient_def]
@@ -52,8 +60,7 @@
Goalw [ensures_def, constrains_def, transient_def]
"acts ~= {} ==> ensures acts A UNIV";
-by (Asm_simp_tac 1); (*omitting this causes PROOF FAILED, even with Safe_tac*)
-by (Blast_tac 1);
+by Auto_tac;
qed "ensures_UNIV";
Goalw [ensures_def]
@@ -165,9 +172,9 @@
Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
\ ==> leadsTo acts B B'";
-(*PROOF FAILED: why?*)
-by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
- leadsTo_weaken_L]) 1);
+(*PROOF FAILED unless leadsTo_Trans is last*)
+by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
+ leadsTo_Trans]) 1);
qed "leadsTo_weaken";
@@ -468,7 +475,7 @@
(*** Completion: Binary and General Finite versions ***)
Goal "[| leadsTo acts A A'; stable acts A'; \
-\ leadsTo acts B B'; stable acts B'; id: acts |] \
+\ leadsTo acts B B'; stable acts B'; id: acts |] \
\ ==> leadsTo acts (A Int B) (A' Int B')";
by (subgoal_tac "stable acts (wlt acts B')" 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
@@ -483,8 +490,8 @@
by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD,
subset_imp_leadsTo]) 2);
-(*Blast_tac gives PROOF FAILED*)
-by (best_tac (claset() addIs [leadsTo_Trans]) 1);
+(*addIs looks safer, but loops with PROOF FAILED*)
+by (blast_tac (claset() addSIs [leadsTo_Trans]) 1);
qed "stable_completion";
--- a/src/HOL/UNITY/WFair.thy Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy Wed Aug 19 10:34:31 1998 +0200
@@ -21,11 +21,12 @@
"ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
(*(unless acts A B) would be equivalent*)
-consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
translations
"leadsTo acts A B" == "(A,B) : leadsto acts"
+ "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
inductive "leadsto acts"
intrs