--- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:13 2014 +0200
@@ -30,8 +30,9 @@
((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id))
-- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",")
-- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id
- -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]"))
- || skip_term >> K NONE) >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
+ -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]"))
+ || (skip_term >> K "") >> (fn x => SOME [x]))
+ >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
fun parse_prem x =
((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x
@@ -66,50 +67,57 @@
assumptions: string list,
rule: string,
used_assumptions: string list,
+ detailed_eigen: string,
generated_goal_assumptions: (string * string list) list}
fun mk_satallax_step id role theorem assumptions rule used_assumptions
- generated_goal_assumptions =
- Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule,
- used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions}
+ generated_goal_assumptions detailed_eigen =
+ Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule,
+ used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions,
+ detailed_eigen = detailed_eigen}
fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) =
the_default [] assumptions
| get_assumptions (_ :: l) = get_assumptions l
| get_assumptions [] = []
+fun get_detailled_eigen ((_, SOME (SOME "eigenvar" , var)) :: _) =
+ hd (the_default [""] var)
+ | get_detailled_eigen (_ :: l) = get_detailled_eigen l
+ | get_detailled_eigen [] = ""
+
fun seperate_dependices dependencies =
- let
- fun sep_dep [] used_assumptions new_goals generated_assumptions _ =
- (used_assumptions, new_goals, generated_assumptions)
- | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state =
- if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then
- if state = 0 then
- sep_dep l (x :: used_assumptions) new_goals generated_assumptions state
- else
- sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3
+ let
+ fun sep_dep [] used_assumptions new_goals generated_assumptions _ =
+ (used_assumptions, new_goals, generated_assumptions)
+ | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state =
+ if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then
+ if state = 0 then
+ sep_dep l (x :: used_assumptions) new_goals generated_assumptions state
else
- if state = 1 orelse state = 0 then
- sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1
- else
- raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l)
- in
- sep_dep dependencies [] [] [] 0
- end
+ sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3
+ else
+ if state = 1 orelse state = 0 then
+ sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1
+ else
+ raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l)
+ in
+ sep_dep dependencies [] [] [] 0
+ end
fun create_grouped_goal_assumption rule new_goals generated_assumptions =
- if length new_goals = length generated_assumptions then
- new_goals ~~ (map single generated_assumptions)
- else if 2 * length new_goals = length generated_assumptions then
- let
- fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
- (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
- | group_by_pair [] [] = []
- in
- group_by_pair new_goals generated_assumptions
- end
- else
- raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
+ if length new_goals = length generated_assumptions then
+ new_goals ~~ (map single generated_assumptions)
+ else if 2 * length new_goals = length generated_assumptions then
+ let
+ fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
+ (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
+ | group_by_pair [] [] = []
+ in
+ group_by_pair new_goals generated_assumptions
+ end
+ else
+ raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
let
@@ -117,32 +125,34 @@
in
mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions
(create_grouped_goal_assumption rule new_goals generated_assumptions)
+ (get_detailled_eigen (the_default [] l))
end
| to_satallax_step (((id, role), formula), NONE) =
- mk_satallax_step id role formula [] "assumption" [] []
+ mk_satallax_step id role formula [] "assumption" [] [] ""
fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse
role = "negated_conjecture" orelse role = "conjecture"
fun seperate_assumptions_and_steps l =
- let
- fun seperate_assumption [] l l' = (l, l')
- | seperate_assumption (step :: steps) l l' =
- if is_assumption step then
- seperate_assumption steps (step :: l) l'
- else
- seperate_assumption steps l (step :: l')
- in
- seperate_assumption l [] []
- end
+ let
+ fun seperate_assumption [] l l' = (l, l')
+ | seperate_assumption (step :: steps) l l' =
+ if is_assumption step then
+ seperate_assumption steps (step :: l) l'
+ else
+ seperate_assumption steps l (step :: l')
+ in
+ seperate_assumption l [] []
+ end
datatype satallax_proof_graph =
- Node_Source of {node: satallax_step, succs: satallax_proof_graph list} |
- Node_Conclusion of {node: satallax_step, deps: satallax_proof_graph list}
+ Linear_Part of {node: satallax_step, succs: satallax_proof_graph list} |
+ Tree_Part of {node: satallax_step, deps: satallax_proof_graph list}
fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h =
if h = id then x else find_proof_step l h
- | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h)
+ | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h ^ "(probably a parsing \
+ \error)")
fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) =
if op1 = op2 andalso op1 = tptp_not then th else x
@@ -152,6 +162,8 @@
fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true
| tptp_term_equal (_, _) = false
+val dummy_true_aterm = ATerm (("$true", [dummy_atype]), [])
+
fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline =
(case List.find (curry (op =) assm o fst) no_inline of
SOME _ => find_assumptions_to_inline ths assms to_inline no_inline
@@ -171,109 +183,113 @@
fun inline_if_needed_and_simplify th assms to_inline no_inline =
(case find_assumptions_to_inline [th] assms to_inline no_inline of
- [] => ATerm (("$true", [dummy_atype]), [])
- | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l)
+ [] => dummy_true_aterm
+ | l => foldl1 (fn (a, b) =>
+ (case b of
+ ATerm (("$false", _), _) => a
+ | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a
+ | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l)
fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem
-fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions,
- rule, generated_goal_assumptions, used_assumptions})) =
- mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions)
- generated_goal_assumptions
+fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions,
+ rule, generated_goal_assumptions, used_assumptions, detailed_eigen})) =
+ mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions)
+ generated_goal_assumptions detailed_eigen
fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions,
- generated_goal_assumptions, used_assumptions, ...}) =
- mk_satallax_step id role theorem assumptions new_rule used_assumptions
- generated_goal_assumptions
+ generated_goal_assumptions, used_assumptions, detailed_eigen, ...}) =
+ mk_satallax_step id role theorem assumptions new_rule used_assumptions
+ generated_goal_assumptions detailed_eigen
fun transform_inline_assumption hypotheses_step proof_sketch =
let
- fun inline_in_step (Node_Source {node as Satallax_Step {generated_goal_assumptions,
- used_assumptions, rule, ...}, succs}) =
+ fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions,
+ used_assumptions, rule, ...}, succs}) =
if generated_goal_assumptions = [] then
- Node_Source {node = node, succs = []}
+ Linear_Part {node = node, succs = []}
else
let
(*one singel goal is created, two hypothesis can be created, for the "and" rule:
(A /\ B) create two hypotheses A, and B.*)
fun set_hypotheses_as_goal [hypothesis] succs =
- Node_Source {node = set_rule rule
- (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)),
+ Linear_Part {node = set_rule rule (add_assumption used_assumptions
+ (find_proof_step hypotheses_step hypothesis)),
succs = map inline_in_step succs}
| set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs =
- Node_Source {node = set_rule rule
- (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)),
+ Linear_Part {node = set_rule rule (add_assumption used_assumptions
+ (find_proof_step hypotheses_step hypothesis)),
succs = [set_hypotheses_as_goal new_goal_hypotheses succs]}
in
set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs
end
- | inline_in_step (Node_Conclusion {node = node, deps}) =
- Node_Conclusion {node = node, deps = map inline_in_step deps}
+ | inline_in_step (Tree_Part {node = node, deps}) =
+ Tree_Part {node = node, deps = map inline_in_step deps}
- fun inline_contradictory_assumptions (Node_Source {node as Satallax_Step{id, theorem, ...},
- succs}) (to_inline, no_inline) =
- let
- val (succs, inliner) = fold_map inline_contradictory_assumptions
- succs (to_inline, (id, theorem) :: no_inline)
- in
- (Node_Source {node = node, succs = succs}, inliner)
- end
- | inline_contradictory_assumptions (Node_Conclusion {node = Satallax_Step {id, role,
- theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
- used_assumptions}, deps}) (to_inline, no_inline) =
- let
- val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
- deps (to_inline, no_inline)
- val to_inline'' = map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
- (List.filter (fn s => nth_string s 0 = "h")
- (used_assumptions @
- (map snd generated_goal_assumptions |> flat)))
- @ to_inline'
- val node' = Satallax_Step {id = id, role = role, theorem =
- AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'),
- assumptions = assumptions, rule = rule,
- generated_goal_assumptions = generated_goal_assumptions,
- used_assumptions =
- List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE)
- used_assumptions}
- in
- (Node_Conclusion {node = node', deps = dep'}, (to_inline'', no_inline'))
- end
+ fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...},
+ succs}) (to_inline, no_inline) =
+ let
+ val (succs, inliner) = fold_map inline_contradictory_assumptions
+ succs (to_inline, (id, theorem) :: no_inline)
+ in
+ (Linear_Part {node = node, succs = succs}, inliner)
+ end
+ | inline_contradictory_assumptions (Tree_Part {node = Satallax_Step {id, role,
+ theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
+ used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) =
+ let
+ val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
+ deps (to_inline, no_inline)
+ val to_inline'' =
+ map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
+ (List.filter (fn s => nth_string s 0 = "h")
+ (used_assumptions @ (map snd generated_goal_assumptions |> flat)))
+ @ to_inline'
+ val node' = Satallax_Step {id = id, role = role, theorem =
+ AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'),
+ assumptions = assumptions, rule = rule,
+ generated_goal_assumptions = generated_goal_assumptions, detailed_eigen = detailed_eigen,
+ used_assumptions =
+ List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE)
+ used_assumptions}
+ in
+ (Tree_Part {node = node', deps = dep'}, (to_inline'', no_inline'))
+ end
in
fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], []))
end
-fun correct_dependencies (Node_Source {node, succs}) =
- Node_Source {node = node, succs = map correct_dependencies succs}
- | correct_dependencies (Node_Conclusion {node, deps}) =
+fun correct_dependencies (Linear_Part {node, succs}) =
+ Linear_Part {node = node, succs = map correct_dependencies succs}
+ | correct_dependencies (Tree_Part {node, deps}) =
let
val new_used_assumptions =
- map (fn Node_Source {node = (Satallax_Step{id, ...}), ...} => id
- | Node_Conclusion {node = (Satallax_Step{id, ...}), ...} => id) deps
+ map (fn Linear_Part {node = (Satallax_Step{id, ...}), ...} => id
+ | Tree_Part {node = (Satallax_Step{id, ...}), ...} => id) deps
in
- Node_Conclusion {node = add_assumption new_used_assumptions node,
+ Tree_Part {node = add_assumption new_used_assumptions node,
deps = map correct_dependencies deps}
end
fun create_satallax_proof_graph (hypotheses_step, proof_sketch) =
- let
- fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) =
- Node_Source {node = step,
- succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch)))
- (map fst generated_goal_assumptions)}
- fun reverted_discharged_steps is_branched (Node_Source {node as
- Satallax_Step {generated_goal_assumptions, ...}, succs}) =
- if is_branched orelse length generated_goal_assumptions > 1 then
- Node_Conclusion {node = node, deps = map (reverted_discharged_steps true) succs}
- else
- Node_Source {node = node, succs = map (reverted_discharged_steps is_branched) succs}
- val proof_with_correct_sense =
- correct_dependencies (reverted_discharged_steps false
- (create_step (find_proof_step proof_sketch "0" )))
- in
- transform_inline_assumption hypotheses_step proof_with_correct_sense
- end
+ let
+ fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) =
+ Linear_Part {node = step,
+ succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch)))
+ (map fst generated_goal_assumptions)}
+ fun reverted_discharged_steps is_branched (Linear_Part {node as
+ Satallax_Step {generated_goal_assumptions, ...}, succs}) =
+ if is_branched orelse length generated_goal_assumptions > 1 then
+ Tree_Part {node = node, deps = map (reverted_discharged_steps true) succs}
+ else
+ Linear_Part {node = node, succs = map (reverted_discharged_steps is_branched) succs}
+ val proof_with_correct_sense =
+ correct_dependencies (reverted_discharged_steps false
+ (create_step (find_proof_step proof_sketch "0" )))
+ in
+ transform_inline_assumption hypotheses_step proof_with_correct_sense
+ end
val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true",
"eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
@@ -281,29 +297,85 @@
"eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
val is_special_satallax_rule = member (op =) satallax_known_theorems
+fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) =
+ let
+ val bdy = terms_to_upper_case var b
+ val ts' = map (terms_to_upper_case var) ts
+ in
+ AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty),
+ bdy), ts')
+ end
+ | terms_to_upper_case var (ATerm ((var', ty), ts)) =
+ ATerm ((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'),
+ ty), map (terms_to_upper_case var) ts)
-fun transform_to_standard_atp_step proof =
+fun add_quantifier_in_tree_part vars_to_add assumption_to_add (Linear_Part {node, succs}) =
+ Linear_Part {node = node, succs = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) succs}
+ | add_quantifier_in_tree_part vars_to_add assumption_to_add (Tree_Part {node = Satallax_Step {rule, detailed_eigen,
+ id, role, theorem = AAtom theorem, assumptions, used_assumptions, generated_goal_assumptions},
+ deps}) =
let
- fun create_fact_step id =
- ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", [])
- fun transform_one_step (Satallax_Step {id, theorem, used_assumptions, role, rule, ...}) =
- let
- val role' = role_of_tptp_string role
- in
- map create_fact_step
- (List.filter (fn s => size s >=4 andalso not (is_special_satallax_rule s))
- used_assumptions)
- @ [((id, []), if role' = Unknown then Plain else role', theorem, rule,
- map (fn s => (s, [])) used_assumptions)]
- end
+ val theorem' = fold (fn v => fn body => terms_to_upper_case v body) vars_to_add theorem
+ val theorem'' = theorem'
+ val node' = mk_satallax_step id role (AAtom theorem'') assumptions rule
+ (used_assumptions @ (filter (curry (op <=) (the (Int.fromString id)) o size)
+ assumption_to_add)) generated_goal_assumptions detailed_eigen
+ in
+ if detailed_eigen <> "" then
+ Tree_Part {node = node',
+ deps = map (add_quantifier_in_tree_part (detailed_eigen :: vars_to_add)
+ (used_assumptions @ assumption_to_add)) deps}
+ else
+ Tree_Part {node = node',
+ deps = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) deps}
+ end
- fun transform_steps (Node_Source {node, succs}) =
- transform_one_step node @ (map transform_steps succs |> flat)
- | transform_steps (Node_Conclusion {node, deps}) =
- ((map transform_steps deps) |> flat) @ (transform_one_step node)
- in
- transform_steps proof
- end
+fun transform_to_standard_atp_step already_transformed proof =
+ let
+ fun create_fact_step id =
+ ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", [])
+ fun transform_one_step already_transformed (Satallax_Step {id, theorem, used_assumptions, role,
+ rule, ...}) =
+ let
+ val role' = role_of_tptp_string role
+ val new_transformed = List.filter
+ (fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not
+ (member (op =) already_transformed s)) used_assumptions
+ in
+ (map create_fact_step new_transformed
+ @ [((id, []), if role' = Unknown then Plain else role', theorem, rule,
+ map (fn s => (s, [])) (filter_out is_special_satallax_rule used_assumptions))],
+ new_transformed @ already_transformed)
+ end
+ fun transform_steps (Linear_Part {node, succs}) (already_transformed:string list) =
+ transform_one_step already_transformed node
+ ||> (fold_map transform_steps succs)
+ ||> apfst flat
+ |> (fn (a, (b, transformed)) => (a @ b, transformed))
+ | transform_steps (Tree_Part {node, deps}) (already_transformed: string list) =
+ fold_map transform_steps deps already_transformed
+ |>> flat
+ ||> (fn transformed => transform_one_step transformed node)
+ |> (fn (a, (b, transformed)) => (a @ b, transformed))
+ in
+ fst (transform_steps proof already_transformed)
+ end
+
+fun remove_unused_dependency steps =
+ let
+ fun find_all_ids [] = []
+ | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
+ fun keep_only_used used_ids steps =
+ let
+ fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) =
+ (((id, ids), role, theorem, rule, filter (member (op =) used_ids o fst) deps) :: steps)
+ | remove_unused [] = []
+ in
+ remove_unused steps
+ end
+ in
+ keep_only_used (find_all_ids steps) steps
+ end
fun parse_proof local_name problem =
@@ -317,13 +389,14 @@
else
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
(Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
- #> fst
- #> rev
- #> map to_satallax_step
- #> seperate_assumptions_and_steps
- #> create_satallax_proof_graph
- #> transform_to_standard_atp_step))
-
+ #> fst
+ #> rev
+ #> map to_satallax_step
+ #> seperate_assumptions_and_steps
+ #> create_satallax_proof_graph
+ #> add_quantifier_in_tree_part [] []
+ #> transform_to_standard_atp_step []
+ #> remove_unused_dependency))
fun atp_proof_of_tstplike_proof _ _ "" = []
| atp_proof_of_tstplike_proof local_prover problem tstp =
@@ -335,5 +408,4 @@
|> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
|> local_prover = zipperpositionN ? rev)
-
end;