equal
deleted
inserted
replaced
29 apply (metis (no_types) Pair_inject lam.distinct)+ |
29 apply (metis (no_types) Pair_inject lam.distinct)+ |
30 apply simp |
30 apply simp |
31 apply (metis (no_types) Pair_inject lam.distinct)+ |
31 apply (metis (no_types) Pair_inject lam.distinct)+ |
32 done |
32 done |
33 |
33 |
34 termination (eqvt) by lexicographic_order |
34 nominal_termination (eqvt) by lexicographic_order |
35 |
35 |
36 lemma lam_rec_cong[fundef_cong]: |
36 lemma lam_rec_cong[fundef_cong]: |
37 " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow> |
37 " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow> |
38 (\<And>t1 t2. l = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow> |
38 (\<And>t1 t2. l = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow> |
39 (\<And>n t. l = Lam [n]. t \<Longrightarrow> fl n t = fl' n t) \<Longrightarrow> |
39 (\<And>n t. l = Lam [n]. t \<Longrightarrow> fl n t = fl' n t) \<Longrightarrow> |
56 (%x t. Lam [x]. (substr t y s)) (Lam [y]. Var y) (y, s) l" |
56 (%x t. Lam [x]. (substr t y s)) (Lam [y]. Var y) (y, s) l" |
57 unfolding eqvt_def substr_graph_def |
57 unfolding eqvt_def substr_graph_def |
58 apply (rule, perm_simp, rule, rule) |
58 apply (rule, perm_simp, rule, rule) |
59 by pat_completeness auto |
59 by pat_completeness auto |
60 |
60 |
61 termination (eqvt) by lexicographic_order |
61 nominal_termination (eqvt) by lexicographic_order |
62 |
62 |
63 lemma fresh_fun_eqvt_app3: |
63 lemma fresh_fun_eqvt_app3: |
64 assumes e: "eqvt f" |
64 assumes e: "eqvt f" |
65 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
65 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
66 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |
66 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |