Theory Aux (Isabelle2009-1: December 2009)

(*  Title:      JinjaThreads/Common/Aux.thy
    Author:     Andreas Lochbihler, David von Oheimb, Tobias Nipkow

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

header {* 
  \isaheader{Auxiliary Definitions and Lemmata}
*}

theory Aux 
imports
  Main
  "../../FinFun/FinFun"
  "Transitive_Closure_Table"
  Code_Char
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]
(*>*)


subsection {*@{text distinct_fst}*}
 
definition
  distinct_fst  :: "('a × 'b) list => bool"
where
  "distinct_fst  ≡  distinct o map fst"

lemma distinct_fst_Nil [simp]:
  "distinct_fst []"
 (*<*)
apply (unfold distinct_fst_def)
apply (simp (no_asm))
done
(*>*)

lemma distinct_fst_Cons [simp]:
  "distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
(*<*)
apply (unfold distinct_fst_def)
apply (auto simp:image_def)
done
(*>*)

lemma distinct_fstD: "[| distinct_fst xs; (x, y) ∈ set xs; (x, z) ∈ set xs |] ==> y = z"
by(induct xs) 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](*>*)


fun flatten :: "'a list list => 'a list" ("\<down>_\<down>" [50] 80)
where
  "flatten [] = []"
| "flatten (xs # xss) = xs @ flatten xss"

lemma set_flatten_Union_set [simp]:
  "set (flatten xs) = Union (set (map set xs))"
by(induct xs, auto)

lemma flatten_append [simp]: "flatten (xs @ ys) = flatten xs @ flatten ys"
by(induct xs, auto)


lemma f_nth_set:
  "[| f (xs ! n) = v; n < length xs |] ==> v ∈ f ` set xs"
apply(induct xs arbitrary: n)
 apply(simp)
apply(case_tac "n")
apply(auto)
done


lemma map_eq_imp_length_eq': 
  "map f xs = map g ys ==> length xs = length ys"
apply(induct xs arbitrary: ys)
 apply(simp)
apply(auto simp add: Cons_eq_map_conv)
done


lemma replicate_eq_append_conv: 
  "(replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n-m) x)"
proof(induct n arbitrary: xs ys)
  case 0 thus ?case by simp
next
  case (Suc n xs ys)
  have IH: "!!xs ys. (replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n - m) x)" by fact
  show ?case
  proof(unfold replicate_Suc, rule iffI)
    assume a: "x # replicate n x = xs @ ys"
    show "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
    proof(cases xs)
      case Nil
      thus ?thesis using a
        by(auto)
    next
      case (Cons X XS)
      with a have x: "x = X" and "replicate n x = XS @ ys" by auto
      hence "∃m≤n. XS = replicate m x ∧ ys = replicate (n - m) x"
        by -(rule IH[THEN iffD1])
      then obtain m where "m ≤ n" and XS: "XS = replicate m x" and ys: "ys = replicate (n - m) x" by blast
      with x Cons show ?thesis
        by(fastsimp)
    qed
  next
    assume "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
    then obtain m where m: "m ≤ Suc n" and xs: "xs = replicate m x" and ys: "ys = replicate (Suc n - m) x" by blast
    thus "x # replicate n x = xs @ ys"
      by(simp add: replicate_add[THEN sym])
  qed
qed

lemma map_eq_append_conv:
  "map f xs = ys @ zs <-> (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
apply(rule iffI)
 apply(metis append_eq_conv_conj append_take_drop_id assms drop_map take_map)
by(clarsimp)

lemma append_eq_map_conv:
  "ys @ zs = map f xs <-> (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
unfolding map_eq_append_conv[symmetric]
by auto

lemma map_eq_map_conv:
  "map f xs = map g ys <-> list_all2 (λx y. f x = g y) xs ys"
apply(induct xs arbitrary: ys)
apply(auto simp add: list_all2_Cons1 Cons_eq_map_conv)
done

lemma map_upd_map_add: "X(V \<mapsto> v) = (X ++ [V \<mapsto> v])"
by(simp)

lemma Collect_eq_singleton_conv:
  "{a. P a} = {a} <-> P a ∧ (∀a'. P a' --> a = a')"
by(auto)

