# HG changeset patch
# User haftmann
# Date 1267870869 -3600
# Node ID 0f2c634c8ab7395c1854810282a6116ecca660f0
# Parent  db4045d1406e41872affeb953909bccda86fe155
"private" map_of_map lemma

diff -r db4045d1406e -r 0f2c634c8ab7 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 06 09:58:33 2010 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 06 11:21:09 2010 +0100
@@ -265,6 +265,10 @@
 abbreviation (input)
   "mtd_mb == snd o snd"
 
+lemma map_of_map:
+  "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = Option.map f (map_of xs k)"
+  by (simp add: map_of_map)
+
 lemma map_of_map_fst: "\<lbrakk> inj f;
   \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
   \<Longrightarrow>  map_of (map g xs) k 
@@ -282,7 +286,6 @@
 apply (simp add: surjective_pairing)
 done
 
-
 lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   ((method (comp G, C) S) = 
   Option.map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
@@ -290,7 +293,7 @@
 apply (simp add: method_def)
 apply (frule wf_subcls1)
 apply (simp add: comp_class_rec)
-apply (simp add: split_iter split_compose map_map[symmetric] del: map_map)
+apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
 apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   in class_rec_relation)
@@ -307,7 +310,7 @@
 defer                           (* inj \<dots> *)
 apply (simp add: inj_on_def split_beta) 
 apply (simp add: split_beta compMethod_def)
-apply (simp add: map_of_map [THEN sym])
+apply (simp add: map_of_map [symmetric])
 apply (simp add: split_beta)
 apply (simp add: Fun.comp_def split_beta)
 apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.