A document for UNITY
authorpaulson
Fri Aug 15 13:07:01 2003 +0200 (2003-08-15)
changeset 141509a23e4eb5eb3
parent 14149 fac076f0c71c
child 14151 b8bb6a6a2c46
A document for UNITY
src/HOL/IsaMakefile
src/HOL/UNITY/Comp/PriorityAux.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
src/HOL/UNITY/document/root.tex
     1.1 --- a/src/HOL/IsaMakefile	Wed Aug 13 17:44:42 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Aug 15 13:07:01 2003 +0200
     1.3 @@ -369,7 +369,8 @@
     1.4    Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
     1.5    Auth/Guard/NS_Public.thy Auth/Guard/OtwayRees.thy \
     1.6    Auth/Guard/P1.thy Auth/Guard/P2.thy \
     1.7 -  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy
     1.8 +  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy\
     1.9 +  Auth/document/root.tex 
    1.10  	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
    1.11  
    1.12  
    1.13 @@ -394,8 +395,9 @@
    1.14    UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
    1.15    UNITY/Comp/PriorityAux.thy \
    1.16    UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
    1.17 -  UNITY/Comp/TimerArray.thy
    1.18 -	@$(ISATOOL) usedir $(OUT)/HOL UNITY
    1.19 +  UNITY/Comp/TimerArray.thy\
    1.20 +  UNITY/document/root.tex 
    1.21 +	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
    1.22  
    1.23  
    1.24  ## HOL-Unix
     2.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Wed Aug 13 17:44:42 2003 +0200
     2.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Fri Aug 15 13:07:01 2003 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4          above_def [simp] reach_def [simp] 
     2.5          reverse_def [simp] neighbors_def [simp]
     2.6  
     2.7 -text{*All vertex sets are finite \<dots>*}
     2.8 +text{*All vertex sets are finite*}
     2.9  declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]
    2.10  
    2.11  text{* and relatons over vertex are finite too *}
     3.1 --- a/src/HOL/UNITY/PPROD.thy	Wed Aug 13 17:44:42 2003 +0200
     3.2 +++ b/src/HOL/UNITY/PPROD.thy	Fri Aug 15 13:07:01 2003 +0200
     3.3 @@ -119,10 +119,11 @@
     3.4  
     3.5  (*** guarantees properties ***)
     3.6  
     3.7 -text{*This rule looks unsatisfactory because it refers to "lift".  One must use
     3.8 -  lift_guarantees_eq_lift_inv to rewrite the first subgoal and
     3.9 -  something like lift_preserves_sub to rewrite the third.  However there's
    3.10 -  no obvious way to alternative for the third premise.*}
    3.11 +text{*This rule looks unsatisfactory because it refers to @{term lift}. 
    3.12 +  One must use
    3.13 +  @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
    3.14 +  something like @{text lift_preserves_sub} to rewrite the third.  However
    3.15 +  there's no obvious alternative for the third premise.*}
    3.16  lemma guarantees_PLam_I:
    3.17      "[| lift i (F i): X guarantees Y;  i \<in> I;
    3.18          OK I (%i. lift i (F i)) |]
     4.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Aug 13 17:44:42 2003 +0200
     4.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Fri Aug 15 13:07:01 2003 +0200
     4.3 @@ -155,7 +155,7 @@
     4.4  
     4.5  lemma closedD:
     4.6     "[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] 
     4.7 -    ==> T \<inter> (B \<union> wp act M) \<in> L"
     4.8 +    ==> T \<inter> (B \<union> wp act M) \<in> L" 
     4.9  by (simp add: closed_def) 
    4.10  
    4.11  text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
    4.12 @@ -600,6 +600,7 @@
    4.13  
    4.14  
    4.15  subsection {*Monotonicity*}
    4.16 +text{*From Meier's thesis, section 4.5.7, page 110*}
    4.17  (*to be continued?*)
    4.18  
    4.19  end
     5.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Wed Aug 13 17:44:42 2003 +0200
     5.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Fri Aug 15 13:07:01 2003 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4  
     5.5  declare asgt_def [THEN def_act_simp,simp]
     5.6  
     5.7 -(*All vertex sets are finite*)
     5.8 +text{*All vertex sets are finite*}
     5.9  declare finite_subset [OF subset_UNIV finite_graph, iff]
    5.10  
    5.11  declare reach_invariant_def [THEN def_set_simp, simp]
     6.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Aug 13 17:44:42 2003 +0200
     6.2 +++ b/src/HOL/UNITY/SubstAx.thy	Fri Aug 15 13:07:01 2003 +0200
     6.3 @@ -182,7 +182,7 @@
     6.4  apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
     6.5  done
     6.6  
     6.7 -text{*Set difference: maybe combine with leadsTo_weaken_L??
     6.8 +text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
     6.9    This is the most useful form of the "disjunction" rule*}
    6.10  lemma LeadsTo_Diff:
    6.11       "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
     7.1 --- a/src/HOL/UNITY/UNITY.thy	Wed Aug 13 17:44:42 2003 +0200
     7.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Aug 15 13:07:01 2003 +0200
     7.3 @@ -283,7 +283,7 @@
     7.4  lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
     7.5  by (simp add: invariant_def)
     7.6  
     7.7 -text{*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*}
     7.8 +text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
     7.9  lemma invariant_Int:
    7.10       "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
    7.11  by (auto simp add: invariant_def stable_Int)
     8.1 --- a/src/HOL/UNITY/Union.thy	Wed Aug 13 17:44:42 2003 +0200
     8.2 +++ b/src/HOL/UNITY/Union.thy	Fri Aug 15 13:07:01 2003 +0200
     8.3 @@ -156,7 +156,7 @@
     8.4  lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
     8.5  
     8.6  
     8.7 -subsection{*\<Squnion>laws*}
     8.8 +subsection{*Laws Governing @{text "\<Squnion>"}*}
     8.9  
    8.10  (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
    8.11  lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
     9.1 --- a/src/HOL/UNITY/WFair.thy	Wed Aug 13 17:44:42 2003 +0200
     9.2 +++ b/src/HOL/UNITY/WFair.thy	Fri Aug 15 13:07:01 2003 +0200
     9.3 @@ -310,7 +310,7 @@
     9.4  by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
     9.5  
     9.6  
     9.7 -(*Set difference: maybe combine with leadsTo_weaken_L?*)
     9.8 +text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
     9.9  lemma leadsTo_Diff:
    9.10       "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
    9.11  by (blast intro: leadsTo_Un leadsTo_weaken)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/UNITY/document/root.tex	Fri Aug 15 13:07:01 2003 +0200
    10.3 @@ -0,0 +1,27 @@
    10.4 +\documentclass[10pt,a4paper,twoside]{article}
    10.5 +\usepackage{graphicx}
    10.6 +\usepackage{latexsym,theorem}
    10.7 +\usepackage{isabelle,isabellesym}
    10.8 +\usepackage{pdfsetup}\urlstyle{rm}
    10.9 +
   10.10 +\begin{document}
   10.11 +
   10.12 +\pagestyle{headings}
   10.13 +\pagenumbering{arabic}
   10.14 +
   10.15 +\title{The UNITY Formalism}
   10.16 +\author{Sidi Ehmety and Lawrence C. Paulson}
   10.17 +\maketitle
   10.18 +
   10.19 +\tableofcontents
   10.20 +
   10.21 +\begin{center}
   10.22 +  \includegraphics[scale=0.5]{session_graph}  
   10.23 +\end{center}
   10.24 +
   10.25 +\newpage
   10.26 +
   10.27 +\parindent 0pt\parskip 0.5ex
   10.28 +
   10.29 +\input{session}
   10.30 +\end{document}