688 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) |
688 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) |
689 | constify_lifted (Free (x as (s, _))) = |
689 | constify_lifted (Free (x as (s, _))) = |
690 (if String.isPrefix lam_lifted_prefix s then Const else Free) x |
690 (if String.isPrefix lam_lifted_prefix s then Const else Free) x |
691 | constify_lifted t = t |
691 | constify_lifted t = t |
692 |
692 |
693 (* Requires bound variables not to clash with any schematic variables (as should |
|
694 be the case right after lambda-lifting). *) |
|
695 fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) = |
|
696 let |
|
697 val names = Name.make_context (map fst (Term.add_var_names t [])) |
|
698 val (s, _) = Name.variant s names |
|
699 in open_form (subst_bound (Var ((s, 0), T), t)) end |
|
700 | open_form t = t |
|
701 |
|
702 fun lift_lams_part_1 ctxt type_enc = |
693 fun lift_lams_part_1 ctxt type_enc = |
703 map close_form #> rpair ctxt |
694 map close_form #> rpair ctxt |
704 #-> Lambda_Lifting.lift_lambdas |
695 #-> Lambda_Lifting.lift_lambdas |
705 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then |
696 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then |
706 lam_lifted_poly_prefix |
697 lam_lifted_poly_prefix |
707 else |
698 else |
708 lam_lifted_mono_prefix) ^ "_a")) |
699 lam_lifted_mono_prefix) ^ "_a")) |
709 Lambda_Lifting.is_quantifier |
700 Lambda_Lifting.is_quantifier |
710 #> fst |
701 #> fst |
711 val lift_lams_part_2 = pairself (map (open_form o constify_lifted)) |
702 val lift_lams_part_2 = pairself (map constify_lifted) |
712 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
703 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
713 |
704 |
714 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
705 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
715 intentionalize_def t |
706 intentionalize_def t |
716 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
707 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
1681 in add end |
1672 in add end |
1682 |
1673 |
1683 fun type_constrs_of_terms thy ts = |
1674 fun type_constrs_of_terms thy ts = |
1684 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) |
1675 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) |
1685 |
1676 |
|
1677 (* Requires bound variables not to clash with any schematic variables (as should |
|
1678 be the case right after lambda-lifting). *) |
|
1679 fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) = |
|
1680 let |
|
1681 val names = Name.make_context (map fst (Term.add_var_names t [])) |
|
1682 val (s, _) = Name.variant s names |
|
1683 in open_form (subst_bound (Var ((s, 0), T), t)) end |
|
1684 | open_form t = t |
|
1685 |
1686 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
1686 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
1687 let val (head, args) = strip_comb t in |
1687 let val (head, args) = strip_comb t in |
1688 (head |> dest_Const |> fst, |
1688 (head |> dest_Const |> fst, |
1689 fold_rev (fn t as Var ((s, _), T) => |
1689 fold_rev (fn t as Var ((s, _), T) => |
1690 (fn u => Abs (s, T, abstract_over (t, u))) |
1690 (fn u => Abs (s, T, abstract_over (t, u))) |
1747 facts |
1747 facts |
1748 |> map_filter (fn (name, (_, t)) => |
1748 |> map_filter (fn (name, (_, t)) => |
1749 make_fact ctxt format type_enc true (name, t) |
1749 make_fact ctxt format type_enc true (name, t) |
1750 |> Option.map (pair name)) |
1750 |> Option.map (pair name)) |
1751 |> ListPair.unzip |
1751 |> ListPair.unzip |
1752 val lifted = lam_facts |> map (extract_lambda_def o snd o snd) |
1752 val lifted = lam_facts |> map (extract_lambda_def o open_form o snd o snd) |
1753 val lam_facts = |
1753 val lam_facts = |
1754 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) |
1754 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) |
1755 val all_ts = concl_t :: hyp_ts @ fact_ts |
1755 val all_ts = concl_t :: hyp_ts @ fact_ts |
1756 val subs = tfree_classes_of_terms all_ts |
1756 val subs = tfree_classes_of_terms all_ts |
1757 val supers = tvar_classes_of_terms all_ts |
1757 val supers = tvar_classes_of_terms all_ts |