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" binds x in t |
|
12 | Let_Rec bp::"bp" t::"trm" binds "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: |
|
32 fixes as bs :: "'a :: fs" |
|
33 and x y :: "'b :: fs" |
|
34 and c::"'c::fs" |
|
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" |
|
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" |
|
41 and props: "eqvt ba" "inj ba" |
|
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 |
|
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"] |
|
59 fin1 fin2 |
|
60 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
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" |
|
63 by (simp only: fr2 perm_supp_eq) |
|
64 finally have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = [ba bs]lst. y" using eq by simp |
|
65 then obtain r::perm where |
|
66 qq1: "q \<bullet> x = r \<bullet> y" and |
|
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)" |
|
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 |
|
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 |
|
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)" |
|
83 by (simp add: permute_bool_def) |
|
84 then have "set (q \<bullet> (ba as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
|
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 |
|
90 then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4 |
|
91 by simp |
|
92 then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)" |
|
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 |
|
98 then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
|
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) |
|
105 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq4 by simp |
|
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) |
|
142 apply(simp add: eqvt_def) |
|
143 apply(perm_simp) |
|
144 apply(simp) |
|
145 apply(simp add: inj_on_def) |
|
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) |
|
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 |
|
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 --"" |
|
184 apply(simp_all add: eqvt_def inj_on_def) |
|
185 apply(perm_simp) |
|
186 apply(simp) |
|
187 apply(perm_simp) |
|
188 apply(simp) |
|
189 done |
|
190 |
|
191 termination by lexicographic_order |
|
192 |
|
193 end |
|
194 |
|
195 |
|
196 |
|