author | haftmann |
Tue, 24 Nov 2009 14:37:23 +0100 | |
changeset 33954 | 1bc3b688548c |
parent 30235 | 58d147683393 |
child 39198 | f967a16dfcdd |
permissions | -rwxr-xr-x |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/AuxLemmas.thy |
2 |
ID: $Id$ |
|
3 |
Author: Martin Strecker |
|
4 |
*) |
|
5 |
||
6 |
||
7 |
(* Auxiliary Lemmas *) |
|
8 |
||
15860 | 9 |
theory AuxLemmas |
10 |
imports "../J/JBasis" |
|
11 |
begin |
|
13673 | 12 |
|
13 |
(**********************************************************************) |
|
14 |
(* List.thy *) |
|
15 |
(**********************************************************************) |
|
16 |
||
17 |
||
18 |
||
19 |
lemma app_nth_greater_len [rule_format (no_asm), simp]: |
|
20 |
"\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind" |
|
21 |
apply (induct "pre") |
|
22 |
apply auto |
|
23 |
apply (case_tac ind) |
|
24 |
apply auto |
|
25 |
done |
|
26 |
||
27 |
lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs" |
|
28 |
by (induct xs, auto) |
|
29 |
||
30 |
lemma nth_length_takeWhile [simp]: |
|
31 |
"v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v" |
|
32 |
by (induct xs, auto) |
|
33 |
||
34 |
||
35 |
lemma map_list_update [simp]: |
|
36 |
"\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> |
|
37 |
(map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = |
|
38 |
map (f(x:=v)) xs" |
|
39 |
apply (induct xs) |
|
40 |
apply simp |
|
41 |
apply (case_tac "x=a") |
|
42 |
apply auto |
|
43 |
done |
|
44 |
||
45 |
||
46 |
(**********************************************************************) |
|
47 |
(* Product_Type.thy *) |
|
48 |
(**********************************************************************) |
|
49 |
||
50 |
||
51 |
lemma split_compose: "(split f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = |
|
52 |
(\<lambda> (a,b). (f (fa a) (fb b)))" |
|
53 |
by (simp add: split_def o_def) |
|
54 |
||
55 |
lemma split_iter: "(\<lambda> (a,b,c). ((g1 a), (g2 b), (g3 c))) = |
|
56 |
(\<lambda> (a,p). ((g1 a), (\<lambda> (b, c). ((g2 b), (g3 c))) p))" |
|
57 |
by (simp add: split_def o_def) |
|
58 |
||
59 |
||
60 |
(**********************************************************************) |
|
61 |
(* Set.thy *) |
|
62 |
(**********************************************************************) |
|
63 |
||
64 |
lemma singleton_in_set: "A = {a} \<Longrightarrow> a \<in> A" by simp |
|
65 |
||
66 |
(**********************************************************************) |
|
67 |
(* Map.thy *) |
|
68 |
(**********************************************************************) |
|
69 |
||
70 |
lemma the_map_upd: "(the \<circ> f(x\<mapsto>v)) = (the \<circ> f)(x:=v)" |
|
71 |
by (simp add: expand_fun_eq) |
|
72 |
||
73 |
lemma map_of_in_set: |
|
74 |
"(map_of xs x = None) = (x \<notin> set (map fst xs))" |
|
75 |
by (induct xs, auto) |
|
76 |
||
77 |
lemma map_map_upd [simp]: |
|
78 |
"y \<notin> set xs \<Longrightarrow> map (the \<circ> f(y\<mapsto>v)) xs = map (the \<circ> f) xs" |
|
79 |
by (simp add: the_map_upd) |
|
80 |
||
81 |
lemma map_map_upds [rule_format (no_asm), simp]: |
|
82 |
"\<forall> f vs. (\<forall>y\<in>set ys. y \<notin> set xs) \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs" |
|
14025 | 83 |
apply (induct xs) |
84 |
apply simp |
|
85 |
apply fastsimp |
|
13673 | 86 |
done |
87 |
||
88 |
lemma map_upds_distinct [rule_format (no_asm), simp]: |
|
89 |
"\<forall> f vs. length ys = length vs \<longrightarrow> distinct ys \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs" |
|
90 |
apply (induct ys) |
|
91 |
apply simp |
|
92 |
apply (intro strip) |
|
93 |
apply (case_tac vs) |
|
94 |
apply simp |
|
14025 | 95 |
apply (simp only: map_upds_Cons distinct.simps hd.simps tl.simps map.simps) |
13673 | 96 |
apply clarify |
14025 | 97 |
apply (simp del: o_apply) |
13673 | 98 |
apply simp |
99 |
done |
|
100 |
||
101 |
||
102 |
lemma map_of_map_as_map_upd [rule_format (no_asm)]: "distinct (map f zs) \<longrightarrow> |
|
103 |
map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)" |
|
104 |
by (induct zs, auto) |
|
105 |
||
106 |
(* In analogy to Map.map_of_SomeD *) |
|
107 |
lemma map_upds_SomeD [rule_format (no_asm)]: |
|
108 |
"\<forall> m ys. (m(xs[\<mapsto>]ys)) k = Some y \<longrightarrow> k \<in> (set xs) \<or> (m k = Some y)" |
|
109 |
apply (induct xs) |
|
110 |
apply simp |
|
14025 | 111 |
apply auto |
112 |
apply(case_tac ys) |
|
13673 | 113 |
apply auto |
114 |
done |
|
115 |
||
116 |
lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y |
|
117 |
\<Longrightarrow> k \<in> (set (xs @ map fst m))" |
|
118 |
by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
|
119 |
||
120 |
||
121 |
lemma map_of_map_prop [rule_format (no_asm)]: |
|
122 |
"(map_of (map f xs) k = Some v) \<longrightarrow> |
|
123 |
(\<forall> x \<in> set xs. (P1 x)) \<longrightarrow> |
|
124 |
(\<forall> x. (P1 x) \<longrightarrow> (P2 (f x))) \<longrightarrow> |
|
125 |
(P2(k, v))" |
|
126 |
by (induct xs,auto) |
|
127 |
||
128 |
lemma map_of_map2: "\<forall> x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
|
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
15860
diff
changeset
|
129 |
map_of (map f xs) a = Option.map (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
13673 | 130 |
by (induct xs, auto) |
131 |
||
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
15860
diff
changeset
|
132 |
lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)" |
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
15860
diff
changeset
|
133 |
by (simp add: Option.map_def split: option.split) |
13673 | 134 |
|
135 |
||
136 |
||
137 |
end |