15 |
15 |
16 use "nominal_dt_quot.ML" |
16 use "nominal_dt_quot.ML" |
17 ML {* open Nominal_Dt_Quot *} |
17 ML {* open Nominal_Dt_Quot *} |
18 |
18 |
19 text {* TEST *} |
19 text {* TEST *} |
20 |
|
21 ML {* |
|
22 fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
|
23 | strip_outer_params B = ([], B) |
|
24 |
|
25 fun strip_params_prems_concl trm = |
|
26 let |
|
27 val (params, body) = strip_outer_params trm |
|
28 val (prems, concl) = Logic.strip_horn body |
|
29 in |
|
30 (params, prems, concl) |
|
31 end |
|
32 |
|
33 fun list_params_prems_concl params prems concl = |
|
34 Logic.list_implies (prems, concl) |
|
35 |> fold_rev mk_all params |
|
36 |
|
37 fun mk_binop_env tys c (t, u) = |
|
38 let val ty = fastype_of1 (tys, t) in |
|
39 Const (c, [ty, ty] ---> ty) $ t $ u |
|
40 end |
|
41 |
|
42 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
|
43 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
|
44 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
|
45 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
|
46 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
|
47 |
|
48 fun fold_left f [] z = z |
|
49 | fold_left f [x] z = x |
|
50 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
|
51 |
|
52 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} |
|
53 *} |
|
54 |
|
55 |
20 |
56 |
21 |
57 ML {* |
22 ML {* |
58 (* adds a freshness condition to the assumptions *) |
23 (* adds a freshness condition to the assumptions *) |
59 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
24 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
117 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
82 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
118 end |
83 end |
119 *} |
84 *} |
120 |
85 |
121 ML {* |
86 ML {* |
122 (* derives an abs_eq theorem of the form |
87 fun abs_const bmode ty = |
123 |
|
124 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
|
125 Exists q. [as].x = [q o as].(q o x) for recursive binders |
|
126 *) |
|
127 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
|
128 (bclause as (BC (bmode, binders, bodies))) = |
|
129 case binders of |
|
130 [] => [] |
|
131 | _ => |
|
132 let |
|
133 val flag = is_recursive_binder bclause |
|
134 val binder_trm = comb_binders ctxt bmode parms binders |
|
135 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
|
136 val body_ty = fastype_of body_trm |
|
137 |
|
138 fun mk_abs cnst_name ty1 ty2 = |
|
139 Const (cnst_name, [ty1, body_ty] ---> Type (ty2, [body_ty])) |
|
140 |
|
141 val abs_const = |
|
142 case bmode of |
|
143 Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst} |
|
144 | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"} @{type_name abs_set} |
|
145 | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"} @{type_name abs_res} |
|
146 |
|
147 val abs_lhs = abs_const $ binder_trm $ body_trm |
|
148 val abs_rhs = |
|
149 if flag |
|
150 then abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm |
|
151 else abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm |
|
152 |
|
153 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
|
154 val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) |
|
155 |
|
156 val goal = HOLogic.mk_conj (abs_eq, peq) |
|
157 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
|
158 |> HOLogic.mk_Trueprop |
|
159 |
|
160 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
|
161 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
|
162 fresh_star_set} @ @{thms finite.intros finite_fset} |
|
163 |
|
164 val tac1 = |
|
165 if flag |
|
166 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
|
167 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
168 |
|
169 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
|
170 in |
|
171 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
|
172 |> (if flag |
|
173 then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
|
174 else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) |
|
175 ] |
|
176 end |
|
177 *} |
|
178 |
|
179 ML {* |
|
180 fun conj_tac tac i = |
|
181 let |
88 let |
182 fun select (t, i) = |
89 val (const_name, binder_ty, abs_ty) = |
183 case t of |
90 case bmode of |
184 @{term "Trueprop"} $ t' => select (t', i) |
91 Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) |
185 | @{term "op \<and>"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i |
92 | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) |
186 | _ => tac i |
93 | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) |
187 in |
94 in |
188 SUBGOAL select i |
95 Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) |
189 end |
96 end |
190 *} |
97 |
191 |
98 fun mk_abs bmode trm1 trm2 = |
192 ML {* |
99 abs_const bmode (fastype_of trm2) $ trm1 $ trm2 |
|
100 |
193 fun is_abs_eq thm = |
101 fun is_abs_eq thm = |
194 let |
102 let |
195 fun is_abs trm = |
103 fun is_abs trm = |
196 case (head_of trm) of |
104 case (head_of trm) of |
197 Const (@{const_name "Abs_set"}, _) => true |
105 Const (@{const_name "Abs_set"}, _) => true |
205 |> fst |
113 |> fst |
206 |> is_abs |
114 |> is_abs |
207 end |
115 end |
208 *} |
116 *} |
209 |
117 |
|
118 |
|
119 |
|
120 ML {* |
|
121 (* derives an abs_eq theorem of the form |
|
122 |
|
123 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
|
124 Exists q. [as].x = [q o as].(q o x) for recursive binders |
|
125 *) |
|
126 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
|
127 (bclause as (BC (bmode, binders, bodies))) = |
|
128 case binders of |
|
129 [] => [] |
|
130 | _ => |
|
131 let |
|
132 val rec_flag = is_recursive_binder bclause |
|
133 val binder_trm = comb_binders ctxt bmode parms binders |
|
134 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
|
135 |
|
136 val abs_lhs = mk_abs bmode binder_trm body_trm |
|
137 val abs_rhs = |
|
138 if rec_flag |
|
139 then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) |
|
140 else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) |
|
141 |
|
142 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
|
143 val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) |
|
144 |
|
145 val goal = HOLogic.mk_conj (abs_eq, peq) |
|
146 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
|
147 |> HOLogic.mk_Trueprop |
|
148 |
|
149 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
|
150 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
|
151 fresh_star_set} @ @{thms finite.intros finite_fset} |
|
152 |
|
153 val tac1 = |
|
154 if rec_flag |
|
155 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
|
156 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
157 |
|
158 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
|
159 in |
|
160 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
|
161 |> (if rec_flag |
|
162 then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
|
163 else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] |
|
164 end |
|
165 *} |
|
166 |
|
167 |
|
168 |
210 lemma setify: |
169 lemma setify: |
211 shows "xs = ys \<Longrightarrow> set xs = set ys" |
170 shows "xs = ys \<Longrightarrow> set xs = set ys" |
212 by simp |
171 by simp |
213 |
172 |
214 ML {* |
173 ML {* |
239 REPEAT o (dtac @{thm setify}), |
198 REPEAT o (dtac @{thm setify}), |
240 full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' |
199 full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' |
241 |
200 |
242 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
201 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
243 |
202 |
244 val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops |
203 val fprops' = |
245 val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops |
204 map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops |
246 |
205 @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops |
247 val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem) |
206 |
248 val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems)) |
207 (* for freshness conditions *) |
249 val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops')) |
208 val tac1 = SOLVED' (EVERY' |
250 val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'')) |
|
251 val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs)) |
|
252 val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs)) |
|
253 |
|
254 |
|
255 val tac1 = EVERY' |
|
256 [ simp_tac (HOL_basic_ss addsimps peqs), |
209 [ simp_tac (HOL_basic_ss addsimps peqs), |
257 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |
210 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |
258 K (print_tac "before solving freshness"), |
211 conj_tac (DETERM o resolve_tac fprops') ]) |
259 conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] |
212 |
260 |
213 (* for equalities between constructors *) |
261 val tac2 = EVERY' |
214 val tac2 = SOLVED' (EVERY' |
262 [ rtac (@{thm ssubst} OF prems), |
215 [ rtac (@{thm ssubst} OF prems), |
263 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), |
216 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), |
264 K (print_tac "before substituting"), |
|
265 rewrite_goal_tac (map safe_mk_equiv abs_eqs), |
217 rewrite_goal_tac (map safe_mk_equiv abs_eqs), |
266 K (print_tac "after substituting"), |
218 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
267 conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)), |
219 |
268 K (print_tac "end") |
220 (* proves goal "P" *) |
269 ] |
|
270 |
|
271 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
221 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
272 (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *) |
222 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |
273 EVERY |
|
274 [ rtac prem 1, |
|
275 print_tac "after applying prem", |
|
276 RANGE [SOLVED' tac1, SOLVED' tac2] 1, |
|
277 print_tac "final" ] ) |
|
278 |> singleton (ProofContext.export ctxt'' ctxt) |
223 |> singleton (ProofContext.export ctxt'' ctxt) |
279 |
|
280 val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm) |
|
281 in |
224 in |
282 rtac side_thm 1 |
225 rtac side_thm 1 |
283 end) ctxt |
226 end) ctxt |
284 in |
227 in |
285 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
228 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
293 val ((_, exhausts'), lthy') = Variable.import true exhausts lthy |
236 val ((_, exhausts'), lthy') = Variable.import true exhausts lthy |
294 |
237 |
295 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
238 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
296 val c = Free (c, TFree (a, @{sort fs})) |
239 val c = Free (c, TFree (a, @{sort fs})) |
297 |
240 |
298 val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *) |
241 val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) |
299 |> map prop_of |
242 |> map prop_of |
300 |> map Logic.strip_horn |
243 |> map Logic.strip_horn |
301 |> split_list |
244 |> split_list |
302 |>> (map o map) strip_params_prems_concl |
245 |
303 |
246 val ecases' = (map o map) strip_full_horn ecases |
304 val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases bclausesss |
247 |
|
248 val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss |
305 |
249 |
306 fun tac bclausess exhaust {prems, context} = |
250 fun tac bclausess exhaust {prems, context} = |
307 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
251 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
308 prems bclausess exhaust |
252 prems bclausess exhaust |
309 |
253 |