65 nominal_primrec |
65 nominal_primrec |
66 f :: "lam \<Rightarrow> ('a::pt)" |
66 f :: "lam \<Rightarrow> ('a::pt)" |
67 where |
67 where |
68 "f (Var x) = f1 x" |
68 "f (Var x) = f1 x" |
69 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
69 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
70 | "atom x \<sharp> (f1, f2, f3) \<Longrightarrow> f (Lam [x].t) = f3 x t (f t)" |
70 | "f (Lam [x].t) = f3 x t (f t)" |
71 apply (simp add: eqvt_def f_graph_def) |
71 apply (simp add: eqvt_def f_graph_def) |
72 apply (perm_simp) |
72 apply (perm_simp) |
73 apply(simp add: eq[simplified eqvt_def]) |
73 apply(simp add: eq[simplified eqvt_def]) |
74 apply(rule_tac y="x" and c="(f1,f2,f3)" in lam_strong_exhaust2) |
74 apply(rule_tac y="x" in lam.exhaust) |
75 apply(auto simp add: fresh_star_def) |
75 apply(auto simp add: fresh_star_def) |
76 apply(rule fs) |
|
77 apply(simp add: fresh_Pair_elim) |
|
78 apply(erule Abs1_eq_fdest) |
76 apply(erule Abs1_eq_fdest) |
79 apply simp_all |
77 apply simp_all |
80 apply(simp add: fcb) |
78 apply(simp add: fcb) |
|
79 apply (rule fresh_fun_eqvt_app3[OF eq(3)]) |
|
80 apply (simp add: fresh_at_base) |
|
81 apply assumption |
|
82 apply (erule fresh_eqvt_at) |
|
83 apply (simp add: finite_supp) |
|
84 apply assumption |
81 apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)") |
85 apply (subgoal_tac "\<And>p y r. p \<bullet> (f3 x y r) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r)") |
82 apply (simp add: eqvt_at_def eqvt_def) |
86 apply (simp add: eqvt_at_def) |
83 apply (simp add: permute_fun_app_eq eq[simplified eqvt_def]) |
87 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
84 sorry |
88 done |
85 |
89 |
86 termination sorry |
90 termination |
|
91 by (relation "measure size") (auto simp add: lam.size) |
87 |
92 |
88 end |
93 end |
89 |
94 |
90 thm test.f.simps |
95 thm test.f.simps |
91 |
96 |
92 thm test_def |
97 thm test_def |
|
98 |
|
99 interpretation hei: test |
|
100 "%n. (1 :: nat)" |
|
101 "%t1 t2 r1 r2. (r1 + r2)" |
|
102 "%n t r. r + 1" |
|
103 apply default |
|
104 apply (auto simp add: pure_fresh supp_Pair) |
|
105 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
|
106 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
|
107 done |
|
108 |
|
109 thm hei.f.simps |
93 |
110 |
94 |
111 |
95 |
112 |
96 inductive |
113 inductive |
97 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
114 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |