more operations and lemmas
authorhaftmann
Sat Apr 12 11:27:36 2014 +0200 (2014-04-12)
changeset 565458f1e7596deb7
parent 56544 b60d5d119489
child 56555 1afb78a93376
more operations and lemmas
src/HOL/Groups_Big.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Permutations.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Groups_Big.thy	Sat Apr 12 17:26:27 2014 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Sat Apr 12 11:27:36 2014 +0200
     1.3 @@ -99,6 +99,23 @@
     1.4    ultimately show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma setdiff_irrelevant:
     1.8 +  assumes "finite A"
     1.9 +  shows "F g (A - {x. g x = z}) = F g A"
    1.10 +  using assms by (induct A) (simp_all add: insert_Diff_if) 
    1.11 +  
    1.12 +lemma not_neutral_contains_not_neutral:
    1.13 +  assumes "F g A \<noteq> z"
    1.14 +  obtains a where "a \<in> A" and "g a \<noteq> z"
    1.15 +proof -
    1.16 +  from assms have "\<exists>a\<in>A. g a \<noteq> z"
    1.17 +  proof (induct A rule: infinite_finite_induct)
    1.18 +    case (insert a A)
    1.19 +    then show ?case by simp (rule, simp)
    1.20 +  qed simp_all
    1.21 +  with that show thesis by blast
    1.22 +qed
    1.23 +
    1.24  lemma reindex:
    1.25    assumes "inj_on h A"
    1.26    shows "F g (h ` A) = F (g \<circ> h) A"
     2.1 --- a/src/HOL/Library/Mapping.thy	Sat Apr 12 17:26:27 2014 +0200
     2.2 +++ b/src/HOL/Library/Mapping.thy	Sat Apr 12 11:27:36 2014 +0200
     2.3 @@ -292,6 +292,10 @@
     2.4    "\<not> is_empty (map_default k v f m)"
     2.5    by (simp add: map_default_def)
     2.6  
     2.7 +lemma keys_dom_lookup:
     2.8 +  "keys m = dom (Mapping.lookup m)"
     2.9 +  by transfer rule
    2.10 +
    2.11  lemma keys_empty [simp]:
    2.12    "keys empty = {}"
    2.13    by transfer simp
     3.1 --- a/src/HOL/Library/Permutations.thy	Sat Apr 12 17:26:27 2014 +0200
     3.2 +++ b/src/HOL/Library/Permutations.thy	Sat Apr 12 11:27:36 2014 +0200
     3.3 @@ -10,17 +10,17 @@
     3.4  
     3.5  subsection {* Transpositions *}
     3.6  
     3.7 -lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
     3.8 -  by (auto simp add: fun_eq_iff swap_def fun_upd_def)
     3.9 -
    3.10  lemma swap_id_refl: "Fun.swap a a id = id"
    3.11 -  by simp
    3.12 +  by (fact swap_self)
    3.13  
    3.14  lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
    3.15 -  by (rule ext, simp add: swap_def)
    3.16 +  by (fact swap_commute)
    3.17 +
    3.18 +lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
    3.19 +  by (fact swap_commute)
    3.20  
    3.21  lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
    3.22 -  by (rule ext, auto simp add: swap_def)
    3.23 +  by (rule ext, auto simp add: Fun.swap_def)
    3.24  
    3.25  lemma inv_unique_comp:
    3.26    assumes fg: "f \<circ> g = id"
    3.27 @@ -32,7 +32,7 @@
    3.28    by (rule inv_unique_comp) simp_all
    3.29  
    3.30  lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    3.31 -  by (simp add: swap_def)
    3.32 +  by (simp add: Fun.swap_def)
    3.33  
    3.34  
    3.35  subsection {* Basic consequences of the definition *}
    3.36 @@ -95,7 +95,7 @@
    3.37    done
    3.38  
    3.39  lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
    3.40 -  unfolding permutes_def swap_def fun_upd_def by auto metis
    3.41 +  unfolding permutes_def Fun.swap_def fun_upd_def by auto metis
    3.42  
    3.43  lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    3.44    by (simp add: Ball_def permutes_def) metis
    3.45 @@ -131,7 +131,7 @@
    3.46    apply (rule permutes_swap_id, simp)
    3.47    using permutes_in_image[OF pS, of a]
    3.48    apply simp
    3.49 -  apply (auto simp add: Ball_def swap_def)
    3.50 +  apply (auto simp add: Ball_def Fun.swap_def)
    3.51    done
    3.52  
    3.53  lemma permutes_insert: "{p. p permutes (insert a S)} =
    3.54 @@ -215,14 +215,14 @@
    3.55            by auto
    3.56          from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x"
    3.57            unfolding permutes_def
    3.58 -          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    3.59 +          by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
    3.60          also have "\<dots> = ?g (c,q) x"
    3.61            using ths(5) `x \<notin> F` eq
    3.62            by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    3.63          also have "\<dots> = c"
    3.64            using ths(5) `x \<notin> F`
    3.65            unfolding permutes_def
    3.66 -          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    3.67 +          by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff)
    3.68          finally have bc: "b = c" .
    3.69          then have "Fun.swap x b id = Fun.swap x c id"
    3.70            by simp
    3.71 @@ -310,15 +310,15 @@
    3.72  
    3.73  lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
    3.74    Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
    3.75 -  by (simp add: fun_eq_iff swap_def)
    3.76 +  by (simp add: fun_eq_iff Fun.swap_def)
    3.77  
    3.78  lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
    3.79    Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
    3.80 -  by (simp add: fun_eq_iff swap_def)
    3.81 +  by (simp add: fun_eq_iff Fun.swap_def)
    3.82  
    3.83  lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
    3.84    Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
    3.85 -  by (simp add: swap_def fun_eq_iff)
    3.86 +  by (simp add: fun_eq_iff Fun.swap_def)
    3.87  
    3.88  
    3.89  subsection {* Permutations as transposition sequences *}
    3.90 @@ -437,7 +437,7 @@
    3.91        (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
    3.92          Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
    3.93      apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
    3.94 -    apply (simp_all only: swapid_sym)
    3.95 +    apply (simp_all only: swap_commute)
    3.96      apply (case_tac "a = c \<and> b = d")
    3.97      apply (clarsimp simp only: swapid_sym swap_id_idempotent)
    3.98      apply (case_tac "a = c \<and> b \<noteq> d")
    3.99 @@ -445,18 +445,18 @@
   3.100      apply (rule_tac x="b" in exI)
   3.101      apply (rule_tac x="d" in exI)
   3.102      apply (rule_tac x="b" in exI)
   3.103 -    apply (clarsimp simp add: fun_eq_iff swap_def)
   3.104 +    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   3.105      apply (case_tac "a \<noteq> c \<and> b = d")
   3.106      apply (rule disjI2)
   3.107      apply (rule_tac x="c" in exI)
   3.108      apply (rule_tac x="d" in exI)
   3.109      apply (rule_tac x="c" in exI)
   3.110 -    apply (clarsimp simp add: fun_eq_iff swap_def)
   3.111 +    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   3.112      apply (rule disjI2)
   3.113      apply (rule_tac x="c" in exI)
   3.114      apply (rule_tac x="d" in exI)
   3.115      apply (rule_tac x="b" in exI)
   3.116 -    apply (clarsimp simp add: fun_eq_iff swap_def)
   3.117 +    apply (clarsimp simp add: fun_eq_iff Fun.swap_def)
   3.118      done
   3.119    with H show ?thesis by metis
   3.120  qed
   3.121 @@ -489,7 +489,7 @@
   3.122  proof (induct n arbitrary: p a b)
   3.123    case 0
   3.124    then show ?case
   3.125 -    by (auto simp add: swap_def fun_upd_def)
   3.126 +    by (auto simp add: Fun.swap_def fun_upd_def)
   3.127  next
   3.128    case (Suc n p a b)
   3.129    from Suc.prems(1) swapidseq_cases[of "Suc n" p]
   3.130 @@ -511,7 +511,7 @@
   3.131      {
   3.132        fix h
   3.133        have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a"
   3.134 -        using H by (simp add: swap_def)
   3.135 +        using H by (simp add: Fun.swap_def)
   3.136      }
   3.137      note th3 = this
   3.138      from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
   3.139 @@ -673,7 +673,7 @@
   3.140      from comp_Suc.hyps(2) have fS: "finite ?S"
   3.141        by simp
   3.142      from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
   3.143 -      by (auto simp add: swap_def)
   3.144 +      by (auto simp add: Fun.swap_def)
   3.145      from finite_subset[OF th fS] show ?case  .
   3.146    qed
   3.147  qed
   3.148 @@ -685,7 +685,7 @@
   3.149    assumes bp: "bij p"
   3.150    shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
   3.151    using surj_f_inv_f[OF bij_is_surj[OF bp]]
   3.152 -  by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
   3.153 +  by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
   3.154  
   3.155  lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
   3.156  proof -
   3.157 @@ -709,12 +709,12 @@
   3.158    let ?r = "Fun.swap a (p a) id \<circ> p"
   3.159    let ?q = "Fun.swap a (p a) id \<circ> ?r"
   3.160    have raa: "?r a = a"
   3.161 -    by (simp add: swap_def)
   3.162 +    by (simp add: Fun.swap_def)
   3.163    from bij_swap_ompose_bij[OF insert(4)]
   3.164    have br: "bij ?r"  .
   3.165  
   3.166    from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
   3.167 -    apply (clarsimp simp add: swap_def)
   3.168 +    apply (clarsimp simp add: Fun.swap_def)
   3.169      apply (erule_tac x="x" in allE)
   3.170      apply auto
   3.171      unfolding bij_iff
   3.172 @@ -1054,7 +1054,7 @@
   3.173        from eq have "(Fun.swap a b id \<circ> p) a  = (Fun.swap a c id \<circ> q) a"
   3.174          by simp
   3.175        then have bc: "b = c"
   3.176 -        by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def
   3.177 +        by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
   3.178              cong del: if_weak_cong split: split_if_asm)
   3.179        from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
   3.180          (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
     4.1 --- a/src/HOL/List.thy	Sat Apr 12 17:26:27 2014 +0200
     4.2 +++ b/src/HOL/List.thy	Sat Apr 12 11:27:36 2014 +0200
     4.3 @@ -5432,6 +5432,40 @@
     4.4    apply (rule allI, case_tac x, simp, simp) 
     4.5    by blast
     4.6  
     4.7 +lemma lexord_irrefl:
     4.8 +  "irrefl R \<Longrightarrow> irrefl (lexord R)"
     4.9 +  by (simp add: irrefl_def lexord_irreflexive)
    4.10 +  
    4.11 +lemma lexord_asym:
    4.12 +  assumes "asym R"
    4.13 +  shows "asym (lexord R)"
    4.14 +proof
    4.15 +  from assms obtain "irrefl R" by (blast elim: asym.cases)
    4.16 +  then show "irrefl (lexord R)" by (rule lexord_irrefl)
    4.17 +next
    4.18 +  fix xs ys
    4.19 +  assume "(xs, ys) \<in> lexord R"
    4.20 +  then show "(ys, xs) \<notin> lexord R"
    4.21 +  proof (induct xs arbitrary: ys)
    4.22 +    case Nil
    4.23 +    then show ?case by simp
    4.24 +  next
    4.25 +    case (Cons x xs)
    4.26 +    then obtain z zs where ys: "ys = z # zs" by (cases ys) auto
    4.27 +    with assms Cons show ?case by (auto elim: asym.cases)
    4.28 +  qed
    4.29 +qed
    4.30 +   
    4.31 +lemma lexord_asymmetric:
    4.32 +  assumes "asym R"
    4.33 +  assumes hyp: "(a, b) \<in> lexord R"
    4.34 +  shows "(b, a) \<notin> lexord R"
    4.35 +proof -
    4.36 +  from `asym R` have "asym (lexord R)" by (rule lexord_asym)
    4.37 +  then show ?thesis by (rule asym.cases) (auto simp add: hyp)
    4.38 +qed
    4.39 +
    4.40 +
    4.41  text {*
    4.42    Predicate version of lexicographic order integrated with Isabelle's order type classes.
    4.43    Author: Andreas Lochbihler
     5.1 --- a/src/HOL/Map.thy	Sat Apr 12 17:26:27 2014 +0200
     5.2 +++ b/src/HOL/Map.thy	Sat Apr 12 11:27:36 2014 +0200
     5.3 @@ -249,6 +249,10 @@
     5.4    "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
     5.5    by (simp add: dom_def)
     5.6  
     5.7 +lemma dom_map_option_comp [simp]:
     5.8 +  "dom (map_option g \<circ> m) = dom m"
     5.9 +  using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
    5.10 +
    5.11  
    5.12  subsection {* @{const map_option} related *}
    5.13  
     6.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 12 17:26:27 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Apr 12 11:27:36 2014 +0200
     6.3 @@ -47,10 +47,10 @@
     6.4    done
     6.5  
     6.6  lemma swap_apply1: "Fun.swap x y f x = f y"
     6.7 -  by (simp add: swap_def)
     6.8 +  by (simp add: Fun.swap_def)
     6.9    
    6.10  lemma swap_apply2: "Fun.swap x y f y = f x"
    6.11 -  by (simp add: swap_def)
    6.12 +  by (simp add: Fun.swap_def)
    6.13  
    6.14  lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
    6.15    by auto
     7.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Apr 12 17:26:27 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Apr 12 11:27:36 2014 +0200
     7.3 @@ -359,7 +359,7 @@
     7.4    have th1: "of_int (-1) = - 1" by simp
     7.5    let ?p = "Fun.swap i j id"
     7.6    let ?A = "\<chi> i. A $ ?p i"
     7.7 -  from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def)
     7.8 +  from r have "A = ?A" by (simp add: vec_eq_iff row_def Fun.swap_def)
     7.9    then have "det A = det ?A" by simp
    7.10    moreover have "det A = - det ?A"
    7.11      by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)
     8.1 --- a/src/HOL/Orderings.thy	Sat Apr 12 17:26:27 2014 +0200
     8.2 +++ b/src/HOL/Orderings.thy	Sat Apr 12 11:27:36 2014 +0200
     8.3 @@ -270,6 +270,35 @@
     8.4  end
     8.5  
     8.6  
     8.7 +text {* Alternative introduction rule with bias towards strict order *}
     8.8 +
     8.9 +lemma order_strictI:
    8.10 +  fixes less (infix "\<sqsubset>" 50)
    8.11 +    and less_eq (infix "\<sqsubseteq>" 50)
    8.12 +  assumes less_eq_less: "\<And>a b. a \<sqsubseteq> b \<longleftrightarrow> a \<sqsubset> b \<or> a = b"
    8.13 +    assumes asym: "\<And>a b. a \<sqsubset> b \<Longrightarrow> \<not> b \<sqsubset> a"
    8.14 +  assumes irrefl: "\<And>a. \<not> a \<sqsubset> a"
    8.15 +  assumes trans: "\<And>a b c. a \<sqsubset> b \<Longrightarrow> b \<sqsubset> c \<Longrightarrow> a \<sqsubset> c"
    8.16 +  shows "class.order less_eq less"
    8.17 +proof
    8.18 +  fix a b
    8.19 +  show "a \<sqsubset> b \<longleftrightarrow> a \<sqsubseteq> b \<and> \<not> b \<sqsubseteq> a"
    8.20 +    by (auto simp add: less_eq_less asym irrefl)
    8.21 +next
    8.22 +  fix a
    8.23 +  show "a \<sqsubseteq> a"
    8.24 +    by (auto simp add: less_eq_less)
    8.25 +next
    8.26 +  fix a b c
    8.27 +  assume "a \<sqsubseteq> b" and "b \<sqsubseteq> c" then show "a \<sqsubseteq> c"
    8.28 +    by (auto simp add: less_eq_less intro: trans)
    8.29 +next
    8.30 +  fix a b
    8.31 +  assume "a \<sqsubseteq> b" and "b \<sqsubseteq> a" then show "a = b"
    8.32 +    by (auto simp add: less_eq_less asym)
    8.33 +qed
    8.34 +
    8.35 +
    8.36  subsection {* Linear (total) orders *}
    8.37  
    8.38  class linorder = order +
    8.39 @@ -341,6 +370,26 @@
    8.40  end
    8.41  
    8.42  
    8.43 +text {* Alternative introduction rule with bias towards strict order *}
    8.44 +
    8.45 +lemma linorder_strictI:
    8.46 +  fixes less (infix "\<sqsubset>" 50)
    8.47 +    and less_eq (infix "\<sqsubseteq>" 50)
    8.48 +  assumes "class.order less_eq less"
    8.49 +  assumes trichotomy: "\<And>a b. a \<sqsubset> b \<or> a = b \<or> b \<sqsubset> a"
    8.50 +  shows "class.linorder less_eq less"
    8.51 +proof -
    8.52 +  interpret order less_eq less
    8.53 +    by (fact `class.order less_eq less`)
    8.54 +  show ?thesis
    8.55 +  proof
    8.56 +    fix a b
    8.57 +    show "a \<sqsubseteq> b \<or> b \<sqsubseteq> a"
    8.58 +      using trichotomy by (auto simp add: le_less)
    8.59 +  qed
    8.60 +qed
    8.61 +
    8.62 +
    8.63  subsection {* Reasoning tools setup *}
    8.64  
    8.65  ML {*
     9.1 --- a/src/HOL/Product_Type.thy	Sat Apr 12 17:26:27 2014 +0200
     9.2 +++ b/src/HOL/Product_Type.thy	Sat Apr 12 11:27:36 2014 +0200
     9.3 @@ -954,6 +954,26 @@
     9.4    "apsnd f (apfst g p) = apfst g (apsnd f p)"
     9.5    by simp
     9.6  
     9.7 +definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
     9.8 +where
     9.9 +  "swap p = (snd p, fst p)"
    9.10 +
    9.11 +lemma swap_simp [simp]:
    9.12 +  "swap (x, y) = (y, x)"
    9.13 +  by (simp add: swap_def)
    9.14 +
    9.15 +lemma pair_in_swap_image [simp]:
    9.16 +  "(y, x) \<in> swap ` A \<longleftrightarrow> (x, y) \<in> A"
    9.17 +  by (auto intro!: image_eqI)
    9.18 +
    9.19 +lemma inj_swap [simp]:
    9.20 +  "inj_on swap A"
    9.21 +  by (rule inj_onI) (auto simp add: swap_def)
    9.22 +
    9.23 +lemma case_swap [simp]:
    9.24 +  "(case swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
    9.25 +  by (cases p) simp
    9.26 +
    9.27  text {*
    9.28    Disjoint union of a family of sets -- Sigma.
    9.29  *}
    9.30 @@ -1085,13 +1105,13 @@
    9.31  *}
    9.32  
    9.33  lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
    9.34 -by blast
    9.35 +  by (fact Sigma_Un_distrib1)
    9.36  
    9.37  lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
    9.38 -by blast
    9.39 +  by (fact Sigma_Int_distrib1)
    9.40  
    9.41  lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
    9.42 -by blast
    9.43 +  by (fact Sigma_Diff_distrib1)
    9.44  
    9.45  lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
    9.46    by auto
    9.47 @@ -1105,6 +1125,14 @@
    9.48  lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
    9.49    by force
    9.50  
    9.51 +lemma vimage_fst:
    9.52 +  "fst -` A = A \<times> UNIV"
    9.53 +  by auto
    9.54 +
    9.55 +lemma vimage_snd:
    9.56 +  "snd -` A = UNIV \<times> A"
    9.57 +  by auto
    9.58 +
    9.59  lemma insert_times_insert[simp]:
    9.60    "insert a A \<times> insert b B =
    9.61     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    10.1 --- a/src/HOL/Relation.thy	Sat Apr 12 17:26:27 2014 +0200
    10.2 +++ b/src/HOL/Relation.thy	Sat Apr 12 11:27:36 2014 +0200
    10.3 @@ -211,13 +211,44 @@
    10.4  
    10.5  definition irrefl :: "'a rel \<Rightarrow> bool"
    10.6  where
    10.7 -  "irrefl r \<longleftrightarrow> (\<forall>x. (x, x) \<notin> r)"
    10.8 +  "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)"
    10.9 +
   10.10 +definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   10.11 +where
   10.12 +  "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)"
   10.13 +
   10.14 +lemma irreflp_irrefl_eq [pred_set_conv]:
   10.15 +  "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 
   10.16 +  by (simp add: irrefl_def irreflp_def)
   10.17 +
   10.18 +lemma irreflI:
   10.19 +  "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
   10.20 +  by (simp add: irrefl_def)
   10.21 +
   10.22 +lemma irreflpI:
   10.23 +  "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
   10.24 +  by (fact irreflI [to_pred])
   10.25  
   10.26  lemma irrefl_distinct [code]:
   10.27 -  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
   10.28 +  "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
   10.29    by (auto simp add: irrefl_def)
   10.30  
   10.31  
   10.32 +subsubsection {* Asymmetry *}
   10.33 +
   10.34 +inductive asym :: "'a rel \<Rightarrow> bool"
   10.35 +where
   10.36 +  asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
   10.37 +
   10.38 +inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   10.39 +where
   10.40 +  asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
   10.41 +
   10.42 +lemma asymp_asym_eq [pred_set_conv]:
   10.43 +  "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" 
   10.44 +  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
   10.45 +
   10.46 +
   10.47  subsubsection {* Symmetry *}
   10.48  
   10.49  definition sym :: "'a rel \<Rightarrow> bool"