Theory AuxLemmas

theory AuxLemmas
imports JBasis
(*  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 auto
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 (λz. z ≠ x) xs) := v] =
map (f(x:=v)) xs"

apply (induct xs)
apply simp
apply (case_tac "x=a")
apply auto
done


(**********************************************************************)
(* Product_Type.thy *)
(**********************************************************************)


lemma split_compose: "(split f) o (λ (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 o f(x\<mapsto>v)) = (the o 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 o f(y\<mapsto>v)) xs = map (the o f) xs"
by (simp add: the_map_upd)

lemma map_map_upds [simp]:
"(∀y∈set ys. y ∉ set xs) ==> map (the o f(ys[\<mapsto>]vs)) xs = map (the o f) xs"
apply (induct xs arbitrary: f vs)
apply simp
apply fastforce
done

lemma map_upds_distinct [simp]:
"distinct ys ==> length ys = length vs ==> map (the o f(ys[\<mapsto>]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) = empty (map f zs [\<mapsto>] map g zs)"
by (induct zs) auto

(* In analogy to Map.map_of_SomeD *)
lemma map_upds_SomeD [rule_format (no_asm)]:
"∀ m ys. (m(xs[\<mapsto>]ys)) k = Some y --> k ∈ (set xs) ∨ (m k = Some y)"
apply (induct xs)
apply simp
apply auto
apply(case_tac ys)
apply auto
done

lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y
==> k ∈ (set (xs @ map fst m))"

by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)


lemma map_of_map_prop [rule_format (no_asm)]:
"(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)

lemma map_of_map2: "∀ x ∈ set xs. (fst (f x)) = (fst x) ==>
map_of (map f xs) a = Option.map (λ b. (snd (f (a, b)))) (map_of xs a)"

by (induct xs, auto)

lemma option_map_of [simp]: "(Option.map f (map_of xs k) = None) = ((map_of xs k) = None)"
by (simp add: Option.map_def split: option.split)



end