--- a/src/HOL/CTL/CTL.thy Thu Apr 28 12:04:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,310 +0,0 @@
-
-theory CTL = Main:
-
-section {* CTL formulae *}
-
-text {*
- We formalize basic concepts of Computational Tree Logic (CTL)
- \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
- simply-typed set theory of HOL.
-
- By using the common technique of ``shallow embedding'', a CTL
- formula is identified with the corresponding set of states where it
- holds. Consequently, CTL operations such as negation, conjunction,
- disjunction simply become complement, intersection, union of sets.
- We only require a separate operation for implication, as point-wise
- inclusion is usually not encountered in plain set-theory.
-*}
-
-lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
-
-types 'a ctl = "'a set"
-constdefs
- imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
- "p \<rightarrow> q \<equiv> - p \<union> q"
-
-lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
-lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
-
-
-text {*
- \smallskip The CTL path operators are more interesting; they are
- based on an arbitrary, but fixed model @{text \<M>}, which is simply
- a transition relation over states @{typ "'a"}.
-*}
-
-consts model :: "('a \<times> 'a) set" ("\<M>")
-
-text {*
- The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
- as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
- defined as derived ones. The formula @{text "\<EX> p"} holds in a
- state @{term s}, iff there is a successor state @{term s'} (with
- respect to the model @{term \<M>}), such that @{term p} holds in
- @{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
- s}, iff there is a path in @{text \<M>}, starting from @{term s},
- such that there exists a state @{term s'} on the path, such that
- @{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
- in a state @{term s}, iff there is a path, starting from @{term s},
- such that for all states @{term s'} on the path, @{term p} holds in
- @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
- "\<EG> p"} may be expressed using least and greatest fixed points
- \cite{McMillan-PhDThesis}.
-*}
-
-constdefs
- EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
- EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
- EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
-
-text {*
- @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
- dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
- "\<EG>"}.
-*}
-
-constdefs
- AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
- AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
- AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
-
-lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
-
-
-section {* Basic fixed point properties *}
-
-text {*
- First of all, we use the de-Morgan property of fixed points
-*}
-
-lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
-proof
- show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
- proof
- fix x assume l: "x \<in> lfp f"
- show "x \<in> - gfp (\<lambda>s. - f (- s))"
- proof
- assume "x \<in> gfp (\<lambda>s. - f (- s))"
- then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
- then have "f (- u) \<subseteq> - u" by auto
- then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
- from l and this have "x \<notin> u" by auto
- then show False by contradiction
- qed
- qed
- show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
- proof (rule lfp_greatest)
- fix u assume "f u \<subseteq> u"
- then have "- u \<subseteq> - f u" by auto
- then have "- u \<subseteq> - f (- (- u))" by simp
- then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
- then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
- qed
-qed
-
-lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
- by (simp add: lfp_gfp)
-
-lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
- by (simp add: lfp_gfp)
-
-text {*
- in order to give dual fixed point representations of @{term "AF p"}
- and @{term "AG p"}:
-*}
-
-lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
-lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
-
-lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
-proof -
- have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
- then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
-qed
-
-lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
-proof -
- have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
- then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
-qed
-
-lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
-proof -
- have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
- then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
-qed
-
-text {*
- From the greatest fixed point definition of @{term "\<AG> p"}, we
- derive as a consequence of the Knaster-Tarski theorem on the one
- hand that @{term "\<AG> p"} is a fixed point of the monotonic
- function @{term "\<lambda>s. p \<inter> \<AX> s"}.
-*}
-
-lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
-proof -
- have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
- then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
-qed
-
-text {*
- This fact may be split up into two inequalities (merely using
- transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
- @{text "\<le>"} in Isabelle/HOL).
-*}
-
-lemma AG_fp_1: "\<AG> p \<subseteq> p"
-proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
- finally show ?thesis .
-qed
-
-text {**}
-
-lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
-proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
- finally show ?thesis .
-qed
-
-text {*
- On the other hand, we have from the Knaster-Tarski fixed point
- theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
- smaller than @{term "AG p"}. A post-fixed point is a set of states
- @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the
- following co-induction principle for @{term "AG p"}.
-*}
-
-lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
- by (simp only: AG_gfp) (rule gfp_upperbound)
-
-
-section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
-
-text {*
- With the most basic facts available, we are now able to establish a
- few more interesting results, leading to the \emph{tree induction}
- principle for @{text AG} (see below). We will use some elementary
- monotonicity and distributivity rules.
-*}
-
-lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
-lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
-lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
- by (simp only: AG_gfp, rule gfp_mono) auto
-
-text {*
- The formula @{term "AG p"} implies @{term "AX p"} (we use
- substitution of @{text "\<subseteq>"} with monotonicity).
-*}
-
-lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
-proof -
- have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
- also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
- finally show ?thesis .
-qed
-
-text {*
- Furthermore we show idempotency of the @{text "\<AG>"} operator.
- The proof is a good example of how accumulated facts may get
- used to feed a single rule step.
-*}
-
-lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
-proof
- show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
-next
- show "\<AG> p \<subseteq> \<AG> \<AG> p"
- proof (rule AG_I)
- have "\<AG> p \<subseteq> \<AG> p" ..
- moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
- ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
- qed
-qed
-
-text {*
- \smallskip We now give an alternative characterization of the @{text
- "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
- an ``operational'' way by tree induction: In a state holds @{term
- "AG p"} iff in that state holds @{term p}, and in all reachable
- states @{term s} follows from the fact that @{term p} holds in
- @{term s}, that @{term p} also holds in all successor states of
- @{term s}. We use the co-induction principle @{thm [source] AG_I}
- to establish this in a purely algebraic manner.
-*}
-
-theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
-proof
- show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
- proof (rule AG_I)
- show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
- proof
- show "?lhs \<subseteq> p" ..
- show "?lhs \<subseteq> \<AX> ?lhs"
- proof -
- {
- have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
- also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
- finally have "?lhs \<subseteq> \<AX> p" by auto
- }
- moreover
- {
- have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
- also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
- finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
- }
- ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
- also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
- finally show ?thesis .
- qed
- qed
- qed
-next
- show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
- proof
- show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
- show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
- proof -
- have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
- also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
- also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
- finally show ?thesis .
- qed
- qed
-qed
-
-
-section {* An application of tree induction \label{sec:calc-ctl-commute} *}
-
-text {*
- Further interesting properties of CTL expressions may be
- demonstrated with the help of tree induction; here we show that
- @{text \<AX>} and @{text \<AG>} commute.
-*}
-
-theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
-proof -
- have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
- also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
- also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
- proof
- have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
- also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
- also note Int_mono AG_mono
- ultimately show "?lhs \<subseteq> \<AG> p" by fast
- next
- have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
- moreover
- {
- have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
- also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
- also note AG_mono
- ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
- }
- ultimately show "\<AG> p \<subseteq> ?lhs" ..
- qed
- finally show ?thesis .
-qed
-
-end
--- a/src/HOL/CTL/ROOT.ML Thu Apr 28 12:04:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-
-use_thy "CTL";
-
--- a/src/HOL/CTL/document/root.bib Thu Apr 28 12:04:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-
-@Misc{McMillan-LectureNotes,
- author = {Ken McMillan},
- title = {Lecture notes on verification of digital and hybrid systems},
- note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
-}
-
-@PhdThesis{McMillan-PhDThesis,
- author = {Ken McMillan},
- title = {Symbolic Model Checking: an approach to the state explosion problem},
- school = {Carnegie Mellon University},
- year = 1992
-}
--- a/src/HOL/CTL/document/root.tex Thu Apr 28 12:04:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
-\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
-\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
-\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
-\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
-\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
-
-
-\begin{document}
-
-\title{Some properties of CTL}
-\author{Gertrud Bauer}
-\maketitle
-
-\tableofcontents
-\bigskip
-
-\parindent 0pt\parskip 0.5ex
-
-\input{session}
-
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
--- a/src/HOL/IsaMakefile Thu Apr 28 12:04:34 2005 +0200
+++ b/src/HOL/IsaMakefile Thu Apr 28 17:08:08 2005 +0200
@@ -16,7 +16,6 @@
HOL-Bali \
HOL-Complex-ex \
HOL-Complex-Import \
- HOL-CTL \
HOL-Extraction \
HOL-Complex-HahnBanach \
HOL-Hoare \
@@ -534,15 +533,6 @@
@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
-## HOL-CTL
-
-HOL-CTL: HOL $(LOG)/HOL-CTL.gz
-
-$(LOG)/HOL-CTL.gz: $(OUT)/HOL \
- CTL/CTL.thy CTL/ROOT.ML CTL/document/root.tex CTL/document/root.bib
- @$(ISATOOL) usedir $(OUT)/HOL CTL
-
-
## HOL-Extraction
HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
@@ -701,7 +691,7 @@
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
- $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
+ $(LOG)/HOL-Bali.gz \
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
$(LOG)/HOL-Lattice \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CTL.thy Thu Apr 28 17:08:08 2005 +0200
@@ -0,0 +1,317 @@
+
+(* Title: HOL/ex/CTL.thy
+ ID: $Id$
+ Author: Gertrud Bauer
+*)
+
+header {* CTL formulae *}
+
+theory CTL = Main:
+
+
+
+text {*
+ We formalize basic concepts of Computational Tree Logic (CTL)
+ \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
+ simply-typed set theory of HOL.
+
+ By using the common technique of ``shallow embedding'', a CTL
+ formula is identified with the corresponding set of states where it
+ holds. Consequently, CTL operations such as negation, conjunction,
+ disjunction simply become complement, intersection, union of sets.
+ We only require a separate operation for implication, as point-wise
+ inclusion is usually not encountered in plain set-theory.
+*}
+
+lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
+
+types 'a ctl = "'a set"
+constdefs
+ imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
+ "p \<rightarrow> q \<equiv> - p \<union> q"
+
+lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
+lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
+
+
+text {*
+ \smallskip The CTL path operators are more interesting; they are
+ based on an arbitrary, but fixed model @{text \<M>}, which is simply
+ a transition relation over states @{typ "'a"}.
+*}
+
+consts model :: "('a \<times> 'a) set" ("\<M>")
+
+text {*
+ The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
+ as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
+ defined as derived ones. The formula @{text "\<EX> p"} holds in a
+ state @{term s}, iff there is a successor state @{term s'} (with
+ respect to the model @{term \<M>}), such that @{term p} holds in
+ @{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
+ s}, iff there is a path in @{text \<M>}, starting from @{term s},
+ such that there exists a state @{term s'} on the path, such that
+ @{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
+ in a state @{term s}, iff there is a path, starting from @{term s},
+ such that for all states @{term s'} on the path, @{term p} holds in
+ @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
+ "\<EG> p"} may be expressed using least and greatest fixed points
+ \cite{McMillan-PhDThesis}.
+*}
+
+constdefs
+ EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
+ EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
+ EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
+
+text {*
+ @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
+ dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
+ "\<EG>"}.
+*}
+
+constdefs
+ AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
+ AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
+ AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
+
+lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
+
+
+section {* Basic fixed point properties *}
+
+text {*
+ First of all, we use the de-Morgan property of fixed points
+*}
+
+lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
+proof
+ show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
+ proof
+ fix x assume l: "x \<in> lfp f"
+ show "x \<in> - gfp (\<lambda>s. - f (- s))"
+ proof
+ assume "x \<in> gfp (\<lambda>s. - f (- s))"
+ then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
+ then have "f (- u) \<subseteq> - u" by auto
+ then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
+ from l and this have "x \<notin> u" by auto
+ then show False by contradiction
+ qed
+ qed
+ show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
+ proof (rule lfp_greatest)
+ fix u assume "f u \<subseteq> u"
+ then have "- u \<subseteq> - f u" by auto
+ then have "- u \<subseteq> - f (- (- u))" by simp
+ then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
+ then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
+ qed
+qed
+
+lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
+ by (simp add: lfp_gfp)
+
+lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
+ by (simp add: lfp_gfp)
+
+text {*
+ in order to give dual fixed point representations of @{term "AF p"}
+ and @{term "AG p"}:
+*}
+
+lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
+lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
+
+lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
+proof -
+ have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
+ then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
+qed
+
+lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
+proof -
+ have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+ then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
+qed
+
+lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
+proof -
+ have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
+ then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
+qed
+
+text {*
+ From the greatest fixed point definition of @{term "\<AG> p"}, we
+ derive as a consequence of the Knaster-Tarski theorem on the one
+ hand that @{term "\<AG> p"} is a fixed point of the monotonic
+ function @{term "\<lambda>s. p \<inter> \<AX> s"}.
+*}
+
+lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
+proof -
+ have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+ then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
+qed
+
+text {*
+ This fact may be split up into two inequalities (merely using
+ transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
+ @{text "\<le>"} in Isabelle/HOL).
+*}
+
+lemma AG_fp_1: "\<AG> p \<subseteq> p"
+proof -
+ note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
+ finally show ?thesis .
+qed
+
+text {**}
+
+lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
+proof -
+ note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
+ finally show ?thesis .
+qed
+
+text {*
+ On the other hand, we have from the Knaster-Tarski fixed point
+ theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
+ smaller than @{term "AG p"}. A post-fixed point is a set of states
+ @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the
+ following co-induction principle for @{term "AG p"}.
+*}
+
+lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
+ by (simp only: AG_gfp) (rule gfp_upperbound)
+
+
+section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
+
+text {*
+ With the most basic facts available, we are now able to establish a
+ few more interesting results, leading to the \emph{tree induction}
+ principle for @{text AG} (see below). We will use some elementary
+ monotonicity and distributivity rules.
+*}
+
+lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
+lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
+ by (simp only: AG_gfp, rule gfp_mono) auto
+
+text {*
+ The formula @{term "AG p"} implies @{term "AX p"} (we use
+ substitution of @{text "\<subseteq>"} with monotonicity).
+*}
+
+lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
+proof -
+ have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
+ also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
+ finally show ?thesis .
+qed
+
+text {*
+ Furthermore we show idempotency of the @{text "\<AG>"} operator.
+ The proof is a good example of how accumulated facts may get
+ used to feed a single rule step.
+*}
+
+lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
+proof
+ show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
+next
+ show "\<AG> p \<subseteq> \<AG> \<AG> p"
+ proof (rule AG_I)
+ have "\<AG> p \<subseteq> \<AG> p" ..
+ moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
+ ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
+ qed
+qed
+
+text {*
+ \smallskip We now give an alternative characterization of the @{text
+ "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
+ an ``operational'' way by tree induction: In a state holds @{term
+ "AG p"} iff in that state holds @{term p}, and in all reachable
+ states @{term s} follows from the fact that @{term p} holds in
+ @{term s}, that @{term p} also holds in all successor states of
+ @{term s}. We use the co-induction principle @{thm [source] AG_I}
+ to establish this in a purely algebraic manner.
+*}
+
+theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
+proof
+ show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
+ proof (rule AG_I)
+ show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
+ proof
+ show "?lhs \<subseteq> p" ..
+ show "?lhs \<subseteq> \<AX> ?lhs"
+ proof -
+ {
+ have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
+ also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
+ finally have "?lhs \<subseteq> \<AX> p" by auto
+ }
+ moreover
+ {
+ have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
+ also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
+ finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
+ }
+ ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
+ also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
+ finally show ?thesis .
+ qed
+ qed
+ qed
+next
+ show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
+ proof
+ show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
+ show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
+ proof -
+ have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
+ also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
+ also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
+ finally show ?thesis .
+ qed
+ qed
+qed
+
+
+section {* An application of tree induction \label{sec:calc-ctl-commute} *}
+
+text {*
+ Further interesting properties of CTL expressions may be
+ demonstrated with the help of tree induction; here we show that
+ @{text \<AX>} and @{text \<AG>} commute.
+*}
+
+theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
+proof -
+ have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
+ also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
+ also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
+ proof
+ have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
+ also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
+ also note Int_mono AG_mono
+ ultimately show "?lhs \<subseteq> \<AG> p" by fast
+ next
+ have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
+ moreover
+ {
+ have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
+ also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
+ also note AG_mono
+ ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
+ }
+ ultimately show "\<AG> p \<subseteq> ?lhs" ..
+ qed
+ finally show ?thesis .
+qed
+
+end
--- a/src/HOL/ex/ROOT.ML Thu Apr 28 12:04:34 2005 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Apr 28 17:08:08 2005 +0200
@@ -22,6 +22,7 @@
time_use_thy "NatSum";
time_use_thy "Intuitionistic";
time_use_thy "Classical";
+time_use_thy "CTL";
time_use_thy "mesontest2";
time_use_thy "PresburgerEx";
time_use_thy "BT";
@@ -30,6 +31,7 @@
time_use_thy "MergeSort";
time_use_thy "Puzzle";
+
time_use_thy "Lagrange";
time_use_thy "set";
--- a/src/HOL/ex/document/root.bib Thu Apr 28 12:04:34 2005 +0200
+++ b/src/HOL/ex/document/root.bib Thu Apr 28 17:08:08 2005 +0200
@@ -1,3 +1,5 @@
+
+
@TechReport{Gordon:1985:HOL,
author = {M. J. C. Gordon},
@@ -105,3 +107,16 @@
publisher = {Springer},
year = 2002,
note = {LNCS 2283}}
+
+@Misc{McMillan-LectureNotes,
+ author = {Ken McMillan},
+ title = {Lecture notes on verification of digital and hybrid systems},
+ note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
+}
+
+@PhdThesis{McMillan-PhDThesis,
+ author = {Ken McMillan},
+ title = {Symbolic Model Checking: an approach to the state explosion problem},
+ school = {Carnegie Mellon University},
+ year = 1992
+}
\ No newline at end of file
--- a/src/HOL/ex/document/root.tex Thu Apr 28 12:04:34 2005 +0200
+++ b/src/HOL/ex/document/root.tex Thu Apr 28 17:08:08 2005 +0200
@@ -11,6 +11,15 @@
\urlstyle{rm}
\isabellestyle{it}
+\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
+\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
+\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
+\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
+\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
+\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
+
+
+
\begin{document}
\title{Miscellaneous HOL Examples}