--- a/src/HOL/UNITY/Alloc.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Wed May 24 18:40:01 2000 +0200
@@ -6,6 +6,9 @@
Specification of Chandy and Charpentier's Allocator
*)
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
+
AddIs [impOfSubs subset_preserves_o];
Addsimps [funPair_o_distrib];
Addsimps [Always_INT_distrib];
--- a/src/HOL/UNITY/Client.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Client.ML Wed May 24 18:40:01 2000 +0200
@@ -12,11 +12,6 @@
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
-fun invariant_tac i =
- rtac invariantI i THEN
- constrains_tac (i+1);
-
-
(*Safety property 1: ask, rel are increasing*)
Goal "Client: UNIV guarantees[funPair rel ask] \
\ Increasing ask Int Increasing rel";
--- a/src/HOL/UNITY/Extend.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML Wed May 24 18:40:01 2000 +0200
@@ -10,6 +10,61 @@
(** These we prove OUTSIDE the locale. **)
+
+(*** Restrict [MOVE to Relation.thy?] ***)
+
+Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
+by (Blast_tac 1);
+qed "Restrict_iff";
+AddIffs [Restrict_iff];
+
+Goal "Restrict UNIV = id";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_UNIV";
+Addsimps [Restrict_UNIV];
+
+Goal "Restrict {} r = {}";
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_empty";
+Addsimps [Restrict_empty];
+
+Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
+by (Blast_tac 1);
+qed "Restrict_Int";
+Addsimps [Restrict_Int];
+
+Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
+by Auto_tac;
+qed "Restrict_triv";
+
+Goalw [Restrict_def] "Restrict A r <= r";
+by Auto_tac;
+qed "Restrict_subset";
+
+Goalw [Restrict_def]
+ "[| A <= B; Restrict B r = Restrict B s |] \
+\ ==> Restrict A r = Restrict A s";
+by (blast_tac (claset() addSEs [equalityE]) 1);
+qed "Restrict_eq_mono";
+
+Goalw [Restrict_def, image_def]
+ "[| s : RR; Restrict A r = Restrict A s |] \
+\ ==> Restrict A r : Restrict A `` RR";
+by Auto_tac;
+qed "Restrict_imageI";
+
+Goal "Domain (Restrict A r) = A Int Domain r";
+by (Blast_tac 1);
+qed "Domain_Restrict";
+
+Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
+by (Blast_tac 1);
+qed "Image_Restrict";
+
+Addsimps [Domain_Restrict, Image_Restrict];
+
+
Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
qed "insert_Id_image_Acts";
--- a/src/HOL/UNITY/Extend.thy Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy Wed May 24 18:40:01 2000 +0200
@@ -12,6 +12,10 @@
constdefs
+ (*MOVE to Relation.thy?*)
+ Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
+ "Restrict A r == r Int (A <*> UNIV)"
+
good_map :: "['a*'b => 'c] => bool"
"good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)"
(*Using the locale constant "f", this is f (h (x,y))) = x*)
--- a/src/HOL/UNITY/Follows.thy Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Follows.thy Wed May 24 18:40:01 2000 +0200
@@ -6,7 +6,7 @@
The "Follows" relation of Charpentier and Sivilotte
*)
-Follows = SubstAx +
+Follows = SubstAx + ListOrder +
constdefs
--- a/src/HOL/UNITY/LessThan.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/LessThan.ML Wed May 24 18:40:01 2000 +0200
@@ -3,223 +3,12 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-lessThan, greaterThan, atLeast, atMost
*)
-(*** Restrict [MOVE TO RELATION.THY??] ***)
-
-Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
-by (Blast_tac 1);
-qed "Restrict_iff";
-AddIffs [Restrict_iff];
-
-Goal "Restrict UNIV = id";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
-qed "Restrict_UNIV";
-Addsimps [Restrict_UNIV];
-
-Goal "Restrict {} r = {}";
-by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
-qed "Restrict_empty";
-Addsimps [Restrict_empty];
-
-Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
-by (Blast_tac 1);
-qed "Restrict_Int";
-Addsimps [Restrict_Int];
-
-Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
-by Auto_tac;
-qed "Restrict_triv";
-
-Goalw [Restrict_def] "Restrict A r <= r";
-by Auto_tac;
-qed "Restrict_subset";
-
-Goalw [Restrict_def]
- "[| A <= B; Restrict B r = Restrict B s |] \
-\ ==> Restrict A r = Restrict A s";
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "Restrict_eq_mono";
-
-Goalw [Restrict_def, image_def]
- "[| s : RR; Restrict A r = Restrict A s |] \
-\ ==> Restrict A r : Restrict A `` RR";
-by Auto_tac;
-qed "Restrict_imageI";
-
-Goal "Domain (Restrict A r) = A Int Domain r";
-by (Blast_tac 1);
-qed "Domain_Restrict";
-
-Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
-by (Blast_tac 1);
-qed "Image_Restrict";
-
-Addsimps [Domain_Restrict, Image_Restrict];
-
-
-
-(*** lessThan ***)
-
-Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
-by (Blast_tac 1);
-qed "lessThan_iff";
-AddIffs [lessThan_iff];
-
-Goalw [lessThan_def] "lessThan 0 = {}";
-by (Simp_tac 1);
-qed "lessThan_0";
-Addsimps [lessThan_0];
-
-Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
-by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
-by (Blast_tac 1);
-qed "lessThan_Suc";
-
-Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
-by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
-qed "lessThan_Suc_atMost";
-
-Goal "finite (lessThan k)";
-by (induct_tac "k" 1);
-by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
-by Auto_tac;
-qed "finite_lessThan";
-
-Goal "(UN m. lessThan m) = UNIV";
-by (Blast_tac 1);
-qed "UN_lessThan_UNIV";
-
-Goalw [lessThan_def, atLeast_def, le_def]
- "-lessThan k = atLeast k";
-by (Blast_tac 1);
-qed "Compl_lessThan";
-
-Goal "{k} - lessThan k = {k}";
-by (Blast_tac 1);
-qed "single_Diff_lessThan";
-Addsimps [single_Diff_lessThan];
-
-(*** greaterThan ***)
-
-Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
-by (Blast_tac 1);
-qed "greaterThan_iff";
-AddIffs [greaterThan_iff];
-
-Goalw [greaterThan_def] "greaterThan 0 = range Suc";
-by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
-qed "greaterThan_0";
-Addsimps [greaterThan_0];
-
-Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
-by (auto_tac (claset() addEs [linorder_neqE], simpset()));
-qed "greaterThan_Suc";
-
-Goal "(INT m. greaterThan m) = {}";
-by (Blast_tac 1);
-qed "INT_greaterThan_UNIV";
-
-Goalw [greaterThan_def, atMost_def, le_def]
- "-greaterThan k = atMost k";
-by (Blast_tac 1);
-qed "Compl_greaterThan";
-
-Goalw [greaterThan_def, atMost_def, le_def]
- "-atMost k = greaterThan k";
-by (Blast_tac 1);
-qed "Compl_atMost";
-
-Goal "less_than ^^ {k} = greaterThan k";
-by (Blast_tac 1);
-qed "Image_less_than";
-
-Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
-
-(*** atLeast ***)
-
-Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
-by (Blast_tac 1);
-qed "atLeast_iff";
-AddIffs [atLeast_iff];
-
-Goalw [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
-by (Simp_tac 1);
-qed "atLeast_0";
-Addsimps [atLeast_0];
-
-Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
-by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
-by (simp_tac (simpset() addsimps [order_le_less]) 1);
-by (Blast_tac 1);
-qed "atLeast_Suc";
-
-Goal "(UN m. atLeast m) = UNIV";
-by (Blast_tac 1);
-qed "UN_atLeast_UNIV";
-
-Goalw [lessThan_def, atLeast_def, le_def]
- "-atLeast k = lessThan k";
-by (Blast_tac 1);
-qed "Compl_atLeast";
-
-Goal "less_than^-1 ^^ {k} = lessThan k";
-by (Blast_tac 1);
-qed "Image_inverse_less_than";
-
-Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
-
-(*** atMost ***)
-
-Goalw [atMost_def] "(i: atMost k) = (i<=k)";
-by (Blast_tac 1);
-qed "atMost_iff";
-AddIffs [atMost_iff];
-
-Goalw [atMost_def] "atMost 0 = {0}";
-by (Simp_tac 1);
-qed "atMost_0";
-Addsimps [atMost_0];
-
-Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
-by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
-by (Blast_tac 1);
-qed "atMost_Suc";
-
-Goal "finite (atMost k)";
-by (induct_tac "k" 1);
-by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
-by Auto_tac;
-qed "finite_atMost";
-
-Goal "(UN m. atMost m) = UNIV";
-by (Blast_tac 1);
-qed "UN_atMost_UNIV";
-
-Goalw [atMost_def, le_def]
- "-atMost k = greaterThan k";
-by (Blast_tac 1);
-qed "Compl_atMost";
-Addsimps [Compl_atMost];
-
-
-(*** Combined properties ***)
-
-Goal "atMost n Int atLeast n = {n}";
-by (blast_tac (claset() addIs [order_antisym]) 1);
-qed "atMost_Int_atLeast";
-
-
-
-
(*** Finally, a few set-theoretic laws...
CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)
-context Set.thy;
-
(** Rewrite rules to eliminate A. Conditions can be satisfied by letting B
be any set including A Int C and contained in A Un C, such as B=A or B=C.
**)
@@ -256,22 +45,3 @@
set_cancel4, set_cancel5, set_cancel6];
-(** More ad-hoc rules **)
-
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-Addsimps [Un_Diff_Diff];
-
-Goal "A Int (B - C) Un C = A Int B Un C";
-by (Blast_tac 1);
-qed "Int_Diff_Un";
-
-Goal "Union(B) Int A = (UN C:B. C Int A)";
-by (Blast_tac 1);
-qed "Int_Union2";
-
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
-by (Blast_tac 1);
-qed "Int_Union_Union";
-
--- a/src/HOL/UNITY/LessThan.thy Wed May 24 18:19:04 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: HOL/UNITY/LessThan
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-lessThan, greaterThan, atLeast, atMost
-
-Could generalize to any linear ordering?
-*)
-
-LessThan = Main +
-
-constdefs
-
- (*MOVE TO RELATION.THY??*)
- Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
- "Restrict A r == r Int (A <*> UNIV)"
-
- lessThan :: "nat => nat set"
- "lessThan n == {i. i<n}"
-
- atMost :: "nat => nat set"
- "atMost n == {i. i<=n}"
-
- greaterThan :: "nat => nat set"
- "greaterThan n == {i. n<i}"
-
- atLeast :: "nat => nat set"
- "atLeast n == {i. n<=i}"
-
-end
--- a/src/HOL/UNITY/Lift_prog.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Wed May 24 18:40:01 2000 +0200
@@ -106,7 +106,7 @@
Goal "lift_set i {s. P s} = {s. P (drop_map i s)}";
by (rtac set_ext 1);
by (asm_simp_tac (simpset() delsimps [image_Collect]
- addsimps [lift_set_def, rename_set_eq_Collect]) 1);
+ addsimps [lift_set_def, bij_image_Collect_eq]) 1);
qed "lift_set_eq_Collect";
Goalw [lift_set_def] "lift_set i {} = {}";
--- a/src/HOL/UNITY/Rename.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML Wed May 24 18:40:01 2000 +0200
@@ -30,11 +30,6 @@
simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
qed "mem_rename_set_iff";
-Goal "bij h ==> h``{s. P s} = {s. P (inv h s)}";
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
-qed "rename_set_eq_Collect";
-
Goal "extend_set (%(x,u). h x) A = h``A";
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_set_def]));
--- a/src/HOL/UNITY/SubstAx.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Wed May 24 18:40:01 2000 +0200
@@ -335,7 +335,7 @@
val prems =
-Goal "(!! m. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \
+Goal "(!!m::nat. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \
\ ==> F : A LeadsTo B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (auto_tac (claset() addIs prems, simpset()));
@@ -353,7 +353,7 @@
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
-Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo \
+Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(lessThan m)) Un B) |] \
\ ==> F : A LeadsTo ((A Int (f-``(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
@@ -361,7 +361,7 @@
by (Asm_simp_tac 1);
qed "LessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo \
+Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(greaterThan m)) Un B) |] \
\ ==> F : A LeadsTo ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
--- a/src/HOL/UNITY/UNITY.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML Wed May 24 18:40:01 2000 +0200
@@ -343,3 +343,27 @@
"F : A co B ==> strongest_rhs F A <= B";
by (Blast_tac 1);
qed "strongest_rhs_is_strongest";
+
+
+(** Ad-hoc set-theory rules **)
+
+Goal "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+Addsimps [Un_Diff_Diff];
+
+Goal "Union(B) Int A = Union((%C. C Int A)``B)";
+by (Blast_tac 1);
+qed "Int_Union_Union";
+
+(** Needed for WF reasoning in WFair.ML **)
+
+Goal "less_than ^^ {k} = greaterThan k";
+by (Blast_tac 1);
+qed "Image_less_than";
+
+Goal "less_than^-1 ^^ {k} = lessThan k";
+by (Blast_tac 1);
+qed "Image_inverse_less_than";
+
+Addsimps [Image_less_than, Image_inverse_less_than];
--- a/src/HOL/UNITY/UNITY.thy Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/UNITY.thy Wed May 24 18:40:01 2000 +0200
@@ -8,8 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = LessThan + ListOrder +
-
+UNITY = Main +
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
--- a/src/HOL/UNITY/WFair.ML Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/WFair.ML Wed May 24 18:40:01 2000 +0200
@@ -400,14 +400,14 @@
(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
val prems =
-Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
+Goal "[| !!m::nat. F : (A Int f-``{m}) leadsTo ((A Int f-``{..m(}) Un B) |] \
\ ==> F : A leadsTo B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs prems) 1);
qed "lessThan_induct";
-Goal "[| ALL m:(greaterThan l). \
+Goal "!!l::nat. [| ALL m:(greaterThan l). \
\ F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
\ ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl,
@@ -416,7 +416,7 @@
by (Asm_simp_tac 1);
qed "lessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). \
+Goal "!!l::nat. [| ALL m:(lessThan l). \
\ F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
\ ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]