# HG changeset patch
# User wenzelm
# Date 1282941025 -7200
# Node ID 62f6ba39b3d45aab3c22298083275b6a7e55c5d5
# Parent  b47ee8df7ab4b65d73fdbca6b84ea7eddefb6140
modernized specifications;

diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -32,17 +32,18 @@
 subsection {* Distinctness of Nodes *}
 
 
-consts set_of:: "'a tree \<Rightarrow> 'a set"
-primrec 
-"set_of Tip = {}"
-"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
+primrec set_of :: "'a tree \<Rightarrow> 'a set"
+where
+  "set_of Tip = {}"
+| "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
 
-consts all_distinct:: "'a tree \<Rightarrow> bool"
-primrec
-"all_distinct Tip = True"
-"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
-                               set_of l \<inter> set_of r = {} \<and>
-                               all_distinct l \<and> all_distinct r)"
+primrec all_distinct :: "'a tree \<Rightarrow> bool"
+where
+  "all_distinct Tip = True"
+| "all_distinct (Node l x d r) =
+    ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
+      set_of l \<inter> set_of r = {} \<and>
+      all_distinct l \<and> all_distinct r)"
 
 text {* Given a binary tree @{term "t"} for which 
 @{const all_distinct} holds, given two different nodes contained in the tree,
@@ -99,19 +100,19 @@
 *}
 
 
-consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
-primrec
-"delete x Tip = None"
-"delete x (Node l y d r) = (case delete x l of
-                              Some l' \<Rightarrow>
-                               (case delete x r of 
-                                  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 
-                                   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))"
+primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
+where
+  "delete x Tip = None"
+| "delete x (Node l y d r) = (case delete x l of
+                                Some l' \<Rightarrow>
+                                 (case delete x r of 
+                                    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 
+                                     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"
@@ -293,15 +294,15 @@
 qed
 
 
-consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
-primrec
-"subtract Tip t = Some t"
-"subtract (Node l x b r) t = 
-   (case delete x t of
-      Some t' \<Rightarrow> (case subtract l t' of 
-                   Some t'' \<Rightarrow> subtract r t''
-                  | None \<Rightarrow> None)
-    | None \<Rightarrow> None)"
+primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
+where
+  "subtract Tip t = Some t"
+| "subtract (Node l x b r) t =
+     (case delete x t of
+        Some t' \<Rightarrow> (case subtract l t' of 
+                     Some t'' \<Rightarrow> subtract r t''
+                    | None \<Rightarrow> None)
+       | 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"
diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -33,10 +33,10 @@
 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
   by (rule refl)
 
-definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+definition lookup :: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
   where "lookup destr n s = destr (s n)"
 
-definition update::
+definition update ::
   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
   where "update destr constr n f s = s(n := constr (f (destr (s n))))"
 
diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -1,14 +1,12 @@
 (*  Title:      StateSpaceEx.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
 header {* Examples \label{sec:Examples} *}
 theory StateSpaceEx
 imports StateSpaceLocale StateSpaceSyntax
+begin
 
-begin
-(* FIXME: Use proper keywords file *)
 (*<*)
 syntax
  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      StateSpaceLocale.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -18,7 +17,7 @@
 
 locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
- and   "inject":: "'a \<Rightarrow> 'value"
+  and inject :: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
 
 lemma (in project_inject)
diff -r b47ee8df7ab4 -r 62f6ba39b3d4 src/HOL/Statespace/StateSpaceSyntax.thy
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Aug 27 22:09:51 2010 +0200
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Aug 27 22:30:25 2010 +0200
@@ -5,7 +5,6 @@
 header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
 theory StateSpaceSyntax
 imports StateSpaceLocale
-
 begin
 
 text {* The state space syntax is kept in an extra theory so that you