(*  Title:      ISM/Basis.thy
    Id:         $Id: Basis.thy,v 1.27 2003/09/12 16:13:02 dvo Exp $
    Author:     David von Oheimb
    License:    (C) 2002 Siemens AG; any non-commercial use is granted

*)

(* header {* Minor extensions of HOL *} *)

theory Basis
imports Main
begin
(*<*)
ML {* Pretty.setmargin 169; quick_and_dirty:=false *}

(*
hide const "inputs"
hide const "outputs"

*)

declare O_assoc [simp]

declare fun_upd_idem_iff [simp] 
lemma o_fun_upd [simp]: "g \<circ> f(x:=y) = (g \<circ> f)(x:=g y)" 
by (rule ext, simp)

(* ####TO HOL/Fun.thy *)
constdefs 
  fun_upd_s :: "('a => 'b) => 'a set => 'b => ('a => 'b)"
                                              ("_/'(_{:=}_/')" [900,0,0] 900)
 "fun_upd_s f A b == %x. if x:A then b else f x" 

  chg_fun :: "('b => 'b) => 'a => ('a => 'b) => ('a => 'b)"
 "chg_fun f x g == g (x:=f (g x))"

lemma fun_upd_s_apply [simp]: "(f(A{:=}b)) x = (if x : A then b else f x)"
by (simp add: fun_upd_s_def)

(* TO HOL/Map.thy?* )
constdefs
  rev_image :: "('a ~=> 'b) => 'b => 'a set"
 "rev_image f b == {a. f a = Some b}"

constdefs
  dist_map :: "('a ~=> 'b * 'c) => ('a ~=> 'b ) * ('a ~=> 'c)"
 "dist_map m == (option_map fst o m, option_map snd o m)"

  graph :: "('a ~=> 'b) => ('a * 'b) set"
 "graph m == {(a, b) |a b. m a = Some b}"
*)
(* These are from HOL/Map.thy, but commented out there *)
(* Uncomment these lines if you use something newer than Isabelle2005 *)
(*
consts
map_subst::"('a ~=> 'b) => 'b => 'b =>
            ('a ~=> 'b)"                         ("_/'(_~>_/')"    [900,0,0]900)
map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
            ('a ~=> 'b)"                         ("_/'(_{|->}_/')" [900,0,0]900)

syntax (xsymbols)
map_subst :: "('a ~=> 'b) => 'b => 'b =>
                ('a ~=> 'b)"                     ("_/'(_\<leadsto>_/')"    [900,0,0]900)
map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
                                                 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
defs
map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"

lemma map_upd_s_apply [simp]:
  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
by (simp add: map_upd_s_def)

lemma map_subst_apply [simp]:
  "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
by (simp add: map_subst_def)
*)

subsection {* folding a relation over a list *}

consts
  fold_rel :: "('a \<times> 'c \<times> 'a) set \<Rightarrow> ('a \<times> 'c list \<times> 'a) set"
(*"fold_rel R cs \<equiv> foldl (\<lambda>r c. r O {(x,y). (c,x,y)\<in>R}) Id cs"*)

inductive "fold_rel R" intros
  Nil:  "(a, [],a) \<in> fold_rel R"
  Cons: "\<lbrakk>(a,x,b) \<in> R; (b,xs,c) \<in> fold_rel R\<rbrakk> \<Longrightarrow> (a,x#xs,c) \<in> fold_rel R"
inductive_cases fold_rel_elim_case [elim!]:
   "(a, [] , b) \<in> fold_rel R"
   "(a, x#xs, b) \<in> fold_rel R"

lemma fold_rel_Nil [intro!]: "a = b \<Longrightarrow> (a, [], b) \<in> fold_rel R" 
by (simp add: fold_rel.Nil)
declare fold_rel.Cons [intro!]


subsection "List maps"

constdefs
  K_Nil :: "'a => 'b list" ("\<currency>")
 "K_Nil \<equiv> \<lambda>x. []"

(*<*)
lemma K_Nil_def2 [simp]: "K_Nil x = []"
by (simp add: K_Nil_def)

lemma K_Nil_eqI: "\<forall>x. m x = [] \<Longrightarrow> m = \<currency>"
by (rule ext, auto)

lemma K_Nil_upd [simp]: "(\<lambda> x. if x=a then b else []) = (\<currency>(a:=b))"
by(simp add:K_Nil_def fun_upd_def)

lemma lmap_upd_cong [simp]: "(m(x := y) = m(x := y')) = (y = y')"
by (safe, drule fun_cong, auto split add: split_if_asm)

(*>*)
constdefs
  lmap_dom :: "('a => 'b list) \<Rightarrow> 'a set"
 "lmap_dom m \<equiv> {x. m x \<noteq> []}"
(*<*)
lemma lmap_dom_def2 [simp]: "x \<in> lmap_dom m = (m x \<noteq> [])" 
by (auto simp add: lmap_dom_def)

lemma lmap_dom_empty_eq [simp]: "lmap_dom m = {} = (m = \<currency>)"
by (auto simp add: lmap_dom_def intro: K_Nil_eqI)

lemma lmap_dom_K_Nil [simp]: "lmap_dom \<currency> = {}"
by simp
(*>*)
constdefs
  lmap_subst :: "'a => 'a => ('a => 'b list) => ('a => 'b list)"
 "lmap_subst x x' m == m(x:=[],x':= m x)"
