--- a/src/HOL/Statespace/DistinctTreeProver.thy Sun Nov 06 16:22:26 2011 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Sun Nov 06 16:29:22 2011 +0100
@@ -57,14 +57,14 @@
lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
by simp
-lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"
+lemma distinct_left: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of l \<Longrightarrow> x \<noteq> y"
by auto
-lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"
+lemma distinct_right: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
by auto
-lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk>
- \<Longrightarrow> x\<noteq>y"
+lemma distinct_left_right:
+ "all_distinct (Node l z b r) \<Longrightarrow> x \<in> set_of l \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
by auto
lemma in_set_root: "x \<in> set_of (Node l x False r)"
@@ -86,17 +86,17 @@
text {* When deriving a state space from other ones, we create a new
name tree which contains all the names of the parent state spaces and
-assumme the predicate @{const all_distinct}. We then prove that the new locale
-interprets all parent locales. Hence we have to show that the new
-distinctness assumption on all names implies the distinctness
+assume the predicate @{const all_distinct}. We then prove that the new
+locale interprets all parent locales. Hence we have to show that the
+new distinctness assumption on all names implies the distinctness
assumptions of the parent locales. This proof is implemented in ML. We
do this efficiently by defining a kind of containment check of trees
-by 'subtraction'. We subtract the parent tree from the new tree. If this
-succeeds we know that @{const all_distinct} of the new tree implies
-@{const all_distinct} of the parent tree. The resulting certificate is
-of the order @{term "n * log(m)"} where @{term "n"} is the size of the
-(smaller) parent tree and @{term "m"} the size of the (bigger) new tree.
-*}
+by ``subtraction''. We subtract the parent tree from the new tree. If
+this succeeds we know that @{const all_distinct} of the new tree
+implies @{const all_distinct} of the parent tree. The resulting
+certificate is of the order @{term "n * log(m)"} where @{term "n"} is
+the size of the (smaller) parent tree and @{term "m"} the size of the
+(bigger) new tree. *}
primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
@@ -108,14 +108,14 @@
Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
| None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
| None \<Rightarrow>
- (case (delete x r) of
+ (case delete x r of
Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
| None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
else None))"
-lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
-proof (induct t)
+lemma delete_Some_set_of: "delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
+proof (induct t arbitrary: t')
case Tip thus ?case by simp
next
case (Node l y d r)
@@ -164,8 +164,8 @@
qed
lemma delete_Some_all_distinct:
- "\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
-proof (induct t)
+ "delete x t = Some t' \<Longrightarrow> all_distinct t \<Longrightarrow> all_distinct t'"
+proof (induct t arbitrary: t')
case Tip thus ?case by simp
next
case (Node l y d r)
@@ -237,8 +237,8 @@
qed
lemma delete_Some_x_set_of:
- "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
-proof (induct t)
+ "delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
+proof (induct t arbitrary: t')
case Tip thus ?case by simp
next
case (Node l y d r)
@@ -304,8 +304,8 @@
| None \<Rightarrow> None)"
lemma subtract_Some_set_of_res:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
+proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
case Tip thus ?case by simp
next
case (Node l x b r)
@@ -349,8 +349,8 @@
qed
lemma subtract_Some_set_of:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"
+proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
case Tip thus ?case by simp
next
case (Node l x d r)
@@ -399,8 +399,8 @@
qed
lemma subtract_Some_all_distinct_res:
- "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t"
+proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
case Tip thus ?case by simp
next
case (Node l x d r)
@@ -447,8 +447,8 @@
lemma subtract_Some_dist_res:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"
+proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
case Tip thus ?case by simp
next
case (Node l x d r)
@@ -501,8 +501,8 @@
qed
lemma subtract_Some_all_distinct:
- "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t\<^isub>1"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t\<^isub>1"
+proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
case Tip thus ?case by simp
next
case (Node l x d r)
--- a/src/HOL/Statespace/StateFun.thy Sun Nov 06 16:22:26 2011 +0100
+++ b/src/HOL/Statespace/StateFun.thy Sun Nov 06 16:29:22 2011 +0100
@@ -58,8 +58,7 @@
lemma id_id_cancel: "id (id x) = x"
by (simp add: id_def)
-lemma destr_contstr_comp_id:
-"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
+lemma destr_contstr_comp_id: "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
by (rule ext) simp
@@ -67,16 +66,16 @@
lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
by simp
-lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
+lemma conj1_False: "P \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
by simp
-lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
+lemma conj2_False: "Q \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
by simp
-lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
+lemma conj_True: "P \<equiv> True \<Longrightarrow> Q \<equiv> True \<Longrightarrow> (P \<and> Q) \<equiv> True"
by simp
-lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
+lemma conj_cong: "P \<equiv> P' \<Longrightarrow> Q \<equiv> Q' \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
by simp
--- a/src/HOL/Statespace/StateSpaceEx.thy Sun Nov 06 16:22:26 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Sun Nov 06 16:29:22 2011 +0100
@@ -12,12 +12,9 @@
"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
(*>*)
-text {* Did you ever dream about records with multiple inheritance.
+text {* Did you ever dream about records with multiple inheritance?
Then you should definitely have a look at statespaces. They may be
-what you are dreaming of. Or at least almost...
-*}
-
-
+what you are dreaming of. Or at least almost \dots *}
text {* Isabelle allows to add new top-level commands to the
@@ -169,12 +166,12 @@
proof -
thm foo1
txt {* The Lemma @{thm [source] foo1} from the parent state space
- is also available here: \begin{center}@{thm foo1}\end{center}.*}
+ is also available here: \begin{center}@{thm foo1}\end{center} *}
have "s<a:=i>\<cdot>a = i"
by (rule foo1)
thm bar1
txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}:
- \begin{center}@{thm bar1}\end{center}.*}
+ \begin{center}@{thm bar1}\end{center} *}
have "s<B:=True>\<cdot>C = s\<cdot>C"
by (rule bar1)
show ?thesis
@@ -198,9 +195,9 @@
by simp
-text {* Hmm, I hoped this would work now...*}
+(*
+text "Hmm, I hoped this would work now..."
-(*
locale fooX = foo +
assumes "s<a:=i>\<cdot>b = k"
*)
--- a/src/HOL/Statespace/StateSpaceLocale.thy Sun Nov 06 16:22:26 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Sun Nov 06 16:29:22 2011 +0100
@@ -19,21 +19,20 @@
fixes project :: "'value \<Rightarrow> 'a"
and inject :: "'a \<Rightarrow> 'value"
assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
+begin
-lemma (in project_inject)
- ex_project [statefun_simp]: "\<exists>v. project v = x"
- apply (rule_tac x= "inject x" in exI)
- apply (simp add: project_inject_cancel)
- done
+lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
+proof
+ show "project (inject x) = x"
+ by (rule project_inject_cancel)
+qed
-lemma (in project_inject)
- project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
+lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
by (rule ext) (simp add: project_inject_cancel)
-lemma (in project_inject)
- project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
+lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
by (rule ext) (simp add: project_inject_cancel)
-
+end
end
\ No newline at end of file
--- a/src/HOL/Statespace/document/root.tex Sun Nov 06 16:22:26 2011 +0100
+++ b/src/HOL/Statespace/document/root.tex Sun Nov 06 16:29:22 2011 +0100
@@ -20,26 +20,34 @@
\section{Introduction}
-These theories introduce a new command called \isacommand{statespace}.
-It's usage is similar to \isacommand{record}s. However, the command does not introduce a new type but an
-abstract specification based on the locale infrastructure. This leads
-to extra flexibility in composing state space components, in particular
-multiple inheritance and renaming of components.
+These theories introduce a new command called \isacommand{statespace}.
+It's usage is similar to \isacommand{record}s. However, the command
+does not introduce a new type but an abstract specification based on
+the locale infrastructure. This leads to extra flexibility in
+composing state space components, in particular multiple inheritance
+and renaming of components.
The state space infrastructure basically manages the following things:
\begin{itemize}
\item distinctness of field names
\item projections~/ injections from~/ to an abstract \emph{value} type
-\item syntax translations for lookup and update, hiding the projections and injections
-\item simplification procedure for lookups~/ updates, similar to records
+\item syntax translations for lookup and update, hiding the
+ projections and injections
+\item simplification procedure for lookups~/ updates, similar to
+ records
\end{itemize}
\paragraph{Overview}
-In Section \ref{sec:DistinctTreeProver} we define distinctness of the nodes in a binary tree and provide the basic prover tools to support efficient distinctness reasoning for field names managed by
-state spaces. The state is represented as a function from (abstract) names to (abstract) values as
-introduced in Section \ref{sec:StateFun}. The basic setup for state spaces is in Section
-\ref{sec:StateSpaceLocale}. Some syntax for lookup and updates is added in Section \ref{sec:StateSpaceSyntax}. Finally Section \ref{sec:Examples} explains the usage of state spaces by examples.
+In Section \ref{sec:DistinctTreeProver} we define distinctness of the
+nodes in a binary tree and provide the basic prover tools to support
+efficient distinctness reasoning for field names managed by state
+spaces. The state is represented as a function from (abstract) names
+to (abstract) values as introduced in Section \ref{sec:StateFun}. The
+basic setup for state spaces is in Section
+\ref{sec:StateSpaceLocale}. Some syntax for lookup and updates is
+added in Section \ref{sec:StateSpaceSyntax}. Finally Section
+\ref{sec:Examples} explains the usage of state spaces by examples.
% generated text of all theories