54 "unique l --> (k, x) : set l --> map_of l k = Some x" |
54 "unique l --> (k, x) : set l --> map_of l k = Some x" |
55 apply (induct_tac "l") |
55 apply (induct_tac "l") |
56 apply auto |
56 apply auto |
57 done |
57 done |
58 |
58 |
59 lemma Ball_set_table_: |
59 lemma Ball_set_table': |
60 "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
60 "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
61 apply(induct_tac "l") |
61 apply(induct_tac "l") |
62 apply(simp_all (no_asm)) |
62 apply(simp_all (no_asm)) |
63 apply safe |
63 apply safe |
64 apply auto |
64 apply auto |
65 done |
65 done |
66 lemmas Ball_set_table = Ball_set_table_ [THEN mp]; |
66 lemmas Ball_set_table = Ball_set_table' [THEN mp]; |
67 |
67 |
68 lemma table_of_remap_SomeD [rule_format (no_asm)]: |
68 lemma table_of_remap_SomeD [rule_format (no_asm)]: |
69 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> |
69 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> |
70 map_of t (k, k') = Some x" |
70 map_of t (k, k') = Some x" |
71 apply (induct_tac "t") |
71 apply (induct_tac "t") |