(*  Title:      statecharts/DataSpace/Contrib.thy
    Author:     Steffen Helke and Florian Kammüller, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Contributions to the Standard Library of HOL›

theory Contrib
imports Main "HOL-Library.FuncSet"
begin

subsection ‹Basic definitions and lemmas›

subsubsection ‹Maps›                  

definition chg_map :: "('b => 'b) => 'a => ('a ⇀ 'b) => ('a ⇀ 'b)" where  
 "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"

lemma map_some_list [simp]:
   "map the (map Some L) = L"
apply (induct_tac L)
apply auto
done

lemma dom_ran_the:
  "[ ran G = {y}; x ∈ (dom G) ] ==> (the (G x)) = y"
apply (unfold ran_def dom_def)
apply auto
done

lemma dom_None:
  "(S ∉ dom F) ==> (F S = None)"
by (unfold dom_def, auto)

lemma ran_dom_the:
  "[ y ∉ Union (ran G); x ∈ dom G ] ==> y ∉ the (G x)"
by (unfold ran_def dom_def, auto)

lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
apply auto
done

subsubsection ‹‹rtrancl››

lemma rtrancl_Int:
 "[ (a,b) ∈ A; (a,b) ∈ B ] ==> (a,b) ∈ (A ∩ B)^*"
by auto

lemma rtrancl_mem_Sigma:
 "[ a ≠ b; (a, b) ∈ (A × A)^* ] ==> b ∈ A"
apply (frule rtranclD)
apply (cut_tac r="A × A" and A=A in trancl_subset_Sigma)
apply auto
done

lemma help_rtrancl_Range:
 "[ a ≠ b; (a,b) ∈ R ^* ] ==> b ∈ Range R"
apply (erule rtranclE)
apply auto
done

lemma rtrancl_Int_help:
  "(a,b) ∈ (A ∩ B) ^* ==> (a,b) ∈ A^* ∧ (a,b) ∈ B^*"
apply (unfold Int_def)
apply auto
apply (rule_tac b=b in rtrancl_induct)
apply auto
apply (rule_tac b=b in rtrancl_induct)
apply auto
done

lemmas rtrancl_Int1 = rtrancl_Int_help [THEN conjunct1]
lemmas rtrancl_Int2 = rtrancl_Int_help [THEN conjunct2]

lemma tranclD3 [rule_format]:
  "(S,T) ∈ R^+ ==> (S,T) ∉ R ⟶ (∃ U. (S,U) ∈ R ∧ (U,T) ∈ R^+)"
apply (rule_tac a="S" and b="T" and r=R in trancl_induct)
apply auto
done

lemma tranclD4 [rule_format]:
  "(S,T) ∈ R^+ ==> (S,T) ∉ R ⟶ (∃ U. (S,U) ∈ R^+ ∧ (U,T) ∈ R)"
apply (rule_tac a="S" and b="T" and r=R in trancl_induct)
apply auto
done

lemma trancl_collect [rule_format]:
  "[ (x,y) ∈ R^*; S ∉ Domain R ] ==> y ≠ S ⟶ (x,y) ∈ {p. fst p ≠ S ∧ snd p ≠ S ∧ p ∈ R}^*"
apply (rule_tac b=y in rtrancl_induct)
apply auto
apply (rule rtrancl_into_rtrancl)
apply fast
apply auto
done

lemma trancl_subseteq:
  "[ R ⊆ Q; S ∈ R^* ] ==> S ∈ Q^*"
apply (frule rtrancl_mono)
apply fast
done

lemma trancl_Int_subset:
   "(R ∩ (A × A))⁺ ⊆ R⁺ ∩ (A × A)"
apply (rule subsetI) 
apply (rename_tac S)
apply (case_tac "S")
apply (rename_tac T V)
apply auto
apply (rule_tac a=T and b=V and r="(R ∩ A × A)" in converse_trancl_induct, auto)+
done

lemma trancl_Int_mem:
   "(S,T) ∈ (R ∩ (A × A))⁺ ==> (S,T) ∈ R⁺ ∩ A × A"
by (rule trancl_Int_subset [THEN subsetD], assumption)

lemma Int_expand: 
  "{(S,S'). P S S' ∧ Q S S'} = ({(S,S'). P S S'} ∩ {(S,S'). Q S S'})"
by auto

subsubsection ‹‹finite››

lemma finite_conj:  
 "finite ({(S,S'). P S S'}::(('a*'b)set)) ⟶
     finite {(S,S'). P (S::'a) (S'::'b) ∧ Q (S::'a) (S'::'b)}"
apply (rule impI)
apply (subst Int_expand)
apply (rule finite_Int)
apply auto
done

lemma finite_conj2:
  "[ finite A; finite B ] ==> finite ({(S,S'). S: A ∧ S' : B})"
by auto

subsubsection ‹‹override››

lemma dom_override_the:
  "(x ∈ (dom G2)) ⟶ ((G1 ++ G2) x) = (G2 x)"
by (auto)

lemma dom_override_the2 [simp]:
  "[ dom G1 ∩ dom G2 = {}; x ∈ (dom G1) ] ==> ((G1 ++ G2) x) = (G1 x)"
apply (unfold dom_def map_add_def)
apply auto
apply (drule sym)
apply (erule equalityE)
apply (unfold Int_def)
apply auto
apply (erule_tac x=x in allE)
apply auto
done 

lemma dom_override_the3 [simp]:
  "[ x ∉ dom G2; x ∈ dom G1 ] ==> ((G1 ++ G2) x) = (G1 x)"
apply (unfold dom_def map_add_def)
apply auto
done

lemma Union_ran_override [simp]:
  "S ∈ dom G ==> ∪ (ran (G ++ Map.empty(S ↦ insert SA (the(G S))))) =
   (insert SA (Union (ran G)))"
apply (unfold dom_def ran_def)
apply auto
apply (rename_tac T)
apply (case_tac "T = S")
apply auto
done

lemma Union_ran_override2 [simp]:
  "S ∈ dom G ==> ∪ (ran (G(S ↦ insert SA (the(G S))))) = (insert SA (Union (ran G)))"
apply (unfold dom_def ran_def)
apply auto
apply (rename_tac T)
apply (case_tac "T = S")
apply auto
done

lemma ran_override [simp]:
  "(dom A ∩ dom B) = {} ==> ran (A ++ B) = (ran A) ∪ (ran B)"
apply (unfold Int_def ran_def)
apply (simp add: map_add_Some_iff)
apply auto
done

lemma chg_map_new [simp]:
  "m a = None ==> chg_map f a m = m"
by (unfold chg_map_def, auto)

lemma chg_map_upd [simp]:
  "m a = Some b ==> chg_map f a m = m(a|->f b)"
by (unfold chg_map_def, auto)

lemma ran_override_chg_map:
  "A ∈ dom G ==> ran (G ++ Map.empty(A|->B)) = (ran (chg_map (λ x. B) A G))"
apply (unfold dom_def ran_def)
apply (subst map_add_Some_iff [THEN ext])
apply auto
apply (rename_tac T)
apply (case_tac "T = A")
apply auto
done

subsubsection ‹‹Part››

definition  Part :: "['a set, 'b => 'a] => 'a set" where
            "Part A h = A ∩ {x. ∃ z. x = h(z)}"
 

lemma Part_UNIV_Inl_comp: 
 "((Part UNIV (Inl o f)) = (Part UNIV (Inl o g))) = ((Part UNIV f) = (Part UNIV g))"
apply (unfold Part_def)
apply auto
apply (erule equalityE)
apply (erule subsetCE)
apply auto
apply (erule equalityE)
apply (erule subsetCE)
apply auto
done

lemma Part_eqI [intro]: "[ a ∈ A; a=h(b) ] ==> a ∈ Part A h"
by (auto simp add: Part_def)

lemmas PartI = Part_eqI [OF _ refl]

lemma PartE [elim!]: "[ a ∈ Part A h; !!z. [ a ∈ A; a=h(z) ] ==> P ] ==> P"
by (auto simp add: Part_def)

lemma Part_subset: "Part A h ⊆ A"
by (auto simp add: Part_def)

lemma Part_mono: "A ⊆ B ==> Part A h ⊆ Part B h"
by blast

lemmas basic_monos = basic_monos Part_mono

lemma PartD1: "a ∈ Part A h ==> a ∈ A"
by (simp add: Part_def)

lemma Part_id: "Part A (λ x. x) = A"
by blast

lemma Part_Int: "Part (A ∩ B) h = (Part A h) ∩ (Part B h)"
by blast

lemma Part_Collect: "Part (A ∩ {x. P x}) h = (Part A h) ∩ {x. P x}"
by blast

subsubsection ‹Set operators›

lemma subset_lemma:
  "[ A ∩ B = {}; A ⊆ B ] ==> A = {}"
by auto

lemma subset_lemma2:
 "[ B ∩ A = {}; C ⊆ A ] ==> C ∩ B = {}"
by auto

lemma insert_inter:
  "[ a ∉ A; (A ∩ B) = {} ] ==> (A ∩ (insert a B)) = {}"
by auto

lemma insert_notmem:
  "[ a ≠ b; a ∉ B ] ==> a ∉ (insert b B)"
by auto

lemma insert_union:
 "A ∪ (insert a B) = insert a A ∪ B"
by auto

lemma insert_or:
     "{s. s = t1 ∨ (P s)} = insert t1 {s. P s }"
by auto

lemma Collect_subset: 
  "{x . x ⊆ A ∧ P x} = {x ∈ Pow A. P x}"
by auto

lemma OneElement_Card [simp]:
  "[ finite M; card M <= Suc 0; t ∈ M ] ==> M = {t}"
apply auto
apply (rename_tac s)
apply (rule_tac P="finite M" in mp)
apply (rule_tac P="card M <= Suc 0" in mp)
apply (rule_tac P="t ∈ M" in mp)
apply (rule_tac F="M" in finite_induct)
apply auto
apply (rule_tac P="finite M" in mp)
apply (rule_tac P="card M <= Suc 0" in mp)
apply (rule_tac P="s ∈ M" in mp)
apply (rule_tac P="t ∈ M" in mp)
apply (rule_tac F="M" in finite_induct)
apply auto
done 
  
subsubsection ‹One point rule›

lemma Ex1_one_point [simp]: 
  "(∃! x. P x ∧ x = a) = P a"
by auto

lemma Ex1_one_point2 [simp]:
  "(∃! x. P x ∧ Q x ∧ x = a) = (P a ∧ Q a)"
by auto

lemma Some_one_point [simp]:
 "P a ==> (SOME x. P x ∧ x = a) = a"
by auto

lemma Some_one_point2 [simp]:
 "[ Q a; P a ] ==> (SOME x. P x ∧ Q x ∧ x = a) = a"
by auto

end