45 apply(rule fresh_star_supp_conv) |
45 apply(rule fresh_star_supp_conv) |
46 apply(simp add: supp_swap fresh_star_def) |
46 apply(simp add: supp_swap fresh_star_def) |
47 apply(simp add: swap_commute) |
47 apply(simp add: swap_commute) |
48 done |
48 done |
49 |
49 |
|
50 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
|
51 frees_set :: "lam \<Rightarrow> atom set" |
|
52 where |
|
53 "frees_set (Var x) = {atom x}" |
|
54 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
|
55 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" |
|
56 apply(simp add: eqvt_def frees_set_graph_def) |
|
57 apply (rule, perm_simp, rule) |
|
58 apply(erule frees_set_graph.induct) |
|
59 apply(simp) |
|
60 apply(simp) |
|
61 apply(simp) |
|
62 apply(rule_tac y="x" in lam.exhaust) |
|
63 apply(auto)[6] |
|
64 apply(simp) |
|
65 apply(simp) |
|
66 apply(simp) |
|
67 apply (erule Abs1_eq_fdest) |
|
68 apply(simp add: fresh_def) |
|
69 apply(subst supp_of_finite_sets) |
|
70 apply(simp) |
|
71 apply(simp add: supp_atom) |
|
72 apply(simp add: fresh_def) |
|
73 apply(subst supp_of_finite_sets) |
|
74 apply(simp) |
|
75 apply(simp add: supp_atom) |
|
76 apply(subst supp_finite_atom_set[symmetric]) |
|
77 apply(simp) |
|
78 apply(simp add: fresh_def[symmetric]) |
|
79 apply(rule fresh_eqvt_at) |
|
80 apply(assumption) |
|
81 apply(simp add: finite_supp) |
|
82 apply(simp) |
|
83 apply(simp add: eqvt_at_def eqvts) |
|
84 apply(simp) |
|
85 done |
|
86 |
|
87 print_theorems |
|
88 |
|
89 termination |
|
90 by (relation "measure size") (auto simp add: lam.size) |
|
91 |
|
92 |
|
93 thm frees_set.simps |
|
94 |
50 lemma fresh_fun_eqvt_app3: |
95 lemma fresh_fun_eqvt_app3: |
51 assumes a: "eqvt f" |
96 assumes a: "eqvt f" |
52 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
97 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
53 shows "a \<sharp> f x y z" |
98 shows "a \<sharp> f x y z" |
54 using fresh_fun_eqvt_app[OF a b(1)] a b |
99 using fresh_fun_eqvt_app[OF a b(1)] a b |
70 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
115 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
71 | "f (Lam [x].t) = f3 x t (f t)" |
116 | "f (Lam [x].t) = f3 x t (f t)" |
72 apply (simp add: eqvt_def f_graph_def) |
117 apply (simp add: eqvt_def f_graph_def) |
73 apply (perm_simp) |
118 apply (perm_simp) |
74 apply(simp add: eq[simplified eqvt_def]) |
119 apply(simp add: eq[simplified eqvt_def]) |
|
120 apply(rule TrueI) |
75 apply(rule_tac y="x" in lam.exhaust) |
121 apply(rule_tac y="x" in lam.exhaust) |
76 apply(auto simp add: fresh_star_def) |
122 apply(auto simp add: fresh_star_def) |
77 apply(erule Abs1_eq_fdest) |
123 apply(erule Abs1_eq_fdest) |
78 apply simp_all |
124 apply simp_all |
79 apply(simp add: fcb) |
125 apply(simp add: fcb) |