93 val strip_psplits = |
93 val strip_psplits = |
94 let |
94 let |
95 fun strip [] qs vs t = (t, rev vs, qs) |
95 fun strip [] qs vs t = (t, rev vs, qs) |
96 | strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) = |
96 | strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) = |
97 strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t |
97 strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t |
98 | strip (p :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t |
98 | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t |
99 | strip (p :: ps) qs vs t = strip ps qs |
99 | strip (_ :: ps) qs vs t = strip ps qs |
100 ((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs) |
100 ((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs) |
101 (incr_boundvars 1 t $ Bound 0) |
101 (incr_boundvars 1 t $ Bound 0) |
102 in strip [[]] [] [] end; |
102 in strip [[]] [] [] end; |
103 |
103 |
104 (* patterns *) |
104 (* patterns *) |
314 |
314 |
315 |
315 |
316 (* preprocessing conversion: |
316 (* preprocessing conversion: |
317 rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *) |
317 rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *) |
318 |
318 |
319 fun comprehension_conv ctxt ct = |
319 fun comprehension_conv ss ct = |
320 let |
320 let |
|
321 val ctxt = Simplifier.the_context ss |
321 fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t) |
322 fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t) |
322 | dest_Collect t = raise TERM ("dest_Collect", [t]) |
323 | dest_Collect t = raise TERM ("dest_Collect", [t]) |
323 fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t |
324 fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t |
324 fun mk_term t = |
325 fun mk_term t = |
325 let |
326 let |
331 val eq = HOLogic.eq_const T $ Bound (length Ts) $ |
332 val eq = HOLogic.eq_const T $ Bound (length Ts) $ |
332 (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts))) |
333 (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts))) |
333 in |
334 in |
334 HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t''))) |
335 HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t''))) |
335 end; |
336 end; |
336 val tac = |
337 val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases} |
|
338 fun tac ctxt = |
337 rtac @{thm set_eqI} |
339 rtac @{thm set_eqI} |
338 THEN' Simplifier.simp_tac |
340 THEN' Simplifier.simp_tac |
339 (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm mem_Collect_eq}, @{thm prod.cases}]) |
341 (Simplifier.inherit_context ss (HOL_basic_ss addsimps unfold_thms)) |
340 THEN' rtac @{thm iffI} |
342 THEN' rtac @{thm iffI} |
341 THEN' REPEAT_DETERM o rtac @{thm exI} |
343 THEN' REPEAT_DETERM o rtac @{thm exI} |
342 THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac |
344 THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac |
343 THEN' REPEAT_DETERM o etac @{thm exE} |
345 THEN' REPEAT_DETERM o etac @{thm exE} |
344 THEN' etac @{thm conjE} |
346 THEN' etac @{thm conjE} |
345 THEN' REPEAT_DETERM o etac @{thm Pair_inject} |
347 THEN' REPEAT_DETERM o etac @{thm Pair_inject} |
346 THEN' hyp_subst_tac |
348 THEN' Subgoal.FOCUS (fn {prems, ...} => |
347 THEN' (atac ORELSE' rtac @{thm refl}) |
349 Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_ss addsimps prems)) 1) ctxt |
348 in |
350 in |
349 case try mk_term (term_of ct) of |
351 case try mk_term (term_of ct) of |
350 NONE => Thm.reflexive ct |
352 NONE => Thm.reflexive ct |
351 | SOME t' => |
353 | SOME t' => |
352 Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) (K (tac 1)) |
354 Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) |
353 RS @{thm eq_reflection} |
355 (fn {context, ...} => tac context 1) |
|
356 RS @{thm eq_reflection} |
354 end |
357 end |
355 |
358 |
356 |
359 |
357 (* main simprocs *) |
360 (* main simprocs *) |
358 |
361 |
362 val post_thms = |
365 val post_thms = |
363 map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]}, |
366 map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]}, |
364 @{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto}, |
367 @{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto}, |
365 @{lemma "(A \<times> B \<inter> C \<times> D) = (A \<inter> C) \<times> (B \<inter> D)" by auto}] |
368 @{lemma "(A \<times> B \<inter> C \<times> D) = (A \<inter> C) \<times> (B \<inter> D)" by auto}] |
366 |
369 |
367 fun conv ctxt t = |
370 fun conv ss t = |
368 let |
371 let |
|
372 val ctxt = Simplifier.the_context ss |
369 val ct = cterm_of (Proof_Context.theory_of ctxt) t |
373 val ct = cterm_of (Proof_Context.theory_of ctxt) t |
370 val prep_eq = (comprehension_conv ctxt then_conv Raw_Simplifier.rewrite true prep_thms) ct |
374 fun unfold_conv thms = |
|
375 Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) |
|
376 (Raw_Simplifier.inherit_context ss empty_ss addsimps thms) |
|
377 val prep_eq = (comprehension_conv ss then_conv unfold_conv prep_thms) ct |
371 val t' = term_of (Thm.rhs_of prep_eq) |
378 val t' = term_of (Thm.rhs_of prep_eq) |
372 fun mk_thm (fm, t'') = Goal.prove ctxt [] [] |
379 fun mk_thm (fm, t'') = Goal.prove ctxt [] [] |
373 (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1) |
380 (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1) |
374 fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans}) |
381 fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans}) |
375 fun post th = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv |
382 val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms))) |
376 (Raw_Simplifier.rewrite true post_thms))) th |
|
377 in |
383 in |
378 Option.map (post o unfold o mk_thm) (rewrite_term t') |
384 Option.map (post o unfold o mk_thm) (rewrite_term t') |
379 end; |
385 end; |
380 |
386 |
381 fun base_simproc ss redex = |
387 fun base_simproc ss redex = |
382 let |
388 let |
383 val ctxt = Simplifier.the_context ss |
|
384 val set_compr = term_of redex |
389 val set_compr = term_of redex |
385 in |
390 in |
386 conv ctxt set_compr |
391 conv ss set_compr |
387 |> Option.map (fn thm => thm RS @{thm eq_reflection}) |
392 |> Option.map (fn thm => thm RS @{thm eq_reflection}) |
388 end; |
393 end; |
389 |
394 |
390 fun instantiate_arg_cong ctxt pred = |
395 fun instantiate_arg_cong ctxt pred = |
391 let |
396 let |
400 let |
405 let |
401 val ctxt = Simplifier.the_context ss |
406 val ctxt = Simplifier.the_context ss |
402 val pred $ set_compr = term_of redex |
407 val pred $ set_compr = term_of redex |
403 val arg_cong' = instantiate_arg_cong ctxt pred |
408 val arg_cong' = instantiate_arg_cong ctxt pred |
404 in |
409 in |
405 conv ctxt set_compr |
410 conv ss set_compr |
406 |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection}) |
411 |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection}) |
407 end; |
412 end; |
408 |
413 |
409 fun code_simproc ss redex = |
414 fun code_simproc ss redex = |
410 let |
415 let |