diff -r 194c7349b6c0 -r 9469c039ff57 doc-src/TutorialI/CTL/Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/CTL/Base.thy	Mon Oct 02 14:32:33 2000 +0200
@@ -0,0 +1,50 @@
+(*<*)theory Base = Main:(*>*)
+
+section{*A verified model checker*}
+
+text{*
+Model checking is a very popular technique for the verification of finite
+state systems (implementations) w.r.t.\ temporal logic formulae
+(specifications) \cite{Clark}. Its foundations are completely set theoretic
+and this section shall develop them in HOL. This is done in two steps: first
+we consider a very simple ``temporal'' logic called propositional dynamic
+logic (PDL) which we then extend to the temporal logic CTL used in many real
+model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
+recursive function @{term mc} that maps a formula into the set of all states of
+the system where the formula is valid. If the system has a finite number of
+states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a
+very efficient one. The main proof obligation is to show that the semantics
+and the model checker agree.
+
+Our models are transition systems.
+
+START with simple example: mutex or something.
+
+Abstracting from this concrete example, we assume there is some type of
+atomic propositions
+*}
+
+typedecl atom
+
+text{*\noindent
+which we merely declare rather than define because it is an implicit parameter of our model.
+Of course it would have been more generic to make @{typ atom} a type parameter of everything
+but fixing @{typ atom} as above reduces clutter.
+
+Instead of introducing both a separate type of states and a function
+telling us which atoms are true in each state we simply identify each
+state with that set of atoms:
+*}
+
+types state = "atom set";
+
+text{*\noindent
+Finally we declare an arbitrary but fixed transition system, i.e.\ relation between states:
+*}
+
+consts M :: "(state \<times> state)set";
+
+text{*\noindent
+Again, we could have made @{term M} a parameter of everything.
+*}
+(*<*)end(*>*)