1 (* Title: Nominal2_Supp |
|
2 Authors: Brian Huffman, Christian Urban |
|
3 |
|
4 Supplementary Lemmas and Definitions for |
|
5 Nominal Isabelle. |
|
6 *) |
|
7 theory Nominal2_Supp |
|
8 imports Nominal2_Base Nominal2_Eqvt |
|
9 begin |
|
10 |
|
11 section {* Induction principle for permutations *} |
|
12 |
|
13 |
|
14 lemma perm_struct_induct[consumes 1, case_names zero swap]: |
|
15 assumes S: "supp p \<subseteq> S" |
|
16 and zero: "P 0" |
|
17 and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
|
18 shows "P p" |
|
19 proof - |
|
20 have "finite (supp p)" by (simp add: finite_supp) |
|
21 then show "P p" using S |
|
22 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
|
23 case (psubset p) |
|
24 then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto |
|
25 have as: "supp p \<subseteq> S" by fact |
|
26 { assume "supp p = {}" |
|
27 then have "p = 0" by (simp add: supp_perm expand_perm_eq) |
|
28 then have "P p" using zero by simp |
|
29 } |
|
30 moreover |
|
31 { assume "supp p \<noteq> {}" |
|
32 then obtain a where a0: "a \<in> supp p" by blast |
|
33 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" |
|
34 using as by (auto simp add: supp_atom supp_perm swap_atom) |
|
35 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
|
36 have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom) |
|
37 moreover |
|
38 have "a \<notin> supp ?q" by (simp add: supp_perm) |
|
39 then have "supp ?q \<noteq> supp p" using a0 by auto |
|
40 ultimately have "supp ?q \<subset> supp p" using a2 by auto |
|
41 then have "P ?q" using ih by simp |
|
42 moreover |
|
43 have "supp ?q \<subseteq> S" using as a2 by simp |
|
44 ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp |
|
45 moreover |
|
46 have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq) |
|
47 ultimately have "P p" by simp |
|
48 } |
|
49 ultimately show "P p" by blast |
|
50 qed |
|
51 qed |
|
52 |
|
53 lemma perm_simple_struct_induct[case_names zero swap]: |
|
54 assumes zero: "P 0" |
|
55 and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
|
56 shows "P p" |
|
57 by (rule_tac S="supp p" in perm_struct_induct) |
|
58 (auto intro: zero swap) |
|
59 |
|
60 lemma perm_subset_induct[consumes 1, case_names zero swap plus]: |
|
61 assumes S: "supp p \<subseteq> S" |
|
62 assumes zero: "P 0" |
|
63 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)" |
|
64 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
|
65 shows "P p" |
|
66 using S |
|
67 by (induct p rule: perm_struct_induct) |
|
68 (auto intro: zero plus swap simp add: supp_swap) |
|
69 |
|
70 lemma supp_perm_eq: |
|
71 assumes "(supp x) \<sharp>* p" |
|
72 shows "p \<bullet> x = x" |
|
73 proof - |
|
74 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
|
75 unfolding supp_perm fresh_star_def fresh_def by auto |
|
76 then show "p \<bullet> x = x" |
|
77 proof (induct p rule: perm_struct_induct) |
|
78 case zero |
|
79 show "0 \<bullet> x = x" by simp |
|
80 next |
|
81 case (swap p a b) |
|
82 then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all |
|
83 then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh) |
|
84 qed |
|
85 qed |
|
86 |
|
87 lemma supp_perm_eq_test: |
|
88 assumes "(supp x) \<sharp>* p" |
|
89 shows "p \<bullet> x = x" |
|
90 proof - |
|
91 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
|
92 unfolding supp_perm fresh_star_def fresh_def by auto |
|
93 then show "p \<bullet> x = x" |
|
94 proof (induct p rule: perm_subset_induct) |
|
95 case zero |
|
96 show "0 \<bullet> x = x" by simp |
|
97 next |
|
98 case (swap a b) |
|
99 then have "a \<sharp> x" "b \<sharp> x" by simp_all |
|
100 then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh) |
|
101 next |
|
102 case (plus p1 p2) |
|
103 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
|
104 then show "(p1 + p2) \<bullet> x = x" by simp |
|
105 qed |
|
106 qed |
|
107 |
|
108 |
|
109 end |
|