# HG changeset patch
# User paulson
# Date 1060945621 -7200
# Node ID 9a23e4eb5eb335f7fc627f94fb7234601c6bcb61
# Parent  fac076f0c71cf4bcade50b7d81e1100eab4d6bd9
A document for UNITY

diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 15 13:07:01 2003 +0200
@@ -369,7 +369,8 @@
   Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
   Auth/Guard/NS_Public.thy Auth/Guard/OtwayRees.thy \
   Auth/Guard/P1.thy Auth/Guard/P2.thy \
-  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy
+  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy\
+  Auth/document/root.tex 
 	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
 
 
@@ -394,8 +395,9 @@
   UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
   UNITY/Comp/PriorityAux.thy \
   UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
-  UNITY/Comp/TimerArray.thy
-	@$(ISATOOL) usedir $(OUT)/HOL UNITY
+  UNITY/Comp/TimerArray.thy\
+  UNITY/document/root.tex 
+	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
 
 
 ## HOL-Unix
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -55,7 +55,7 @@
         above_def [simp] reach_def [simp] 
         reverse_def [simp] neighbors_def [simp]
 
-text{*All vertex sets are finite \<dots>*}
+text{*All vertex sets are finite*}
 declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]
 
 text{* and relatons over vertex are finite too *}
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/PPROD.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -119,10 +119,11 @@
 
 (*** guarantees properties ***)
 
-text{*This rule looks unsatisfactory because it refers to "lift".  One must use
-  lift_guarantees_eq_lift_inv to rewrite the first subgoal and
-  something like lift_preserves_sub to rewrite the third.  However there's
-  no obvious way to alternative for the third premise.*}
+text{*This rule looks unsatisfactory because it refers to @{term lift}. 
+  One must use
+  @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
+  something like @{text lift_preserves_sub} to rewrite the third.  However
+  there's no obvious alternative for the third premise.*}
 lemma guarantees_PLam_I:
     "[| lift i (F i): X guarantees Y;  i \<in> I;
         OK I (%i. lift i (F i)) |]
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -155,7 +155,7 @@
 
 lemma closedD:
    "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
-    ==> T \<inter> (B \<union> wp act M) \<in> L"
+    ==> T \<inter> (B \<union> wp act M) \<in> L" 
 by (simp add: closed_def) 
 
 text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
@@ -600,6 +600,7 @@
 
 
 subsection {*Monotonicity*}
+text{*From Meier's thesis, section 4.5.7, page 110*}
 (*to be continued?*)
 
 end
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -55,7 +55,7 @@
 
 declare asgt_def [THEN def_act_simp,simp]
 
-(*All vertex sets are finite*)
+text{*All vertex sets are finite*}
 declare finite_subset [OF subset_UNIV finite_graph, iff]
 
 declare reach_invariant_def [THEN def_set_simp, simp]
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -182,7 +182,7 @@
 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
 done
 
-text{*Set difference: maybe combine with leadsTo_weaken_L??
+text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
   This is the most useful form of the "disjunction" rule*}
 lemma LeadsTo_Diff:
      "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -283,7 +283,7 @@
 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
 by (simp add: invariant_def)
 
-text{*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*}
+text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
 lemma invariant_Int:
      "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
 by (auto simp add: invariant_def stable_Int)
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/Union.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -156,7 +156,7 @@
 lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
 
 
-subsection{*\<Squnion>laws*}
+subsection{*Laws Governing @{text "\<Squnion>"}*}
 
 (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
 lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/WFair.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -310,7 +310,7 @@
 by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
 
 
-(*Set difference: maybe combine with leadsTo_weaken_L?*)
+text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
 lemma leadsTo_Diff:
      "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
 by (blast intro: leadsTo_Un leadsTo_weaken)
diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/document/root.tex	Fri Aug 15 13:07:01 2003 +0200
@@ -0,0 +1,27 @@
+\documentclass[10pt,a4paper,twoside]{article}
+\usepackage{graphicx}
+\usepackage{latexsym,theorem}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\begin{document}
+
+\pagestyle{headings}
+\pagenumbering{arabic}
+
+\title{The UNITY Formalism}
+\author{Sidi Ehmety and Lawrence C. Paulson}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+  \includegraphics[scale=0.5]{session_graph}  
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+\end{document}