lemmas filter_replicate_conv = filter_replicate

lemma if_else_if_else_eq_if_else [simp]:
  "(if b then x else if b then y else z) = (if b then x else z)"
by(simp)

lemma disjE3: "[| P ∨ Q ∨ R; P ==> S; Q ==> S; R ==> S |] ==> S"
by auto

lemma length_greater_Suc_0_conv: "Suc 0 < length xs <-> (∃x x' xs'. xs = x # x' # xs')"
by(cases xs, auto simp add: neq_Nil_conv)

lemmas zip_same_conv = zip_same_conv_map

lemma map_eq_all_nth_conv:
  "map f xs = ys <-> length xs = length ys ∧ (∀n < length xs. f (xs ! n) = ys ! n)"
apply(induct xs arbitrary: ys)
apply(fastsimp simp add: nth_Cons Suc_length_conv split: nat.splits)+
done

lemma nth_Cons_subtract: "0 < n ==> (x # xs) ! n = xs ! (n - 1)"
by(auto simp add: nth_Cons split: nat.split)

lemma prod_rec_split [simp]: "prod_rec = split"
by(simp add: expand_fun_eq)

lemma rtranclp_False [simp]: "(λa b. False)^*^* = op ="
by(auto simp add: expand_fun_eq elim: rtranclp_induct)

lemmas rtranclp_induct3 =
  rtranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct3 =
  tranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas rtranclp_induct4 =
  rtranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct4 =
  tranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemma converse_tranclpE:
  assumes "tranclp r x z"
  obtains (base) "r x z"
        | (step) y where "r x y" "tranclp r y z"
using tranclpD[OF assms]
by(blast elim: converse_rtranclpE dest: rtranclp_into_tranclp2)

lemmas converse_tranclp_induct2 =
  converse_tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,
                 consumes 1, case_names base step]

lemma wfP_induct' [consumes 1, case_names wfP]:
  "[|wfP r; !!x. (!!y. r y x ==> P y) ==> P x|] ==> P a"
by(blast intro: wfP_induct)

lemma wfP_induct2 [consumes 1, case_names wfP]:
  "[|wfP r; !!x x'. (!!y y'. r (y, y') (x, x') ==> P y y') ==> P x x' |] ==> P x x'"
