equal
deleted
inserted
replaced
48 ('a, 'b) atp_step |
48 ('a, 'b) atp_step |
49 val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format -> |
49 val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format -> |
50 ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> |
50 ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> |
51 int Symtab.table -> string atp_proof -> (term, string) atp_step list |
51 int Symtab.table -> string atp_proof -> (term, string) atp_step list |
52 val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list |
52 val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list |
53 val infer_formula_types : Proof.context -> term -> term |
53 val infer_formula_types : Proof.context -> term list -> term list |
54 val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list |
54 val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list |
55 val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> |
55 val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> |
56 (term, string) atp_step list |
56 (term, string) atp_step list |
57 end; |
57 end; |
58 |
58 |
528 (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then |
528 (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then |
529 tptp_equal |
529 tptp_equal |
530 else |
530 else |
531 s |
531 s |
532 |
532 |
|
533 fun set_var_index j = map_aterms (fn Var ((s, _), T) => Var ((s, j), T) | t => t) |
|
534 |
533 fun infer_formula_types ctxt = |
535 fun infer_formula_types ctxt = |
534 Type.constraint HOLogic.boolT |
536 map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT)) |
535 #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |
537 #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |
|
538 #> map (set_var_index 0) |
536 |
539 |
537 val combinator_table = |
540 val combinator_table = |
538 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), |
541 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), |
539 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), |
542 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), |
540 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), |
543 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), |
569 val thy = Proof_Context.theory_of ctxt |
572 val thy = Proof_Context.theory_of ctxt |
570 val t = u |
573 val t = u |
571 |> prop_of_atp ctxt format type_enc true sym_tab |
574 |> prop_of_atp ctxt format type_enc true sym_tab |
572 |> uncombine_term thy |
575 |> uncombine_term thy |
573 |> unlift_term lifted |
576 |> unlift_term lifted |
574 |> infer_formula_types ctxt |
|
575 |> HOLogic.mk_Trueprop |
|
576 in |
577 in |
577 SOME (name, role, t, rule, deps) |
578 SOME (name, role, t, rule, deps) |
578 end |
579 end |
579 |
580 |
580 val waldmeister_conjecture_num = "1.0.0.0" |
581 val waldmeister_conjecture_num = "1.0.0.0" |
589 else line :: repair_body lines |
590 else line :: repair_body lines |
590 in |
591 in |
591 repair_body proof |
592 repair_body proof |
592 end |
593 end |
593 |
594 |
|
595 fun map_proof_terms f (lines : ('a * 'b * 'c * 'd * 'e) list) = |
|
596 map2 (fn c => fn (a, b, _, d, e) => (a, b, c, d, e)) (f (map #3 lines)) lines |
|
597 |
594 fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab = |
598 fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab = |
595 nasty_atp_proof pool |
599 nasty_atp_proof pool |
596 #> map_term_names_in_atp_proof repair_name |
600 #> map_term_names_in_atp_proof repair_name |
597 #> map_filter (termify_line ctxt format type_enc lifted sym_tab) |
601 #> map_filter (termify_line ctxt format type_enc lifted sym_tab) |
|
602 #> map_proof_terms (infer_formula_types ctxt #> map HOLogic.mk_Trueprop) |
598 #> local_prover = waldmeisterN ? repair_waldmeister_endgame |
603 #> local_prover = waldmeisterN ? repair_waldmeister_endgame |
599 |
604 |
600 fun take_distinct_vars seen ((t as Var _) :: ts) = |
605 fun take_distinct_vars seen ((t as Var _) :: ts) = |
601 if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts |
606 if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts |
602 | take_distinct_vars seen _ = rev seen |
607 | take_distinct_vars seen _ = rev seen |