# HG changeset patch
# User haftmann
# Date 1397294856 -7200
# Node ID 8f1e7596deb7db5943b24680a3583267ce190f80
# Parent  b60d5d11948917a9a85ee35538a8449b2ac7dd43
more operations and lemmas

diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -99,6 +99,23 @@
   ultimately show ?thesis by simp
 qed
 
+lemma setdiff_irrelevant:
+  assumes "finite A"
+  shows "F g (A - {x. g x = z}) = F g A"
+  using assms by (induct A) (simp_all add: insert_Diff_if) 
+  
+lemma not_neutral_contains_not_neutral:
+  assumes "F g A \<noteq> z"
+  obtains a where "a \<in> A" and "g a \<noteq> z"
+proof -
+  from assms have "\<exists>a\<in>A. g a \<noteq> z"
+  proof (induct A rule: infinite_finite_induct)
+    case (insert a A)
+    then show ?case by simp (rule, simp)
+  qed simp_all
+  with that show thesis by blast
+qed
+
 lemma reindex:
   assumes "inj_on h A"
   shows "F g (h ` A) = F (g \<circ> h) A"
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Library/Mapping.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -292,6 +292,10 @@
   "\<not> is_empty (map_default k v f m)"
   by (simp add: map_default_def)
 
+lemma keys_dom_lookup:
+  "keys m = dom (Mapping.lookup m)"
+  by transfer rule
+
 lemma keys_empty [simp]:
   "keys empty = {}"
   by transfer simp
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Library/Permutations.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -10,17 +10,17 @@
 
 subsection {* Transpositions *}
 
-lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
-  by (auto simp add: fun_eq_iff swap_def fun_upd_def)
-
 lemma swap_id_refl: "Fun.swap a a id = id"
-  by simp
+  by (fact swap_self)
 
 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
-  by (rule ext, simp add: swap_def)
+  by (fact swap_commute)
+
+lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
+  by (fact swap_commute)
 
 lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
-  by (rule ext, auto simp add: swap_def)
+  by (rule ext, auto simp add: Fun.swap_def)
 
 lemma inv_unique_comp:
   assumes fg: "f \<circ> g = id"
@@ -32,7 +32,7 @@
   by (rule inv_unique_comp) simp_all
 
 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
-  by (simp add: swap_def)
+  by (simp add: Fun.swap_def)
 
 
 subsection {* Basic consequences of the definition *}
@@ -95,7 +95,7 @@
   done
 
 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
-  unfolding permutes_def swap_def fun_upd_def by auto metis
+  unfolding permutes_def Fun.swap_def fun_upd_def by auto metis
 
 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
   by (simp add: Ball_def permutes_def) metis
@@ -131,7 +131,7 @@
   apply (rule permutes_swap_id, simp)
   using permutes_in_image[OF pS, of a]
   apply simp
-  apply (auto simp add: Ball_def swap_def)
+  apply (auto simp add: Ball_def Fun.swap_def)
   done
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
@@ -215,14 +215,14 @@
           by auto
         from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x"
           unfolding permutes_def
-          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
+          by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
         also have "\<dots> = ?g (c,q) x"
           using ths(5) `x \<notin> F` eq
           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
         also have "\<dots> = c"
           using ths(5) `x \<notin> F`
           unfolding permutes_def
-          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
+          by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
         finally have bc: "b = c" .
         then have "Fun.swap x b id = Fun.swap x c id"
           by simp
@@ -310,15 +310,15 @@
 
 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
   Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
-  by (simp add: fun_eq_iff swap_def)
+  by (simp add: fun_eq_iff Fun.swap_def)
 
 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
   Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
-  by (simp add: fun_eq_iff swap_def)
+  by (simp add: fun_eq_iff Fun.swap_def)
 
 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
   Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
-  by (simp add: swap_def fun_eq_iff)
+  by (simp add: fun_eq_iff Fun.swap_def)
 
 
 subsection {* Permutations as transposition sequences *}
