|
(* Title: HOL/MicroJava/Comp/AuxLemmas.thy
Author: Martin Strecker
*)
(* Auxiliary Lemmas *)
theory AuxLemmas
imports "../J/JBasis"
begin
(**********************************************************************)
(* List.thy *)
(**********************************************************************)
lemma app_nth_greater_len [simp]:
"length pre \ ind \ (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind"
apply (induct pre arbitrary: ind)
apply clarsimp
apply (case_tac ind)
apply auto
done
lemma length_takeWhile: "v \ set xs \ length (takeWhile (\z. z \ v) xs) < length xs"
by (induct xs) auto
lemma nth_length_takeWhile [simp]:
"v \ set xs \ xs ! (length (takeWhile (%z. z~=v) xs)) = v"
by (induct xs) auto
lemma map_list_update [simp]:
"\ x \ set xs; distinct xs\ \
(map f xs) [length (takeWhile (\<lambda>z. z \<noteq> x) xs) := v] = map (f(x:=v)) xs"
apply (induct xs)
apply simp
apply (rename_tac a xs)
apply (case_tac "x=a")
apply auto
done
(**********************************************************************)
(* Product_Type.thy *)
(**********************************************************************)
lemma split_compose:
"(case_prod f) \ (\ (a,b). ((fa a), (fb b))) = (\ (a,b). (f (fa a) (fb b)))"
by (simp add: split_def o_def)
lemma split_iter:
"(\ (a,b,c). ((g1 a), (g2 b), (g3 c))) = (\ (a,p). ((g1 a), (\ (b, c). ((g2 b), (g3 c))) p))"
by (simp add: split_def o_def)
(**********************************************************************)
(* Set.thy *)
(**********************************************************************)
lemma singleton_in_set: "A = {a} \ a \ A" by simp
(**********************************************************************)
(* Map.thy *)
(**********************************************************************)
lemma the_map_upd: "(the \ f(x\v)) = (the \ f)(x:=v)"
by (simp add: fun_eq_iff)
lemma map_of_in_set:
"(map_of xs x = None) = (x \ set (map fst xs))"
by (induct xs, auto)
lemma map_map_upd [simp]:
"y \ set xs \ map (the \ f(y\v)) xs = map (the \ f) xs"
by (simp add: the_map_upd)
lemma map_map_upds [simp]:
"(\y\set ys. y \ set xs) \ map (the \ f(ys[\]vs)) xs = map (the \ f) xs"
by (induct xs arbitrary: f vs) auto
lemma map_upds_distinct [simp]:
"distinct ys \ length ys = length vs \ map (the \ f(ys[\]vs)) ys = vs"
apply (induct ys arbitrary: f vs)
apply simp
apply (case_tac vs)
apply simp_all
done
lemma map_of_map_as_map_upd:
"distinct (map f zs) \ map_of (map (\ p. (f p, g p)) zs) = Map.empty (map f zs [\] map g zs)"
by (induct zs) auto
(* In analogy to Map.map_of_SomeD *)
lemma map_upds_SomeD:
"(m(xs[\]ys)) k = Some y \ k \ (set xs) \ (m k = Some y)"
apply (induct xs arbitrary: m ys)
apply simp
apply (case_tac ys)
apply fastforce+
done
lemma map_of_upds_SomeD: "(map_of m (xs[\]ys)) k = Some y
\<Longrightarrow> k \<in> (set (xs @ map fst m))"
by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
lemma map_of_map_prop:
"\map_of (map f xs) k = Some v; \x \ set xs. P1 x; \x. P1 x \ P2 (f x)\ \ P2 (k, v)"
by (induct xs) (auto split: if_split_asm)
lemma map_of_map2: "\x \ set xs. (fst (f x)) = (fst x) \
map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
by (induct xs, auto)
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
