--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Thu Jan 29 15:21:16 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Thu Jan 29 15:27:29 2015 +0100
@@ -29,16 +29,16 @@
type 'a atp_proof = 'a ATP_Proof.atp_proof
type stature = ATP_Problem_Generate.stature
type waldmeister_info = (string * (term list * (term option * term))) list
-
+
val waldmeister_skolemize_rule : string
-
+
val generate_waldmeister_problem : Proof.context -> term list -> term ->
((string * stature) * term) list ->
- string atp_problem * string Symtab.table * (string * term) list * int Symtab.table *
+ string atp_problem * string Symtab.table * (string * term) list * int Symtab.table *
waldmeister_info
val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof ->
(term, string) atp_step list
- val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list ->
+ val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list ->
(term, string) atp_step list
end;
@@ -64,7 +64,7 @@
fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) =
let
- val (fun_trm, ctxt1_new, ctxt2_new) =
+ val (fun_trm, ctxt1_new, ctxt2_new) =
mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty)
in
(Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new)
@@ -81,7 +81,7 @@
fun skolem_bound is_free ctxt1 ctxt2 spets vars x =
if is_free then
- let
+ let
val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x
in
(ctxt1', ctxt2',spets, trm', vars)
@@ -107,9 +107,9 @@
| skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) =
if name = @{const_name Ex} orelse name = @{const_name All} then
let
- val is_free = (name = @{const_name Ex} andalso pos)
+ val is_free = (name = @{const_name Ex} andalso pos)
orelse (name = @{const_name All} andalso not pos)
- val (ctxt1', ctxt2', spets', trm', vars') =
+ val (ctxt1', ctxt2', spets', trm', vars') =
skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x
in
skolemize' pos ctxt1' ctxt2' spets' vars' trm'
@@ -117,7 +117,7 @@
else
(ctxt1, ctxt2, spets, trm)
| skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) =
- if name = @{const_name conj} orelse name = @{const_name disj} orelse
+ if name = @{const_name conj} orelse name = @{const_name disj} orelse
name = @{const_name implies} then
let
val pos_a = if name = @{const_name implies} then not pos else pos
@@ -131,11 +131,11 @@
else
(ctxt1,ctxt2,spets,c $ a $ b)
| skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm)
-
+
fun vars_of trm =
rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm []));
- fun skolemize positve ctxt trm =
+ fun skolemize positve ctxt trm =
let
val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm
in
@@ -156,36 +156,36 @@
val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis]
-fun encode_type (Type (name, types)) =
- type_prefix ^ open_paranthesis ^ name ^ delimiter ^
- (map encode_type types |> String.concatWith delimiter) ^ close_parathesis
-| encode_type (TFree (name, sorts)) =
- tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^
+fun encode_type (Type (name, types)) =
+ type_prefix ^ open_paranthesis ^ name ^ delimiter ^
+ (map encode_type types |> space_implode delimiter) ^ close_parathesis
+| encode_type (TFree (name, sorts)) =
+ tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ space_implode delimiter sorts ^
close_parathesis
| encode_type (TVar ((name, i), sorts)) =
- tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^
- close_parathesis ^ delimiter ^ (String.concatWith delimiter sorts) ^ close_parathesis
+ tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^
+ close_parathesis ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis
-fun encode_types types = (String.concatWith delimiter (map encode_type types))
+fun encode_types types = space_implode delimiter (map encode_type types)
fun parse_identifier x =
(Scan.many identifier_character >> implode) x
-
-fun parse_star delim scanner x =
+
+fun parse_star delim scanner x =
(Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x
-
+
fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --|
$$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x
and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --|
$$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x
and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis
- |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$
- close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --|
+ |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$
+ close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --|
$$ close_parathesis >> TVar) x
and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x
fun parse_types x = parse_star delimiter parse_any_type x
-
+
fun decode_type_string s = Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
quote s)) parse_type)) (Symbol.explode s) |> fst
@@ -253,7 +253,7 @@
val is_lambda_name = String.isPrefix lam_lifted_poly_prefix
-fun lookup table k =
+fun lookup table k =
List.find (fn (key, _) => key = k) table
fun dest_list' (f $ t) =
@@ -286,7 +286,7 @@
val (function, trms) = dest_list trm
val info' = map_minimal_app' info trms
in
- case function of
+ case function of
(Const _) => list_update (function, length trms) info' |
(Free _) => list_update (function, length trms) info' |
_ => info
@@ -300,14 +300,14 @@
fun map_minimal_app trms = map_minimal_app' [] trms
fun mk_waldmeister_app function [] = function
- | mk_waldmeister_app function (a :: args) =
+ | mk_waldmeister_app function (a :: args) =
let
val funT = type_of function
val argT = type_of a
val resT = dest_funT funT |> snd
val newT = funT --> argT --> resT
in
- mk_waldmeister_app (Const (waldmeister_apply ^ "," ^
+ mk_waldmeister_app (Const (waldmeister_apply ^ "," ^
encode_types [resT, argT], newT) $ function $ a) args
end
@@ -318,8 +318,8 @@
in
case function of
Var _ => mk_waldmeister_app function trms' |
- _ =>
- let
+ _ =>
+ let
val min_args = lookup info function |> the |> snd
val args0 = List.take (trms',min_args)
val args1 = List.drop (trms',min_args)
@@ -349,9 +349,9 @@
in
[ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)]
end
- | trm_to_atp'' _ (Free (x, _)) args =
+ | trm_to_atp'' _ (Free (x, _)) args =
[ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)]
- | trm_to_atp'' _ (Var ((x, _), _)) args =
+ | trm_to_atp'' _ (Var ((x, _), _)) args =
[ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)]
| trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args)
| trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term")
@@ -374,7 +374,7 @@
let
val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then
(waldmeister_apply, []) else decode_const encoded_name
- val const_trans_name =
+ val const_trans_name =
if is_lambda_name const_name then
lam_lift_waldmeister_prefix ^ (* ?? *)
String.extract(const_name, size lam_lifted_poly_prefix, NONE)
@@ -390,20 +390,20 @@
else if prefix = free_prefix then
Free (encoded_name, dummy_fun_type ())
else if Char.isUpper prefix then
- Var ((name, 0), dummy_fun_type ())
+ Var ((name, 0), dummy_fun_type ())
(* Use name instead of encoded_name because Waldmeister renames free variables. *)
else if name = waldmeister_equals then
- (case args of
+ (case args of
[_, _] => eq_const dummyT
- | _ => raise FailureMessage
- (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^
+ | _ => raise FailureMessage
+ (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^
Int.toString (length args)))
else if name = waldmeister_true then
@{term True}
else if name = waldmeister_false then
@{term False}
else
- raise FailureMessage
+ raise FailureMessage
(WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name)
end
@@ -421,7 +421,7 @@
fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy
| formula_to_trm thy (AConn (ANot, [aterm])) =
mk_not (formula_to_trm thy aterm)
- | formula_to_trm _ _ =
+ | formula_to_trm _ _ =
raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn")
(* Abstract translation *)
@@ -460,11 +460,11 @@
end
fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs []
-
- fun skolemize_fact ctxt (name, trm) =
- let
- val (ctxt', (steps, trm')) = skolemize true ctxt trm
- in
+
+ fun skolemize_fact ctxt (name, trm) =
+ let
+ val (ctxt', (steps, trm')) = skolemize true ctxt trm
+ in
(ctxt', (name, (steps, trm')))
end
@@ -472,7 +472,7 @@
| name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1)
fun name_list prefix xs = name_list' prefix xs 0
-
+
(* Skolemization, hiding lambdas and translating formulas to equations *)
val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts
val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions
@@ -486,13 +486,13 @@
skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem))
val sko_eq_info =
- (((conj_identifier, eq_conseq) :: sko_eq_conditions0)
+ (((conj_identifier, eq_conseq) :: sko_eq_conditions0)
@ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0)
(* Translation of partial function applications *)
val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info)
- fun hide_partial_apps_in_last (x, (y, (z, term))) =
+ fun hide_partial_apps_in_last (x, (y, (z, term))) =
(x, (y, (z, hide_partial_applications fun_app_info term)))
val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0
@@ -547,9 +547,9 @@
SOME x => x |
NONE => NONE
-fun fix_name name =
+fun fix_name name =
if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then
- String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |>
+ String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |>
(fn x => fact_prefix ^ "0_" ^ x)
else
name
@@ -573,7 +573,7 @@
| mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]),
Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule,
[(waldmeister_name ^ "_" ^ Int.toString (i-1),
- if i = 1 then isabelle_names else [])])
+ if i = 1 then isabelle_names else [])])
:: mk_steps (i+1) xs
val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown,
@@ -584,13 +584,13 @@
val skolem_steps = first_step :: sub_steps
val num_of_steps = length skolem_steps
in
- (skolem_steps @
+ (skolem_steps @
[((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule,
[(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1),
if num_of_steps = 1 then isabelle_names else [])])])
end
end
-
+
fun introduce_waldmeister_skolems info proof_steps = proof_steps
|> maps (skolemization_steps info)
end;