--- 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
--- 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 *}
--- 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)) |]
--- 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
--- 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]
--- 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 |]
--- 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)
--- 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)"
--- 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)
--- /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}