293 (case Term.strip_comb t of |
293 (case Term.strip_comb t of |
294 (q as Const (@{const_name All}, _), [Abs (x, T, u)]) => |
294 (q as Const (@{const_name All}, _), [Abs (x, T, u)]) => |
295 q $ Abs (x, T, in_trigger (T :: Ts) u) |
295 q $ Abs (x, T, in_trigger (T :: Ts) u) |
296 | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => |
296 | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => |
297 q $ Abs (x, T, in_trigger (T :: Ts) u) |
297 q $ Abs (x, T, in_trigger (T :: Ts) u) |
298 | (q as Const (@{const_name Let}, _), [u1 as Abs _, u2]) => |
298 | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => |
299 q $ traverse Ts u1 $ traverse Ts u2 |
299 q $ traverse Ts u1 $ traverse Ts u2 |
300 | (u as Const (c as (_, T)), ts) => |
300 | (u as Const (c as (_, T)), ts) => |
301 (case SMT_Builtin.dest_builtin ctxt c ts of |
301 (case SMT_Builtin.dest_builtin ctxt c ts of |
302 SOME (_, _, us, mk) => mk (map (traverse Ts) us) |
302 SOME (_, _, us, mk) => mk (map (traverse Ts) us) |
303 | NONE => app_func u T (map (traverse Ts) ts)) |
303 | NONE => app_func u T (map (traverse Ts) ts)) |
535 |
535 |
536 val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
536 val ((funcs, dtyps, tr_context, ctxt1), ts2) = |
537 ((make_tr_context prefixes, ctxt), ts1) |
537 ((make_tr_context prefixes, ctxt), ts1) |
538 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
538 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) |
539 |
539 |
|
540 fun is_binder (Const (@{const_name Let}, _) $ _) = true |
|
541 | is_binder t = Lambda_Lifting.is_quantifier t |
|
542 |
|
543 fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = |
|
544 q $ Abs (n, T, mk_trigger t) |
|
545 | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = |
|
546 Term.domain_type T --> @{typ SMT.pattern} |
|
547 |> (fn T => Const (@{const_name SMT.pat}, T) $ lhs) |
|
548 |> HOLogic.mk_list @{typ SMT.pattern} o single |
|
549 |> HOLogic.mk_list @{typ "SMT.pattern list"} o single |
|
550 |> (fn t => @{const SMT.trigger} $ t $ eq) |
|
551 | mk_trigger t = t |
|
552 |
540 val (ctxt2, ts3) = |
553 val (ctxt2, ts3) = |
541 ts2 |
554 ts2 |
542 |> eta_expand ctxt1 is_fol funcs |
555 |> eta_expand ctxt1 is_fol funcs |
543 |> Lambda_Lifting.lift_lambdas ctxt1 true |
556 |> rpair ctxt1 |
544 ||> (op @) |
557 |>> tap (map (tracing o PolyML.makestring)) |
545 |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) |
558 |-> Lambda_Lifting.lift_lambdas NONE is_binder |
|
559 |-> (fn (ts', defs) => fn ctxt' => |
|
560 map mk_trigger defs @ ts' |
|
561 |> tap (map (tracing o PolyML.makestring)) |
|
562 |> intro_explicit_application ctxt' funcs |
|
563 |> pair ctxt') |
546 |
564 |
547 val ((rewrite_rules, extra_thms, builtin), ts4) = |
565 val ((rewrite_rules, extra_thms, builtin), ts4) = |
548 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |
566 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 |
549 |
567 |
550 val rewrite_rules' = fun_app_eq :: rewrite_rules |
568 val rewrite_rules' = fun_app_eq :: rewrite_rules |