171 val gcase = Term.list_comb (casex, eta_gs); |
172 val gcase = Term.list_comb (casex, eta_gs); |
172 |
173 |
173 val exist_xs_v_eq_ctrs = |
174 val exist_xs_v_eq_ctrs = |
174 map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; |
175 map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; |
175 |
176 |
176 fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT); |
177 val unique_disc_no_def = TrueI; (*arbitrary marker*) |
177 |
178 val alternate_disc_no_def = FalseE; (*arbitrary marker*) |
178 fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); |
179 |
179 |
180 fun alternate_disc_lhs get_disc k = |
180 fun alternate_disc_lhs k = |
|
181 HOLogic.mk_not |
181 HOLogic.mk_not |
182 (case nth disc_binders (k - 1) of |
182 (case nth disc_binders (k - 1) of |
183 NONE => nth exist_xs_v_eq_ctrs (k - 1) |
183 NONE => nth exist_xs_v_eq_ctrs (k - 1) |
184 | SOME b => disc_free b $ v); |
184 | SOME b => get_disc b (k - 1) $ v); |
185 |
185 |
186 fun alternate_disc k = |
186 val (discs, selss, disc_defs, sel_defss, lthy') = |
187 if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here" |
187 if no_dests then |
188 |
188 ([], [], [], [], no_defs_lthy) |
189 fun mk_sel_case_args proto_sels T = |
189 else |
190 map2 (fn Ts => fn i => |
190 let |
191 case AList.lookup (op =) proto_sels i of |
191 fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT); |
192 NONE => mk_undef T Ts |
192 |
193 | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks; |
193 fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); |
194 |
194 |
195 fun sel_spec b proto_sels = |
195 fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k)); |
196 let |
196 |
197 val _ = |
197 fun mk_sel_case_args proto_sels T = |
198 (case duplicates (op =) (map fst proto_sels) of |
198 map2 (fn Ts => fn i => |
199 k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ |
199 case AList.lookup (op =) proto_sels i of |
200 " for constructor " ^ quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1)))) |
200 NONE => mk_undef T Ts |
201 | [] => ()) |
201 | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks; |
202 val T = |
202 |
203 (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of |
203 fun sel_spec b proto_sels = |
204 [T] => T |
204 let |
205 | T :: T' :: _ => error ("Inconsistent range type for selector " ^ |
205 val _ = |
206 quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ |
206 (case duplicates (op =) (map fst proto_sels) of |
207 " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); |
207 k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ |
208 in |
208 " for constructor " ^ |
209 mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v, |
209 quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1)))) |
210 Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v) |
210 | [] => ()) |
211 end; |
211 val T = |
212 |
212 (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of |
213 val missing_unique_disc_def = TrueI; (*arbitrary marker*) |
213 [T] => T |
214 val missing_alternate_disc_def = FalseE; (*arbitrary marker*) |
214 | T :: T' :: _ => error ("Inconsistent range type for selector " ^ |
215 |
215 quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ |
216 val proto_selss = map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss; |
216 " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); |
217 val sel_bundles = AList.group Binding.eq_name (flat sel_binderss ~~ flat proto_selss); |
217 in |
218 val sel_binders = map fst sel_bundles; |
218 mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v, |
219 |
219 Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v) |
220 fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; |
220 end; |
221 |
221 |
222 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = |
222 val proto_selss = map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss; |
223 no_defs_lthy |
223 val sel_bundles = AList.group Binding.eq_name (flat sel_binderss ~~ flat proto_selss); |
224 |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => |
224 val sel_binders = map fst sel_bundles; |
225 fn NONE => |
225 |
226 if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), missing_unique_disc_def) |
226 fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; |
227 else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) |
227 |
228 else pair (alternate_disc k, missing_alternate_disc_def) |
228 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = |
229 | SOME b => Specification.definition (SOME (b, NONE, NoSyn), |
229 no_defs_lthy |
230 ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) |
230 |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr => |
231 ks ms exist_xs_v_eq_ctrs disc_binders |
231 fn NONE => |
232 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
232 if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), unique_disc_no_def) |
233 Specification.definition (SOME (b, NONE, NoSyn), |
233 else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl) |
234 ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles |
234 else pair (alternate_disc k, alternate_disc_no_def) |
235 ||> `Local_Theory.restore; |
235 | SOME b => Specification.definition (SOME (b, NONE, NoSyn), |
236 |
236 ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) |
237 (*transforms defined frees into consts (and more)*) |
237 ks ms exist_xs_v_eq_ctrs disc_binders |
238 val phi = Proof_Context.export_morphism lthy lthy'; |
238 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
239 |
239 Specification.definition (SOME (b, NONE, NoSyn), |
240 val disc_defs = map (Morphism.thm phi) raw_disc_defs; |
240 ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles |
241 val sel_defss = unflat_selss (map (Morphism.thm phi) raw_sel_defs); |
241 ||> `Local_Theory.restore; |
242 |
242 |
243 val discs0 = map (Morphism.term phi) raw_discs; |
243 (*transforms defined frees into consts (and more)*) |
244 val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); |
244 val phi = Proof_Context.export_morphism lthy lthy'; |
245 |
245 |
246 fun mk_disc_or_sel Ts c = |
246 val disc_defs = map (Morphism.thm phi) raw_disc_defs; |
247 Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c; |
247 val sel_defss = unflat_selss (map (Morphism.thm phi) raw_sel_defs); |
248 |
248 |
249 val discs = map (mk_disc_or_sel As) discs0; |
249 val discs0 = map (Morphism.term phi) raw_discs; |
250 val selss = map (map (mk_disc_or_sel As)) selss0; |
250 val selss0 = unflat_selss (map (Morphism.term phi) raw_sels); |
|
251 |
|
252 fun mk_disc_or_sel Ts c = |
|
253 Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c; |
|
254 |
|
255 val discs = map (mk_disc_or_sel As) discs0; |
|
256 val selss = map (map (mk_disc_or_sel As)) selss0; |
|
257 in |
|
258 (discs, selss, disc_defs, sel_defss, lthy') |
|
259 end; |
251 |
260 |
252 fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); |
261 fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); |
253 |
262 |
254 val goal_exhaust = |
263 val goal_exhaust = |
255 let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in |
264 let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in |
307 Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); |
316 Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); |
308 in |
317 in |
309 Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) |
318 Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) |
310 end; |
319 end; |
311 |
320 |
312 val sel_thmss = |
321 val (sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, collapse_thms, |
313 map2 (fn case_thm => map (fn sel_def => case_thm RS (sel_def RS trans))) case_thms |
322 case_eq_thms) = |
314 sel_defss; |
323 if no_dests then |
315 |
324 ([], [], [], [], [], [], []) |
316 fun mk_unique_disc_def () = |
|
317 let |
|
318 val m = the_single ms; |
|
319 val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); |
|
320 in |
|
321 Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm') |
|
322 |> singleton (Proof_Context.export names_lthy lthy) |
|
323 |> Thm.close_derivation |
|
324 end; |
|
325 |
|
326 fun mk_alternate_disc_def k = |
|
327 let |
|
328 val goal = |
|
329 mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)), |
|
330 nth exist_xs_v_eq_ctrs (k - 1)); |
|
331 in |
|
332 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
333 mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k)) |
|
334 exhaust_thm') |
|
335 |> singleton (Proof_Context.export names_lthy lthy) |
|
336 |> Thm.close_derivation |
|
337 end; |
|
338 |
|
339 val has_alternate_disc_def = |
|
340 exists (fn def => Thm.eq_thm_prop (def, missing_alternate_disc_def)) disc_defs; |
|
341 |
|
342 val disc_defs' = |
|
343 map2 (fn k => fn def => |
|
344 if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def () |
|
345 else if Thm.eq_thm_prop (def, missing_alternate_disc_def) then mk_alternate_disc_def k |
|
346 else def) |
|
347 ks disc_defs; |
|
348 |
|
349 val discD_thms = map (fn def => def RS iffD1) disc_defs'; |
|
350 val discI_thms = |
|
351 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs'; |
|
352 val not_discI_thms = |
|
353 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
|
354 (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
|
355 ms disc_defs'; |
|
356 |
|
357 val (disc_thmss', disc_thmss) = |
|
358 let |
|
359 fun mk_thm discI _ [] = refl RS discI |
|
360 | mk_thm _ not_discI [distinct] = distinct RS not_discI; |
|
361 fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; |
|
362 in |
|
363 map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose |
|
364 end; |
|
365 |
|
366 val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss); |
|
367 |
|
368 val disc_exclude_thms = |
|
369 if has_alternate_disc_def then |
|
370 [] |
|
371 else |
325 else |
372 let |
326 let |
373 fun mk_goal [] = [] |
327 val sel_thmss = |
374 | mk_goal [((_, true), (_, true))] = [] |
328 map2 (fn case_thm => map (fn sel_def => case_thm RS (sel_def RS trans))) case_thms |
375 | mk_goal [(((_, disc), _), ((_, disc'), _))] = |
329 sel_defss; |
376 [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), |
330 |
377 HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; |
331 fun mk_unique_disc_def () = |
378 fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); |
332 let |
379 |
333 val m = the_single ms; |
380 val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; |
334 val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs); |
381 val half_pairss = mk_half_pairss bundles; |
335 in |
382 |
336 Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm') |
383 val goal_halvess = map mk_goal half_pairss; |
337 |> singleton (Proof_Context.export names_lthy lthy) |
384 val half_thmss = |
338 |> Thm.close_derivation |
385 map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm => |
339 end; |
386 [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) |
340 |
387 goal_halvess half_pairss (flat disc_thmss'); |
341 fun mk_alternate_disc_def k = |
388 |
342 let |
389 val goal_other_halvess = map (mk_goal o map swap) half_pairss; |
343 val goal = |
390 val other_half_thmss = |
344 mk_Trueprop_eq (alternate_disc_lhs (K (nth discs)) (3 - k), |
391 map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss goal_other_halvess; |
345 nth exist_xs_v_eq_ctrs (k - 1)); |
|
346 in |
|
347 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
348 mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) |
|
349 (nth distinct_thms (2 - k)) exhaust_thm') |
|
350 |> singleton (Proof_Context.export names_lthy lthy) |
|
351 |> Thm.close_derivation |
|
352 end; |
|
353 |
|
354 val has_alternate_disc_def = |
|
355 exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs; |
|
356 |
|
357 val disc_defs' = |
|
358 map2 (fn k => fn def => |
|
359 if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def () |
|
360 else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k |
|
361 else def) ks disc_defs; |
|
362 |
|
363 val discD_thms = map (fn def => def RS iffD1) disc_defs'; |
|
364 val discI_thms = |
|
365 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms |
|
366 disc_defs'; |
|
367 val not_discI_thms = |
|
368 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
|
369 (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
|
370 ms disc_defs'; |
|
371 |
|
372 val (disc_thmss', disc_thmss) = |
|
373 let |
|
374 fun mk_thm discI _ [] = refl RS discI |
|
375 | mk_thm _ not_discI [distinct] = distinct RS not_discI; |
|
376 fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss; |
|
377 in |
|
378 map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose |
|
379 end; |
|
380 |
|
381 val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss); |
|
382 |
|
383 val disc_exclude_thms = |
|
384 if has_alternate_disc_def then |
|
385 [] |
|
386 else |
|
387 let |
|
388 fun mk_goal [] = [] |
|
389 | mk_goal [((_, true), (_, true))] = [] |
|
390 | mk_goal [(((_, disc), _), ((_, disc'), _))] = |
|
391 [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), |
|
392 HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; |
|
393 fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); |
|
394 |
|
395 val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; |
|
396 val half_pairss = mk_half_pairss bundles; |
|
397 |
|
398 val goal_halvess = map mk_goal half_pairss; |
|
399 val half_thmss = |
|
400 map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => |
|
401 fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal]) |
|
402 goal_halvess half_pairss (flat disc_thmss'); |
|
403 |
|
404 val goal_other_halvess = map (mk_goal o map swap) half_pairss; |
|
405 val other_half_thmss = |
|
406 map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss |
|
407 goal_other_halvess; |
|
408 in |
|
409 interleave (flat half_thmss) (flat other_half_thmss) |
|
410 end; |
|
411 |
|
412 val disc_exhaust_thms = |
|
413 if has_alternate_disc_def orelse no_discs_at_all then |
|
414 [] |
|
415 else |
|
416 let |
|
417 fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; |
|
418 val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs)); |
|
419 in |
|
420 [Skip_Proof.prove lthy [] [] goal (fn _ => |
|
421 mk_disc_exhaust_tac n exhaust_thm discI_thms)] |
|
422 end; |
|
423 |
|
424 val collapse_thms = |
|
425 if no_dests then |
|
426 [] |
|
427 else |
|
428 let |
|
429 fun mk_goal ctr disc sels = |
|
430 let |
|
431 val prem = HOLogic.mk_Trueprop (betapply (disc, v)); |
|
432 val concl = |
|
433 mk_Trueprop_eq ((null sels ? swap) |
|
434 (Term.list_comb (ctr, map ap_v sels), v)); |
|
435 in |
|
436 if prem aconv concl then NONE |
|
437 else SOME (Logic.all v (Logic.mk_implies (prem, concl))) |
|
438 end; |
|
439 val goals = map3 mk_goal ctrs discs selss; |
|
440 in |
|
441 map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => |
|
442 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
443 mk_collapse_tac ctxt m discD sel_thms) |
|
444 |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals |
|
445 |> map_filter I |
|
446 end; |
|
447 |
|
448 val case_eq_thms = |
|
449 if no_dests then |
|
450 [] |
|
451 else |
|
452 let |
|
453 fun mk_body f sels = Term.list_comb (f, map ap_v sels); |
|
454 val goal = |
|
455 mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss)); |
|
456 in |
|
457 [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
458 mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)] |
|
459 |> Proof_Context.export names_lthy lthy |
|
460 end; |
392 in |
461 in |
393 interleave (flat half_thmss) (flat other_half_thmss) |
462 (sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, |
|
463 collapse_thms, case_eq_thms) |
394 end; |
464 end; |
395 |
|
396 val disc_exhaust_thms = |
|
397 if has_alternate_disc_def orelse no_discs_at_all then |
|
398 [] |
|
399 else |
|
400 let |
|
401 fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; |
|
402 val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs)); |
|
403 in |
|
404 [Skip_Proof.prove lthy [] [] goal (fn _ => |
|
405 mk_disc_exhaust_tac n exhaust_thm discI_thms)] |
|
406 end; |
|
407 |
|
408 val collapse_thms = |
|
409 let |
|
410 fun mk_goal ctr disc sels = |
|
411 let |
|
412 val prem = HOLogic.mk_Trueprop (betapply (disc, v)); |
|
413 val concl = |
|
414 mk_Trueprop_eq ((null sels ? swap) (Term.list_comb (ctr, map ap_v sels), v)); |
|
415 in |
|
416 if prem aconv concl then NONE |
|
417 else SOME (Logic.all v (Logic.mk_implies (prem, concl))) |
|
418 end; |
|
419 val goals = map3 mk_goal ctrs discs selss; |
|
420 in |
|
421 map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => |
|
422 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
423 mk_collapse_tac ctxt m discD sel_thms) |
|
424 |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals |
|
425 |> map_filter I |
|
426 end; |
|
427 |
|
428 val case_eq_thm = |
|
429 let |
|
430 fun mk_body f sels = Term.list_comb (f, map ap_v sels); |
|
431 val goal = |
|
432 mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss)); |
|
433 in |
|
434 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
|
435 mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss) |
|
436 |> singleton (Proof_Context.export names_lthy lthy) |
|
437 end; |
|
438 |
465 |
439 val (case_cong_thm, weak_case_cong_thm) = |
466 val (case_cong_thm, weak_case_cong_thm) = |
440 let |
467 let |
441 fun mk_prem xctr xs f g = |
468 fun mk_prem xctr xs f g = |
442 fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), |
469 fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (w, xctr), |