Theory JinjaDCI.Auxiliary

(*  Title:      JinjaDCI/Common/Auxiliary.thy

    Author:     David von Oheimb, Tobias Nipkow, Susannah Mansky
    Copyright   1999 TU Muenchen, 2019-20 UIUC

    Based on the Jinja theory Common/Auxiliary.thy by David von Oheimb and Tobias Nipkow
*)

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 @{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