--- 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},
--- 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 **)
--- 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:
--- 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}" *)
--- 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
--- 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*)
--- 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 =
--- 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*)
--- 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)"