# HG changeset patch # User blanchet # Date 1276504561 -7200 # Node ID 2bf7e6136047da259803c8707037e97e97bc8bf6 # Parent 6c9f23863808483d70310b4374751b4637c61ba9 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Jun 14 10:36:01 2010 +0200 @@ -25,11 +25,8 @@ ("Tools/Sledgehammer/metis_tactics.ML") begin -definition skolem_Eps :: "('a \ bool) \ 'a" where -[no_atp]: "skolem_Eps = Eps" - -lemma skolem_someI_ex [no_atp]: "\x. P x \ P (skolem_Eps (\x. P x))" -unfolding skolem_Eps_def by (rule someI_ex) +definition skolem_id :: "'a \ 'a" where +[no_atp]: "skolem_id = (\x. x)" definition COMBI :: "'a \ 'a" where [no_atp]: "COMBI P \ P" diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 14 10:36:01 2010 +0200 @@ -139,7 +139,7 @@ let val thy = ProofContext.theory_of ctxt val (skolem_somes, (mlits, types_sorts)) = - th |> prop_of |> kill_skolem_Eps j skolem_somes + th |> prop_of |> conceal_skolem_somes j skolem_somes ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) in if is_conjecture then @@ -235,24 +235,14 @@ SOME tf => mk_tfree ctxt tf | NONE => raise Fail ("fol_type_to_isa: " ^ x)); -fun reintroduce_skolem_Eps thy skolem_somes = - let - fun aux Ts args t = - case t of - t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1 - | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args) - | Const (s, T) => - if String.isPrefix skolem_Eps_pseudo_theory s then - let - val (T', args', def') = AList.lookup (op =) skolem_somes s |> the - in - def' |> subst_free (args' ~~ args) - |> map_types Type_Infer.paramify_vars - end - else - list_comb (t, args) - | t => list_comb (t, args) - in aux [] [] end +fun reveal_skolem_somes skolem_somes = + map_aterms (fn t as Const (s, T) => + if String.isPrefix skolem_theory_name s then + AList.lookup (op =) skolem_somes s + |> the |> map_types Type_Infer.paramify_vars + else + t + | t => t) (*Maps metis terms to isabelle terms*) fun hol_term_from_fol_PT ctxt fol_tm = @@ -360,8 +350,7 @@ val ts = map (hol_term_from_fol mode ctxt) fol_tms val _ = trace_msg (fn () => " calling type inference:") val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = - ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> infer_types ctxt + val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt val _ = app (fn t => trace_msg (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) @@ -418,7 +407,7 @@ fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) fun subst_translation (x,y) = let val v = find_var x - (* We call "reintroduce_skolem_Eps" and "infer_types" below. *) + (* We call "reveal_skolem_somes" and "infer_types" below. *) val t = hol_term_from_fol mode ctxt y in SOME (cterm_of thy (Var v), t) end handle Option => @@ -434,7 +423,7 @@ val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) - val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes) + val tms = rawtms |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) val substs' = ListPair.zip (vars, map ctm_of tms) @@ -638,7 +627,7 @@ type logic_map = {axioms: (Metis.Thm.thm * thm) list, tfrees: type_literal list, - skolem_somes: (string * (typ * term list * term)) list} + skolem_somes: (string * term) list} fun const_in_metis c (pred, tm_list) = let @@ -708,12 +697,7 @@ val lmap = lmap |> mode <> FO ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) - in - (mode, add_type_thm (type_ext thy - (* FIXME: Call"kill_skolem_Eps" here? *) - (map ((*snd o kill_skolem_Eps ~1 skolem_somes o*) prop_of) - (cls @ ths))) lmap) - end; + in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end fun refute cls = Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 14 10:36:01 2010 +0200 @@ -117,7 +117,7 @@ add_const_typ_table (const_with_typ thy (c,typ), tab) | add_term_consts_typs_rm thy (Free(c, typ), tab) = add_const_typ_table (const_with_typ thy (c,typ), tab) - | add_term_consts_typs_rm _ (Const (@{const_name skolem_Eps}, _) $ _, tab) = + | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) = tab | add_term_consts_typs_rm thy (t $ u, tab) = add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) @@ -471,7 +471,8 @@ (* ATP invocation methods setup *) (***************************************************************) -fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 [] +fun is_quasi_fol_term thy = + Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] (*Ensures that no higher-order theorems "leak out"*) fun restrict_to_logic thy true cls = diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 14 10:36:01 2010 +0200 @@ -10,11 +10,10 @@ val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit - val skolem_Eps_pseudo_theory: string + val skolem_theory_name: string val skolem_prefix: string val skolem_infix: string val is_skolem_const_name: string -> bool - val skolem_type_and_args: typ -> term -> typ * term list val cnf_axiom: theory -> thm -> thm list val multi_base_blacklist: string list val is_theorem_bad_for_atps: thm -> bool @@ -42,7 +41,7 @@ val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); -val skolem_Eps_pseudo_theory = "Sledgehammer.Eps" +val skolem_theory_name = "Sledgehammer.Sko" val skolem_prefix = "sko_" val skolem_infix = "$" @@ -76,9 +75,6 @@ (**** SKOLEMIZATION BY INFERENCE (lcp) ****) -fun skolem_Eps_const T = - Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T) - (*Keep the full complexity of the original name*) fun flatten_name s = space_implode "_X" (Long_Name.explode s); @@ -120,7 +116,7 @@ val id = skolem_name s (Unsynchronized.inc skolem_count) s' val (cT, args) = skolem_type_and_args T body val rhs = list_abs_free (map dest_Free args, - skolem_Eps_const T $ body) + HOLogic.choice_const T $ body) (*Forms a lambda-abstraction over the formal parameters*) val (c, thy) = Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy @@ -139,6 +135,9 @@ | dec_sko t thx = thx in dec_sko (prop_of th) ([], thy) end +fun mk_skolem_id t = + let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end + (*Traverse a theorem, accumulating Skolem function definitions.*) fun assume_skolem_funs inline s th = let @@ -152,7 +151,9 @@ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) val id = skolem_name s (Unsynchronized.inc skolem_count) s' val c = Free (id, cT) - val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body) + val rhs = list_abs_free (map dest_Free args, + HOLogic.choice_const T $ body) + |> inline ? mk_skolem_id (*Forms a lambda-abstraction over the formal parameters*) val def = Logic.mk_equals (c, rhs) val comb = list_comb (if inline then rhs else c, args) @@ -295,23 +296,26 @@ Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) fun skolem_theorem_of_def inline def = let - val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) - val (ch, frees) = c_variant_abs_multi (rhs, []) - val (chilbert,cabs) = Thm.dest_comb ch + val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) + val rhs' = rhs |> inline ? (snd o Thm.dest_comb) + val (ch, frees) = c_variant_abs_multi (rhs', []) + val (chilbert, cabs) = ch |> Thm.dest_comb val thy = Thm.theory_of_cterm chilbert val t = Thm.term_of chilbert val T = case t of - Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T - | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def]) + Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T + | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t]) val cex = Thm.cterm_of thy (HOLogic.exists_const T) val ex_tm = c_mkTrueprop (Thm.capply cex cabs) and conc = Drule.list_comb (if inline then rhs else c, frees) |> Drule.beta_conv cabs |> c_mkTrueprop fun tacf [prem] = - (if inline then all_tac else rewrite_goals_tac [def]) - THEN rtac (prem RS @{thm skolem_someI_ex}) 1 + (if inline then rewrite_goals_tac @{thms skolem_id_def_raw} + else rewrite_goals_tac [def]) + THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw}) + RS @{thm someI_ex}) 1 in Goal.prove_internal [ex_tm] conc tacf |> forall_intr_list frees |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) @@ -398,12 +402,7 @@ let val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 - - val inline = false -(* -FIXME: Reintroduce code: val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth) -*) val defs = skolem_theorems_of_assume inline s nnfth val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt in @@ -492,7 +491,8 @@ I else fold_index (fn (i, th) => - if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then + if is_theorem_bad_for_atps th orelse + is_some (lookup_cache thy th) then I else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 10:36:01 2010 +0200 @@ -29,9 +29,8 @@ val type_of_combterm : combterm -> fol_type val strip_combterm_comb : combterm -> combterm * combterm list val literals_of_term : theory -> term -> literal list * typ list - val kill_skolem_Eps : - int -> (string * (typ * term list * term)) list -> term - -> (string * (typ * term list * term)) list * term + val conceal_skolem_somes : + int -> (string * term) list -> term -> (string * term) list * term exception TRIVIAL val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list val make_axiom_clauses : bool -> theory -> @@ -123,7 +122,7 @@ let val (tp, ts) = type_of dfg T val tvar_list = - (if String.isPrefix skolem_Eps_pseudo_theory c then + (if String.isPrefix skolem_theory_name c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) @@ -163,46 +162,24 @@ skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ skolem_infix ^ "g" -val flip_type = - map_atyps (fn TFree (s, S) => TVar ((s, 0), S) - | TVar ((s, 0), S) => TFree (s, S) - | T as TVar (_, S) => raise TYPE ("nonzero TVar", [T], []) - | T => T) -val flip_term = - map_aterms (fn Free (s, T) => Var ((s, 0), T) - | Var ((s, 0), T) => Free (s, T) - | t as Var (_, S) => raise TERM ("nonzero Var", [t]) - | t => t) - #> map_types flip_type - -fun flipped_skolem_type_and_args bound_T body = - skolem_type_and_args (flip_type bound_T) (flip_term body) - |>> flip_type ||> map flip_term - -fun triple_aconv ((T1, ts1, t1), (T2, ts2, t2)) = - T1 = T2 andalso length ts1 = length ts2 andalso - forall (op aconv) (ts1 ~~ ts2) andalso t1 aconv t2 - -fun kill_skolem_Eps i skolem_somes t = - if exists_Const (curry (op =) @{const_name skolem_Eps} o fst) t then +fun conceal_skolem_somes i skolem_somes t = + if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then let fun aux skolem_somes - (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) = + (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) = let - val bound_T = range_type eps_T - val (T, args) = flipped_skolem_type_and_args bound_T t2 val (skolem_somes, s) = if i = ~1 then (skolem_somes, @{const_name undefined}) - else case AList.find triple_aconv skolem_somes (T, args, t) of + else case AList.find (op aconv) skolem_somes t of s :: _ => (skolem_somes, s) | _ => let - val s = skolem_Eps_pseudo_theory ^ "." ^ + val s = skolem_theory_name ^ "." ^ skolem_name i (length skolem_somes) (length (Term.add_tvarsT T [])) - in ((s, (T, args, t)) :: skolem_somes, s) end - in (skolem_somes, list_comb (Const (s, T), args)) end + in ((s, t) :: skolem_somes, s) end + in (skolem_somes, Const (s, T)) end | aux skolem_somes (t1 $ t2) = let val (skolem_somes, t1) = aux skolem_somes t1 @@ -224,7 +201,7 @@ fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes = let val (skolem_somes, t) = - th |> prop_of |> kill_skolem_Eps clause_id skolem_somes + th |> prop_of |> conceal_skolem_somes clause_id skolem_somes val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t in if forall isFalse lits then diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 14 10:36:01 2010 +0200 @@ -261,8 +261,8 @@ (instances of) Skolem pseudoconstants, this information is encoded in the constant name. *) fun num_type_args thy s = - if String.isPrefix skolem_Eps_pseudo_theory s then - s |> unprefix skolem_Eps_pseudo_theory + if String.isPrefix skolem_theory_name s then + s |> unprefix skolem_theory_name |> space_explode skolem_infix |> hd |> space_explode "_" |> List.last |> Int.fromString |> the else @@ -324,7 +324,7 @@ else (* Extra args from "hAPP" come after any arguments given directly to the constant. *) - if String.isPrefix skolem_Eps_pseudo_theory c then + if String.isPrefix skolem_theory_name c then map fastype_of ts ---> HOLogic.typeT else Sign.const_instance thy (c, diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Sat Jun 12 15:48:17 2010 +0200 +++ b/src/HOL/Tools/meson.ML Mon Jun 14 10:36:01 2010 +0200 @@ -98,9 +98,8 @@ val tmA = concl_of thA val Const("==>",_) $ tmB $ _ = prop_of thB val tenv = - Pattern.first_order_match thy - (pairself Envir.beta_eta_contract (tmB, tmA)) - (Vartab.empty, Vartab.empty) |> snd + Pattern.first_order_match thy (tmB, tmA) + (Vartab.empty, Vartab.empty) |> snd val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) in thA RS (cterm_instantiate ct_pairs thB) end) () of SOME th => th @@ -317,17 +316,17 @@ val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); -fun apply_skolem_ths (th, rls) = +fun apply_skolem_theorem (th, rls) = let - fun tryall [] = raise THM ("apply_skolem_ths", 0, th::rls) + fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) | tryall (rl :: rls) = first_order_resolve th rl handle THM _ => tryall rls in tryall rls end -(*Conjunctive normal form, adding clauses from th in front of ths (for foldr). - Strips universal quantifiers and breaks up conjunctions. - Eliminates existential quantifiers using skoths: Skolemization theorems.*) -fun cnf skoths ctxt (th,ths) = +(* Conjunctive normal form, adding clauses from th in front of ths (for foldr). + Strips universal quantifiers and breaks up conjunctions. + Eliminates existential quantifiers using Skolemization theorems. *) +fun cnf skolem_ths ctxt (th, ths) = let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) @@ -341,7 +340,7 @@ in ctxtr := ctxt'; cnf_aux (th', ths) end | Const ("Ex", _) => (*existential quantifier: Insert Skolem functions*) - cnf_aux (apply_skolem_ths (th,skoths), ths) + cnf_aux (apply_skolem_theorem (th, skolem_ths), ths) | Const ("op |", _) => (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using all combinations of converting P, Q to CNF.*) @@ -357,7 +356,7 @@ else cnf_aux (th,ths) in (cls, !ctxtr) end; -fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []); +fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []); (*Generalization, removal of redundant equalities, removal of tautologies.*) fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);