33 thm single_let.fv_bn_eqvt |
32 thm single_let.fv_bn_eqvt |
34 thm single_let.size_eqvt |
33 thm single_let.size_eqvt |
35 thm single_let.supports |
34 thm single_let.supports |
36 thm single_let.fsupp |
35 thm single_let.fsupp |
37 |
36 |
38 |
37 lemma supp_abs_sum: |
39 |
38 fixes a b::"'a::fs" |
40 |
39 shows "supp (Abs x a) \<union> supp (Abs x b) = supp (Abs x (a, b))" |
41 (* |
40 and "supp (Abs_res x a) \<union> supp (Abs_res x b) = supp (Abs_res x (a, b))" |
|
41 and "supp (Abs_lst y a) \<union> supp (Abs_lst y b) = supp (Abs_lst y (a, b))" |
|
42 apply (simp_all add: supp_abs supp_Pair) |
|
43 apply blast+ |
|
44 done |
|
45 |
|
46 |
42 lemma test: |
47 lemma test: |
43 "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))" |
48 "(\<exists>p. (bs, x) \<approx>gen (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
44 oops |
49 sorry |
45 |
50 |
46 lemma Abs_eq_iff: |
51 lemma Abs_eq_iff: |
47 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
52 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
48 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
53 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
49 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
54 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
50 by (lifting alphas_abs) |
55 by (lifting alphas_abs) |
51 *) |
56 |
52 |
57 lemma test2: |
53 (* |
58 assumes "fv_trm t = supp t" |
|
59 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
|
60 sorry |
|
61 |
|
62 lemma yy: |
|
63 "X = Y \<Longrightarrow> finite X = finite Y" by simp |
|
64 |
|
65 |
54 lemma supp_fv: |
66 lemma supp_fv: |
55 "supp t = fv_trm t \<and> supp b = fv_bn b" |
67 "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}" |
56 apply(rule single_let.induct) |
68 apply(rule single_let.induct) |
57 apply(simp_all only: single_let.fv_defs)[2] |
69 apply(simp_all only: single_let.fv_defs)[2] |
58 apply(simp_all only: supp_def)[2] |
70 apply(simp_all only: supp_def)[2] |
59 apply(simp_all only: single_let.perm_simps)[2] |
71 apply(simp_all only: single_let.perm_simps)[2] |
60 apply(simp_all only: single_let.eq_iff)[2] |
72 apply(simp_all only: single_let.eq_iff)[2] |
61 apply(simp_all only: de_Morgan_conj)[2] |
73 apply(simp_all only: de_Morgan_conj)[2] |
62 apply(simp_all only: Collect_disj_eq)[2] |
74 apply(simp_all only: Collect_disj_eq)[2] |
63 apply(simp_all only: finite_Un)[2] |
75 apply(simp_all only: finite_Un)[2] |
64 apply(simp_all only: de_Morgan_conj)[2] |
76 apply(simp_all only: de_Morgan_conj)[2] |
65 apply(simp_all only: Collect_disj_eq)[2] |
77 apply(simp_all only: Collect_disj_eq)[2] |
66 apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)") |
78 --" 1 " |
67 apply(simp only: single_let.fv_defs) |
79 apply(simp only: single_let.fv_defs) |
68 apply(simp only: supp_abs) |
80 apply(simp add: supp_abs(1)[symmetric]) |
69 apply(simp) |
81 apply(simp (no_asm) only: supp_def) |
70 apply(simp (no_asm) only: supp_def) |
82 apply(simp only: single_let.perm_simps) |
71 apply(simp only: single_let.perm_simps) |
83 apply(simp only: single_let.eq_iff) |
72 apply(simp only: single_let.eq_iff) |
84 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
73 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
85 apply(perm_simp) |
74 apply(simp only: Abs_eq_iff) |
86 apply(simp only: Abs_eq_iff) |
75 apply(subst test) |
87 apply(simp add: alphas) |
76 apply(rule refl) |
88 apply(drule test2) |
77 sorry |
89 apply(simp) |
78 *) |
90 -- " 2 " |
|
91 apply(erule conjE)+ |
|
92 apply(simp only: single_let.fv_defs) |
|
93 apply(simp add: supp_abs(1)[symmetric]) |
|
94 apply(simp (no_asm) only: supp_def) |
|
95 apply(simp only: single_let.perm_simps) |
|
96 apply(simp only: single_let.eq_iff) |
|
97 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
|
98 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
99 apply(simp only: de_Morgan_conj) |
|
100 apply(simp only: Collect_disj_eq) |
|
101 apply(simp only: Abs_eq_iff) |
|
102 apply(simp only: finite_Un) |
|
103 apply(simp only: de_Morgan_conj) |
|
104 apply(simp only: Collect_disj_eq) |
|
105 apply(simp add: alphas) |
|
106 apply(drule test2) |
|
107 apply(simp) |
|
108 -- " 3 " |
|
109 apply(simp only: single_let.fv_defs) |
|
110 apply(simp only: supp_Pair[symmetric]) |
|
111 apply(simp add: supp_abs(1)[symmetric]) |
|
112 apply(simp (no_asm) only: supp_def) |
|
113 apply(simp only: single_let.perm_simps) |
|
114 apply(simp only: single_let.eq_iff) |
|
115 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
|
116 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
117 apply(simp only: Abs_eq_iff) |
|
118 apply(simp add: alphas) |
|
119 apply(simp add: supp_Pair) |
|
120 apply(drule test2)+ |
|
121 apply(simp) |
|
122 apply(simp add: prod_alpha_def) |
|
123 apply(simp add: Un_assoc) |
|
124 apply(rule Collect_cong) |
|
125 apply(rule arg_cong) |
|
126 back |
|
127 apply(rule yy) |
|
128 apply(rule Collect_cong) |
|
129 apply(auto)[1] |
|
130 -- " Bar " |
|
131 apply(simp only: single_let.fv_defs) |
|
132 apply(simp only: supp_Pair[symmetric]) |
|
133 apply(simp add: supp_abs(1)[symmetric]) |
|
134 apply(simp (no_asm) only: supp_def) |
|
135 apply(simp only: single_let.perm_simps) |
|
136 apply(simp only: single_let.eq_iff) |
|
137 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
|
138 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
139 apply(simp only: Abs_eq_iff) |
|
140 apply(simp add: alphas prod_alpha_def) |
|
141 apply(drule test2) |
|
142 apply(simp add: supp_Pair) |
|
143 apply(subst atom_eqvt) |
|
144 apply(simp) |
|
145 apply(simp add: Un_assoc) |
|
146 apply(rule Collect_cong) |
|
147 apply(rule arg_cong) |
|
148 back |
|
149 apply(rule yy) |
|
150 apply(rule Collect_cong) |
|
151 -- "last" |
|
152 prefer 3 |
|
153 apply(rule conjI) |
|
154 apply(simp only: single_let.fv_defs) |
|
155 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
156 apply(simp add: supp_abs(1)[symmetric]) |
|
157 apply(simp (no_asm) only: supp_def) |
|
158 apply(simp only: single_let.perm_simps) |
|
159 apply(simp only: single_let.eq_iff) |
|
160 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
|
161 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
162 apply(simp only: Abs_eq_iff) |
|
163 apply(simp only: de_Morgan_conj) |
|
164 apply(simp only: Collect_disj_eq) |
|
165 apply(simp only: finite_Un) |
|
166 apply(simp only: de_Morgan_conj) |
|
167 apply(simp only: Collect_disj_eq) |
|
168 apply(simp add: alphas prod_alpha_def) |
|
169 apply(drule test2) |
|
170 apply(simp add: supp_Pair) |
|
171 apply(simp only: permute_set_eq) |
|
172 apply(simp) |
|
173 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
174 apply(simp only: single_let.eq_iff) |
|
175 apply(simp only: single_let.fv_defs) |
|
176 apply(simp add: supp_abs(1)[symmetric]) |
|
177 apply(simp (no_asm) only: supp_def) |
|
178 apply(perm_simp) |
|
179 oops |
|
180 |
|
181 |
|
182 |
|
183 |
|
184 |
|
185 text {* *} |
|
186 |
79 (* |
187 (* |
80 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
188 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
81 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
189 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
82 |
190 |
83 lemma y: |
191 lemma y: |