equal
deleted
inserted
replaced
431 } |
431 } |
432 ultimately show "P p" by blast |
432 ultimately show "P p" by blast |
433 qed |
433 qed |
434 qed |
434 qed |
435 |
435 |
|
436 lemma perm_struct_induct2[case_names zero swap]: |
|
437 assumes zero: "P 0" |
|
438 assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
|
439 shows "P p" |
|
440 by (rule_tac S="supp p" in perm_struct_induct) |
|
441 (auto intro: zero swap) |
|
442 |
436 lemma perm_subset_induct [consumes 1, case_names zero swap plus]: |
443 lemma perm_subset_induct [consumes 1, case_names zero swap plus]: |
437 assumes S: "supp p \<subseteq> S" |
444 assumes S: "supp p \<subseteq> S" |
438 assumes zero: "P 0" |
445 assumes zero: "P 0" |
439 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
446 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
440 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
447 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |