# HG changeset patch # User nipkow # Date 1412617222 -7200 # Node ID bca419a7f9eb1516f59c460aa9a2fd9c7cd5d18a # Parent 85fa90262807312d77e9e49933fdeb2c8780b11a# Parent ab56811d76c656c03ecaff99664ec0226961d76d merged diff -r ab56811d76c6 -r bca419a7f9eb src/HOL/SMT.thy --- 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 @@ "\Q. \x. \y ya. Q x y ya \ \f fa. \x. Q x (f x) (fa x)" "\Q. \x. \y ya yb. Q x y ya yb \ \f fa fb. \x. Q x (f x) (fa x) (fb x)" "\Q. \x. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x. Q x (f x) (fa x) (fb x) (fc x)" + "\Q. \x. \y ya yb yc yd. Q x y ya yb yc yd \ + \f fa fb fc fd. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" + "\Q. \x. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ + \f fa fb fc fd fe. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" + "\Q. \x. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ + \f fa fb fc fd fe ff. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" + "\Q. \x. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ + \f fa fb fc fd fe ff fg. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" by metis+ lemma bchoices: "\Q. \x \ S. \y ya. Q x y ya \ \f fa. \x \ S. Q x (f x) (fa x)" "\Q. \x \ S. \y ya yb. Q x y ya yb \ \f fa fb. \x \ S. Q x (f x) (fa x) (fb x)" "\Q. \x \ S. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x \ S. Q x (f x) (fa x) (fb x) (fc x)" + "\Q. \x \ S. \y ya yb yc yd. Q x y ya yb yc yd \ + \f fa fb fc fd. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" + "\Q. \x \ S. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ + \f fa fb fc fd fe. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" + "\Q. \x \ S. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ + \f fa fb fc fd fe ff. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" + "\Q. \x \ S. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ + \f fa fb fc fd fe ff fg. \x \ 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 = {* diff -r ab56811d76c6 -r bca419a7f9eb src/HOL/Tools/ATP/atp_problem.ML --- 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 = diff -r ab56811d76c6 -r bca419a7f9eb src/HOL/Tools/ATP/atp_proof.ML --- 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 diff -r ab56811d76c6 -r bca419a7f9eb src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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