Quellcode-Bibliothek AuxLemmas.thy Sprache: Isabelle

(*  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

quality97%

¤ 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.0.11Bemerkung: ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.