equal
deleted
inserted
replaced
125 abbreviation "s0 == Norm (empty, empty)" |
125 abbreviation "s0 == Norm (empty, empty)" |
126 abbreviation "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
126 abbreviation "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
127 abbreviation "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
127 abbreviation "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
128 abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
128 abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
129 |
129 |
130 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *} |
130 lemmas map_of_Cons = map_of.simps(2) |
|
131 |
131 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
132 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
132 apply (simp (no_asm)) |
133 apply (simp (no_asm)) |
133 done |
134 done |
134 lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa" |
135 lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa" |
135 apply (simp (no_asm_simp)) |
136 apply (simp (no_asm_simp)) |