--- a/src/HOL/UNITY/Constrains.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Wed Sep 23 10:11:18 1998 +0200
@@ -217,6 +217,8 @@
Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsI";
+(* [| Invariant prg INV; Constrains prg (INV Int A) A |]
+ ==> Stable prg A *)
bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
Goal "[| Invariant prg INV; Constrains prg A A' |] \
--- a/src/HOL/UNITY/Deadlock.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Wed Sep 23 10:11:18 1998 +0200
@@ -66,9 +66,9 @@
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
- (simpset() addsimps (Int_ac @
- [Int_Un_distrib, Int_Un_distrib2, lemma,
- Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
+ (simpset() addsimps Int_ac @
+ [Int_Un_distrib, Int_Un_distrib2, lemma,
+ Collect_less_Suc_insert, Collect_le_Suc_insert]) 1);
qed "INT_le_equals_Int";
Goal "(INT i:{i. i <= Suc n}. A i) = \
@@ -88,6 +88,6 @@
constrains_Int RS constrains_weaken) 1);
by (simp_tac (simpset() addsimps [Collect_le_Int_equals,
Int_assoc, INT_absorb]) 1);
-by (simp_tac (simpset() addsimps ([INT_le_Suc_equals_Int])) 1);
+by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
result();
--- a/src/HOL/UNITY/LessThan.thy Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/LessThan.thy Wed Sep 23 10:11:18 1998 +0200
@@ -4,6 +4,8 @@
Copyright 1998 University of Cambridge
lessThan, greaterThan, atLeast, atMost
+
+Could generalize to any linear ordering?
*)
LessThan = Main +
--- a/src/HOL/UNITY/NSP_Bad.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML Wed Sep 23 10:11:18 1998 +0200
@@ -31,9 +31,9 @@
by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
-br reachable.Init 5;
+by (rtac reachable.Init 5);
by (ALLGOALS Asm_simp_tac);
-by (REPEAT_FIRST (resolve_tac [exI]));
+by (REPEAT_FIRST (rtac exI ));
by possibility_tac;
result();
@@ -75,7 +75,7 @@
*)
Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)";
-be reachable.induct 1;
+by (etac reachable.induct 1);
by Auto_tac;
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
--- a/src/HOL/UNITY/Reach.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Wed Sep 23 10:11:18 1998 +0200
@@ -113,7 +113,7 @@
by (ensures_tac "asgt a b" 1);
by (Blast_tac 2);
by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
-bd (metric_le RS le_anti_sym) 1;
+by (dtac (metric_le RS le_anti_sym) 1);
by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
simpset()));
qed "LeadsTo_Diff_fixedpoint";
--- a/src/HOL/UNITY/SubstAx.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Wed Sep 23 10:11:18 1998 +0200
@@ -267,7 +267,7 @@
Goal "[| LeadsTo prg A A'; Stable prg B |] \
\ ==> LeadsTo prg (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
qed "PSP_stable2";
Goalw [LeadsTo_def, Constrains_def]
@@ -278,7 +278,7 @@
Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
qed "PSP2";
Goalw [Unless_def]
--- a/src/HOL/UNITY/WFair.ML Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Wed Sep 23 10:11:18 1998 +0200
@@ -281,7 +281,7 @@
Goal "[| leadsTo acts A A'; stable acts B |] \
\ ==> leadsTo acts (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (psp_stable::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
qed "psp_stable2";
Goalw [ensures_def, constrains_def]
@@ -306,7 +306,7 @@
Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (psp::Int_ac)) 1);
+by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
qed "psp2";