author | kleing |
Thu, 28 May 2015 17:25:57 +1000 | |
changeset 60304 | 3f429b7d8eb5 |
parent 55466 | 786edc984c98 |
child 61424 | c3658c18b7bc |
permissions | -rw-r--r-- |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/AuxLemmas.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
5 |
||
6 |
(* Auxiliary Lemmas *) |
|
7 |
||
15860 | 8 |
theory AuxLemmas |
9 |
imports "../J/JBasis" |
|
10 |
begin |
|
13673 | 11 |
|
12 |
(**********************************************************************) |
|
13 |
(* List.thy *) |
|
14 |
(**********************************************************************) |
|
15 |
||
16 |
||
17 |
||
52866 | 18 |
lemma app_nth_greater_len [simp]: |
60304 | 19 |
"length pre \<le> ind \<Longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind" |
20 |
apply (induct pre arbitrary: ind) |
|
21 |
apply clarsimp |
|
22 |
apply (case_tac ind) |
|
23 |
apply auto |
|
24 |
done |
|
13673 | 25 |
|
60304 | 26 |
lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (\<lambda>z. z \<noteq> v) xs) < length xs" |
27 |
by (induct xs) auto |
|
13673 | 28 |
|
29 |
lemma nth_length_takeWhile [simp]: |
|
30 |
"v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v" |
|
60304 | 31 |
by (induct xs) auto |
13673 | 32 |
|
33 |
||
34 |
lemma map_list_update [simp]: |
|
35 |
"\<lbrakk> x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> |
|
60304 | 36 |
(map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = map (f(x:=v)) xs" |
37 |
apply (induct xs) |
|
38 |
apply simp |
|
39 |
apply (rename_tac a xs) |
|
40 |
apply (case_tac "x=a") |
|
41 |
apply auto |
|
42 |
done |
|
13673 | 43 |
|
44 |
||
45 |
(**********************************************************************) |
|
46 |
(* Product_Type.thy *) |
|
47 |
(**********************************************************************) |
|
48 |
||
49 |
||
60304 | 50 |
lemma split_compose: |
51 |
"(split f) \<circ> (\<lambda> (a,b). ((fa a), (fb b))) = (\<lambda> (a,b). (f (fa a) (fb b)))" |
|
52 |
by (simp add: split_def o_def) |
|
13673 | 53 |
|
60304 | 54 |
lemma split_iter: |
55 |
"(\<lambda> (a,b,c). ((g1 a), (g2 b), (g3 c))) = (\<lambda> (a,p). ((g1 a), (\<lambda> (b, c). ((g2 b), (g3 c))) p))" |
|
56 |
by (simp add: split_def o_def) |
|
13673 | 57 |
|
58 |
||
59 |
(**********************************************************************) |
|
60 |
(* Set.thy *) |
|
61 |
(**********************************************************************) |
|
62 |
||
63 |
lemma singleton_in_set: "A = {a} \<Longrightarrow> a \<in> A" by simp |
|
64 |
||
65 |
(**********************************************************************) |
|
66 |
(* Map.thy *) |
|
67 |
(**********************************************************************) |
|
68 |
||
69 |
lemma the_map_upd: "(the \<circ> f(x\<mapsto>v)) = (the \<circ> f)(x:=v)" |
|
60304 | 70 |
by (simp add: fun_eq_iff) |
13673 | 71 |
|
72 |
lemma map_of_in_set: |
|
73 |
"(map_of xs x = None) = (x \<notin> set (map fst xs))" |
|
60304 | 74 |
by (induct xs, auto) |
13673 | 75 |
|
76 |
lemma map_map_upd [simp]: |
|
77 |
"y \<notin> set xs \<Longrightarrow> map (the \<circ> f(y\<mapsto>v)) xs = map (the \<circ> f) xs" |
|
60304 | 78 |
by (simp add: the_map_upd) |
13673 | 79 |
|
39917
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
80 |
lemma map_map_upds [simp]: |
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
81 |
"(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs" |
60304 | 82 |
by (induct xs arbitrary: f vs) auto |
13673 | 83 |
|
39917
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
84 |
lemma map_upds_distinct [simp]: |
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
85 |
"distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs" |
60304 | 86 |
apply (induct ys arbitrary: f vs) |
87 |
apply simp |
|
88 |
apply (case_tac vs) |
|
89 |
apply simp_all |
|
90 |
done |
|
13673 | 91 |
|
39917
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
92 |
lemma map_of_map_as_map_upd: |
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
93 |
"distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)" |
b85bfa89a387
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39302
diff
changeset
|
94 |
by (induct zs) auto |
13673 | 95 |
|
96 |
(* In analogy to Map.map_of_SomeD *) |
|
60304 | 97 |
lemma map_upds_SomeD: |
98 |
"(m(xs[\<mapsto>]ys)) k = Some y \<Longrightarrow> k \<in> (set xs) \<or> (m k = Some y)" |
|
99 |
apply (induct xs arbitrary: m ys) |
|
100 |
apply simp |
|
101 |
apply (case_tac ys) |
|
102 |
apply fastforce+ |
|
103 |
done |
|
13673 | 104 |
|
105 |
lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y |
|
106 |
\<Longrightarrow> k \<in> (set (xs @ map fst m))" |
|
60304 | 107 |
by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma) |
13673 | 108 |
|
60304 | 109 |
lemma map_of_map_prop: |
110 |
"\<lbrakk>map_of (map f xs) k = Some v; \<forall>x \<in> set xs. P1 x; \<forall>x. P1 x \<longrightarrow> P2 (f x)\<rbrakk> \<Longrightarrow> P2 (k, v)" |
|
111 |
by (induct xs) (auto split: split_if_asm) |
|
13673 | 112 |
|
60304 | 113 |
lemma map_of_map2: "\<forall>x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow> |
55466 | 114 |
map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)" |
60304 | 115 |
by (induct xs, auto) |
13673 | 116 |
|
117 |
end |