Theory Aux

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

header {* \isaheader{Auxiliary Definitions} *}

theory Aux
imports Main 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 *)
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  ("(⌊_⌋)")

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 (simp add:append_eq_append_conv2)
  apply (auto simp:in_set_conv_decomp)
     apply (subgoal_tac "hd (us @ C'#Ds') = C'")
      apply (case_tac us)
       apply simp
      apply fastsimp
     apply simp
    apply (subgoal_tac "hd (us @ C'#Ds') = C'")
     apply (case_tac us)
      apply simp
     apply fastsimp
    apply simp
   apply (subgoal_tac "hd (us @ C'#Cs') = C'")
    apply (case_tac us)
     apply simp
    apply fastsimp
   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 fastsimp
  apply (subgoal_tac "hd(C'#Ds') = C'")
   apply simp
  apply (simp (no_asm))
  done


constdefs
  pick ::"'a set => 'a"
  "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)


constdefs
  set2list :: "'a set => 'a list"
  "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)



section {*@{text distinct_fst}*}
 
constdefs
  distinct_fst  :: "('a × 'b) list => bool"
  "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 map_of_SomeI:
  "[| distinct_fst kxs; (k,x) ∈ set kxs |] ==> map_of kxs k = Some x"
by (induct kxs) (auto simp:fun_upd_apply)


section {* Using @{term list_all2} for relations *}

constdefs
  fun_of :: "('a × 'b) set => 'a => 'b => bool"
  "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