Theory Contrib

(*  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