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 |
693 (* Requires bound variables not to clash with any schematic variables (as should |
694 be the case right after lambda-lifting). *) |
694 be the case right after lambda-lifting). *) |
695 fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) = |
695 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) = |
696 let |
696 (case try unprefix s of |
697 val names = Name.make_context (map fst (Term.add_var_names t [])) |
697 SOME s => |
698 val (s, _) = Name.variant s names |
698 let |
699 in open_form (subst_bound (Var ((s, 0), T), t)) end |
699 val names = Name.make_context (map fst (Term.add_var_names t' [])) |
700 | open_form t = t |
700 val (s, _) = Name.variant s names |
|
701 in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end |
|
702 | NONE => t) |
|
703 | open_form _ t = t |
701 |
704 |
702 fun lift_lams_part_1 ctxt type_enc = |
705 fun lift_lams_part_1 ctxt type_enc = |
703 map close_form #> rpair ctxt |
706 map close_form #> rpair ctxt |
704 #-> Lambda_Lifting.lift_lambdas |
707 #-> Lambda_Lifting.lift_lambdas |
705 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then |
708 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then |
706 lam_lifted_poly_prefix |
709 lam_lifted_poly_prefix |
707 else |
710 else |
708 lam_lifted_mono_prefix) ^ "_a")) |
711 lam_lifted_mono_prefix) ^ "_a")) |
709 Lambda_Lifting.is_quantifier |
712 Lambda_Lifting.is_quantifier |
710 #> fst |
713 #> fst |
711 val lift_lams_part_2 = pairself (map (open_form o constify_lifted)) |
714 fun lift_lams_part_2 (facts, lifted) = |
|
715 (map (open_form (unprefix close_form_prefix) o constify_lifted) facts, |
|
716 map (open_form I o constify_lifted) lifted) |
712 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
717 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
713 |
718 |
714 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
719 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
715 intentionalize_def t |
720 intentionalize_def t |
716 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
721 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
1233 name stature Axiom of |
1238 name stature Axiom of |
1234 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => |
1239 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => |
1235 if s = tptp_true then NONE else SOME formula |
1240 if s = tptp_true then NONE else SOME formula |
1236 | formula => SOME formula |
1241 | formula => SOME formula |
1237 |
1242 |
1238 fun not_trueprop (@{const Trueprop} $ t) = |
1243 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t |
1239 @{const Trueprop} $ (@{const Not} $ t) |
1244 | s_not_trueprop t = |
1240 | not_trueprop t = |
1245 if fastype_of t = @{typ bool} then s_not t |
1241 if fastype_of t = @{typ bool} then @{const Not} $ t |
|
1242 else @{prop False} (* "t" is too meta *) |
1246 else @{prop False} (* "t" is too meta *) |
1243 |
1247 |
1244 fun make_conjecture ctxt format type_enc = |
1248 fun make_conjecture ctxt format type_enc = |
1245 map (fn ((name, stature), (kind, t)) => |
1249 map (fn ((name, stature), (kind, t)) => |
1246 t |> kind = Conjecture ? not_trueprop |
1250 t |> kind = Conjecture ? s_not_trueprop |
1247 |> make_formula ctxt format type_enc (format <> CNF) name stature |
1251 |> make_formula ctxt format type_enc (format <> CNF) name stature |
1248 kind) |
1252 kind) |
1249 |
1253 |
1250 (** Finite and infinite type inference **) |
1254 (** Finite and infinite type inference **) |
1251 |
1255 |
1728 val hyp_ts = |
1732 val hyp_ts = |
1729 hyp_ts |
1733 hyp_ts |
1730 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) |
1734 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) |
1731 val facts = facts |> map (apsnd (pair Axiom)) |
1735 val facts = facts |> map (apsnd (pair Axiom)) |
1732 val conjs = |
1736 val conjs = |
1733 map (pair prem_kind) hyp_ts @ [(Conjecture, not_trueprop concl_t)] |
1737 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)] |
1734 |> map (apsnd freeze_term) |
1738 |> map (apsnd freeze_term) |
1735 |> map2 (pair o rpair (Local, General) o string_of_int) |
1739 |> map2 (pair o rpair (Local, General) o string_of_int) |
1736 (0 upto length hyp_ts) |
1740 (0 upto length hyp_ts) |
1737 val ((conjs, facts), lam_facts) = |
1741 val ((conjs, facts), lam_facts) = |
1738 (conjs, facts) |
1742 (conjs, facts) |