formal markup of @{syntax_const} and @{const_syntax};
authorwenzelm
Thu Feb 11 22:55:16 2010 +0100 (2010-02-11)
changeset 35114b1fd1d756e20
parent 35113 1a0c129bb2e0
child 35115 446c5063e4fd
formal markup of @{syntax_const} and @{const_syntax};
authentic syntax for extra robustness;
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/StateSpaceSyntax.thy
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:19:58 2010 +0100
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:55:16 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      StateFun.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Norbert Schirmer, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -34,12 +33,12 @@
    1.10  lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    1.11    by (rule refl)
    1.12  
    1.13 -constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    1.14 -"lookup destr n s \<equiv> destr (s n)"
    1.15 +definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    1.16 +  where "lookup destr n s = destr (s n)"
    1.17  
    1.18 -constdefs update:: 
    1.19 +definition update::
    1.20    "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    1.21 -"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
    1.22 +  where "update destr constr n f s = s(n := constr (f (destr (s n))))"
    1.23  
    1.24  lemma lookup_update_same:
    1.25    "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
     2.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 22:19:58 2010 +0100
     2.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 22:55:16 2010 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      StateSpaceSyntax.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Norbert Schirmer, TU Muenchen
     2.7  *)
     2.8  
     2.9 @@ -13,30 +12,27 @@
    2.10  can choose if you want to use it or not.  *}
    2.11  
    2.12  syntax 
    2.13 - "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
    2.14 - "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
    2.15 - "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
    2.16 +  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
    2.17 +  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
    2.18 +  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
    2.19  
    2.20  translations
    2.21 -  "_statespace_updates f (_updbinds b bs)"  == 
    2.22 -     "_statespace_updates (_statespace_updates f b) bs"
    2.23 -  "s<x:=y>"                     == "_statespace_update s x y"
    2.24 +  "_statespace_updates f (_updbinds b bs)" ==
    2.25 +    "_statespace_updates (_statespace_updates f b) bs"
    2.26 +  "s<x:=y>" == "_statespace_update s x y"
    2.27  
    2.28  
    2.29  parse_translation (advanced)
    2.30  {*
    2.31 -[("_statespace_lookup",StateSpace.lookup_tr),
    2.32 - ("_get",StateSpace.lookup_tr),
    2.33 - ("_statespace_update",StateSpace.update_tr)] 
    2.34 + [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
    2.35 +  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
    2.36  *}
    2.37  
    2.38  
    2.39  print_translation (advanced)
    2.40  {*
    2.41 -[("lookup",StateSpace.lookup_tr'),
    2.42 - ("StateFun.lookup",StateSpace.lookup_tr'),
    2.43 - ("update",StateSpace.update_tr'),
    2.44 - ("StateFun.update",StateSpace.update_tr')] 
    2.45 + [(@{const_syntax lookup}, StateSpace.lookup_tr'),
    2.46 +  (@{const_syntax update}, StateSpace.update_tr')]
    2.47  *}
    2.48  
    2.49 -end
    2.50 \ No newline at end of file
    2.51 +end