by(drule wfP_induct'[where P="λ(x, y). P x y"]) blast+

lemma wfP_minimalE:
  assumes "wfP r"
  and "P x"
  obtains z where "P z" "r^** z x" "!!y. r y z ==> ¬ P y"
proof -
  let ?Q = "λx'. P x' ∧ r^** x' x"
  from `P x` have "?Q x" by blast
  from `wfP r` have "!!Q. x ∈ Q --> (∃z∈Q. ∀y. r y z --> y ∉ Q)"
    unfolding wfP_eq_minimal by blast
  from this[rule_format, of ?Q] `?Q x`
  obtain z where "?Q z" and min: "!!y. r y z ==> ¬ ?Q y" by(auto simp add: mem_def)
  from `?Q z` have "P z" "r^** z x" by auto
  moreover
  { fix y
    assume "r y z"
    hence "¬ ?Q y" by(rule min)
    moreover from `r y z` `r^** z x` have "r^** y x"
      by(rule converse_rtranclp_into_rtranclp)
    ultimately have "¬ P y" by blast }
  ultimately show thesis ..
qed

subsection {* reflexive transitive closure for label relations *}

inductive converse3p :: "('a => 'b => 'c => bool) => 'c => 'b => 'a => bool"
  for r :: "'a => 'b => 'c => bool"
where
  converse3pI: "r a b c ==> converse3p r c b a"

lemma converse3p_converse3p: "converse3p (converse3p r) = r"
by(auto intro: converse3pI intro!: ext elim: converse3p.cases)

lemma converse3pD: "converse3p r c b a ==> r a b c"
by(auto elim: converse3p.cases)

inductive rtrancl3p :: "('a => 'b => 'a => bool) => 'a => 'b list => 'a => bool"
  for r :: "'a => 'b => 'a => bool"
  where 
  rtrancl3p_refl [intro!, simp]: "rtrancl3p r a [] a"
| rtrancl3p_step: "[| rtrancl3p r a bs a'; r a' b a'' |] ==> rtrancl3p r a (bs @ [b]) a''"

lemmas rtrancl3p_induct3 =
  rtrancl3p.induct[of _ "(ax,ay,az)" _ "(cx,cy,cz)", split_format (complete),
                 consumes 1, case_names refl step]

lemmas rtrancl3p_induct4 = 
  rtrancl3p.induct[of _ "(ax,ay,az,aw)" _ "(cx,cy,cz,cw)", split_format (complete),
                 consumes 1, case_names refl step]

lemma rtrancl3p_induct4' [consumes 1, case_names refl step]:
  assumes major: "rtrancl3p r (ax, (ay, az), aw) bs (cx, (cy, cz), cw)"
  and refl: "!!a aa b ba. P a aa b ba [] a aa b ba"
  and step: "!!a aa b ba bs ab ac bb bc bd ad ae be bf.
       [| rtrancl3p r (a, (aa, b), ba) bs (ab, (ac, bb), bc);
         P a aa b ba bs ab ac bb bc; r (ab, (ac, bb), bc) bd (ad, (ae, be), bf) |]
       ==> P a aa b ba (bs @ [bd]) ad ae be bf"
  shows "P ax ay az aw bs cx cy cz cw"
using major
apply -
apply(drule_tac P="λ(a, (aa, b), ba) bs (cx, (cy, cz), cw). P a aa b ba bs cx cy cz cw" in rtrancl3p.induct)
by(auto intro: refl step)

lemma rtrancl3p_induct1:
  "[| rtrancl3p r a bs c; P a; !!bs c b d. [| rtrancl3p r a bs c; r c b d; P c |] ==> P d |] ==> P c"
apply(induct rule: rtrancl3p.induct)
apply(auto)
done

lemma rtrancl3p_trans [trans]:
  assumes one: "rtrancl3p r a bs a'"
  and two: "rtrancl3p r a' bs' a''"
  shows "rtrancl3p r a (bs @ bs') a''"
using two one
proof(induct rule: rtrancl3p.induct)
  case rtrancl3p_refl thus ?case by simp
next
  case rtrancl3p_step thus ?case
    by(auto simp only: append_assoc[symmetric] intro: rtrancl3p.rtrancl3p_step)
qed

lemma rtrancl3p_step_converse:
  assumes step: "r a b a'"
  and stepify: "rtrancl3p r a' bs a''"
  shows "rtrancl3p r a (b # bs) a''"
using stepify step
proof(induct rule: rtrancl3p.induct)
  case rtrancl3p_refl 
  with rtrancl3p.rtrancl3p_refl[where r=r and a=a] show ?case 
    by(auto dest: rtrancl3p.rtrancl3p_step simp del: rtrancl3p.rtrancl3p_refl)
next
  case rtrancl3p_step thus ?case
    unfolding append_Cons[symmetric]
    by -(rule rtrancl3p.rtrancl3p_step)
qed

lemma converse_rtrancl3p_step:
  "rtrancl3p r a (b # bs) a'' ==> ∃a'. r a b a' ∧ rtrancl3p r a' bs a''"
apply(induct bs arbitrary: a'' rule: rev_induct)
 apply(erule rtrancl3p.cases)
  apply(clarsimp)+
 apply(erule rtrancl3p.cases)
  apply(clarsimp)
  apply(rule_tac x="a''a" in exI)
  apply(clarsimp)
 apply(clarsimp)
apply(erule rtrancl3p.cases)
 apply(clarsimp)
apply(clarsimp)
by(fastsimp intro: rtrancl3p_step)

lemma converse_rtrancl3pD:
  "rtrancl3p (converse3p r) a' bs a ==> rtrancl3p r a (rev bs) a'"
apply(induct rule: rtrancl3p.induct)
 apply(fastsimp intro: rtrancl3p.intros)
apply(auto dest: converse3pD intro: rtrancl3p_step_converse)
done

lemma rtrancl3p_converseD:
  "rtrancl3p r a bs a' ==> rtrancl3p (converse3p r) a' (rev bs) a"
proof(induct rule: rtrancl3p.induct)
  case rtrancl3p_refl thus ?case
    by(auto intro: rtrancl3p.intros)
next
  case rtrancl3p_step thus ?case
    by(auto intro: rtrancl3p_step_converse converse3p.intros)
qed

lemma rtrancl3p_converse_induct [consumes 1, case_names refl step]:
  assumes ih: "rtrancl3p r a bs a''"
  and refl: "!!a. P a [] a"
  and step: "!!a b a' bs a''. [| rtrancl3p r a' bs a''; r a b a'; P a' bs a'' |] ==> P a (b # bs) a''"
  shows "P a bs a''"
  using ih
proof(induct bs arbitrary: a a'')
  case Nil thus ?case
    by(auto elim: rtrancl3p.cases intro: refl)
next
  case Cons thus ?case
    by(auto dest!: converse_rtrancl3p_step intro: step)
qed  

lemma rtrancl3p_converse_induct' [consumes 1, case_names refl step]:
  assumes ih: "rtrancl3p r a bs a''"
  and refl: "P a'' []"
  and step: "!!a b a' bs. [| rtrancl3p r a' bs a''; r a b a'; P a' bs |] ==> P a (b # bs)"
  shows "P a bs"
using rtrancl3p_converse_induct[OF ih, where P="λa bs a'. a' = a'' --> P a bs"]
by(auto intro: refl step)

lemma rtrancl3p_converseE[consumes 1, case_names refl step]:
  "[| rtrancl3p r a bs a'';
     [| a = a''; bs = [] |] ==> thesis;
     !!bs' b a'. [| bs = b # bs'; r a b a'; rtrancl3p r a' bs' a'' |] ==> thesis |]
  ==> thesis"
by(induct rule: rtrancl3p_converse_induct)(auto)


lemma rtrancl3p_induct' [consumes 1, case_names refl step]:
  assumes major: "rtrancl3p r a bs c"
  and refl: "P a [] a"
  and step: "!!bs a' b a''. [| rtrancl3p r a bs a'; P a bs a'; r a' b a'' |]
             ==> P a (bs @ [b]) a''"
  shows "P a bs c"
proof -
  from major have "(P a [] a ∧ (∀bs a' b a''. rtrancl3p r a bs a' ∧ P a bs a' ∧ r a' b a'' --> P a (bs @ [b]) a'')) --> P a bs c"
    by-(erule rtrancl3p.induct, blast+)
  with refl step show ?thesis by blast
qed



lemma list_all2_induct[consumes 1, case_names Nil Cons]:
  assumes major: "list_all2 P xs ys"
  and Nil: "Q [] []"
  and Cons: "!!x xs y ys. [| P x y; Q xs ys |] ==> Q (x # xs) (y # ys)"
  shows "Q xs ys"
using major
by(induct xs arbitrary: ys)(auto simp add: list_all2_Cons1 Nil intro!: Cons)

lemma list_all2_split:
  assumes major: "list_all2 P xs ys"
  and split: "!!x y. P x y ==> ∃z. Q x z ∧ R z y"
  shows "∃zs. list_all2 Q xs zs ∧ list_all2 R zs ys"
using major
by(induct rule: list_all2_induct)(auto dest: split)

subsection {* Concatenation for @{typ String.literal} *}

definition concat :: "String.literal list => String.literal"
where [code del]: "concat xs = implode (List.concat (map explode xs))"

code_const concat
  (SML "String.concat")
  (Haskell "concat")
  (OCaml "String.concat \"\"")

hide (open) const concat

lemma map_le_SomeD: "[| m ⊆_m m'; m x = ⌊y⌋ |] ==> m' x = ⌊y⌋"
by(auto simp add: map_le_def dest: bspec)

lemma take_eq_take_le_eq:
  "[| take n xs = take n ys; m ≤ n |] ==> take m xs = take m ys"
by(metis min_max.le_iff_inf take_take)

lemma take_list_update_beyond:
  "n ≤ m ==> take n (xs[m := x]) = take n xs"
by(cases "n ≤ length xs")(rule nth_take_lemma, simp_all)

lemma nat_fun_sum_eq_conv:
  fixes f :: "'a => nat"
  shows "(λa. f a + g a) = (λa. 0) <-> f = (λa .0) ∧ g = (λa. 0)"
by(auto simp add: expand_fun_eq)

end