--- 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"
--- 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
--- 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
--- 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
--- 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 *}
--- 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
--- 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)
--- 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 {*
--- 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)"
--- 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"