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 *))