--- a/src/HOL/SMT.thy Mon Oct 06 19:37:42 2014 +0200
+++ b/src/HOL/SMT.thy Mon Oct 06 19:40:22 2014 +0200
@@ -15,19 +15,37 @@
"\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
"\<And>Q. \<forall>x. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x. Q x (f x) (fa x) (fb x)"
"\<And>Q. \<forall>x. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x. Q x (f x) (fa x) (fb x) (fc x)"
+ "\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow>
+ \<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)"
+ "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow>
+ \<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)"
+ "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow>
+ \<exists>f fa fb fc fd fe ff. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)"
+ "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow>
+ \<exists>f fa fb fc fd fe ff fg. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)"
by metis+
lemma bchoices:
"\<And>Q. \<forall>x \<in> S. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x \<in> S. Q x (f x) (fa x)"
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x \<in> S. Q x (f x) (fa x) (fb x)"
"\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x)"
+ "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow>
+ \<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)"
+ "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow>
+ \<exists>f fa fb fc fd fe. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)"
+ "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow>
+ \<exists>f fa fb fc fd fe ff. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)"
+ "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow>
+ \<exists>f fa fb fc fd fe ff fg. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)"
by metis+
ML {*
fun moura_tac ctxt =
Atomize_Elim.atomize_elim_tac ctxt THEN'
SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
- ALLGOALS (blast_tac ctxt));
+ ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs)
+ ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE'
+ blast_tac ctxt))
*}
method_setup moura = {*
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Oct 06 19:37:42 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Oct 06 19:40:22 2014 +0200
@@ -96,6 +96,7 @@
val tptp_true : string
val tptp_lambda : string
val tptp_empty_list : string
+ val dfg_individual_type : string
val isabelle_info_prefix : string
val isabelle_info : string -> int -> (string, 'a) atp_term list
val extract_isabelle_status : (string, 'a) atp_term list -> string option
@@ -251,6 +252,9 @@
val tptp_true = "$true"
val tptp_lambda = "^"
val tptp_empty_list = "[]"
+
+val dfg_individual_type = "iii" (* cannot clash *)
+
val isabelle_info_prefix = "isabelle_"
val inductionN = "induction"
@@ -386,8 +390,6 @@
| uncurry_type _ =
raise Fail "unexpected higher-order type in first-order format"
-val dfg_individual_type = "iii" (* cannot clash *)
-
val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
fun str_of_type format ty =
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Oct 06 19:37:42 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Oct 06 19:40:22 2014 +0200
@@ -350,7 +350,9 @@
(* We currently half ignore types. *)
fun parse_optional_type_signature x =
- Scan.option ($$ tptp_has_type |-- parse_type) x
+ (Scan.option ($$ tptp_has_type |-- parse_type)
+ >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some
+ | res => res)) x
and parse_arg x =
($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature
|| scan_general_id -- parse_optional_type_signature
@@ -519,7 +521,7 @@
| remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t)
fun parse_thf0_typed_var x =
- (Scan.repeat (scan_general_id -- Scan.option ($$ ":" |-- parse_thf0_type)
+ (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_thf0_type)
--| Scan.option (Scan.this_string ","))
|| $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
@@ -535,7 +537,8 @@
else I))
ys t)
|| Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
- || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
+ || scan_general_id --| $$ tptp_has_type -- parse_thf0_type
+ >> (fn (var, typ) => ATerm ((var, [typ]), []))
|| parse_ho_quantifier >> mk_simple_aterm
|| $$ "(" |-- parse_thf0_term --| $$ ")"
|| scan_general_id >> mk_simple_aterm
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Oct 06 19:37:42 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Oct 06 19:40:22 2014 +0200
@@ -133,7 +133,12 @@
fun var_name_of_typ (Type (@{type_name fun}, [_, T])) =
if body_type T = HOLogic.boolT then "p" else "f"
- | var_name_of_typ (Type (@{type_name set}, [T])) = single_letter true (var_name_of_typ T)
+ | var_name_of_typ (Type (@{type_name set}, [T])) =
+ let fun default () = single_letter true (var_name_of_typ T) in
+ (case T of
+ Type (s, [T1, T2]) => if String.isSuffix "prod" s andalso T1 = T2 then "r" else default ()
+ | _ => default ())
+ end
| var_name_of_typ (Type (s, Ts)) =
if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s"
else single_letter false (Long_Name.base_name s)
@@ -626,36 +631,31 @@
fun unskolemize_term skos =
let
- val is_skolem = member (op =) skos
+ val is_skolem_name = member (op =) skos
fun find_argless_skolem (Free _ $ Var _) = NONE
- | find_argless_skolem (Free (x as (s, _))) = if is_skolem s then SOME x else NONE
+ | find_argless_skolem (Free (x as (s, _))) = if is_skolem_name s then SOME x else NONE
| find_argless_skolem (t $ u) =
(case find_argless_skolem t of NONE => find_argless_skolem u | sk => sk)
| find_argless_skolem (Abs (_, _, t)) = find_argless_skolem t
| find_argless_skolem _ = NONE
- fun find_skolem_arg (Free (s, _) $ Var v) = if is_skolem s then SOME v else NONE
+ fun find_skolem_arg (Free (s, _) $ Var v) = if is_skolem_name s then SOME v else NONE
| find_skolem_arg (t $ u) = (case find_skolem_arg t of NONE => find_skolem_arg u | v => v)
| find_skolem_arg (Abs (_, _, t)) = find_skolem_arg t
| find_skolem_arg _ = NONE
+ fun kill_skolem_arg (t as Free (s, T) $ Var _) =
+ if is_skolem_name s then Free (s, range_type T) else t
+ | kill_skolem_arg (t $ u) = kill_skolem_arg t $ kill_skolem_arg u
+ | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t)
+ | kill_skolem_arg t = t
+
fun find_var (Var v) = SOME v
| find_var (t $ u) = (case find_var t of NONE => find_var u | v => v)
| find_var (Abs (_, _, t)) = find_var t
| find_var _ = NONE
- fun find_next_var t =
- (case find_skolem_arg t of
- NONE => find_var t
- | v => v)
-
- fun kill_skolem_arg (t as Free (s, T) $ Var _) =
- if is_skolem s then Free (s, range_type T) else t
- | kill_skolem_arg (t $ u) = kill_skolem_arg t $ kill_skolem_arg u
- | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t)
- | kill_skolem_arg t = t
-
val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1)
fun unskolem t =
@@ -663,19 +663,23 @@
SOME (x as (s, T)) =>
HOLogic.exists_const T $ Abs (s, T, unskolem (safe_abstract_over (Free x, t)))
| NONE =>
- (case find_next_var t of
+ (case find_skolem_arg t of
SOME (v as ((s, _), T)) =>
let
val (haves, have_nots) =
HOLogic.disjuncts t
- |> List.partition (Term.exists_subterm (curry (op =) (Var v)))
+ |> List.partition (exists_subterm (curry (op =) (Var v)))
|> pairself (fn lits => fold (curry s_disj) lits @{term False})
in
s_disj (HOLogic.all_const T
$ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
unskolem have_nots)
end
- | NONE => t))
+ | NONE =>
+ (case find_var t of
+ SOME (v as ((s, _), T)) =>
+ HOLogic.all_const T $ Abs (s, T, unskolem (safe_abstract_over (Var v, t)))
+ | NONE => t)))
in
HOLogic.mk_Trueprop o unskolem o HOLogic.dest_Trueprop
end
@@ -714,38 +718,44 @@
val (input_steps, other_steps) = List.partition (null o #5) proof
- val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_skolem t []) input_steps
- val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
- val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
+ (* The names of the formulas are added to the Skolem constants, to ensure that formulas giving
+ rise to several clauses are skolemized together. *)
+ val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps
+ val groups0 = Graph.strong_conn (fold add_cycle skoXss Graph.empty)
+ val groups = filter (exists (String.isPrefix spass_skolem_prefix)) groups0
- fun step_name_of_group skos = (implode skos, [])
+ val skoXss_input_steps = skoXss ~~ input_steps
+
+ fun step_name_of_group skoXs = (implode skoXs, [])
fun in_group group = member (op =) group o hd
- fun group_of sko = the (find_first (fn group => in_group group sko) groups)
+ fun group_of skoX = find_first (fn group => in_group group skoX) groups
- fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
+ fun new_steps skoXss_steps group =
let
val name = step_name_of_group group
val name0 = name |>> prefix "0"
val t =
- (case map (snd #> #3) skoss_steps of
+ (case map (snd #> #3) skoXss_steps of
[t] => t
| ts => ts
|> map (HOLogic.dest_Trueprop #> rename_skolem_args)
|> Library.foldr1 s_conj
|> HOLogic.mk_Trueprop)
- val skos = fold (union (op =) o fst) skoss_steps []
- val deps = map (snd #> #1) skoss_steps
+ val skos =
+ fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps []
+ val deps = map (snd #> #1) skoXss_steps
in
[(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
(name, Unknown, t, spass_skolemize_rule, [name0])]
end
val sko_steps =
- maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group) groups
+ maps (fn group => new_steps (filter (in_group group o fst) skoXss_input_steps) group) groups
val old_news =
- map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
- skoss_input_steps
+ map_filter (fn (skoXs, (name, _, _, _, _)) =>
+ Option.map (pair name o single o step_name_of_group) (group_of skoXs))
+ skoXss_input_steps
val repair_deps = fold replace_dependencies_in_line old_news
in
input_steps @ sko_steps @ map repair_deps other_steps