constdefs
 "restrict_lmap" :: "['a => 'b list, 'a set] => ('a => 'b list)"
                                                      ("_[\<lfloor>]_" [90, 91] 90)
  "m[\<lfloor>]A == %x. if x : A then m x else []"

(*<*)
lemma restrict_lmap_K_Nil [simp]: "\<currency>[\<lfloor>]A = \<currency>"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_empty [simp]: "a[\<lfloor>]{} = \<currency>"
by (rule ext, auto simp: restrict_lmap_def)

lemma restrict_lmap_restrict_lmap [simp]: "a[\<lfloor>]A[\<lfloor>]B = a[\<lfloor>](A\<inter>B)"
by (rule ext, auto simp: restrict_lmap_def)

lemma restrict_lmap_upd_in [simp]: "x \<in> A \<Longrightarrow> m(x:=y)[\<lfloor>]A = (m[\<lfloor>]A)(x:=y)"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_upd_notin [simp]: "x \<notin> A \<Longrightarrow> m(x:=y)[\<lfloor>]A = m[\<lfloor>]A"
by (rule ext, auto simp add: restrict_lmap_def)

lemma restrict_lmap_contains [simp]: 
  "x \<in> set ((m[\<lfloor>]A) p) = (x \<in> set (m p) \<and> p \<in> A)"
by (auto simp add: restrict_lmap_def)

lemma lmap_dom_restrict_lmap [simp]: "lmap_dom (a[\<lfloor>]A) = lmap_dom a \<inter> A" 
by (auto simp add: restrict_lmap_def split add: split_if_asm)

lemma restrict_lmap_dom_eq [simp]: "(m[\<lfloor>]A = m) = (lmap_dom m \<subseteq> A)"
apply safe
apply (drule_tac x = x in fun_cong)
apply (rule_tac [2] ext)
apply (rule_tac [2] sym)
apply (auto simp add: restrict_lmap_def lmap_dom_def split add: split_if_asm)
done

(*>*)constdefs
  fappend :: "('a => 'b list) => ('a => 'b list) => ('a => 'b list)" 
                                                      (infixr ".@." 65) 
 "a .@. b == %n. a n @ b n"

(*<*)
lemma fappend_def2 [simp]: "(a .@. b) n = a n @ b n"
apply (unfold fappend_def)
apply (rule refl)
done

lemma fappend_K_Nil [simp]: "a .@. \<currency> = a"
by (auto simp add: fappend_def)

lemma K_Nil_fappend [simp]: "\<currency> .@. a = a"
by (auto simp add: fappend_def)

lemma fappend_inj1 [simp]: "a .@. b = a' .@. b = (a = a')"
apply auto
apply (unfold fappend_def)
apply (rule ext)
apply (drule_tac x=x in fun_cong)
apply simp
done

lemma fappend_inj2 [simp]: "a .@. b = a .@. b' = (b = b')"
apply auto
apply (unfold fappend_def)
apply (rule ext)
apply (drule_tac x=x in fun_cong)
apply simp
done

lemma fappend_assoc [simp]: "(a .@. b) .@. c = a .@. b .@. c"
apply (unfold fappend_def)
apply auto
done

lemma fappend_commut_disjunct_lmap_dom: 
  "lmap_dom a \<inter> lmap_dom b = {} \<Longrightarrow> a .@. b = b .@. a"
apply (rule ext, auto simp: fappend_def)
apply (drule equalityD1)
apply (simp add: subset_def)
apply (erule_tac x = x in allE)
apply auto
done

lemma "fappend_upd_conv" [simp]: "a .@. b(n:=[v]) = (a .@. b)(n:=a n @ [v])"
apply (rule ext)
apply (simp add: K_Nil_def)
done

lemma "upd_fappend_conv" [simp]: "a(n:=[v]) .@. b  = (a .@. b)(n:=v#b n)"
apply (rule ext)
apply (simp add: K_Nil_def)
done

lemma fappend_eq_Nil [simp]: "(a .@. b = \<currency>) = (a = \<currency> \<and> b = \<currency>)"
apply (auto simp add: fappend_def)
apply (rule_tac [!] ext)
apply auto
apply (drule_tac [!] x = x in fun_cong)
apply auto
done

lemma fappend_not_K_Nil [dest!]: "a(x := y a # f a) = \<currency> \<Longrightarrow> False"
by (drule fun_cong [of _ _ x], auto)

lemma K_Nil_not_fappend_not [dest!]: "\<currency> = a(x := y a # f a)  \<Longrightarrow> False"
by (drule fun_cong [of _ _ x], auto)

lemma fappend_restrict_lmap [simp]: "(a .@. b)[\<lfloor>]A = a[\<lfloor>]A .@. b[\<lfloor>]A"
by (rule ext, auto simp add: restrict_lmap_def)

lemma fappend_compl_restrict_lmap [simp]: "a[\<lfloor>]A .@. a[\<lfloor>](-A) = a"
by (rule ext, auto simp add: restrict_lmap_def)

lemma fappend_incr_length [simp]: "length (bs x) \<le> length ((bs .@. b) x)"
by (auto simp add: fappend_def)

(*>*)
end