# HG changeset patch
# User nipkow
# Date 1170427678 -3600
# Node ID bdec4a82f385e51a14c4b0147455df14f25535d6
# Parent  8e127313ed55c0152bcff0bb105608c8b77cf735
a few additions and deletions

diff -r 8e127313ed55 -r bdec4a82f385 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Feb 01 20:59:50 2007 +0100
+++ b/src/HOL/Datatype.thy	Fri Feb 02 15:47:58 2007 +0100
@@ -558,6 +558,9 @@
   inject Inl_eq Inr_eq
   induction sum_induct
 
+lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
+  by (rule ext) (simp split: sum.split)
+
 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
   apply (rule_tac s = s in sumE)
    apply (erule ssubst)
diff -r 8e127313ed55 -r bdec4a82f385 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Thu Feb 01 20:59:50 2007 +0100
+++ b/src/HOL/HoareParallel/Graph.thy	Fri Feb 02 15:47:58 2007 +0100
@@ -222,7 +222,7 @@
    apply clarify
    apply(rule_tac x = "j" in exI)
    apply(case_tac "Suc i<m")
-    apply(simp add: nth_append min_def)
+    apply(simp add: nth_append)
     apply(case_tac "R=j")
      apply(simp add: nth_list_update)
      apply(case_tac "i=m")
@@ -230,7 +230,7 @@
      apply(erule_tac x = "i" in allE)
      apply force
     apply(force simp add: nth_list_update)
-   apply(simp add: nth_append min_def)
+   apply(simp add: nth_append)
    apply(subgoal_tac "i=m - 1")
     prefer 2 apply arith
    apply(case_tac "R=j")
diff -r 8e127313ed55 -r bdec4a82f385 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Feb 01 20:59:50 2007 +0100
+++ b/src/HOL/Map.thy	Fri Feb 02 15:47:58 2007 +0100
@@ -86,49 +86,12 @@
 defs
   map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
 
-(* special purpose constants that should be defined somewhere else and
-whose syntax is a bit odd as well:
-
- "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
-                                          ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
-  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
-
-map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
-            ('a ~=> 'b)"                         ("_/'(_{|->}_/')" [900,0,0]900)
-map_subst::"('a ~=> 'b) => 'b => 'b =>
-            ('a ~=> 'b)"                         ("_/'(_~>_/')"    [900,0,0]900)
-
-map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
-map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
-
-  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
-                                                 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
-  map_subst :: "('a ~=> 'b) => 'b => 'b =>
-                ('a ~=> 'b)"                     ("_/'(_\<leadsto>_/')"    [900,0,0]900)
-
-
-subsection {* @{term [source] map_upd_s} *}
-
-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 {* @{term [source] empty} *}
 
 lemma empty_upd_none [simp]: "empty(x := None) = empty"
   by (rule ext) simp
 
-(* FIXME: what is this sum_case nonsense?? *)
-lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
-  by (rule ext) (simp split: sum.split)
-
 
 subsection {* @{term [source] map_upd} *}
 
@@ -166,22 +129,6 @@
   done
 
 
-(* FIXME: what is this sum_case nonsense?? *)
-subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
-
-lemma sum_case_map_upd_empty [simp]:
-    "sum_case (m(k|->y)) empty = (sum_case m empty)(Inl k|->y)"
-  by (rule ext) (simp split: sum.split)
-
-lemma sum_case_empty_map_upd [simp]:
-    "sum_case empty (m(k|->y)) = (sum_case empty m)(Inr k|->y)"
-  by (rule ext) (simp split: sum.split)
-
-lemma sum_case_map_upd_map_upd [simp]:
-    "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
-  by (rule ext) (simp split: sum.split)
-
-
 subsection {* @{term [source] map_of} *}
 
 lemma map_of_eq_None_iff:
@@ -506,6 +453,11 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
   by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+(* Due to John Matthews - could be rephrased with dom *)
+lemma finite_map_freshness:
+  "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
+   \<exists>x. f x = None"
+by(bestsimp dest:ex_new_if_finite)
 
 subsection {* @{term [source] ran} *}
 
diff -r 8e127313ed55 -r bdec4a82f385 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Feb 01 20:59:50 2007 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Fri Feb 02 15:47:58 2007 +0100
@@ -986,7 +986,6 @@
   shows "(mult_matrix fmul fadd A (singleton_matrix j i e)) = apply_matrix (% x. fmul x e) (move_matrix (column_of_matrix A j) 0 (int i))"
   apply (simp add: mult_matrix_def)
   apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
-  apply (simp add: max_def)+
   apply (auto)
   apply (simp add: prems)+
   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)