doc-src/TutorialI/Overview/LNCS/Sets.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

(*<*)theory Sets = Main:(*>*)

section{*Sets, Functions and Relations*}

subsection{*Set Notation*}

text{*
\begin{center}
\begin{tabular}{ccc}
@{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\
@{term "a \<in> A"} & @{term "b \<notin> A"} \\
@{term "{a,b}"} & @{text "{x. P x}"} \\
@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
\end{tabular}
\end{center}*}
(*<*)term "A \<union> B" term "A \<inter> B" term "A - B"
term "a \<in> A" term "b \<notin> A"
term "{a,b}" term "{x. P x}"
term "\<Union> M"  term "\<Union>a \<in> A. F a"(*>*)


subsection{*Some Functions*}

text{*
\begin{tabular}{l}
@{thm id_def}\\
@{thm o_def[no_vars]}\\
@{thm image_def[no_vars]}\\
@{thm vimage_def[no_vars]}
\end{tabular}*}
(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)


subsection{*Some Relations*}

text{*
\begin{tabular}{l}
@{thm Id_def}\\
@{thm converse_def[no_vars]}\\
@{thm Image_def[no_vars]}\\
@{thm rtrancl_refl[no_vars]}\\
@{thm rtrancl_into_rtrancl[no_vars]}
\end{tabular}*}
(*<*)thm Id_def
thm converse_def[no_vars] Image_def[no_vars]
thm relpow.simps[no_vars]
thm rtrancl.intros[no_vars](*>*)


subsection{*Wellfoundedness*}

text{*
\begin{tabular}{l}
@{thm wf_def[no_vars]}\\
@{thm wf_iff_no_infinite_down_chain[no_vars]}
\end{tabular}*}
(*<*)thm wf_def[no_vars]
thm wf_iff_no_infinite_down_chain[no_vars](*>*)


subsection{*Fixed Point Operators*}

text{*
\begin{tabular}{l}
@{thm lfp_def[no_vars]}\\
@{thm lfp_unfold[no_vars]}\\
@{thm lfp_induct[no_vars]}
\end{tabular}*}
(*<*)thm lfp_def[no_vars] gfp_def[no_vars]
thm lfp_unfold[no_vars]
thm lfp_induct[no_vars](*>*)


subsection{*Case Study: Verified Model Checking*}

typedecl state

consts M :: "(state \<times> state)set"

typedecl atom

consts L :: "state \<Rightarrow> atom set"

datatype formula = Atom atom
                 | Neg formula
                 | And formula formula
                 | AX formula
                 | EF formula

consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   ("(_ \<Turnstile> _)" [80,80] 80)

primrec
"s \<Turnstile> Atom a  = (a \<in> L s)"
"s \<Turnstile> Neg f   = (\<not>(s \<Turnstile> f))"
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"

consts mc :: "formula \<Rightarrow> state set"
primrec
"mc(Atom a)  = {s. a \<in> L s}"
"mc(Neg f)   = -mc f"
"mc(And f g) = mc f \<inter> mc g"
"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
"mc(EF f)    = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"

lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))"
apply(rule monoI)
apply blast
done

lemma EF_lemma:
  "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
apply(rule equalityI)
 thm lfp_lowerbound
 apply(rule lfp_lowerbound)
 apply(blast intro: rtrancl_trans)
apply(rule subsetI)
apply clarsimp
apply(erule converse_rtrancl_induct)
thm lfp_unfold[OF mono_ef]
 apply(subst lfp_unfold[OF mono_ef])
 apply(blast)
apply(subst lfp_unfold[OF mono_ef])
apply(blast)
done

theorem "mc f = {s. s \<Turnstile> f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma)
done

text{*Preview of coming attractions: a structured proof of the
@{thm[source]EF_lemma}.*}
lemma EF_lemma:
  "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
  (is "lfp ?F = ?R") 
proof
  show "lfp ?F \<subseteq> ?R"
  proof (rule lfp_lowerbound)
    show "?F ?R \<subseteq> ?R" by(blast intro: rtrancl_trans)
  qed
next
  show "?R \<subseteq> lfp ?F"
  proof
    fix s assume "s \<in> ?R"
    then obtain t where st: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast
    from st show "s \<in> lfp ?F"
    proof (rule converse_rtrancl_induct)
      show "t \<in> lfp ?F"
      proof (subst lfp_unfold[OF mono_ef])
	show "t \<in> ?F(lfp ?F)" using tA by blast
      qed
    next
      fix s s'
      assume ss': "(s,s') \<in> M" and s't: "(s',t) \<in> M\<^sup>*"
         and IH: "s' \<in> lfp ?F"
      show "s \<in> lfp ?F"
      proof (subst lfp_unfold[OF mono_ef])
	show "s \<in> ?F(lfp ?F)" using prems by blast
      qed
    qed
  qed
qed

text{*
\begin{exercise}
@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
(``there exists a next state such that'') with the intended semantics
@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?

Show that the semantics for @{term EF} satisfies the following recursion equation:
@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
\end{exercise}*}
(*<*)end(*>*)