Theory Auxiliary
chapter ‹ Jinja Source Language \label{cha:j} ›
section ‹ Auxiliary Definitions ›
theory Auxiliary imports Main begin
lemma nat_add_max_le[simp]:
"((n::nat) + max i j ≤ m) = (n + i ≤ m ∧ n + j ≤ m)"
by arith
lemma Suc_add_max_le[simp]:
"(Suc(n + max i j) ≤ m) = (Suc(n + i) ≤ m ∧ Suc(n + j) ≤ m)"
by arith
notation Some (‹(⌊_⌋)›)
declare
option.splits[split]
Let_def[simp]
subset_insertI2 [simp]
Cons_eq_map_conv [iff]
subsection ‹@{text distinct_fst}›
definition distinct_fst :: "('a × 'b) list ⇒ bool"
where
"distinct_fst ≡ distinct ∘ map fst"
lemma distinct_fst_Nil [simp]:
"distinct_fst []"
by (unfold distinct_fst_def) (simp (no_asm))
lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
by (unfold distinct_fst_def) (auto simp:image_def)
lemma distinct_fst_appendD:
"distinct_fst(kxs @ kxs') ⟹ distinct_fst kxs ∧ distinct_fst kxs'"
by(induct kxs, auto)
lemma map_of_SomeI:
"⟦ distinct_fst kxs; (k,x) ∈ set kxs ⟧ ⟹ map_of kxs k = Some x"
by (induct kxs) (auto simp:fun_upd_apply)
subsection ‹ Using @{term list_all2} for relations ›
definition fun_of :: "('a × 'b) set ⇒ 'a ⇒ 'b ⇒ bool"
where
"fun_of S ≡ λx y. (x,y) ∈ S"
text ‹ Convenience lemmas ›
declare fun_of_def [simp]
lemma rel_list_all2_Cons [iff]:
"list_all2 (fun_of S) (x#xs) (y#ys) =
((x,y) ∈ S ∧ list_all2 (fun_of S) xs ys)"
by simp
lemma rel_list_all2_Cons1:
"list_all2 (fun_of S) (x#xs) ys =
(∃z zs. ys = z#zs ∧ (x,z) ∈ S ∧ list_all2 (fun_of S) xs zs)"
by (cases ys) auto
lemma rel_list_all2_Cons2:
"list_all2 (fun_of S) xs (y#ys) =
(∃z zs. xs = z#zs ∧ (z,y) ∈ S ∧ list_all2 (fun_of S) zs ys)"
by (cases xs) auto
lemma rel_list_all2_refl:
"(⋀x. (x,x) ∈ S) ⟹ list_all2 (fun_of S) xs xs"
by (simp add: list_all2_refl)
lemma rel_list_all2_antisym:
"⟦ (⋀x y. ⟦(x,y) ∈ S; (y,x) ∈ T⟧ ⟹ x = y);
list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs ⟧ ⟹ xs = ys"
by (rule list_all2_antisym) auto
lemma rel_list_all2_trans:
"⟦ ⋀a b c. ⟦(a,b) ∈ R; (b,c) ∈ S⟧ ⟹ (a,c) ∈ T;
list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs⟧
⟹ list_all2 (fun_of T) as cs"
by (rule list_all2_trans) auto
lemma rel_list_all2_update_cong:
"⟦ i<size xs; list_all2 (fun_of S) xs ys; (x,y) ∈ S ⟧
⟹ list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"
by (simp add: list_all2_update_cong)
lemma rel_list_all2_nthD:
"⟦ list_all2 (fun_of S) xs ys; p < size xs ⟧ ⟹ (xs!p,ys!p) ∈ S"
by (drule list_all2_nthD) auto
lemma rel_list_all2I:
"⟦ length a = length b; ⋀n. n < length a ⟹ (a!n,b!n) ∈ S ⟧ ⟹ list_all2 (fun_of S) a b"
by (erule list_all2_all_nthI) simp
declare fun_of_def [simp del]
subsection ‹ Auxiliary properties of @{text "map_of"} function ›
lemma map_of_set_pcs_notin: "C ∉ (λt. snd (fst t)) ` set FDTs ⟹ map_of FDTs (F, C) = None"
by (metis image_eqI image_image map_of_eq_None_iff snd_conv)
lemma map_of_insertmap_SomeD':
"map_of fs F = Some y ⟹ map_of (map (λ(F, y). (F, D, y)) fs) F = Some(D,y)"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_reinsert_neq_None:
"Ca ≠ D ⟹ map_of (map (λ(F, y). ((F, Ca), y)) fs) (F, D) = None"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_remap_insertmap:
"map_of (map ((λ((F, D), b, T). (F, D, b, T)) ∘ (λ(F, y). ((F, D), y))) fs)
= map_of (map (λ(F, y). (F, D, y)) fs)"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_reinsert_SomeD:
"map_of (map (λ(F, y). ((F, D), y)) fs) (F, D) = Some T ⟹ map_of fs F = Some T"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_filtered_SomeD:
"map_of fs (F,D) = Some (a, T) ⟹ Q ((F,D),a,T) ⟹
map_of (map (λ((F,D), b, T). ((F,D), P T)) (filter Q fs))
(F,D) = Some (P T)"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_remove_filtered_SomeD:
"map_of fs (F,C) = Some (a, T) ⟹ Q ((F,C),a,T) ⟹
map_of (map (λ((F,D), b, T). (F, P T)) [((F, D), b, T)←fs . Q ((F, D), b, T) ∧ D = C])
F = Some (P T)"
by (induct fs) (auto simp:fun_upd_apply split: if_split_asm)
lemma map_of_Some_None_split:
assumes "t = map (λ(F, y). ((F, C), y)) fs @ t'" "map_of t' (F, C) = None" "map_of t (F, C) = Some y"
shows "map_of (map (λ((F, D), b, T). (F, D, b, T)) t) F = Some (C, y)"
proof -
have "map_of (map (λ(F, y). ((F, C), y)) fs) (F, C) = Some y" using assms by auto
then have "∀p. map_of fs F = Some p ∨ Some y ≠ Some p"
by (metis map_of_reinsert_SomeD)
then have "∀f b p pa. ((f ++ map_of (map (λ(a, p). (a, b::'b, p)) fs)) F = Some p ∨ Some (b, pa) ≠ Some p)
∨ Some y ≠ Some pa"
by (metis (no_types) map_add_find_right map_of_insertmap_SomeD')
then have "(map_of (map (λ((a, b), c, d). (a, b, c, d)) t')
++ map_of (map (λ(a, p). (a, C, p)) fs)) F = Some (C, y)"
by blast
then have "(map_of (map (λ((a, b), c, d). (a, b, c, d)) t')
++ map_of (map ((λ((a, b), c, d). (a, b, c, d)) ∘ (λ(a, y). ((a, C), y))) fs)) F = Some (C, y)"
by (simp add: map_of_remap_insertmap)
then show ?thesis using assms by auto
qed
end