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
begin

subsection ‹Basic definitions and lemmas›

subsubsection ‹Lambda expressions›                  

definition restrict :: "['a => 'b, 'a set] => ('a => 'b)" where
 "restrict f A = (%x. if x : A then f x else (@ y. True))"

syntax (ASCII)
  "_lambda_in" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
syntax
  "_lambda_in" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3λ__./ _)" [0, 0, 3] 3)
translations 
  "λxA. f"  == "CONST restrict (%x. f) A"


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