Read about our upcoming Code of Conduct on this issue

Commit 15d5befc authored by haftmann's avatar haftmann
Browse files

more lemmas

parent 25aa6648a101
......@@ -125,13 +125,13 @@ definition try_swap :: "'person \<Rightarrow> 'color \<Rightarrow> 'color \<Righ
"try_swap p c\<^sub>1 c\<^sub>2 w x = (if c\<^sub>1 = blue \<or> c\<^sub>2 = blue \<or> x \<noteq> p then w x else Fun.swap c\<^sub>1 c\<^sub>2 id (w x))"
lemma try_swap_valid[simp]: "valid (try_swap p c\<^sub>1 c\<^sub>2 w) = valid w"
by (auto simp add: try_swap_def valid_def swap_def)
by (auto simp add: try_swap_def valid_def swap_id_eq)
lemma try_swap_eq[simp]: "try_swap p c\<^sub>1 c\<^sub>2 w x = try_swap p c\<^sub>1 c\<^sub>2 w' x \<longleftrightarrow> w x = w' x"
by (auto simp add: try_swap_def swap_def)
by (auto simp add: try_swap_def swap_id_eq)
lemma try_swap_inv[simp]: "try_swap p c\<^sub>1 c\<^sub>2 (try_swap p c\<^sub>1 c\<^sub>2 w) = w"
by (rule ext) (auto simp add: try_swap_def swap_def)
by (rule ext) (auto simp add: try_swap_def swap_id_eq)
lemma leaves_try_swap[simp]:
assumes "valid w"
......
......@@ -572,14 +572,14 @@ lemma det_identical_cols:
proof (transfer fixing: i i')
fix A :: "'a \<Rightarrow> 'a \<Rightarrow> 'b" assume "(\<chi> j. A j i) = (\<chi> i. A i i')"
then have [simp]: "\<And>j q. A j (Fun.swap i i' id (q j)) = A j (q j)"
by (auto simp: vec_eq_iff swap_def)
by (auto simp: vec_eq_iff swap_id_eq)
let ?p = "\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A i (p i))"
let ?s = "\<lambda>q. Fun.swap i i' id \<circ> q"
let ?E = "{p. p permutes UNIV \<and> evenperm p}"
have [simp]: "inj_on ?s ?E"
by (auto simp: inj_on_def fun_eq_iff swap_def)
by (auto simp: inj_on_def fun_eq_iff swap_id_eq)
note p = permutes_UNIV_permutation evenperm_comp permutes_swap_id evenperm_swap permutes_compose
sign_compose sign_swap_id
......
......@@ -85,8 +85,11 @@ proof (rule bij_imp_permutes')
(simp add: assms(1) permutes_in_image permutes_inv)
from assms have "inj (p(x := x, inv p x := p x))"
by (intro injI) (auto split: if_split_asm; metis permutes_inverses(2))+
from assms this show "bij (p(x := x, inv p x := p x))"
by (metis UNIV_I bij_betw_imageI bij_betw_swap_iff permutes_inj permutes_surj surj_f_inv_f swap_def)
moreover have "surj (p(x := x, inv p x := p x))"
using assms UNIV_I bij_betw_swap_iff permutes_inj permutes_surj surj_f_inv_f
by (metis (no_types, hide_lams) Fun.swap_def bij_betw_def)
ultimately show "bij (p(x := x, inv p x := p x))"
by (rule bijI)
qed
lemma permutes_drop_cycle_size_two:
......
......@@ -44,7 +44,7 @@ lemma in_pair_trans [trans]:
using assms by (auto simp: in_pair_def)
lemma in_pair_same [simp]: "p \<in>\<^sub>p A \<times> A \<longleftrightarrow> p \<in> A \<times> A"
by (auto simp: in_pair_def swap_def)
by (auto simp: in_pair_def)
lemma subset_pairsI [intro]:
assumes "\<And>x. x \<in>\<^sub>p A \<Longrightarrow> x \<in>\<^sub>p B"
......@@ -2004,7 +2004,7 @@ next
case True
moreover from \<open>a1 \<in> set gs \<union> set bs\<close> \<open>b1 \<in> set gs \<union> set bs\<close> disj1
have "(a1, b1) \<notin>\<^sub>p set hs \<times> (set gs \<union> set bs \<union> set hs)"
by (auto simp: in_pair_def swap_def)
by (auto simp: in_pair_def)
ultimately have "(a1, b1) \<in>\<^sub>p set (ps -- sps) -\<^sub>p set ps'" by auto
with \<open>fst a1 \<noteq> 0\<close> \<open>fst b1 \<noteq> 0\<close> show ?thesis by (rule a)
next
......
......@@ -239,7 +239,7 @@ qed (insert k, auto)
lemma swap_rows_mat_eq_permute:
"k < n \<Longrightarrow> l < n \<Longrightarrow> swaprows_mat n k l = mat n n (\<lambda>(i, j). 1\<^sub>m n $$ (Fun.swap k l id i, j))"
by (rule eq_matI, auto simp: swap_def)
by (rule eq_matI) (auto simp add: swap_id_eq)
lemma det_swaprows_mat: assumes k: "k < n" and l: "l < n" and kl: "k \<noteq> l"
shows "det (swaprows_mat n k l) = - 1"
......@@ -321,8 +321,8 @@ proof-
from permutes_compose[OF q p] sign_compose[OF pp[OF p] pp[OF q], unfolded sp sq]
have "?p o q \<in> ?one" by auto
hence "?p o (?p o q) \<in> ?pone" by auto
also have "?p o (?p o q) = q" unfolding o_def
by (intro ext, auto simp: swap_def)
also have "?p o (?p o q) = q"
by (auto simp: swap_id_eq)
finally have "q \<in> ?pone" .
}
moreover
......@@ -1526,8 +1526,8 @@ lemma permutation_insert_row_step:
(is "?l = ?r")
proof (rule ext)
fix x show "?l x = ?r x"
apply (cases rule: linorder_cases[of "x" "i"])
unfolding permutation_insert_expand swap_def by auto
by (cases rule: linorder_cases[of "x" "i"])
(auto simp add: swap_id_eq permutation_insert_expand)
qed
lemma permutation_insert_column_step:
......
......@@ -268,7 +268,7 @@ shows "index (xs[i := xs!j, j := xs!i]) x =
proof-
have "distinct(xs[i := xs!j, j := xs!i])" using assms by simp
with assms show ?thesis
apply (auto simp: swap_def simp del: distinct_swap)
apply (auto simp: simp del: distinct_swap)
apply (metis index_nth_id list_update_same_conv)
apply (metis (erased, hide_lams) index_nth_id length_list_update list_update_swap nth_list_update_eq)
apply (metis index_nth_id length_list_update nth_list_update_eq)
......
......@@ -411,6 +411,8 @@ proof -
show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
next
case (swap a b p)
then have \<open>permutation p\<close>
by (auto intro: permutes_imp_permutation)
let ?sab = "Fun.swap a b id"
let ?sfab = "Fun.swap (?fn a) (?fn b) id"
have p_sab: "permutation ?sab" by (rule permutation_swap_id)
......@@ -435,7 +437,7 @@ proof -
show "?ft (Fun.swap a b id \<circ> p) c = (Fun.swap (?fn a) (?fn b) id \<circ> ?ft p) c"
proof (cases "p (?tn c) = a \<or> p (?tn c) = b")
case True
thus ?thesis by (cases, auto simp add: o_def swap_def)
thus ?thesis by (cases, auto simp add: swap_id_eq)
next
case False
hence neq: "p (?tn c) \<noteq> a" "p (?tn c) \<noteq> b" by auto
......@@ -443,10 +445,10 @@ proof -
by (simp add: to_nat_less_card)
from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
have "?fn (p (?tn c)) \<noteq> ?fn a" "?fn (p (?tn c)) \<noteq> ?fn b" .
with neq show ?thesis by (auto simp: o_def swap_def)
with neq show ?thesis by (auto simp: swap_id_eq)
qed
qed
show ?case unfolding IH2 id sign_compose[OF p_sab swap(3)] sign_compose[OF p_sfab p_ftp] id2
show ?case unfolding IH2 id sign_compose[OF p_sab \<open>permutation p\<close>] sign_compose[OF p_sfab p_ftp] id2
by (rule conjI[OF refl perm1])
qed
thus "signof p = of_int (sign ?q)" unfolding signof_def sign_def by auto
......
......@@ -267,5 +267,4 @@ qed
end
thm perron_frobenius_spectral_radius_yun_real_roots
end
......@@ -1587,7 +1587,7 @@ context digraph_map begin
{
fix x show "(x \<in> arcs G) = (edge_rev (rev_swap a b) x \<noteq> x)"
using assms(2)
by (cases "x \<in> {a,b}") (auto simp: rev_swap_def perm_swap_def arev_dom swap_def split: if_splits)
by (cases "x \<in> {a,b}") (auto simp: rev_swap_def perm_swap_def arev_dom swap_id_eq split: if_splits)
next
fix x assume "x \<in> arcs G" then show "edge_rev ?M' (edge_rev ?M' x) = x"
by (auto simp: rev_swap_def perm_swap_comp[symmetric])
......
......@@ -339,6 +339,8 @@ proof -
show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
next
case (swap a b p)
then have \<open>permutation p\<close>
using permutes_imp_permutation by blast
let ?sab = "Fun.swap a b id"
let ?sfab = "Fun.swap (?fn a) (?fn b) id"
have p_sab: "permutation ?sab" by (rule permutation_swap_id)
......@@ -363,7 +365,7 @@ proof -
show "?ft (Fun.swap a b id \<circ> p) c = (Fun.swap (?fn a) (?fn b) id \<circ> ?ft p) c"
proof (cases "p (?tn c) = a \<or> p (?tn c) = b")
case True
thus ?thesis by (cases, auto simp add: o_def swap_def)
thus ?thesis by (cases, auto simp add: o_def swap_id_eq)
next
case False
hence neq: "p (?tn c) \<noteq> a" "p (?tn c) \<noteq> b" by auto
......@@ -371,10 +373,10 @@ proof -
by (simp add: to_nat_less_card)
from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
have "?fn (p (?tn c)) \<noteq> ?fn a" "?fn (p (?tn c)) \<noteq> ?fn b" .
with neq show ?thesis by (auto simp: o_def swap_def)
with neq show ?thesis by (auto simp: o_def swap_id_eq)
qed
qed
show ?case unfolding IH2 id sign_compose[OF p_sab swap(3)] sign_compose[OF p_sfab p_ftp] id2
show ?case unfolding IH2 id sign_compose[OF p_sab \<open>permutation p\<close>] sign_compose[OF p_sfab p_ftp] id2
by (rule conjI[OF refl perm1])
qed
thus "signof p = of_int (sign ?q)" unfolding signof_def sign_def by auto
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment