# Theory Auxiliary

```(*  Title:       CoreC++
Author:      David von Oheimb, Tobias Nipkow, Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Auxiliary Definitions›

theory Auxiliary
imports Complex_Main "HOL-Library.While_Combinator"
begin

declare
option.splits[split]
Let_def[simp]
subset_insertI2 [simp]
Cons_eq_map_conv [iff]

(* FIXME move and possibly turn into a general simproc *)
"((n::nat) + max i j ≤ m) = (n + i ≤ m ∧ n + j ≤ m)"
by arith

"(Suc(n + max i j) ≤ m) = (Suc(n + i) ≤ m ∧ Suc(n + j) ≤ m)"
by arith

notation Some  ("(⌊_⌋)")

lemma butlast_tail:
"butlast (Xs@[X,Y]) = Xs@[X]"
by (induct Xs) auto

lemma butlast_noteq:"Cs ≠ [] ⟹ butlast Cs ≠ Cs"
by(induct Cs)simp_all

lemma app_hd_tl:"⟦Cs ≠ []; Cs = Cs' @ tl Cs⟧ ⟹ Cs' = [hd Cs]"

apply (subgoal_tac "[hd Cs] @ tl Cs = Cs' @ tl Cs")
apply fast
apply simp
done

lemma only_one_append:"⟦C' ∉ set Cs; C' ∉ set Cs'; Ds@ C'#Ds' = Cs@ C'#Cs'⟧
⟹ Cs = Ds ∧ Cs' = Ds'"

apply -
apply (auto simp:in_set_conv_decomp)
apply (subgoal_tac "hd (us @ C'#Ds') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply simp
apply (subgoal_tac "hd (us @ C'#Ds') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply simp
apply (subgoal_tac "hd (us @ C'#Cs') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply (subgoal_tac "hd(C'#Ds') = C'")
apply simp
apply (simp (no_asm))
apply (subgoal_tac "hd (us @ C'#Cs') = C'")
apply (case_tac us)
apply simp
apply fastforce
apply (subgoal_tac "hd(C'#Ds') = C'")
apply simp
apply (simp (no_asm))
done

definition pick :: "'a set ⇒ 'a" where
"pick A ≡ SOME x. x ∈ A"

lemma pick_is_element:"x ∈ A ⟹ pick A ∈ A"
by (unfold pick_def,rule_tac x="x" in someI)

definition set2list :: "'a set ⇒ 'a list" where
"set2list A ≡ fst (while (λ(Es,S). S ≠ {})
(λ(Es,S). let x = pick S in (x#Es,S-{x}))
([],A) )"

lemma card_pick:"⟦finite A; A ≠ {}⟧ ⟹ Suc(card(A-{pick(A)})) = card A"
by (drule card_Suc_Diff1,auto dest!:pick_is_element simp:ex_in_conv)

lemma set2list_prop:"⟦finite A; A ≠ {}⟧ ⟹
∃xs. while (λ(Es,S). S ≠ {})
(λ(Es,S). let x = pick S in (x#Es,S-{x}))
([],A) = (xs,{}) ∧ (set xs ∪ {} = A)"

apply(rule_tac P="(λxs. (set(fst xs) ∪ snd xs = A))" and
r="measure (card o snd)"  in while_rule)
apply(auto dest:pick_is_element)
apply(auto dest:card_pick simp:ex_in_conv measure_def inv_image_def)
done

lemma set2list_correct:"⟦finite A; A ≠ {}; set2list A = xs⟧ ⟹ set xs = A"
by (auto dest:set2list_prop simp:set2list_def)

subsection ‹‹distinct_fst››

definition distinct_fst :: "('a × 'b) list ⇒ bool" where
"distinct_fst  ≡  distinct ∘ 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 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"

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])"