@@ -437,7 +437,7 @@
       (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
         Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
     apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
-    apply (simp_all only: swapid_sym)
+    apply (simp_all only: swap_commute)
     apply (case_tac "a = c \<and> b = d")
     apply (clarsimp simp only: swapid_sym swap_id_idempotent)
     apply (case_tac "a = c \<and> b \<noteq> d")
@@ -445,18 +445,18 @@
     apply (rule_tac x="b" in exI)
     apply (rule_tac x="d" in exI)
     apply (rule_tac x="b" in exI)
-    apply (clarsimp simp add: fun_eq_iff swap_def)
+    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
     apply (case_tac "a \<noteq> c \<and> b = d")
     apply (rule disjI2)
     apply (rule_tac x="c" in exI)
     apply (rule_tac x="d" in exI)
     apply (rule_tac x="c" in exI)
-    apply (clarsimp simp add: fun_eq_iff swap_def)
+    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
     apply (rule disjI2)
     apply (rule_tac x="c" in exI)
     apply (rule_tac x="d" in exI)
     apply (rule_tac x="b" in exI)
-    apply (clarsimp simp add: fun_eq_iff swap_def)
+    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
     done
   with H show ?thesis by metis
 qed
@@ -489,7 +489,7 @@
 proof (induct n arbitrary: p a b)
   case 0
   then show ?case
-    by (auto simp add: swap_def fun_upd_def)
+    by (auto simp add: Fun.swap_def fun_upd_def)
 next
   case (Suc n p a b)
   from Suc.prems(1) swapidseq_cases[of "Suc n" p]
@@ -511,7 +511,7 @@
     {
       fix h
       have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a"
-        using H by (simp add: swap_def)
+        using H by (simp add: Fun.swap_def)
     }
     note th3 = this
     from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
@@ -673,7 +673,7 @@
     from comp_Suc.hyps(2) have fS: "finite ?S"
       by simp
     from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
-      by (auto simp add: swap_def)
+      by (auto simp add: Fun.swap_def)
     from finite_subset[OF th fS] show ?case  .
   qed
 qed
@@ -685,7 +685,7 @@
   assumes bp: "bij p"
   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
   using surj_f_inv_f[OF bij_is_surj[OF bp]]
-  by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
+  by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
 
 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
 proof -
@@ -709,12 +709,12 @@
   let ?r = "Fun.swap a (p a) id \<circ> p"
   let ?q = "Fun.swap a (p a) id \<circ> ?r"
   have raa: "?r a = a"
-    by (simp add: swap_def)
+    by (simp add: Fun.swap_def)
   from bij_swap_ompose_bij[OF insert(4)]
   have br: "bij ?r"  .
 
   from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
-    apply (clarsimp simp add: swap_def)
+    apply (clarsimp simp add: Fun.swap_def)
     apply (erule_tac x="x" in allE)
     apply auto
     unfolding bij_iff
@@ -1054,7 +1054,7 @@
       from eq have "(Fun.swap a b id \<circ> p) a  = (Fun.swap a c id \<circ> q) a"
         by simp
       then have bc: "b = c"
-        by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def
+        by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
             cong del: if_weak_cong split: split_if_asm)
       from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
         (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/List.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -5432,6 +5432,40 @@
   apply (rule allI, case_tac x, simp, simp) 
   by blast
 
+lemma lexord_irrefl:
+  "irrefl R \<Longrightarrow> irrefl (lexord R)"
+  by (simp add: irrefl_def lexord_irreflexive)
+  
+lemma lexord_asym:
+  assumes "asym R"
+  shows "asym (lexord R)"
+proof
+  from assms obtain "irrefl R" by (blast elim: asym.cases)
+  then show "irrefl (lexord R)" by (rule lexord_irrefl)
+next
+  fix xs ys
+  assume "(xs, ys) \<in> lexord R"
+  then show "(ys, xs) \<notin> lexord R"
+  proof (induct xs arbitrary: ys)
+    case Nil
+    then show ?case by simp
+  next
+    case (Cons x xs)
+    then obtain z zs where ys: "ys = z # zs" by (cases ys) auto
+    with assms Cons show ?case by (auto elim: asym.cases)
+  qed
+qed
+   
+lemma lexord_asymmetric:
+  assumes "asym R"
+  assumes hyp: "(a, b) \<in> lexord R"
+  shows "(b, a) \<notin> lexord R"
+proof -
+  from `asym R` have "asym (lexord R)" by (rule lexord_asym)
+  then show ?thesis by (rule asym.cases) (auto simp add: hyp)
+qed
+
+
 text {*
   Predicate version of lexicographic order integrated with Isabelle's order type classes.
   Author: Andreas Lochbihler
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Map.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -249,6 +249,10 @@
   "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   by (simp add: dom_def)
 
+lemma dom_map_option_comp [simp]:
+  "dom (map_option g \<circ> m) = dom m"
+  using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
+
 
 subsection {* @{const map_option} related *}
 
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -47,10 +47,10 @@
   done
 
 lemma swap_apply1: "Fun.swap x y f x = f y"
-  by (simp add: swap_def)
+  by (simp add: Fun.swap_def)
   
 lemma swap_apply2: "Fun.swap x y f y = f x"
-  by (simp add: swap_def)
+  by (simp add: Fun.swap_def)
 
 lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
   by auto
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -359,7 +359,7 @@
   have th1: "of_int (-1) = - 1" by simp
   let ?p = "Fun.swap i j id"
   let ?A = "\<chi> i. A $ ?p i"
-  from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def)
+  from r have "A = ?A" by (simp add: vec_eq_iff row_def Fun.swap_def)
   then have "det A = det ?A" by simp
   moreover have "det A = - det ?A"
     by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Orderings.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -270,6 +270,35 @@
 end
 
 
+text {* Alternative introduction rule with bias towards strict order *}
+
+lemma order_strictI:
+  fixes less (infix "\<sqsubset>" 50)
+    and less_eq (infix "\<sqsubseteq>" 50)
+  assumes less_eq_less: "\<And>a b. a \<sqsubseteq> b \<longleftrightarrow> a \<sqsubset> b \<or> a = b"
+    assumes asym: "\<And>a b. a \<sqsubset> b \<Longrightarrow> \<not> b \<sqsubset> a"
+  assumes irrefl: "\<And>a. \<not> a \<sqsubset> a"
+  assumes trans: "\<And>a b c. a \<sqsubset> b \<Longrightarrow> b \<sqsubset> c \<Longrightarrow> a \<sqsubset> c"
+  shows "class.order less_eq less"
+proof
+  fix a b
+  show "a \<sqsubset> b \<longleftrightarrow> a \<sqsubseteq> b \<and> \<not> b \<sqsubseteq> a"
+    by (auto simp add: less_eq_less asym irrefl)
+next
+  fix a
+  show "a \<sqsubseteq> a"
+    by (auto simp add: less_eq_less)
+next
+  fix a b c
+  assume "a \<sqsubseteq> b" and "b \<sqsubseteq> c" then show "a \<sqsubseteq> c"
+    by (auto simp add: less_eq_less intro: trans)
+next
+  fix a b
+  assume "a \<sqsubseteq> b" and "b \<sqsubseteq> a" then show "a = b"
+    by (auto simp add: less_eq_less asym)
+qed
+
+
 subsection {* Linear (total) orders *}
 
 class linorder = order +
@@ -341,6 +370,26 @@
 end
 
 
+text {* Alternative introduction rule with bias towards strict order *}
+
+lemma linorder_strictI:
+  fixes less (infix "\<sqsubset>" 50)
+    and less_eq (infix "\<sqsubseteq>" 50)
+  assumes "class.order less_eq less"
+  assumes trichotomy: "\<And>a b. a \<sqsubset> b \<or> a = b \<or> b \<sqsubset> a"
+  shows "class.linorder less_eq less"
+proof -
+  interpret order less_eq less
+    by (fact `class.order less_eq less`)
+  show ?thesis
+  proof
+    fix a b
+    show "a \<sqsubseteq> b \<or> b \<sqsubseteq> a"
+      using trichotomy by (auto simp add: le_less)
+  qed
+qed
+
+
 subsection {* Reasoning tools setup *}
 
 ML {*
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Product_Type.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -954,6 +954,26 @@
   "apsnd f (apfst g p) = apfst g (apsnd f p)"
   by simp
 
+definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
+where
+  "swap p = (snd p, fst p)"
+
+lemma swap_simp [simp]:
+  "swap (x, y) = (y, x)"
+  by (simp add: swap_def)
+
+lemma pair_in_swap_image [simp]:
+  "(y, x) \<in> swap ` A \<longleftrightarrow> (x, y) \<in> A"
+  by (auto intro!: image_eqI)
+
+lemma inj_swap [simp]:
+  "inj_on swap A"
+  by (rule inj_onI) (auto simp add: swap_def)
+
+lemma case_swap [simp]:
+  "(case swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
+  by (cases p) simp
+
 text {*
   Disjoint union of a family of sets -- Sigma.
 *}
@@ -1085,13 +1105,13 @@
 *}
 
 lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
-by blast
+  by (fact Sigma_Un_distrib1)
 
 lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
-by blast
+  by (fact Sigma_Int_distrib1)
 
 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
-by blast
+  by (fact Sigma_Diff_distrib1)
 
 lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   by auto
@@ -1105,6 +1125,14 @@
 lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
   by force
 
+lemma vimage_fst:
+  "fst -` A = A \<times> UNIV"
+  by auto
+
+lemma vimage_snd:
+  "snd -` A = UNIV \<times> A"
+  by auto
+
 lemma insert_times_insert[simp]:
   "insert a A \<times> insert b B =
    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
diff -r b60d5d119489 -r 8f1e7596deb7 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Relation.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -211,13 +211,44 @@
 
 definition irrefl :: "'a rel \<Rightarrow> bool"
 where
-  "irrefl r \<longleftrightarrow> (\<forall>x. (x, x) \<notin> r)"
+  "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)"
+
+definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+  "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)"
+
+lemma irreflp_irrefl_eq [pred_set_conv]:
+  "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 
+  by (simp add: irrefl_def irreflp_def)
+
+lemma irreflI:
+  "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
+  by (simp add: irrefl_def)
+
+lemma irreflpI:
+  "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
+  by (fact irreflI [to_pred])
 
 lemma irrefl_distinct [code]:
-  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
   by (auto simp add: irrefl_def)
 
 
+subsubsection {* Asymmetry *}
+
+inductive asym :: "'a rel \<Rightarrow> bool"
+where
+  asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
+
+inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+  asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
+
+lemma asymp_asym_eq [pred_set_conv]:
+  "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" 
+  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
+
+
 subsubsection {* Symmetry *}
 
 definition sym :: "'a rel \<Rightarrow> bool"