equal
deleted
inserted
replaced
33 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
33 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T" |
34 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
34 and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
35 and "sort_of (atom x) = sort_of (atom y)" |
35 and "sort_of (atom x) = sort_of (atom y)" |
36 shows "f x T = f y S" |
36 shows "f x T = f y S" |
37 using assms apply - |
37 using assms apply - |
|
38 thm Abs1_eq_iff' |
38 apply (subst (asm) Abs1_eq_iff') |
39 apply (subst (asm) Abs1_eq_iff') |
39 apply simp_all |
40 apply simp_all |
40 apply (elim conjE disjE) |
41 apply (elim conjE disjE) |
41 apply simp |
42 apply simp |
42 apply(rule trans) |
43 apply(rule trans) |
60 assumes fs: "finite (supp (f1, f2, f3))" |
61 assumes fs: "finite (supp (f1, f2, f3))" |
61 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
62 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
62 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
63 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
63 begin |
64 begin |
64 |
65 |
65 nominal_primrec |
66 nominal_primrec |
66 f :: "lam \<Rightarrow> ('a::pt)" |
67 f :: "lam \<Rightarrow> ('a::pt)" |
67 where |
68 where |
68 "f (Var x) = f1 x" |
69 "f (Var x) = f1 x" |
69 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
70 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
70 | "f (Lam [x].t) = f3 x t (f t)" |
71 | "f (Lam [x].t) = f3 x t (f t)" |
90 termination |
91 termination |
91 by (relation "measure size") (auto simp add: lam.size) |
92 by (relation "measure size") (auto simp add: lam.size) |
92 |
93 |
93 end |
94 end |
94 |
95 |
|
96 |
95 thm test.f.simps |
97 thm test.f.simps |
|
98 thm test.f.simps[simplified test_def] |
96 |
99 |
97 thm test_def |
100 thm test_def |
98 |
101 |
99 interpretation hei: test |
102 interpretation hei: test |
100 "%n. (1 :: nat)" |
103 "%n. (1 :: nat)" |