227 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) |
227 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) |
228 (map all_modes_of_typ' S) [Bool] |
228 (map all_modes_of_typ' S) [Bool] |
229 else |
229 else |
230 [Input, Output] |
230 [Input, Output] |
231 end |
231 end |
232 | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
232 | all_modes_of_typ' (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
233 map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) |
233 map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2) |
234 | all_modes_of_typ' _ = [Input, Output] |
234 | all_modes_of_typ' _ = [Input, Output] |
235 |
235 |
236 fun all_modes_of_typ (T as Type ("fun", _)) = |
236 fun all_modes_of_typ (T as Type ("fun", _)) = |
237 let |
237 let |
238 val (S, U) = strip_type T |
238 val (S, U) = strip_type T |
239 in |
239 in |
240 if U = @{typ bool} then |
240 if U = \<^typ>\<open>bool\<close> then |
241 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) |
241 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) |
242 (map all_modes_of_typ' S) [Bool] |
242 (map all_modes_of_typ' S) [Bool] |
243 else |
243 else |
244 raise Fail "Invocation of all_modes_of_typ with a non-predicate type" |
244 raise Fail "Invocation of all_modes_of_typ with a non-predicate type" |
245 end |
245 end |
246 | all_modes_of_typ @{typ bool} = [Bool] |
246 | all_modes_of_typ \<^typ>\<open>bool\<close> = [Bool] |
247 | all_modes_of_typ _ = |
247 | all_modes_of_typ _ = |
248 raise Fail "Invocation of all_modes_of_typ with a non-predicate type" |
248 raise Fail "Invocation of all_modes_of_typ with a non-predicate type" |
249 |
249 |
250 fun all_smodes_of_typ (T as Type ("fun", _)) = |
250 fun all_smodes_of_typ (T as Type ("fun", _)) = |
251 let |
251 let |
252 val (S, U) = strip_type T |
252 val (S, U) = strip_type T |
253 fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
253 fun all_smodes (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
254 map_product (curry Pair) (all_smodes T1) (all_smodes T2) |
254 map_product (curry Pair) (all_smodes T1) (all_smodes T2) |
255 | all_smodes _ = [Input, Output] |
255 | all_smodes _ = [Input, Output] |
256 in |
256 in |
257 if U = HOLogic.boolT then |
257 if U = HOLogic.boolT then |
258 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool] |
258 fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool] |
271 |
271 |
272 fun ho_args_of mode ts = |
272 fun ho_args_of mode ts = |
273 let |
273 let |
274 fun ho_arg (Fun _) (SOME t) = [t] |
274 fun ho_arg (Fun _) (SOME t) = [t] |
275 | ho_arg (Fun _) NONE = raise Fail "mode and term do not match" |
275 | ho_arg (Fun _) NONE = raise Fail "mode and term do not match" |
276 | ho_arg (Pair (m1, m2)) (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) = |
276 | ho_arg (Pair (m1, m2)) (SOME (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2)) = |
277 ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2) |
277 ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2) |
278 | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE |
278 | ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE |
279 | ho_arg _ _ = [] |
279 | ho_arg _ _ = [] |
280 in |
280 in |
281 flat (map2_optional ho_arg (strip_fun_mode mode) ts) |
281 flat (map2_optional ho_arg (strip_fun_mode mode) ts) |
282 end |
282 end |
283 |
283 |
284 fun ho_args_of_typ T ts = |
284 fun ho_args_of_typ T ts = |
285 let |
285 let |
286 fun ho_arg (T as Type ("fun", [_, _])) (SOME t) = |
286 fun ho_arg (T as Type ("fun", [_, _])) (SOME t) = |
287 if body_type T = @{typ bool} then [t] else [] |
287 if body_type T = \<^typ>\<open>bool\<close> then [t] else [] |
288 | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match" |
288 | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match" |
289 | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) |
289 | ho_arg (Type(\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) |
290 (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) = |
290 (SOME (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2)) = |
291 ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2) |
291 ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2) |
292 | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) NONE = |
292 | ho_arg (Type(\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) NONE = |
293 ho_arg T1 NONE @ ho_arg T2 NONE |
293 ho_arg T1 NONE @ ho_arg T2 NONE |
294 | ho_arg _ _ = [] |
294 | ho_arg _ _ = [] |
295 in |
295 in |
296 flat (map2_optional ho_arg (binder_types T) ts) |
296 flat (map2_optional ho_arg (binder_types T) ts) |
297 end |
297 end |
298 |
298 |
299 fun ho_argsT_of_typ Ts = |
299 fun ho_argsT_of_typ Ts = |
300 let |
300 let |
301 fun ho_arg (T as Type("fun", [_,_])) = if body_type T = @{typ bool} then [T] else [] |
301 fun ho_arg (T as Type("fun", [_,_])) = if body_type T = \<^typ>\<open>bool\<close> then [T] else [] |
302 | ho_arg (Type (@{type_name "Product_Type.prod"}, [T1, T2])) = |
302 | ho_arg (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
303 ho_arg T1 @ ho_arg T2 |
303 ho_arg T1 @ ho_arg T2 |
304 | ho_arg _ = [] |
304 | ho_arg _ = [] |
305 in |
305 in |
306 maps ho_arg Ts |
306 maps ho_arg Ts |
307 end |
307 end |
309 |
309 |
310 (* temporary function should be replaced by unsplit_input or so? *) |
310 (* temporary function should be replaced by unsplit_input or so? *) |
311 fun replace_ho_args mode hoargs ts = |
311 fun replace_ho_args mode hoargs ts = |
312 let |
312 let |
313 fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs') |
313 fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs') |
314 | replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs = |
314 | replace (Pair (m1, m2), Const (\<^const_name>\<open>Pair\<close>, T) $ t1 $ t2) hoargs = |
315 let |
315 let |
316 val (t1', hoargs') = replace (m1, t1) hoargs |
316 val (t1', hoargs') = replace (m1, t1) hoargs |
317 val (t2', hoargs'') = replace (m2, t2) hoargs' |
317 val (t2', hoargs'') = replace (m2, t2) hoargs' |
318 in |
318 in |
319 (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'') |
319 (Const (\<^const_name>\<open>Pair\<close>, T) $ t1' $ t2', hoargs'') |
320 end |
320 end |
321 | replace (_, t) hoargs = (t, hoargs) |
321 | replace (_, t) hoargs = (t, hoargs) |
322 in |
322 in |
323 fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs) |
323 fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs) |
324 end |
324 end |
325 |
325 |
326 fun ho_argsT_of mode Ts = |
326 fun ho_argsT_of mode Ts = |
327 let |
327 let |
328 fun ho_arg (Fun _) T = [T] |
328 fun ho_arg (Fun _) T = [T] |
329 | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
329 | ho_arg (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
330 ho_arg m1 T1 @ ho_arg m2 T2 |
330 ho_arg m1 T1 @ ho_arg m2 T2 |
331 | ho_arg _ _ = [] |
331 | ho_arg _ _ = [] |
332 in |
332 in |
333 flat (map2 ho_arg (strip_fun_mode mode) Ts) |
333 flat (map2 ho_arg (strip_fun_mode mode) Ts) |
334 end |
334 end |
335 |
335 |
336 (* splits mode and maps function to higher-order argument types *) |
336 (* splits mode and maps function to higher-order argument types *) |
337 fun split_map_mode f mode ts = |
337 fun split_map_mode f mode ts = |
338 let |
338 let |
339 fun split_arg_mode' (m as Fun _) t = f m t |
339 fun split_arg_mode' (m as Fun _) t = f m t |
340 | split_arg_mode' (Pair (m1, m2)) (Const (@{const_name Pair}, _) $ t1 $ t2) = |
340 | split_arg_mode' (Pair (m1, m2)) (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) = |
341 let |
341 let |
342 val (i1, o1) = split_arg_mode' m1 t1 |
342 val (i1, o1) = split_arg_mode' m1 t1 |
343 val (i2, o2) = split_arg_mode' m2 t2 |
343 val (i2, o2) = split_arg_mode' m2 t2 |
344 in |
344 in |
345 (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) |
345 (comb_option HOLogic.mk_prod (i1, i2), comb_option HOLogic.mk_prod (o1, o2)) |
354 |
354 |
355 (* splits mode and maps function to higher-order argument types *) |
355 (* splits mode and maps function to higher-order argument types *) |
356 fun split_map_modeT f mode Ts = |
356 fun split_map_modeT f mode Ts = |
357 let |
357 let |
358 fun split_arg_mode' (m as Fun _) T = f m T |
358 fun split_arg_mode' (m as Fun _) T = f m T |
359 | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
359 | split_arg_mode' (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
360 let |
360 let |
361 val (i1, o1) = split_arg_mode' m1 T1 |
361 val (i1, o1) = split_arg_mode' m1 T1 |
362 val (i2, o2) = split_arg_mode' m2 T2 |
362 val (i2, o2) = split_arg_mode' m2 T2 |
363 in |
363 in |
364 (comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2)) |
364 (comb_option HOLogic.mk_prodT (i1, i2), comb_option HOLogic.mk_prodT (o1, o2)) |
370 (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) |
370 (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) |
371 end |
371 end |
372 |
372 |
373 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts |
373 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts |
374 |
374 |
375 fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s = |
375 fun fold_map_aterms_prodT comb f (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) s = |
376 let |
376 let |
377 val (x1, s') = fold_map_aterms_prodT comb f T1 s |
377 val (x1, s') = fold_map_aterms_prodT comb f T1 s |
378 val (x2, s'') = fold_map_aterms_prodT comb f T2 s' |
378 val (x2, s'') = fold_map_aterms_prodT comb f T2 s' |
379 in |
379 in |
380 (comb x1 x2, s'') |
380 (comb x1 x2, s'') |
381 end |
381 end |
382 | fold_map_aterms_prodT _ f T s = f T s |
382 | fold_map_aterms_prodT _ f T s = f T s |
383 |
383 |
384 fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) = |
384 fun map_filter_prod f (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) = |
385 comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2) |
385 comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2) |
386 | map_filter_prod f t = f t |
386 | map_filter_prod f t = f t |
387 |
387 |
388 fun split_modeT mode Ts = |
388 fun split_modeT mode Ts = |
389 let |
389 let |
390 fun split_arg_mode (Fun _) _ = ([], []) |
390 fun split_arg_mode (Fun _) _ = ([], []) |
391 | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = |
391 | split_arg_mode (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = |
392 let |
392 let |
393 val (i1, o1) = split_arg_mode m1 T1 |
393 val (i1, o1) = split_arg_mode m1 T1 |
394 val (i2, o2) = split_arg_mode m2 T2 |
394 val (i2, o2) = split_arg_mode m2 T2 |
395 in |
395 in |
396 (i1 @ i2, o1 @ o2) |
396 (i1 @ i2, o1 @ o2) |
449 | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T)))) |
449 | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T)))) |
450 |
450 |
451 |
451 |
452 (* general syntactic functions *) |
452 (* general syntactic functions *) |
453 |
453 |
454 fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = true |
454 fun is_equationlike_term (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _) = true |
455 | is_equationlike_term |
455 | is_equationlike_term |
456 (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true |
456 (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true |
457 | is_equationlike_term _ = false |
457 | is_equationlike_term _ = false |
458 |
458 |
459 val is_equationlike = is_equationlike_term o Thm.prop_of |
459 val is_equationlike = is_equationlike_term o Thm.prop_of |
460 |
460 |
461 fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) = |
461 fun is_pred_equation_term (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ u $ v) = |
462 (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) |
462 (fastype_of u = \<^typ>\<open>bool\<close>) andalso (fastype_of v = \<^typ>\<open>bool\<close>) |
463 | is_pred_equation_term _ = false |
463 | is_pred_equation_term _ = false |
464 |
464 |
465 val is_pred_equation = is_pred_equation_term o Thm.prop_of |
465 val is_pred_equation = is_pred_equation_term o Thm.prop_of |
466 |
466 |
467 fun is_intro_term constname t = |
467 fun is_intro_term constname t = |
541 fun fold_atoms f intro s = |
541 fun fold_atoms f intro s = |
542 let |
542 let |
543 val (literals, _) = Logic.strip_horn intro |
543 val (literals, _) = Logic.strip_horn intro |
544 fun appl t s = |
544 fun appl t s = |
545 (case t of |
545 (case t of |
546 (@{term Not} $ t') => f t' s |
546 (\<^term>\<open>Not\<close> $ t') => f t' s |
547 | _ => f t s) |
547 | _ => f t s) |
548 in fold appl (map HOLogic.dest_Trueprop literals) s end |
548 in fold appl (map HOLogic.dest_Trueprop literals) s end |
549 |
549 |
550 fun fold_map_atoms f intro s = |
550 fun fold_map_atoms f intro s = |
551 let |
551 let |
552 val (literals, head) = Logic.strip_horn intro |
552 val (literals, head) = Logic.strip_horn intro |
553 fun appl t s = |
553 fun appl t s = |
554 (case t of |
554 (case t of |
555 (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s) |
555 (\<^term>\<open>Not\<close> $ t') => apfst HOLogic.mk_not (f t' s) |
556 | _ => f t s) |
556 | _ => f t s) |
557 val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s |
557 val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s |
558 in |
558 in |
559 (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') |
559 (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') |
560 end; |
560 end; |
809 | rewrite_args (arg::args) (pats, intro_t, ctxt) = |
809 | rewrite_args (arg::args) (pats, intro_t, ctxt) = |
810 (case HOLogic.strip_tupleT (fastype_of arg) of |
810 (case HOLogic.strip_tupleT (fastype_of arg) of |
811 (_ :: _ :: _) => |
811 (_ :: _ :: _) => |
812 let |
812 let |
813 fun rewrite_arg' |
813 fun rewrite_arg' |
814 (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2])) |
814 (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ t2, Type (\<^type_name>\<open>Product_Type.prod\<close>, [_, T2])) |
815 (args, (pats, intro_t, ctxt)) = |
815 (args, (pats, intro_t, ctxt)) = |
816 rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) |
816 rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) |
817 | rewrite_arg' |
817 | rewrite_arg' |
818 (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) = |
818 (t, Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) (args, (pats, intro_t, ctxt)) = |
819 let |
819 let |
820 val thy = Proof_Context.theory_of ctxt |
820 val thy = Proof_Context.theory_of ctxt |
821 val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt |
821 val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt |
822 val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) |
822 val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) |
823 val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t |
823 val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t |
852 (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th) |
852 (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th) |
853 end |
853 end |
854 |
854 |
855 fun dest_conjunct_prem th = |
855 fun dest_conjunct_prem th = |
856 (case HOLogic.dest_Trueprop (Thm.prop_of th) of |
856 (case HOLogic.dest_Trueprop (Thm.prop_of th) of |
857 (Const (@{const_name HOL.conj}, _) $ _ $ _) => |
857 (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _) => |
858 dest_conjunct_prem (th RS @{thm conjunct1}) @ |
858 dest_conjunct_prem (th RS @{thm conjunct1}) @ |
859 dest_conjunct_prem (th RS @{thm conjunct2}) |
859 dest_conjunct_prem (th RS @{thm conjunct2}) |
860 | _ => [th]) |
860 | _ => [th]) |
861 |
861 |
862 fun expand_tuples thy intro = |
862 fun expand_tuples thy intro = |
906 let |
906 let |
907 val comb = make_case_comb thy Tcon; |
907 val comb = make_case_comb thy Tcon; |
908 val Type ("fun", [T, T']) = fastype_of comb; |
908 val Type ("fun", [T, T']) = fastype_of comb; |
909 val (Const (case_name, _), fs) = strip_comb comb |
909 val (Const (case_name, _), fs) = strip_comb comb |
910 val used = Term.add_tfree_names comb [] |
910 val used = Term.add_tfree_names comb [] |
911 val U = TFree (singleton (Name.variant_list used) "'t", @{sort type}) |
911 val U = TFree (singleton (Name.variant_list used) "'t", \<^sort>\<open>type\<close>) |
912 val x = Free ("x", T) |
912 val x = Free ("x", T) |
913 val f = Free ("f", T' --> U) |
913 val f = Free ("f", T' --> U) |
914 fun apply_f f' = |
914 fun apply_f f' = |
915 let |
915 let |
916 val Ts = binder_types (fastype_of f') |
916 val Ts = binder_types (fastype_of f') |
933 val th = case_rewrite thy Tcon |
933 val th = case_rewrite thy Tcon |
934 val ctxt = Proof_Context.init_global thy |
934 val ctxt = Proof_Context.init_global thy |
935 val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))) |
935 val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th))))) |
936 val Type ("fun", [uninst_T, uninst_T']) = fastype_of f |
936 val Type ("fun", [uninst_T, uninst_T']) = fastype_of f |
937 val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt |
937 val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt |
938 val T' = TFree ("'t'", @{sort type}) |
938 val T' = TFree ("'t'", \<^sort>\<open>type\<close>) |
939 val U = TFree ("'u", @{sort type}) |
939 val U = TFree ("'u", \<^sort>\<open>type\<close>) |
940 val y = Free (yname, U) |
940 val y = Free (yname, U) |
941 val f' = absdummy (U --> T') (Bound 0 $ y) |
941 val f' = absdummy (U --> T') (Bound 0 $ y) |
942 val th' = |
942 val th' = |
943 Thm.instantiate |
943 Thm.instantiate |
944 ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), |
944 ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), |
961 |
961 |
962 (*** conversions ***) |
962 (*** conversions ***) |
963 |
963 |
964 fun imp_prems_conv cv ct = |
964 fun imp_prems_conv cv ct = |
965 (case Thm.term_of ct of |
965 (case Thm.term_of ct of |
966 Const (@{const_name Pure.imp}, _) $ _ $ _ => |
966 Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => |
967 Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
967 Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
968 | _ => Conv.all_conv ct) |
968 | _ => Conv.all_conv ct) |
969 |
969 |
970 |
970 |
971 (** eta contract higher-order arguments **) |
971 (** eta contract higher-order arguments **) |
1019 |
1019 |
1020 |
1020 |
1021 (* Some last processing *) |
1021 (* Some last processing *) |
1022 |
1022 |
1023 fun remove_pointless_clauses intro = |
1023 fun remove_pointless_clauses intro = |
1024 if Logic.strip_imp_prems (Thm.prop_of intro) = [@{prop "False"}] then |
1024 if Logic.strip_imp_prems (Thm.prop_of intro) = [\<^prop>\<open>False\<close>] then |
1025 [] |
1025 [] |
1026 else [intro] |
1026 else [intro] |
1027 |
1027 |
1028 |
1028 |
1029 (* some peephole optimisations *) |
1029 (* some peephole optimisations *) |
1030 |
1030 |
1031 fun peephole_optimisation thy intro = |
1031 fun peephole_optimisation thy intro = |
1032 let |
1032 let |
1033 val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
1033 val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
1034 val process = |
1034 val process = |
1035 rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp}) |
1035 rewrite_rule ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>code_pred_simp\<close>) |
1036 fun process_False intro_t = |
1036 fun process_False intro_t = |
1037 if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} |
1037 if member (op =) (Logic.strip_imp_prems intro_t) \<^prop>\<open>False\<close> |
1038 then NONE else SOME intro_t |
1038 then NONE else SOME intro_t |
1039 fun process_True intro_t = |
1039 fun process_True intro_t = |
1040 map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t |
1040 map_filter_premises (fn p => if p = \<^prop>\<open>True\<close> then NONE else SOME p) intro_t |
1041 in |
1041 in |
1042 Option.map (Skip_Proof.make_thm thy) |
1042 Option.map (Skip_Proof.make_thm thy) |
1043 (process_False (process_True (Thm.prop_of (process intro)))) |
1043 (process_False (process_True (Thm.prop_of (process intro)))) |
1044 end |
1044 end |
1045 |
1045 |
1096 end |
1096 end |
1097 |
1097 |
1098 |
1098 |
1099 (* generation of case rules from user-given introduction rules *) |
1099 (* generation of case rules from user-given introduction rules *) |
1100 |
1100 |
1101 fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st = |
1101 fun mk_args2 (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) st = |
1102 let |
1102 let |
1103 val (t1, st') = mk_args2 T1 st |
1103 val (t1, st') = mk_args2 T1 st |
1104 val (t2, st'') = mk_args2 T2 st' |
1104 val (t2, st'') = mk_args2 T2 st' |
1105 in |
1105 in |
1106 (HOLogic.mk_prod (t1, t2), st'') |
1106 (HOLogic.mk_prod (t1, t2), st'') |
1184 fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy |
1184 fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy |
1185 |
1185 |
1186 |
1186 |
1187 (* defining a quickcheck predicate *) |
1187 (* defining a quickcheck predicate *) |
1188 |
1188 |
1189 fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B |
1189 fun strip_imp_prems (Const(\<^const_name>\<open>HOL.implies\<close>, _) $ A $ B) = A :: strip_imp_prems B |
1190 | strip_imp_prems _ = []; |
1190 | strip_imp_prems _ = []; |
1191 |
1191 |
1192 fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B |
1192 fun strip_imp_concl (Const(\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ B) = strip_imp_concl B |
1193 | strip_imp_concl A = A; |
1193 | strip_imp_concl A = A; |
1194 |
1194 |
1195 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A) |
1195 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A) |
1196 |
1196 |
1197 fun define_quickcheck_predicate t thy = |
1197 fun define_quickcheck_predicate t thy = |
1200 val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) |
1200 val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) |
1201 val t'' = subst_bounds (map Free (rev vs'), t') |
1201 val t'' = subst_bounds (map Free (rev vs'), t') |
1202 val (prems, concl) = strip_horn t'' |
1202 val (prems, concl) = strip_horn t'' |
1203 val constname = "quickcheck" |
1203 val constname = "quickcheck" |
1204 val full_constname = Sign.full_bname thy constname |
1204 val full_constname = Sign.full_bname thy constname |
1205 val constT = map snd vs' ---> @{typ bool} |
1205 val constT = map snd vs' ---> \<^typ>\<open>bool\<close> |
1206 val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy |
1206 val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy |
1207 val const = Const (full_constname, constT) |
1207 val const = Const (full_constname, constT) |
1208 val t = |
1208 val t = |
1209 Logic.list_implies |
1209 Logic.list_implies |
1210 (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |
1210 (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |