12 lemmas [simp] = Let_def |
12 lemmas [simp] = Let_def |
13 |
13 |
14 section "unique" |
14 section "unique" |
15 |
15 |
16 definition unique :: "('a \<times> 'b) list => bool" where |
16 definition unique :: "('a \<times> 'b) list => bool" where |
17 "unique == distinct \<circ> map fst" |
17 "unique == distinct \<circ> map fst" |
18 |
18 |
19 |
19 |
20 lemma fst_in_set_lemma [rule_format (no_asm)]: |
20 lemma fst_in_set_lemma: "(x, y) : set xys ==> x : fst ` set xys" |
21 "(x, y) : set xys --> x : fst ` set xys" |
21 by (induct xys) auto |
22 apply (induct_tac "xys") |
|
23 apply auto |
|
24 done |
|
25 |
22 |
26 lemma unique_Nil [simp]: "unique []" |
23 lemma unique_Nil [simp]: "unique []" |
27 apply (unfold unique_def) |
24 by (simp add: unique_def) |
28 apply (simp (no_asm)) |
|
29 done |
|
30 |
25 |
31 lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" |
26 lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" |
32 apply (unfold unique_def) |
27 by (auto simp: unique_def dest: fst_in_set_lemma) |
33 apply (auto dest: fst_in_set_lemma) |
|
34 done |
|
35 |
28 |
36 lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> |
29 lemma unique_append: "unique l' ==> unique l ==> |
37 (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')" |
30 (!(x,y):set l. !(x',y'):set l'. x' ~= x) ==> unique (l @ l')" |
38 apply (induct_tac "l") |
31 by (induct l) (auto dest: fst_in_set_lemma) |
39 apply (auto dest: fst_in_set_lemma) |
|
40 done |
|
41 |
32 |
42 lemma unique_map_inj [rule_format (no_asm)]: |
33 lemma unique_map_inj: "unique l ==> inj f ==> unique (map (%(k,x). (f k, g k x)) l)" |
43 "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)" |
34 by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq) |
44 apply (induct_tac "l") |
35 |
45 apply (auto dest: fst_in_set_lemma simp add: inj_eq) |
|
46 done |
|
47 |
36 |
48 section "More about Maps" |
37 section "More about Maps" |
49 |
38 |
50 lemma map_of_SomeI [rule_format (no_asm)]: |
39 lemma map_of_SomeI: "unique l ==> (k, x) : set l ==> map_of l k = Some x" |
51 "unique l --> (k, x) : set l --> map_of l k = Some x" |
40 by (induct l) auto |
52 apply (induct_tac "l") |
|
53 apply auto |
|
54 done |
|
55 |
41 |
56 lemma Ball_set_table': |
42 lemma Ball_set_table: "(\<forall>(x,y)\<in>set l. P x y) ==> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
57 "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)" |
43 by (induct l) auto |
58 apply(induct_tac "l") |
|
59 apply(simp_all (no_asm)) |
|
60 apply safe |
|
61 apply auto |
|
62 done |
|
63 lemmas Ball_set_table = Ball_set_table' [THEN mp]; |
|
64 |
44 |
65 lemma table_of_remap_SomeD [rule_format (no_asm)]: |
45 lemma table_of_remap_SomeD: |
66 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> |
46 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==> |
67 map_of t (k, k') = Some x" |
47 map_of t (k, k') = Some x" |
68 apply (induct_tac "t") |
48 by (atomize (full), induct t) auto |
69 apply auto |
|
70 done |
|
71 |
49 |
72 end |
50 end |