--- 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"
--- 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))))"
--- 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)
--- 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)
--- 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