202 shows "a \<sharp> f x y z" |
202 shows "a \<sharp> f x y z" |
203 using fresh_fun_eqvt_app[OF a b(1)] a b |
203 using fresh_fun_eqvt_app[OF a b(1)] a b |
204 by (metis fresh_fun_app) |
204 by (metis fresh_fun_app) |
205 |
205 |
206 |
206 |
207 section {* A test with a locale and an interpretation. *} |
|
208 |
|
209 text {* conclusion: it is no necessary *} |
|
210 |
|
211 locale test = |
|
212 fixes f1::"name \<Rightarrow> ('a::pt)" |
|
213 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
|
214 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
|
215 assumes fs: "finite (supp (f1, f2, f3))" |
|
216 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
|
217 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
|
218 begin |
|
219 |
|
220 nominal_primrec |
|
221 f :: "lam \<Rightarrow> ('a::pt)" |
|
222 where |
|
223 "f (Var x) = f1 x" |
|
224 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
|
225 | "f (Lam [x].t) = f3 x t (f t)" |
|
226 apply (simp add: eqvt_def f_graph_def) |
|
227 apply (perm_simp) |
|
228 apply(simp add: eq[simplified eqvt_def]) |
|
229 apply(rule TrueI) |
|
230 apply(rule_tac y="x" in lam.exhaust) |
|
231 apply(auto simp add: fresh_star_def) |
|
232 apply(erule Abs_lst1_fcb) |
|
233 apply simp_all |
|
234 apply(simp add: fcb) |
|
235 apply (rule fresh_fun_eqvt_app3[OF eq(3)]) |
|
236 apply (simp add: fresh_at_base) |
|
237 apply assumption |
|
238 apply (erule fresh_eqvt_at) |
|
239 apply (simp add: finite_supp) |
|
240 apply assumption |
|
241 apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)") |
|
242 apply (simp add: eqvt_at_def) |
|
243 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
|
244 done |
|
245 |
|
246 termination |
|
247 by lexicographic_order |
|
248 |
|
249 end |
|
250 |
|
251 interpretation hei: test |
|
252 "%n. (1 :: nat)" |
|
253 "%t1 t2 r1 r2. (r1 + r2)" |
|
254 "%n t r. r + 1" |
|
255 apply default |
|
256 apply (auto simp add: pure_fresh supp_Pair) |
|
257 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
|
258 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
|
259 done |
|
260 |
|
261 section {* height function *} |
207 section {* height function *} |
262 |
208 |
263 nominal_primrec |
209 nominal_primrec |
264 height :: "lam \<Rightarrow> int" |
210 height :: "lam \<Rightarrow> int" |
265 where |
211 where |
815 apply(perm_simp) |
761 apply(perm_simp) |
816 apply(rule allI) |
762 apply(rule allI) |
817 apply(rule refl) |
763 apply(rule refl) |
818 oops |
764 oops |
819 |
765 |
|
766 |
|
767 lemma test: |
|
768 assumes "t = s" |
|
769 and "supp p \<sharp>* t" "supp p \<sharp>* x" |
|
770 and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y" |
|
771 shows "x = y" |
|
772 using assms by (simp add: perm_supp_eq) |
|
773 |
|
774 lemma test2: |
|
775 assumes "cs \<subseteq> as \<union> bs" |
|
776 and "as \<sharp>* x" "bs \<sharp>* x" |
|
777 shows "cs \<sharp>* x" |
|
778 using assms |
|
779 by (auto simp add: fresh_star_def) |
|
780 |
|
781 lemma test3: |
|
782 assumes "cs \<subseteq> as" |
|
783 and "as \<sharp>* x" |
|
784 shows "cs \<sharp>* x" |
|
785 using assms |
|
786 by (auto simp add: fresh_star_def) |
|
787 |
|
788 |
|
789 |
|
790 nominal_primrec (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y") |
|
791 aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
|
792 where |
|
793 "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)" |
|
794 | "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
|
795 | "aux (Var x) (App t1 t2) xs = False" |
|
796 | "aux (Var x) (Lam [y].t) xs = False" |
|
797 | "aux (App t1 t2) (Var x) xs = False" |
|
798 | "aux (App t1 t2) (Lam [x].t) xs = False" |
|
799 | "aux (Lam [x].t) (Var y) xs = False" |
|
800 | "aux (Lam [x].t) (App t1 t2) xs = False" |
|
801 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> |
|
802 aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)" |
|
803 apply (simp add: eqvt_def aux_graph_def) |
|
804 apply (rule, perm_simp, rule) |
|
805 apply(erule aux_graph.induct) |
|
806 apply(simp_all add: fresh_star_def pure_fresh)[9] |
|
807 apply(case_tac x) |
|
808 apply(simp) |
|
809 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
|
810 apply(simp) |
|
811 apply(rule_tac y="b" and c="c" in lam.strong_exhaust) |
|
812 apply(metis)+ |
|
813 apply(simp) |
|
814 apply(rule_tac y="b" and c="c" in lam.strong_exhaust) |
|
815 apply(metis)+ |
|
816 apply(simp) |
|
817 apply(rule_tac y="b" and c="(lam, c, name)" in lam.strong_exhaust) |
|
818 apply(metis)+ |
|
819 apply(simp) |
|
820 apply(drule_tac x="name" in meta_spec) |
|
821 apply(drule_tac x="lama" in meta_spec) |
|
822 apply(drule_tac x="c" in meta_spec) |
|
823 apply(drule_tac x="namea" in meta_spec) |
|
824 apply(drule_tac x="lam" in meta_spec) |
|
825 apply(simp add: fresh_star_Pair) |
|
826 apply(simp add: fresh_star_def fresh_at_base lam.fresh) |
|
827 apply(auto)[1] |
|
828 apply(simp_all)[44] |
|
829 apply(simp del: Product_Type.prod.inject) |
|
830 sorry |
|
831 |
|
832 termination by lexicographic_order |
|
833 |
820 end |
834 end |
821 |
835 |
822 |
836 |
823 |
837 |