# HG changeset patch
# User paulson
# Date 959186401 -7200
# Node ID b797cfa3548d8cf05704107f696511201ab87b5d
# Parent  971aedd340e477aa39784e8f9caf44686ebcdfda
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML

diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Alloc.ML
--- 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];
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Client.ML
--- 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";
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Extend.ML
--- 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";
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Extend.thy
--- 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*)
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Follows.thy
--- 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
 
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/LessThan.ML
--- 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";
-
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/LessThan.thy
--- 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
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Lift_prog.ML
--- 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 {} = {}";
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/Rename.ML
--- 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]));
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/SubstAx.ML
--- 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")]
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/UNITY.ML
--- 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];
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/UNITY.thy
--- 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}"
diff -r 971aedd340e4 -r b797cfa3548d src/HOL/UNITY/WFair.ML
--- 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")]