modernized specifications;
authorwenzelm
Fri Aug 27 22:30:25 2010 +0200 (2010-08-27)
changeset 3883862f6ba39b3d4
parent 38837 b47ee8df7ab4
child 38839 be9dace0ff58
child 38858 1920158cfa17
modernized specifications;
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/Statespace/StateSpaceSyntax.thy
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:09:51 2010 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Aug 27 22:30:25 2010 +0200
     1.3 @@ -32,17 +32,18 @@
     1.4  subsection {* Distinctness of Nodes *}
     1.5  
     1.6  
     1.7 -consts set_of:: "'a tree \<Rightarrow> 'a set"
     1.8 -primrec 
     1.9 -"set_of Tip = {}"
    1.10 -"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    1.11 +primrec set_of :: "'a tree \<Rightarrow> 'a set"
    1.12 +where
    1.13 +  "set_of Tip = {}"
    1.14 +| "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    1.15  
    1.16 -consts all_distinct:: "'a tree \<Rightarrow> bool"
    1.17 -primrec
    1.18 -"all_distinct Tip = True"
    1.19 -"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    1.20 -                               set_of l \<inter> set_of r = {} \<and>
    1.21 -                               all_distinct l \<and> all_distinct r)"
    1.22 +primrec all_distinct :: "'a tree \<Rightarrow> bool"
    1.23 +where
    1.24 +  "all_distinct Tip = True"
    1.25 +| "all_distinct (Node l x d r) =
    1.26 +    ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    1.27 +      set_of l \<inter> set_of r = {} \<and>
    1.28 +      all_distinct l \<and> all_distinct r)"
    1.29  
    1.30  text {* Given a binary tree @{term "t"} for which 
    1.31  @{const all_distinct} holds, given two different nodes contained in the tree,
    1.32 @@ -99,19 +100,19 @@
    1.33  *}
    1.34  
    1.35  
    1.36 -consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.37 -primrec
    1.38 -"delete x Tip = None"
    1.39 -"delete x (Node l y d r) = (case delete x l of
    1.40 -                              Some l' \<Rightarrow>
    1.41 -                               (case delete x r of 
    1.42 -                                  Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
    1.43 -                                | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
    1.44 -                             | None \<Rightarrow>
    1.45 -                                (case (delete x r) of 
    1.46 -                                   Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
    1.47 -                                 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
    1.48 -                                           else None))"
    1.49 +primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.50 +where
    1.51 +  "delete x Tip = None"
    1.52 +| "delete x (Node l y d r) = (case delete x l of
    1.53 +                                Some l' \<Rightarrow>
    1.54 +                                 (case delete x r of 
    1.55 +                                    Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
    1.56 +                                  | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
    1.57 +                               | None \<Rightarrow>
    1.58 +                                  (case (delete x r) of 
    1.59 +                                     Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
    1.60 +                                   | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
    1.61 +                                             else None))"
    1.62  
    1.63  
    1.64  lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
    1.65 @@ -293,15 +294,15 @@
    1.66  qed
    1.67  
    1.68  
    1.69 -consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.70 -primrec
    1.71 -"subtract Tip t = Some t"
    1.72 -"subtract (Node l x b r) t = 
    1.73 -   (case delete x t of
    1.74 -      Some t' \<Rightarrow> (case subtract l t' of 
    1.75 -                   Some t'' \<Rightarrow> subtract r t''
    1.76 -                  | None \<Rightarrow> None)
    1.77 -    | None \<Rightarrow> None)"
    1.78 +primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
    1.79 +where
    1.80 +  "subtract Tip t = Some t"
    1.81 +| "subtract (Node l x b r) t =
    1.82 +     (case delete x t of
    1.83 +        Some t' \<Rightarrow> (case subtract l t' of 
    1.84 +                     Some t'' \<Rightarrow> subtract r t''
    1.85 +                    | None \<Rightarrow> None)
    1.86 +       | None \<Rightarrow> None)"
    1.87  
    1.88  lemma subtract_Some_set_of_res: 
    1.89    "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
     2.1 --- a/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:09:51 2010 +0200
     2.2 +++ b/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:30:25 2010 +0200
     2.3 @@ -33,10 +33,10 @@
     2.4  lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
     2.5    by (rule refl)
     2.6  
     2.7 -definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
     2.8 +definition lookup :: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
     2.9    where "lookup destr n s = destr (s n)"
    2.10  
    2.11 -definition update::
    2.12 +definition update ::
    2.13    "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    2.14    where "update destr constr n f s = s(n := constr (f (destr (s n))))"
    2.15  
     3.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Fri Aug 27 22:09:51 2010 +0200
     3.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Fri Aug 27 22:30:25 2010 +0200
     3.3 @@ -1,14 +1,12 @@
     3.4  (*  Title:      StateSpaceEx.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Norbert Schirmer, TU Muenchen
     3.7  *)
     3.8  
     3.9  header {* Examples \label{sec:Examples} *}
    3.10  theory StateSpaceEx
    3.11  imports StateSpaceLocale StateSpaceSyntax
    3.12 +begin
    3.13  
    3.14 -begin
    3.15 -(* FIXME: Use proper keywords file *)
    3.16  (*<*)
    3.17  syntax
    3.18   "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
     4.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:09:51 2010 +0200
     4.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Fri Aug 27 22:30:25 2010 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      StateSpaceLocale.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Norbert Schirmer, TU Muenchen
     4.7  *)
     4.8  
     4.9 @@ -18,7 +17,7 @@
    4.10  
    4.11  locale project_inject =
    4.12   fixes project :: "'value \<Rightarrow> 'a"
    4.13 - and   "inject":: "'a \<Rightarrow> 'value"
    4.14 +  and inject :: "'a \<Rightarrow> 'value"
    4.15   assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
    4.16  
    4.17  lemma (in project_inject)
     5.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Aug 27 22:09:51 2010 +0200
     5.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Aug 27 22:30:25 2010 +0200
     5.3 @@ -5,7 +5,6 @@
     5.4  header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
     5.5  theory StateSpaceSyntax
     5.6  imports StateSpaceLocale
     5.7 -
     5.8  begin
     5.9  
    5.10  text {* The state space syntax is kept in an extra theory so that you