replaced syntax/translations by abbreviation;
authorwenzelm
Thu Sep 28 23:42:39 2006 +0200 (2006-09-28)
changeset 207695d538d3d5e2a
parent 20768 1d478c2d621f
child 20770 2c583720436e
replaced syntax/translations by abbreviation;
fixed translations: CONST;
src/HOL/Bali/Example.thy
     1.1 --- a/src/HOL/Bali/Example.thy	Thu Sep 28 23:42:35 2006 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Thu Sep 28 23:42:39 2006 +0200
     1.3 @@ -86,28 +86,33 @@
     1.4    surj_vnam_:  "\<exists>m. n = vnam_  m"
     1.5    surj_label_:" \<exists>m. n = label_ m"
     1.6  
     1.7 -syntax
     1.8 -
     1.9 +abbreviation
    1.10    HasFoo :: qtname
    1.11 -  Base   :: qtname
    1.12 -  Ext    :: qtname
    1.13 -  Main   :: qtname
    1.14 -  arr :: ename
    1.15 -  vee :: ename
    1.16 -  z   :: ename
    1.17 -  e   :: ename
    1.18 +  "HasFoo == \<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
    1.19 +
    1.20 +  Base :: qtname
    1.21 +  "Base == \<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
    1.22 +
    1.23 +  Ext :: qtname
    1.24 +  "Ext == \<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
    1.25 +
    1.26 +  Main :: qtname
    1.27 +  "Main == \<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
    1.28 +
    1.29 +  arr :: vname
    1.30 +  "arr == (vnam_ arr_)"
    1.31 +
    1.32 +  vee :: vname
    1.33 +  "vee == (vnam_ vee_)"
    1.34 +
    1.35 +  z :: vname
    1.36 +  "z == (vnam_ z_)"
    1.37 +
    1.38 +  e :: vname
    1.39 +  "e == (vnam_ e_)"
    1.40 +
    1.41    lab1:: label
    1.42 -translations
    1.43 -
    1.44 -  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
    1.45 -  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
    1.46 -  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
    1.47 -  "Main"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
    1.48 -  "arr"    ==        "(vnam_ arr_)"
    1.49 -  "vee"    ==        "(vnam_ vee_)"
    1.50 -  "z"      ==        "(vnam_ z_)"
    1.51 -  "e"      ==        "(vnam_ e_)"
    1.52 -  "lab1"   ==        "label_ lab1_"
    1.53 +  "lab1 == label_ lab1_"
    1.54  
    1.55  
    1.56  lemma neq_Base_Object [simp]: "Base\<noteq>Object"
    1.57 @@ -255,11 +260,9 @@
    1.58  
    1.59  section "program"
    1.60  
    1.61 -syntax
    1.62 +abbreviation
    1.63    tprg :: prog
    1.64 -
    1.65 -translations
    1.66 -  "tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
    1.67 +  "tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
    1.68  
    1.69  constdefs
    1.70    test    :: "(ty)list \<Rightarrow> stmt"
    1.71 @@ -1191,11 +1194,14 @@
    1.72    a :: loc
    1.73    b :: loc
    1.74    c :: loc
    1.75 -  
    1.76 -syntax
    1.77  
    1.78 -  tprg :: prog
    1.79 +abbreviation
    1.80 +  "one == Suc 0"
    1.81 +  "two == Suc one"
    1.82 +  "tree == Suc two"
    1.83 +  "four == Suc tree"
    1.84  
    1.85 +syntax
    1.86    obj_a :: obj
    1.87    obj_b :: obj
    1.88    obj_c :: obj
    1.89 @@ -1225,34 +1231,31 @@
    1.90    s8' :: state
    1.91  
    1.92  translations
    1.93 -
    1.94 -  "tprg"    == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
    1.95 -  
    1.96 -  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) two
    1.97 -                ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
    1.98 -  "obj_b"   <= "\<lparr>tag=CInst Ext
    1.99 -                ,values=(empty(Inl (vee, Base)\<mapsto>Null   ) 
   1.100 -			      (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
   1.101 -  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
   1.102 -  "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
   1.103 -  "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
   1.104 -  "globs1"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
   1.105 -		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
   1.106 -		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
   1.107 -  "globs2"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
   1.108 -		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
   1.109 -		     (Inl a\<mapsto>obj_a)
   1.110 -		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
   1.111 +  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
   1.112 +                ,values=CONST empty(Inr 0\<mapsto>Bool False)(Inr (CONST one)\<mapsto>Bool False)\<rparr>"
   1.113 +  "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
   1.114 +                ,values=(CONST empty(Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
   1.115 +                              (Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
   1.116 +  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
   1.117 +  "arr_N"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
   1.118 +  "arr_a"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
   1.119 +  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
   1.120 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
   1.121 +                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)"
   1.122 +  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
   1.123 +                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
   1.124 +                     (Inl a\<mapsto>obj_a)
   1.125 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
   1.126    "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
   1.127    "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
   1.128 -  "locs3"   == "empty(VName e\<mapsto>Addr b)"
   1.129 -  "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
   1.130 -  "locs8"   == "locs3(VName z\<mapsto>Addr c)"
   1.131 -  "s0"  == "       st empty  empty"
   1.132 +  "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
   1.133 +  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(Inr()\<mapsto>Addr b)"
   1.134 +  "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
   1.135 +  "s0"  == "       st (CONST empty) (CONST empty)"
   1.136    "s0'" == " Norm  s0"
   1.137 -  "s1"  == "       st globs1 empty"
   1.138 +  "s1"  == "       st globs1 (CONST empty)"
   1.139    "s1'" == " Norm  s1"
   1.140 -  "s2"  == "       st globs2 empty"
   1.141 +  "s2"  == "       st globs2 (CONST empty)"
   1.142    "s2'" == " Norm  s2"
   1.143    "s3"  == "       st globs3 locs3 "
   1.144    "s3'" == " Norm  s3"
   1.145 @@ -1265,16 +1268,6 @@
   1.146    "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
   1.147  
   1.148  
   1.149 -syntax "four"::nat
   1.150 -       "tree"::nat
   1.151 -       "two" ::nat
   1.152 -       "one" ::nat
   1.153 -translations 
   1.154 -  "one"  == "Suc 0"
   1.155 -  "two"  == "Suc one"
   1.156 -  "tree" == "Suc two"
   1.157 -  "four" == "Suc tree"
   1.158 -
   1.159  declare Pair_eq [simp del]
   1.160  lemma exec_test: 
   1.161  "\<lbrakk>the (new_Addr (heap  s1)) = a;