92 next |
92 next |
93 show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def |
93 show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def |
94 by (rule, perm_simp, rule) |
94 by (rule, perm_simp, rule) |
95 qed |
95 qed |
96 |
96 |
97 termination |
97 termination (eqvt) by lexicographic_order |
98 by (relation "measure (\<lambda>(t). size t)") |
|
99 (simp_all add: lam.size) |
|
100 |
|
101 lemma numeral_eqvt[eqvt]: "p \<bullet> \<lbrace>x\<rbrace> = \<lbrace>p \<bullet> x\<rbrace>" |
|
102 by (induct x rule: lam.induct) |
|
103 (simp_all add: Var_App_Abs_eqvt) |
|
104 |
98 |
105 lemma supp_numeral[simp]: |
99 lemma supp_numeral[simp]: |
106 "supp \<lbrace>x\<rbrace> = supp x" |
100 "supp \<lbrace>x\<rbrace> = supp x" |
107 by (induct x rule: lam.induct) |
101 by (induct x rule: lam.induct) |
108 (simp_all add: lam.supp) |
102 (simp_all add: lam.supp) |
143 apply (subgoal_tac "eqvt app_lst") |
137 apply (subgoal_tac "eqvt app_lst") |
144 apply (erule fresh_fun_eqvt_app2) |
138 apply (erule fresh_fun_eqvt_app2) |
145 apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) |
139 apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) |
146 done |
140 done |
147 |
141 |
148 termination |
142 termination (eqvt) by lexicographic_order |
149 by (relation "measure (\<lambda>t. size t)") |
|
150 (simp_all add: lam.size) |
|
151 |
|
152 lemma ltgt_eqvt[eqvt]: |
|
153 "p \<bullet> \<guillemotleft>t\<guillemotright> = \<guillemotleft>p \<bullet> t\<guillemotright>" |
|
154 proof - |
|
155 obtain x :: var where "atom x \<sharp> (t, p \<bullet> t)" using obtain_fresh by auto |
|
156 then have *: "atom x \<sharp> t" "atom x \<sharp> (p \<bullet> t)" using fresh_Pair by simp_all |
|
157 then show ?thesis using *[unfolded fresh_def] |
|
158 apply (simp add: Abs1_eq_iff lam.fresh app_lst_eqvt Ltgt.simps) |
|
159 apply (case_tac "p \<bullet> x = x") |
|
160 apply (simp_all add: eqvts) |
|
161 apply rule |
|
162 apply (subst swap_fresh_fresh) |
|
163 apply (simp_all add: fresh_at_base_permute_iff fresh_def[symmetric] fresh_at_base) |
|
164 apply (subgoal_tac "eqvt app_lst") |
|
165 apply (erule fresh_fun_eqvt_app2) |
|
166 apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev) |
|
167 done |
|
168 qed |
|
169 |
143 |
170 lemma ltgt_eq_iff[simp]: |
144 lemma ltgt_eq_iff[simp]: |
171 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
145 "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N" |
172 proof auto |
146 proof auto |
173 obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
147 obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto |
238 |
212 |
239 lemma Lam_F: |
213 lemma Lam_F: |
240 "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))" |
214 "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))" |
241 "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))" |
215 "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))" |
242 "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))" |
216 "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))" |
243 apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base) |
217 apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base) |
244 apply (smt cx_cy_cz permute_flip_at)+ |
218 apply (smt cx_cy_cz permute_flip_at)+ |
245 done |
219 done |
246 |
220 |
247 lemma supp_F[simp]: |
221 lemma supp_F[simp]: |
248 "supp F1 = {}" "supp F2 = {}" "supp F3 = {}" |
222 "supp F1 = {}" "supp F2 = {}" "supp F3 = {}" |
289 definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)" |
263 definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)" |
290 lemma Lam_A: |
264 lemma Lam_A: |
291 "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)" |
265 "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)" |
292 "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)" |
266 "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)" |
293 "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)" |
267 "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)" |
294 apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base F_eqvt ltgt_eqvt) |
268 apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt) |
295 apply (smt cx_cy_cz permute_flip_at)+ |
269 apply (smt cx_cy_cz permute_flip_at)+ |
296 done |
270 done |
297 |
271 |
298 lemma supp_A[simp]: |
272 lemma supp_A[simp]: |
299 "supp A1 = {}" "supp A2 = {}" "supp A3 = {}" |
273 "supp A1 = {}" "supp A2 = {}" "supp A3 = {}" |