135 apply (auto simp add: fresh_Pair)[1] |
135 apply (auto simp add: fresh_Pair)[1] |
136 apply (simp_all add: fresh_def supp_def permute_fun_def)[3] |
136 apply (simp_all add: fresh_def supp_def permute_fun_def)[3] |
137 apply (simp add: eqvts permute_pure) |
137 apply (simp add: eqvts permute_pure) |
138 done |
138 done |
139 |
139 |
|
140 lemma lam_strong_exhaust2: |
|
141 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
|
142 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
|
143 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
|
144 finite (supp c)\<rbrakk> |
|
145 \<Longrightarrow> P" |
|
146 sorry |
|
147 |
|
148 nominal_primrec |
|
149 g |
|
150 where |
|
151 "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t" |
|
152 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x" |
|
153 | "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)" |
|
154 | "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)" |
|
155 apply (simp add: eqvt_def g_graph_def) |
|
156 apply (rule, perm_simp, rule) |
|
157 apply (case_tac x) |
|
158 apply (case_tac "finite (supp (a, b, c))") |
|
159 prefer 2 |
|
160 apply simp |
|
161 apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2) |
|
162 apply simp_all |