src/HOL/Bali/Example.thy
changeset 35067 af4c18c30593
parent 33965 f57c11db4ad4
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Bali/Example.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -1202,74 +1202,52 @@
     1.4  
     1.5  abbreviation "one == Suc 0"
     1.6  abbreviation "two == Suc one"
     1.7 -abbreviation "tree == Suc two"
     1.8 -abbreviation "four == Suc tree"
     1.9 +abbreviation "three == Suc two"
    1.10 +abbreviation "four == Suc three"
    1.11 +
    1.12 +abbreviation
    1.13 +  "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
    1.14 +                ,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
    1.15  
    1.16 -syntax
    1.17 -  obj_a :: obj
    1.18 -  obj_b :: obj
    1.19 -  obj_c :: obj
    1.20 -  arr_N :: "(vn, val) table"
    1.21 -  arr_a :: "(vn, val) table"
    1.22 -  globs1 :: globs
    1.23 -  globs2 :: globs
    1.24 -  globs3 :: globs
    1.25 -  globs8 :: globs
    1.26 -  locs3 :: locals
    1.27 -  locs4 :: locals
    1.28 -  locs8 :: locals
    1.29 -  s0  :: state
    1.30 -  s0' :: state
    1.31 -  s9' :: state
    1.32 -  s1  :: state
    1.33 -  s1' :: state
    1.34 -  s2  :: state
    1.35 -  s2' :: state
    1.36 -  s3  :: state
    1.37 -  s3' :: state
    1.38 -  s4  :: state
    1.39 -  s4' :: state
    1.40 -  s6' :: state
    1.41 -  s7' :: state
    1.42 -  s8  :: state
    1.43 -  s8' :: state
    1.44 +abbreviation
    1.45 +  "obj_b == \<lparr>tag=CInst Ext
    1.46 +                ,values=(empty(Inl (vee, Base)\<mapsto>Null   )
    1.47 +                              (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
    1.48 +
    1.49 +abbreviation
    1.50 +  "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    1.51 +
    1.52 +abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
    1.53 +abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
    1.54 +
    1.55 +abbreviation
    1.56 +  "globs1 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    1.57 +                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
    1.58 +                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)"
    1.59  
    1.60 -translations
    1.61 -  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two)
    1.62 -                ,values=CONST empty(CONST Inr 0\<mapsto>Bool False)(CONST Inr (CONST one)\<mapsto>Bool False)\<rparr>"
    1.63 -  "obj_b"   <= "\<lparr>tag=CInst (CONST Ext)
    1.64 -                ,values=(CONST empty(CONST Inl (CONST vee, CONST Base)\<mapsto>Null   ) 
    1.65 -                              (CONST Inl (CONST vee, CONST Ext )\<mapsto>Intg 0))\<rparr>"
    1.66 -  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    1.67 -  "arr_N"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Null)"
    1.68 -  "arr_a"   == "CONST empty(CONST Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    1.69 -  "globs1"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.70 -                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    1.71 -                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    1.72 -  "globs2"  == "CONST empty(CONST Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.73 -                     (CONST Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.74 -                     (CONST Inl a\<mapsto>obj_a)
    1.75 -                     (CONST Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    1.76 -  "globs3"  == "globs2(CONST Inl b\<mapsto>obj_b)"
    1.77 -  "globs8"  == "globs3(CONST Inl c\<mapsto>obj_c)"
    1.78 -  "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
    1.79 -  "locs4"   == "CONST empty(VName (CONST z)\<mapsto>Null)(CONST Inr()\<mapsto>Addr b)"
    1.80 -  "locs8"   == "locs3(VName (CONST z)\<mapsto>Addr c)"
    1.81 -  "s0"  == "       st (CONST empty) (CONST empty)"
    1.82 -  "s0'" == " Norm  s0"
    1.83 -  "s1"  == "       st globs1 (CONST empty)"
    1.84 -  "s1'" == " Norm  s1"
    1.85 -  "s2"  == "       st globs2 (CONST empty)"
    1.86 -  "s2'" == " Norm  s2"
    1.87 -  "s3"  == "       st globs3 locs3 "
    1.88 -  "s3'" == " Norm  s3"
    1.89 -  "s4"  == "       st globs3 locs4"
    1.90 -  "s4'" == " Norm  s4"
    1.91 -  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
    1.92 -  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
    1.93 -  "s8"  == "       st globs8 locs8"
    1.94 -  "s8'" == " Norm  s8"
    1.95 -  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
    1.96 +abbreviation
    1.97 +  "globs2 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    1.98 +                     (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
    1.99 +                     (Inl a\<mapsto>obj_a)
   1.100 +                     (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
   1.101 +
   1.102 +abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
   1.103 +abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
   1.104 +abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
   1.105 +abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
   1.106 +
   1.107 +abbreviation "s0 == st empty empty"
   1.108 +abbreviation "s0' == Norm  s0"
   1.109 +abbreviation "s1 == st globs1 empty"
   1.110 +abbreviation "s1' == Norm s1"
   1.111 +abbreviation "s2 == st globs2 empty"
   1.112 +abbreviation "s2' == Norm s2"
   1.113 +abbreviation "s3 == st globs3 locs3"
   1.114 +abbreviation "s3' == Norm s3"
   1.115 +abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)"
   1.116 +abbreviation "s8 == st globs8 locs8"
   1.117 +abbreviation "s8' == Norm s8"
   1.118 +abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
   1.119  
   1.120  
   1.121  declare Pair_eq [simp del]
   1.122 @@ -1293,7 +1271,7 @@
   1.123  apply  (rule eval_Is (* NewC *))
   1.124        (* begin init Ext *)
   1.125  apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
   1.126 -apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
   1.127 +apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
   1.128  apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
   1.129  apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
   1.130  apply   (rule eval_Is (* Init Ext *))
   1.131 @@ -1336,7 +1314,7 @@
   1.132  apply (drule alloc_one)
   1.133  apply  (simp (no_asm_simp))
   1.134  apply clarsimp
   1.135 -apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
   1.136 +apply (erule_tac V = "atleast_free ?h three" in thin_rl)
   1.137  apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
   1.138  apply (simp (no_asm_use))
   1.139  apply (rule eval_Is (* Try *))