a few additions and deletions
authornipkow
Fri Feb 02 15:47:58 2007 +0100 (2007-02-02)
changeset 22230bdec4a82f385
parent 22229 8e127313ed55
child 22231 f76f187c91f9
a few additions and deletions
src/HOL/Datatype.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/Map.thy
src/HOL/Matrix/MatrixGeneral.thy
     1.1 --- a/src/HOL/Datatype.thy	Thu Feb 01 20:59:50 2007 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Feb 02 15:47:58 2007 +0100
     1.3 @@ -558,6 +558,9 @@
     1.4    inject Inl_eq Inr_eq
     1.5    induction sum_induct
     1.6  
     1.7 +lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
     1.8 +  by (rule ext) (simp split: sum.split)
     1.9 +
    1.10  lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.11    apply (rule_tac s = s in sumE)
    1.12     apply (erule ssubst)
     2.1 --- a/src/HOL/HoareParallel/Graph.thy	Thu Feb 01 20:59:50 2007 +0100
     2.2 +++ b/src/HOL/HoareParallel/Graph.thy	Fri Feb 02 15:47:58 2007 +0100
     2.3 @@ -222,7 +222,7 @@
     2.4     apply clarify
     2.5     apply(rule_tac x = "j" in exI)
     2.6     apply(case_tac "Suc i<m")
     2.7 -    apply(simp add: nth_append min_def)
     2.8 +    apply(simp add: nth_append)
     2.9      apply(case_tac "R=j")
    2.10       apply(simp add: nth_list_update)
    2.11       apply(case_tac "i=m")
    2.12 @@ -230,7 +230,7 @@
    2.13       apply(erule_tac x = "i" in allE)
    2.14       apply force
    2.15      apply(force simp add: nth_list_update)
    2.16 -   apply(simp add: nth_append min_def)
    2.17 +   apply(simp add: nth_append)
    2.18     apply(subgoal_tac "i=m - 1")
    2.19      prefer 2 apply arith
    2.20     apply(case_tac "R=j")
     3.1 --- a/src/HOL/Map.thy	Thu Feb 01 20:59:50 2007 +0100
     3.2 +++ b/src/HOL/Map.thy	Fri Feb 02 15:47:58 2007 +0100
     3.3 @@ -86,49 +86,12 @@
     3.4  defs
     3.5    map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
     3.6  
     3.7 -(* special purpose constants that should be defined somewhere else and
     3.8 -whose syntax is a bit odd as well:
     3.9 -
    3.10 - "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    3.11 -                                          ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    3.12 -  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    3.13 -
    3.14 -map_upd_s::"('a ~=> 'b) => 'a set => 'b =>
    3.15 -            ('a ~=> 'b)"                         ("_/'(_{|->}_/')" [900,0,0]900)
    3.16 -map_subst::"('a ~=> 'b) => 'b => 'b =>
    3.17 -            ('a ~=> 'b)"                         ("_/'(_~>_/')"    [900,0,0]900)
    3.18 -
    3.19 -map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    3.20 -map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    3.21 -
    3.22 -  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    3.23 -                                                 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    3.24 -  map_subst :: "('a ~=> 'b) => 'b => 'b =>
    3.25 -                ('a ~=> 'b)"                     ("_/'(_\<leadsto>_/')"    [900,0,0]900)
    3.26 -
    3.27 -
    3.28 -subsection {* @{term [source] map_upd_s} *}
    3.29 -
    3.30 -lemma map_upd_s_apply [simp]:
    3.31 -  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
    3.32 -by (simp add: map_upd_s_def)
    3.33 -
    3.34 -lemma map_subst_apply [simp]:
    3.35 -  "(m(a~>b)) x = (if m x = Some a then Some b else m x)"
    3.36 -by (simp add: map_subst_def)
    3.37 -
    3.38 -*)
    3.39 -
    3.40  
    3.41  subsection {* @{term [source] empty} *}
    3.42  
    3.43  lemma empty_upd_none [simp]: "empty(x := None) = empty"
    3.44    by (rule ext) simp
    3.45  
    3.46 -(* FIXME: what is this sum_case nonsense?? *)
    3.47 -lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
    3.48 -  by (rule ext) (simp split: sum.split)
    3.49 -
    3.50  
    3.51  subsection {* @{term [source] map_upd} *}
    3.52  
    3.53 @@ -166,22 +129,6 @@
    3.54    done
    3.55  
    3.56  
    3.57 -(* FIXME: what is this sum_case nonsense?? *)
    3.58 -subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
    3.59 -
    3.60 -lemma sum_case_map_upd_empty [simp]:
    3.61 -    "sum_case (m(k|->y)) empty = (sum_case m empty)(Inl k|->y)"
    3.62 -  by (rule ext) (simp split: sum.split)
    3.63 -
    3.64 -lemma sum_case_empty_map_upd [simp]:
    3.65 -    "sum_case empty (m(k|->y)) = (sum_case empty m)(Inr k|->y)"
    3.66 -  by (rule ext) (simp split: sum.split)
    3.67 -
    3.68 -lemma sum_case_map_upd_map_upd [simp]:
    3.69 -    "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
    3.70 -  by (rule ext) (simp split: sum.split)
    3.71 -
    3.72 -
    3.73  subsection {* @{term [source] map_of} *}
    3.74  
    3.75  lemma map_of_eq_None_iff:
    3.76 @@ -506,6 +453,11 @@
    3.77  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
    3.78    by (rule ext) (force simp: map_add_def dom_def split: option.split)
    3.79  
    3.80 +(* Due to John Matthews - could be rephrased with dom *)
    3.81 +lemma finite_map_freshness:
    3.82 +  "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
    3.83 +   \<exists>x. f x = None"
    3.84 +by(bestsimp dest:ex_new_if_finite)
    3.85  
    3.86  subsection {* @{term [source] ran} *}
    3.87  
     4.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Feb 01 20:59:50 2007 +0100
     4.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Fri Feb 02 15:47:58 2007 +0100
     4.3 @@ -986,7 +986,6 @@
     4.4    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))"
     4.5    apply (simp add: mult_matrix_def)
     4.6    apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
     4.7 -  apply (simp add: max_def)+
     4.8    apply (auto)
     4.9    apply (simp add: prems)+
    4.10    apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)