# HG changeset patch
# User wenzelm
# Date 1315685515 -7200
# Node ID fbfdc5ac86be20a51052a296bdf5d68f49105d29
# Parent  0d23a8ae14df28e92b768fb73058486e489fe5cf
misc tuning and clarification;

diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -275,9 +275,6 @@
                   (plam x: lessThan Nclients. rename client_map Client))"
 **)
 
-(*Perhaps equalities.ML shouldn't add this in the first place!*)
-declare image_Collect [simp del]
-
 declare subset_preserves_o [THEN [2] rev_subsetD, intro]
 declare subset_preserves_o [THEN [2] rev_subsetD, simp]
 declare funPair_o_distrib [simp]
@@ -332,7 +329,7 @@
 ML {*
 fun record_auto_tac ctxt =
   let val ctxt' =
-    (ctxt addIs [ext])
+    ctxt
     |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
     |> map_simpset (fn ss => ss addsimps
        [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -5,7 +5,7 @@
 
 header{*Implementation of a multiple-client allocator from a single-client allocator*}
 
-theory AllocImpl imports AllocBase Follows PPROD begin
+theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
 
 
 (** State definitions.  OUTPUT variables are locals **)
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Guar.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -309,8 +309,7 @@
       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
 apply (unfold guar_def, clarify)
 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
-apply (auto intro: OK_imp_ok 
-            simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
+apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
 done
 
 
@@ -431,9 +430,9 @@
 lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
 apply (unfold ex_prop_def, safe)
  apply (drule_tac x = "G\<squnion>Ga" in spec)
- apply (force simp add: ok_Join_iff1 Join_assoc)
+ apply (force simp add: Join_assoc)
 apply (drule_tac x = "F\<squnion>Ga" in spec)
-apply (simp add: ok_Join_iff1 ok_commute  Join_ac) 
+apply (simp add: ok_commute  Join_ac) 
 done
 
 text{* Equivalence with the other definition of wx *}
@@ -466,7 +465,7 @@
 apply (rule guaranteesI)
 apply (simp add: Join_commute)
 apply (rule stable_Join_Always1)
- apply (simp_all add: invariant_def Join_stable)
+ apply (simp_all add: invariant_def)
 done
 
 lemma constrains_guarantees_leadsTo:
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Channel.thy
--- a/src/HOL/UNITY/Simple/Channel.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Channel.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -17,9 +17,9 @@
 definition minSet :: "nat set => nat option" where
     "minSet A == if A={} then None else Some (LEAST x. x \<in> A)"
 
-axioms
+axiomatization where
 
-  UC1:  "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
+  UC1:  "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" and
 
   (*  UC1  "F \<in> {s. minSet s = x} co {s. x \<subseteq> minSet s}"  *)
 
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -17,11 +17,11 @@
   ftime :: "nat=>nat"
   gtime :: "nat=>nat"
 
-axioms
-  fmono: "m \<le> n ==> ftime m \<le> ftime n"
-  gmono: "m \<le> n ==> gtime m \<le> gtime n"
+axiomatization where
+  fmono: "m \<le> n ==> ftime m \<le> ftime n" and
+  gmono: "m \<le> n ==> gtime m \<le> gtime n" and
 
-  fasc:  "m \<le> ftime n"
+  fasc:  "m \<le> ftime n" and
   gasc:  "m \<le> gtime n"
 
 definition common :: "nat set" where
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Deadlock.thy
--- a/src/HOL/UNITY/Simple/Deadlock.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Deadlock.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -6,11 +6,11 @@
     Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-theory Deadlock imports UNITY begin
+theory Deadlock imports "../UNITY" begin
 
 (*Trivial, two-process case*)
 lemma "[| F \<in> (A \<inter> B) co A;  F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)"
-by (unfold constrains_def stable_def, blast)
+  unfolding constrains_def stable_def by blast
 
 
 (*a simplification step*)
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -7,7 +7,6 @@
 
 theory Lift
 imports "../UNITY_Main"
-
 begin
 
 record state =
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Network.thy
--- a/src/HOL/UNITY/Simple/Network.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -7,7 +7,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), section 5.7.
 *)
 
-theory Network imports UNITY begin
+theory Network imports "../UNITY" begin
 
 (*The state assigns a number to each process variable*)
 
diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -34,7 +34,7 @@
 
 
 text{**We assume that the set of vertices is finite*}
-axioms 
+axiomatization where
   finite_graph:  "finite (UNIV :: vertex set)"