Theory Auxiliary

(*  Title:      Jinja/Common/Basis.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 TU Muenchen
*)

chapter ‹Jinja Source Language \label{cha:j}›

section ‹Auxiliary Definitions›

theory Auxiliary imports Main begin
(* FIXME move and possibly turn into a general simproc *)
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 ‹‹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_append:
 "⟦ distinct_fst kxs'; distinct_fst kxs; ∀(k,x) ∈ set kxs. ∀(k',x') ∈ set kxs'. k' ≠ k ⟧
  ⟹ distinct_fst(kxs @ kxs')"
by (induct kxs) (auto dest: fst_in_set_lemma)

lemma distinct_fst_map_inj:
  "⟦ distinct_fst kxs; inj f ⟧ ⟹ distinct_fst (map (λ(k,x). (f k, g k x)) kxs)"
by (induct kxs) (auto dest: fst_in_set_lemma simp: inj_eq)
*)

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

end