# HG changeset patch
# User wenzelm
# Date 1320593362 -3600
# Node ID 4849133d7a7862d45306ebb47fff5fa90decfd07
# Parent  454b06bc9601884494b726ab3d3545c4bb570cd4
tuned document;
tuned proofs;

diff -r 454b06bc9601 -r 4849133d7a78 src/HOL/Statespace/DistinctTreeProver.thy
--- 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)
diff -r 454b06bc9601 -r 4849133d7a78 src/HOL/Statespace/StateFun.thy
--- 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
 
 
diff -r 454b06bc9601 -r 4849133d7a78 src/HOL/Statespace/StateSpaceEx.thy
--- 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"
 *)
diff -r 454b06bc9601 -r 4849133d7a78 src/HOL/Statespace/StateSpaceLocale.thy
--- 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
diff -r 454b06bc9601 -r 4849133d7a78 src/HOL/Statespace/document/root.tex
--- 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