2915
|
1 |
theory LetRecB
|
|
2 |
imports "../Nominal2"
|
|
3 |
begin
|
|
4 |
|
|
5 |
atom_decl name
|
|
6 |
|
|
7 |
nominal_datatype let_rec:
|
|
8 |
trm =
|
|
9 |
Var "name"
|
|
10 |
| App "trm" "trm"
|
|
11 |
| Lam x::"name" t::"trm" bind x in t
|
|
12 |
| Let_Rec bp::"bp" t::"trm" bind "bn bp" in bp t
|
|
13 |
and bp =
|
|
14 |
Bp "name" "trm"
|
|
15 |
binder
|
|
16 |
bn::"bp \<Rightarrow> atom list"
|
|
17 |
where
|
|
18 |
"bn (Bp x t) = [atom x]"
|
|
19 |
|
|
20 |
thm let_rec.distinct
|
|
21 |
thm let_rec.induct
|
|
22 |
thm let_rec.exhaust
|
|
23 |
thm let_rec.fv_defs
|
|
24 |
thm let_rec.bn_defs
|
|
25 |
thm let_rec.perm_simps
|
|
26 |
thm let_rec.eq_iff
|
|
27 |
thm let_rec.fv_bn_eqvt
|
|
28 |
thm let_rec.size_eqvt
|
|
29 |
|
|
30 |
|
|
31 |
lemma Abs_lst_fcb2:
|
2917
|
32 |
fixes as bs :: "'a :: fs"
|
2915
|
33 |
and x y :: "'b :: fs"
|
|
34 |
and c::"'c::fs"
|
2917
|
35 |
assumes eq: "[ba as]lst. x = [ba bs]lst. y"
|
|
36 |
and fcb1: "(set (ba as)) \<sharp>* f as x c"
|
|
37 |
and fresh1: "set (ba as) \<sharp>* c"
|
|
38 |
and fresh2: "set (ba bs) \<sharp>* c"
|
2915
|
39 |
and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
|
|
40 |
and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
|
2917
|
41 |
and props: "eqvt ba" "inj ba"
|
2915
|
42 |
shows "f as x c = f bs y c"
|
|
43 |
proof -
|
|
44 |
have "supp (as, x, c) supports (f as x c)"
|
|
45 |
unfolding supports_def fresh_def[symmetric]
|
|
46 |
by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)
|
|
47 |
then have fin1: "finite (supp (f as x c))"
|
|
48 |
by (auto intro: supports_finite simp add: finite_supp)
|
|
49 |
have "supp (bs, y, c) supports (f bs y c)"
|
|
50 |
unfolding supports_def fresh_def[symmetric]
|
|
51 |
by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)
|
|
52 |
then have fin2: "finite (supp (f bs y c))"
|
|
53 |
by (auto intro: supports_finite simp add: finite_supp)
|
|
54 |
obtain q::"perm" where
|
2917
|
55 |
fr1: "(q \<bullet> (set (ba as))) \<sharp>* (x, c, f as x c, f bs y c)" and
|
|
56 |
fr2: "supp q \<sharp>* ([ba as]lst. x)" and
|
|
57 |
inc: "supp q \<subseteq> (set (ba as)) \<union> q \<bullet> (set (ba as))"
|
|
58 |
using at_set_avoiding3[where xs="set (ba as)" and c="(x, c, f as x c, f bs y c)" and x="[ba as]lst. x"]
|
2915
|
59 |
fin1 fin2
|
|
60 |
by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
|
2917
|
61 |
have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = q \<bullet> ([ba as]lst. x)" by simp
|
|
62 |
also have "\<dots> = [ba as]lst. x"
|
2915
|
63 |
by (simp only: fr2 perm_supp_eq)
|
2917
|
64 |
finally have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = [ba bs]lst. y" using eq by simp
|
2915
|
65 |
then obtain r::perm where
|
|
66 |
qq1: "q \<bullet> x = r \<bullet> y" and
|
2917
|
67 |
qq2: "q \<bullet> (ba as) = r \<bullet> (ba bs)" and
|
|
68 |
qq3: "supp r \<subseteq> (q \<bullet> (set (ba as))) \<union> set (ba bs)"
|
2915
|
69 |
apply(drule_tac sym)
|
|
70 |
apply(simp only: Abs_eq_iff2 alphas)
|
|
71 |
apply(erule exE)
|
|
72 |
apply(erule conjE)+
|
|
73 |
apply(drule_tac x="p" in meta_spec)
|
|
74 |
apply(simp add: set_eqvt)
|
|
75 |
apply(blast)
|
|
76 |
done
|
2916
|
77 |
have qq4: "q \<bullet> as = r \<bullet> bs" using qq2 props unfolding eqvt_def inj_on_def
|
|
78 |
apply(perm_simp)
|
|
79 |
apply(simp)
|
|
80 |
done
|
2917
|
81 |
have "(set (ba as)) \<sharp>* f as x c" by (rule fcb1)
|
|
82 |
then have "q \<bullet> ((set (ba as)) \<sharp>* f as x c)"
|
2915
|
83 |
by (simp add: permute_bool_def)
|
2917
|
84 |
then have "set (q \<bullet> (ba as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
|
2915
|
85 |
apply(simp add: fresh_star_eqvt set_eqvt)
|
|
86 |
apply(subst (asm) perm1)
|
|
87 |
using inc fresh1 fr1
|
|
88 |
apply(auto simp add: fresh_star_def fresh_Pair)
|
|
89 |
done
|
2917
|
90 |
then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4
|
2916
|
91 |
by simp
|
2917
|
92 |
then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)"
|
2915
|
93 |
apply(simp add: fresh_star_eqvt set_eqvt)
|
|
94 |
apply(subst (asm) perm2[symmetric])
|
|
95 |
using qq3 fresh2 fr1
|
|
96 |
apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
|
|
97 |
done
|
2917
|
98 |
then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def)
|
2915
|
99 |
have "f as x c = q \<bullet> (f as x c)"
|
|
100 |
apply(rule perm_supp_eq[symmetric])
|
|
101 |
using inc fcb1 fr1 by (auto simp add: fresh_star_def)
|
|
102 |
also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
|
|
103 |
apply(rule perm1)
|
|
104 |
using inc fresh1 fr1 by (auto simp add: fresh_star_def)
|
2916
|
105 |
also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq4 by simp
|
2915
|
106 |
also have "\<dots> = r \<bullet> (f bs y c)"
|
|
107 |
apply(rule perm2[symmetric])
|
|
108 |
using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
|
|
109 |
also have "... = f bs y c"
|
|
110 |
apply(rule perm_supp_eq)
|
|
111 |
using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)
|
|
112 |
finally show ?thesis by simp
|
|
113 |
qed
|
|
114 |
|
|
115 |
|
|
116 |
lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
|
|
117 |
by (simp add: permute_pure)
|
|
118 |
|
|
119 |
nominal_primrec
|
|
120 |
height_trm :: "trm \<Rightarrow> nat"
|
|
121 |
and height_bp :: "bp \<Rightarrow> nat"
|
|
122 |
where
|
|
123 |
"height_trm (Var x) = 1"
|
|
124 |
| "height_trm (App l r) = max (height_trm l) (height_trm r)"
|
|
125 |
| "height_trm (Lam v b) = 1 + (height_trm b)"
|
|
126 |
| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
|
|
127 |
| "height_bp (Bp v t) = height_trm t"
|
|
128 |
--"eqvt"
|
|
129 |
apply (simp only: eqvt_def height_trm_height_bp_graph_def)
|
|
130 |
apply (rule, perm_simp, rule, rule TrueI)
|
|
131 |
--"completeness"
|
|
132 |
apply (case_tac x)
|
|
133 |
apply (case_tac a rule: let_rec.exhaust(1))
|
|
134 |
apply (auto)[4]
|
|
135 |
apply (case_tac b rule: let_rec.exhaust(2))
|
|
136 |
apply blast
|
|
137 |
apply(simp_all)
|
|
138 |
apply (erule_tac c="()" in Abs_lst_fcb2)
|
|
139 |
apply (simp_all add: fresh_star_def pure_fresh)[3]
|
|
140 |
apply (simp add: eqvt_at_def)
|
|
141 |
apply (simp add: eqvt_at_def)
|
2916
|
142 |
apply(simp add: eqvt_def)
|
|
143 |
apply(perm_simp)
|
|
144 |
apply(simp)
|
|
145 |
apply(simp add: inj_on_def)
|
2918
|
146 |
--"The following could be done by nominal"
|
|
147 |
apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
|
|
148 |
apply (simp add: meta_eq_to_obj_eq[OF height_bp_def, symmetric, unfolded fun_eq_iff])
|
|
149 |
apply (subgoal_tac "eqvt_at height_bp bp")
|
|
150 |
apply (subgoal_tac "eqvt_at height_bp bpa")
|
|
151 |
apply (subgoal_tac "eqvt_at height_trm b")
|
|
152 |
apply (subgoal_tac "eqvt_at height_trm ba")
|
|
153 |
apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bp)")
|
|
154 |
apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bpa)")
|
|
155 |
apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl b)")
|
|
156 |
apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl ba)")
|
|
157 |
defer
|
|
158 |
apply (simp add: eqvt_at_def height_trm_def)
|
|
159 |
apply (simp add: eqvt_at_def height_trm_def)
|
|
160 |
apply (simp add: eqvt_at_def height_bp_def)
|
|
161 |
apply (simp add: eqvt_at_def height_bp_def)
|
2919
|
162 |
apply (subgoal_tac "height_bp bp = height_bp bpa")
|
|
163 |
apply (subgoal_tac "height_trm b = height_trm ba")
|
|
164 |
apply simp
|
|
165 |
apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c")
|
|
166 |
apply simp
|
2920
|
167 |
apply (erule_tac c="()" in Abs_lst_fcb2)
|
|
168 |
apply (simp add: fresh_star_def pure_fresh)
|
|
169 |
apply (simp add: fresh_star_def pure_fresh)
|
|
170 |
apply (simp add: fresh_star_def pure_fresh)
|
|
171 |
apply (simp add: eqvt_at_def)
|
|
172 |
apply (simp add: eqvt_at_def)
|
|
173 |
defer defer
|
|
174 |
apply (subgoal_tac "(\<lambda>as x c. height_bp (fst (bp, b))) as x c = (\<lambda>as x c. height_bp (fst (bpa, ba))) as x c")
|
|
175 |
apply simp
|
|
176 |
apply (erule_tac c="()" in Abs_lst_fcb2)
|
|
177 |
apply (simp add: fresh_star_def pure_fresh)
|
|
178 |
apply (simp add: fresh_star_def pure_fresh)
|
|
179 |
apply (simp add: fresh_star_def pure_fresh)
|
|
180 |
apply (simp add: fresh_star_def pure_fresh)
|
|
181 |
apply (simp add: eqvt_at_def)
|
|
182 |
apply (simp add: eqvt_at_def)
|
|
183 |
--""
|
2922
|
184 |
apply(simp_all add: eqvt_def inj_on_def)
|
|
185 |
apply(perm_simp)
|
|
186 |
apply(simp)
|
|
187 |
apply(perm_simp)
|
|
188 |
apply(simp)
|
2915
|
189 |
done
|
|
190 |
|
|
191 |
termination by lexicographic_order
|
|
192 |
|
|
193 |
end
|
|
194 |
|
|
195 |
|
|
196 |
|