src/HOL/NanoJava/Equivalence.thy

--- a/src/HOL/NanoJava/Equivalence.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/NanoJava/Equivalence.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   2001 Technische Universitaet Muenchen
 *)
@@ -10,27 +9,25 @@
 
 subsection "Validity"
 
-constdefs
-  valid   :: "[assn,stmt, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+definition valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
  "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n\<rightarrow> t) --> Q   t"
 
- evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+definition evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
  "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e\<succ>v-n\<rightarrow> t) --> Q v t"
 
-
- nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60)
+definition nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60) where
  "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n\<rightarrow> t --> P s --> Q   t"
 
-envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60)
+definition envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60) where
  "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e\<succ>v-n\<rightarrow> t --> P s --> Q v t"
 
-  nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
+definition nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60) where
  "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
 
- cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"  [61,61] 60)
+definition cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"  [61,61] 60) where
  "A ||=  C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
 
-cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
+definition cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60) where
  "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
 
 syntax (xsymbols)
@@ -160,10 +157,12 @@
 
 subsection "(Relative) Completeness"
 
-constdefs MGT    :: "stmt => state =>  triple"
+definition MGT :: "stmt => state => triple" where
          "MGT  c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda>  t. \<exists>n. Z -c-  n\<rightarrow> t)"
-          MGTe   :: "expr => state => etriple"
+
+definition MGTe   :: "expr => state => etriple" where
          "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
+
 syntax (xsymbols)
          MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
 syntax (HTML output)