98 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
98 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
99 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
99 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
100 unfolding eqvt_def frees_lst_graph_def |
100 unfolding eqvt_def frees_lst_graph_def |
101 apply (rule, perm_simp, rule) |
101 apply (rule, perm_simp, rule) |
102 apply(rule_tac y="x" in lam.exhaust) |
102 apply(rule_tac y="x" in lam.exhaust) |
103 apply(simp_all)[3] |
103 apply(auto) |
104 apply(auto)[1] |
|
105 apply(simp_all) |
|
106 apply (erule Abs1_eq_fdest) |
104 apply (erule Abs1_eq_fdest) |
107 apply(simp add: supp_removeAll fresh_def) |
105 apply(simp add: supp_removeAll fresh_def) |
108 apply(drule supp_eqvt_at) |
106 apply(drule supp_eqvt_at) |
109 apply(simp add: finite_supp) |
107 apply(simp add: finite_supp) |
110 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
108 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
111 done |
109 done |
112 |
110 |
113 termination |
111 termination |
114 apply(relation "measure size") |
112 by (relation "measure size") (simp_all add: lam.size) |
115 apply(simp_all add: lam.size) |
|
116 done |
|
117 |
113 |
118 text {* a small test lemma *} |
114 text {* a small test lemma *} |
119 lemma |
115 lemma |
120 shows "supp t = set (frees_lst t)" |
116 shows "supp t = set (frees_lst t)" |
121 apply(induct t rule: frees_lst.induct) |
117 apply(induct t rule: frees_lst.induct) |
145 apply(simp add: eqvt_at_def) |
141 apply(simp add: eqvt_at_def) |
146 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
142 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+ |
147 done |
143 done |
148 |
144 |
149 termination |
145 termination |
150 by (relation "measure (\<lambda>(t,_,_). size t)") |
146 by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size) |
151 (simp_all add: lam.size) |
|
152 |
147 |
153 lemma subst_eqvt[eqvt]: |
148 lemma subst_eqvt[eqvt]: |
154 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
149 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
155 by (induct t x s rule: subst.induct) (simp_all) |
150 by (induct t x s rule: subst.induct) (simp_all) |
156 |
151 |
509 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
504 map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam" |
510 where |
505 where |
511 "map_term f (Var x) = f (Var x)" |
506 "map_term f (Var x) = f (Var x)" |
512 | "map_term f (App t1 t2) = App (f t1) (f t2)" |
507 | "map_term f (App t1 t2) = App (f t1) (f t2)" |
513 | "map_term f (Lam [x].t) = Lam [x].(f t)" |
508 | "map_term f (Lam [x].t) = Lam [x].(f t)" |
|
509 unfolding eqvt_def map_term_graph_def |
|
510 apply (rule, perm_simp, rule) |
|
511 apply (case_tac x, case_tac b rule: lam.exhaust) |
|
512 apply auto |
|
513 (*apply (erule Abs1_eq_fdest)*) |
514 oops |
514 oops |
515 |
515 |
516 nominal_primrec |
516 nominal_primrec |
517 A :: "lam => lam" |
517 A :: "lam => lam" |
518 where |
518 where |