# HG changeset patch # User blanchet # Date 1276333974 -7200 # Node ID e6b1a0693f3fc89cec345e278276254045639230 # Parent fe6262d929a3090133e14b5d8b213d3d6b0504f7# Parent 7e3d7af862150ae826185ebc344fd119de7ffb48 merged diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Nitpick.thy Sat Jun 12 11:12:54 2010 +0200 @@ -214,6 +214,10 @@ definition inverse_frac :: "'a \ 'a" where "inverse_frac q \ frac (denom q) (num q)" +definition less_frac :: "'a \ 'a \ bool" where +[nitpick_simp]: +"less_frac q r \ num (plus_frac q (uminus_frac r)) < 0" + definition less_eq_frac :: "'a \ 'a \ bool" where [nitpick_simp]: "less_eq_frac q r \ num (plus_frac q (uminus_frac r)) \ 0" @@ -245,7 +249,7 @@ wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac - less_eq_frac of_frac + less_frac less_eq_frac of_frac hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit word hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def @@ -254,6 +258,6 @@ list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def number_of_frac_def - inverse_frac_def less_eq_frac_def of_frac_def + inverse_frac_def less_frac_def less_eq_frac_def of_frac_def end diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sat Jun 12 11:12:54 2010 +0200 @@ -95,20 +95,20 @@ nitpick [expect = genuine] oops -lemma "Pair a b \ Abs_Prod (Pair_Rep a b)" +lemma "Pair a b = Abs_prod (Pair_Rep a b)" nitpick [card = 1\2, expect = none] by (rule Pair_def) -lemma "Pair a b \ Abs_Prod (Pair_Rep b a)" +lemma "Pair a b = Abs_prod (Pair_Rep b a)" nitpick [card = 1\2, expect = none] nitpick [dont_box, expect = genuine] oops -lemma "fst (Abs_Prod (Pair_Rep a b)) = a" +lemma "fst (Abs_prod (Pair_Rep a b)) = a" nitpick [card = 2, expect = none] -by (simp add: Pair_def [THEN symmetric]) +by (simp add: Pair_def [THEN sym]) -lemma "fst (Abs_Prod (Pair_Rep a b)) = b" +lemma "fst (Abs_prod (Pair_Rep a b)) = b" nitpick [card = 1\2, expect = none] nitpick [dont_box, expect = genuine] oops @@ -117,19 +117,19 @@ nitpick [expect = none] apply (rule ccontr) apply simp -apply (drule subst [where P = "\r. Abs_Prod r = Abs_Prod (Pair_Rep a b)"]) +apply (drule subst [where P = "\r. Abs_prod r = Abs_prod (Pair_Rep a b)"]) apply (rule refl) -by (simp add: Pair_def [THEN symmetric]) +by (simp add: Pair_def [THEN sym]) -lemma "Abs_Prod (Rep_Prod a) = a" +lemma "Abs_prod (Rep_prod a) = a" nitpick [card = 2, expect = none] -by (rule Rep_Prod_inverse) +by (rule Rep_prod_inverse) -lemma "Inl \ \a. Abs_Sum (Inl_Rep a)" +lemma "Inl \ \a. Abs_sum (Inl_Rep a)" nitpick [card = 1, expect = none] -by (simp only: Inl_def o_def) +by (simp add: Inl_def o_def) -lemma "Inl \ \a. Abs_Sum (Inr_Rep a)" +lemma "Inl \ \a. Abs_sum (Inr_Rep a)" nitpick [card = 1, card "'a + 'a" = 2, expect = genuine] oops @@ -137,20 +137,20 @@ nitpick [expect = none] by (rule Inl_Rep_not_Inr_Rep) -lemma "Abs_Sum (Rep_Sum a) = a" +lemma "Abs_sum (Rep_sum a) = a" nitpick [card = 1, expect = none] nitpick [card = 2, expect = none] -by (rule Rep_Sum_inverse) +by (rule Rep_sum_inverse) lemma "0::nat \ Abs_Nat Zero_Rep" nitpick [expect = none] by (rule Zero_nat_def_raw) -lemma "Suc \ \n. Abs_Nat (Suc_Rep (Rep_Nat n))" +lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" nitpick [expect = none] by (rule Suc_def) -lemma "Suc \ \n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))" +lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))" nitpick [expect = genuine] oops diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Rat.thy --- a/src/HOL/Rat.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Rat.thy Sat Jun 12 11:12:54 2010 +0200 @@ -1182,15 +1182,16 @@ (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}), (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), + (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}), (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})] *} lemmas [nitpick_def] = inverse_rat_inst.inverse_rat - number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat - plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat - zero_rat_inst.zero_rat + number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat + ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat + uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat subsection{* Float syntax *} diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/RealDef.thy Sat Jun 12 11:12:54 2010 +0200 @@ -1806,12 +1806,13 @@ (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}), (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}), (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}), + (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}), (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})] *} lemmas [nitpick_def] = inverse_real_inst.inverse_real number_real_inst.number_of_real one_real_inst.one_real - ord_real_inst.less_eq_real plus_real_inst.plus_real + ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real times_real_inst.times_real uminus_real_inst.uminus_real zero_real_inst.zero_real diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Sat Jun 12 11:12:54 2010 +0200 @@ -25,6 +25,12 @@ ("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 COMBI :: "'a \ 'a" where [no_atp]: "COMBI P \ P" diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Nitpick/minipick.ML Sat Jun 12 11:12:54 2010 +0200 @@ -80,7 +80,7 @@ fun kodkod_formula_from_term ctxt card frees = let - fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r = + fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r = let val jss = atom_schema_of SRep card T1 |> map (rpair 0) |> all_combinations @@ -115,7 +115,7 @@ @{const Not} $ t1 => Not (to_F Ts t1) | @{const False} => False | @{const True} => True - | Const (@{const_name All}, _) $ Abs (s, T, t') => + | Const (@{const_name All}, _) $ Abs (_, T, t') => All (decls_for SRep card Ts T, to_F (T :: Ts) t') | (t0 as Const (@{const_name All}, _)) $ t1 => to_F Ts (t0 $ eta_expand Ts t1 1) diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Sat Jun 12 11:12:54 2010 +0200 @@ -298,7 +298,6 @@ val peephole_optim = true val nat_card = 4 val int_card = 9 - val bits = 8 val j0 = 0 val constrs = kodkod_constrs peephole_optim nat_card int_card j0 val (free_rels, pool, table) = diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Jun 12 11:12:54 2010 +0200 @@ -18,6 +18,7 @@ structure Metis_Tactics : METIS_TACTICS = struct +open Sledgehammer_Util open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause @@ -84,7 +85,7 @@ val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis.Term.Var v - | _ => error "hol_term_to_fol_FO"; + | _ => raise Fail "hol_term_to_fol_FO"; fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = @@ -118,7 +119,7 @@ metis_lit pol "=" (map hol_term_to_fol_FT tms) | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); -fun literals_of_hol_thm thy mode t = +fun literals_of_hol_term thy mode t = let val (lits, types_sorts) = literals_of_term thy t in (map (hol_literal_to_fol mode) lits, types_sorts) end; @@ -134,21 +135,24 @@ fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf)); -fun hol_thm_to_fol is_conjecture ctxt mode th = - let val thy = ProofContext.theory_of ctxt - val (mlits, types_sorts) = - (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th +fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th = + let + val thy = ProofContext.theory_of ctxt + val (skolem_somes, (mlits, types_sorts)) = + th |> prop_of |> kill_skolem_Eps j skolem_somes + ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) in if is_conjecture then (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), - type_literals_for_types types_sorts) + type_literals_for_types types_sorts, skolem_somes) else let val tylits = filter_out (default_sort ctxt) types_sorts |> type_literals_for_types val mtylits = if Config.get ctxt type_lits then map (metis_of_type_literals false) tylits else [] in - (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) + (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [], + skolem_somes) end end; @@ -194,7 +198,7 @@ fun apply_list rator nargs rands = let val trands = terms_of rands in if length trands = nargs then Term (list_comb(rator, trands)) - else error + else raise Fail ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ " expected " ^ Int.toString nargs ^ " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) @@ -229,12 +233,32 @@ | NONE => case strip_prefix tfree_prefix x of SOME tf => mk_tfree ctxt tf - | NONE => error ("fol_type_to_isa: " ^ x)); + | 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 (*Maps metis terms to isabelle terms*) -fun fol_term_to_hol_RAW ctxt fol_tm = +fun hol_term_from_fol_PT ctxt fol_tm = let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) + val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^ + Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = (case strip_prefix tvar_prefix v of SOME w => Type (make_tvar w) @@ -250,7 +274,7 @@ Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) | _ => case tm_to_tt rator of Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) - | _ => error "tm_to_tt: HO application" + | _ => raise Fail "tm_to_tt: HO application" end | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) and applic_to_tt ("=",ts) = @@ -265,12 +289,13 @@ val tys = types_of (List.take(tts,ntypes)) in if length tys = ntypes then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) - else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) + else + raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ + " but gets " ^ Int.toString (length tys) ^ + " type arguments\n" ^ + cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ + " the terms are \n" ^ + cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) case strip_prefix tconst_prefix a of @@ -284,12 +309,17 @@ SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end - | NONE => error ("unexpected metis function: " ^ a) - in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end; + | NONE => raise Fail ("unexpected metis function: " ^ a) + in + case tm_to_tt fol_tm of + Term t => t + | _ => raise Fail "fol_tm_to_tt: Term expected" + end (*Maps fully-typed metis terms to isabelle terms*) -fun fol_term_to_hol_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) +fun hol_term_from_fol_FT ctxt fol_tm = + let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^ + Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = (case strip_prefix schematic_var_prefix v of SOME w => mk_var(w, dummyT) @@ -302,7 +332,7 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) - | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) + | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = cvt tm1 $ cvt tm2 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) @@ -316,21 +346,22 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); - fol_term_to_hol_RAW ctxt t)) - | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); - fol_term_to_hol_RAW ctxt t) - in cvt fol_tm end; + | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x); + hol_term_from_fol_PT ctxt t)) + | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t); + hol_term_from_fol_PT ctxt t) + in fol_tm |> cvt end -fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt - | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt - | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt; +fun hol_term_from_fol FT = hol_term_from_fol_FT + | hol_term_from_fol _ = hol_term_from_fol_PT -fun fol_terms_to_hol ctxt mode fol_tms = - let val ts = map (fol_term_to_hol ctxt mode) fol_tms +fun hol_terms_from_fol ctxt mode skolem_somes fol_tms = + let val thy = ProofContext.theory_of ctxt + 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' = infer_types ctxt ts; + val ts' = + ts |> map (reintroduce_skolem_Eps thy 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))) @@ -354,7 +385,8 @@ fun lookth thpairs (fth : Metis.Thm.thm) = the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) - handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); + handle Option => + raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); fun is_TrueI th = Thm.eq_thm(TrueI,th); @@ -371,22 +403,23 @@ (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) (* INFERENCE RULE: ASSUME *) -fun assume_inf ctxt mode atm = +fun assume_inf ctxt mode skolem_somes atm = inst_excluded_middle (ProofContext.theory_of ctxt) - (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)); + (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm)) (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange that new TVars are distinct and that types can be inferred from terms.*) -fun inst_inf ctxt mode thpairs fsubst th = +fun inst_inf ctxt mode skolem_somes thpairs fsubst th = let val thy = ProofContext.theory_of ctxt val i_th = lookth thpairs th val i_th_vars = Term.add_vars (prop_of i_th) [] 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 - val t = fol_term_to_hol ctxt mode y (*we call infer_types below*) + (* We call "reintroduce_skolem_Eps" and "infer_types" below. *) + val t = hol_term_from_fol mode ctxt y in SOME (cterm_of thy (Var v), t) end handle Option => (trace_msg (fn() => "List.find failed for the variable " ^ x ^ @@ -401,7 +434,8 @@ 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 = infer_types ctxt rawtms; + val tms = rawtms |> map (reintroduce_skolem_Eps thy 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) val _ = trace_msg (fn () => @@ -409,10 +443,11 @@ (substs' |> map (fn (x, y) => Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th end + in cterm_instantiate substs' i_th end handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg) | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^ - "\n(Perhaps you want to try \"metisFT\".)") + "\n(Perhaps you want to try \"metisFT\" if you \ + \haven't done so already.)") (* INFERENCE RULE: RESOLVE *) @@ -428,7 +463,7 @@ | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) end; -fun resolve_inf ctxt mode thpairs atm th1 th2 = +fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 = let val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) @@ -438,15 +473,16 @@ else if is_TrueI i_th2 then i_th1 else let - val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm) + val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes) + (Metis.Term.Fn atm) val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) val prems_th1 = prems_of i_th1 val prems_th2 = prems_of i_th2 val index_th1 = get_index (mk_not i_atm) prems_th1 - handle Empty => error "Failed to find literal in th1" + handle Empty => raise Fail "Failed to find literal in th1" val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) val index_th2 = get_index i_atm prems_th2 - handle Empty => error "Failed to find literal in th2" + handle Empty => raise Fail "Failed to find literal in th2" val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end end; @@ -455,9 +491,9 @@ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; -fun refl_inf ctxt mode t = +fun refl_inf ctxt mode skolem_somes t = let val thy = ProofContext.theory_of ctxt - val i_t = singleton (fol_terms_to_hol ctxt mode) t + val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end; @@ -467,10 +503,10 @@ | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) -fun equality_inf ctxt mode (pos, atm) fp fr = +fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr = let val thy = ProofContext.theory_of ctxt val m_tm = Metis.Term.Fn atm - val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr] + val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr] val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls @@ -491,6 +527,10 @@ fun path_finder_HO tm [] = (tm, Term.Bound 0) | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + | path_finder_HO tm ps = + raise Fail ("equality_inf, path_finder_HO: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm) fun path_finder_FT tm [] _ = (tm, Term.Bound 0) | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = path_finder_FT tm ps t1 @@ -498,10 +538,11 @@ (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis.Term.toString t) + | path_finder_FT tm ps t = + raise Fail ("equality_inf, path_finder_FT: path = " ^ + space_implode " " (map Int.toString ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + " fol-term: " ^ Metis.Term.toString t) fun path_finder FO tm ps _ = path_finder_FO tm ps | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = (*equality: not curried, as other predicates are*) @@ -539,24 +580,28 @@ val factor = Seq.hd o distinct_subgoals_tac; -fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th) - | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm - | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) = - factor (inst_inf ctxt mode thpairs f_subst f_th1) - | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = - factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) - | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm - | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = - equality_inf ctxt mode f_lit f_p f_r; +fun step ctxt mode skolem_somes thpairs p = + case p of + (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th) + | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm + | (_, Metis.Proof.Subst (f_subst, f_th1)) => + factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1) + | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) => + factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2) + | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm + | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) => + equality_inf ctxt mode skolem_somes f_lit f_p f_r fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); -fun translate _ _ thpairs [] = thpairs - | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = +(* FIXME: use "fold" instead *) +fun translate _ _ _ thpairs [] = thpairs + | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) = let val _ = trace_msg (fn () => "=============================================") val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) - val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf)) + val th = Meson.flexflex_first_order (step ctxt mode skolem_somes + thpairs (fol_th, inf)) val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) val _ = trace_msg (fn () => "=============================================") val n_metis_lits = @@ -564,7 +609,7 @@ in if nprems_of th = n_metis_lits then () else error "Metis: proof reconstruction has gone wrong"; - translate mode ctxt ((fol_th, th) :: thpairs) infpairs + translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs end; (*Determining which axiom clauses are actually used*) @@ -592,7 +637,8 @@ type logic_map = {axioms: (Metis.Thm.thm * thm) list, - tfrees: type_literal list}; + tfrees: type_literal list, + skolem_somes: (string * (typ * term list * term)) list} fun const_in_metis c (pred, tm_list) = let @@ -610,14 +656,15 @@ (*transform isabelle type / arity clause to metis clause *) fun add_type_thm [] lmap = lmap - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} = - add_type_thm cls {axioms = (mth, ith) :: axioms, - tfrees = tfrees} + | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} = + add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, + skolem_somes = skolem_somes} (*Insert non-logical axioms corresponding to all accumulated TFrees*) -fun add_tfrees {axioms, tfrees} : logic_map = - {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms, - tfrees = tfrees}; +fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map = + {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ + axioms, + tfrees = tfrees, skolem_somes = skolem_somes} fun string_of_mode FO = "FO" | string_of_mode HO = "HO" @@ -628,18 +675,27 @@ let val thy = ProofContext.theory_of ctxt (*The modes FO and FT are sticky. HO can be downgraded to FO.*) fun set_mode FO = FO - | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO + | set_mode HO = + if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO + else HO | set_mode FT = FT val mode = set_mode mode0 (*transform isabelle clause to metis clause *) - fun add_thm is_conjecture ith {axioms, tfrees} : logic_map = - let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith + fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map = + let + val (mth, tfree_lits, skolem_somes) = + hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes + ith in {axioms = (mth, Meson.make_meta_clause ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees} + tfrees = union (op =) tfree_lits tfrees, + skolem_somes = skolem_somes} end; - val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt} - val lmap = fold (add_thm false) ths (add_tfrees lmap0) + val lmap as {skolem_somes, ...} = + {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} + |> fold (add_thm true) cls + |> add_tfrees + |> fold (add_thm false) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists (*Now check for the existence of certain combinators*) @@ -649,10 +705,14 @@ val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else [] val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else [] val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else [] - val lmap' = if mode=FO then lmap - else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap + val lmap = + lmap |> mode <> FO + ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) in - (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') + (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; fun refute cls = @@ -664,7 +724,7 @@ exception METIS of string; -(* Main function to start metis prove and reconstruction *) +(* Main function to start metis proof and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt val th_cls_pairs = @@ -674,7 +734,7 @@ val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg (fn () => "THEOREM CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths - val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths + val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees) @@ -694,7 +754,7 @@ val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt (*add constraints arising from converting goal to clause form*) val proof = Metis.Proof.proof mth - val result = translate mode ctxt' axioms proof + val result = translate ctxt' mode skolem_somes axioms proof and used = map_filter (used_axioms axioms) proof val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Jun 12 11:12:54 2010 +0200 @@ -21,6 +21,7 @@ val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list + val is_quasi_fol_term : theory -> term -> bool val relevant_facts : bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> thm list @@ -116,6 +117,8 @@ 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) = + 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)) | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) @@ -368,38 +371,35 @@ fun valid_facts facts = (facts, []) |-> Facts.fold_static (fn (name, ths0) => - let - fun check_thms a = - (case try (ProofContext.get_thms ctxt) a of - NONE => false - | SOME ths1 => Thm.eq_thms (ths0, ths1)); + if Facts.is_concealed facts name orelse + (respect_no_atp andalso is_package_def name) orelse + member (op =) multi_base_blacklist (Long_Name.base_name name) then + I + else + let + fun check_thms a = + (case try (ProofContext.get_thms ctxt) a of + NONE => false + | SOME ths1 => Thm.eq_thms (ths0, ths1)); - val name1 = Facts.extern facts name; - val name2 = Name_Space.extern full_space name; - val ths = filter_out is_theorem_bad_for_atps ths0; - in - if Facts.is_concealed facts name orelse - (respect_no_atp andalso is_package_def name) then - I - else case find_first check_thms [name1, name2, name] of - NONE => I - | SOME name' => - cons (name' |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix, ths) - end); + val name1 = Facts.extern facts name; + val name2 = Name_Space.extern full_space name; + val ths = filter_out is_theorem_bad_for_atps ths0; + in + case find_first check_thms [name1, name2, name] of + NONE => I + | SOME name' => + cons (name' |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix, ths) + end) in valid_facts global_facts @ valid_facts local_facts end; fun multi_name a th (n, pairs) = (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); -fun add_single_names (a, []) pairs = pairs - | add_single_names (a, [th]) pairs = (a, th) :: pairs - | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)); - -(*Ignore blacklisted basenames*) -fun add_multi_names (a, ths) pairs = - if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs - else add_single_names (a, ths) pairs; +fun add_names (a, []) pairs = pairs + | add_names (a, [th]) pairs = (a, th) :: pairs + | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; @@ -408,8 +408,7 @@ fun name_thm_pairs respect_no_atp ctxt name_thms_pairs = let val (mults, singles) = List.partition is_multi name_thms_pairs - val ps = [] |> fold add_single_names singles - |> fold add_multi_names mults + val ps = [] |> fold add_names singles |> fold add_names mults in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; fun is_named ("", th) = @@ -472,8 +471,11 @@ (* ATP invocation methods setup *) (***************************************************************) +fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 [] + (*Ensures that no higher-order theorems "leak out"*) -fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls +fun restrict_to_logic thy true cls = + filter (is_quasi_fol_term thy o prop_of o fst) cls | restrict_to_logic thy false cls = cls; (**** Predicates to detect unwanted clauses (prolific or likely to cause @@ -531,7 +533,7 @@ fun remove_dangerous_clauses full_types add_thms = filter_out (is_dangerous_theorem full_types add_thms o fst) -fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of +fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of fun relevant_facts full_types respect_no_atp relevance_threshold relevance_convergence defs_relevant max_new theory_relevant @@ -542,17 +544,17 @@ else let val thy = ProofContext.theory_of ctxt - val add_thms = cnf_for_facts ctxt add val has_override = not (null add) orelse not (null del) - val is_FO = is_first_order thy goal_cls + val is_FO = is_fol_goal thy goal_cls val axioms = - checked_name_thm_pairs respect_no_atp ctxt + checked_name_thm_pairs (respect_no_atp andalso not only) ctxt (if only then map (name_thms_pair_from_ref ctxt chained_ths) add else all_name_thms_pairs respect_no_atp ctxt chained_ths) |> cnf_rules_pairs thy |> not has_override ? make_unique - |> restrict_to_logic thy is_FO - |> not only ? remove_dangerous_clauses full_types add_thms + |> not only ? restrict_to_logic thy is_FO + |> (if only then I + else remove_dangerous_clauses full_types (cnf_for_facts ctxt add)) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override @@ -564,7 +566,7 @@ create additional clauses based on the information from extra_cls *) fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy = let - val is_FO = is_first_order thy goal_cls + val is_FO = is_fol_goal thy goal_cls val ccls = subtract_cls extra_cls goal_cls val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls val ccltms = map prop_of ccls @@ -576,7 +578,7 @@ val conjectures = make_conjecture_clauses dfg thy ccls val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) - val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, []) + val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers val classrel_clauses = make_classrel_clauses thy subs supers' in diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 12 11:12:54 2010 +0200 @@ -10,8 +10,11 @@ val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit + val skolem_Eps_pseudo_theory: 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 @@ -39,6 +42,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_prefix = "sko_" val skolem_infix = "$" @@ -72,13 +76,22 @@ (**** 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); -fun skolem_name thm_name nref var_name = - skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^ +fun skolem_name thm_name j var_name = + skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^ skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name) +(* Hack: Could return false positives (e.g., a user happens to declare a + constant called "SomeTheory.sko_means_shoe_in_$wedish". *) +val is_skolem_const_name = + Long_Name.base_name + #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix + fun rhs_extra_types lhsT rhs = let val lhs_vars = Term.add_tfreesT lhsT [] fun add_new_TFrees (TFree v) = @@ -87,34 +100,39 @@ val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; +fun skolem_type_and_args bound_T body = + let + val args1 = OldTerm.term_frees body + val Ts1 = map type_of args1 + val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body + val args2 = map (fn T => Free (gensym "vsk", T)) Ts2 + in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end + (* Traverse a theorem, declaring Skolem function definitions. String "s" is the suggested prefix for the Skolem constants. *) fun declare_skolem_funs s th thy = let - val nref = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) = - (*Existential: declare a Skolem function, then insert into body and continue*) - let - val cname = skolem_name s nref s' - val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) - val Ts = map type_of args0 - val extraTs = rhs_extra_types (Ts ---> T) xtp - val argsx = map (fn T => Free (gensym "vsk", T)) extraTs - val args = argsx @ args0 - val cT = extraTs ---> Ts ---> T - val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) - (*Forms a lambda-abstraction over the formal parameters*) - val (c, thy) = - Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy - val cdef = cname ^ "_def" - val ((_, ax), thy) = - Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy - val ax' = Drule.export_without_context ax - in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end + val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) + fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) + (axs, thy) = + (*Existential: declare a Skolem function, then insert into body and continue*) + let + 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) + (*Forms a lambda-abstraction over the formal parameters*) + val (c, thy) = + Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy + val cdef = id ^ "_def" + val ((_, ax), thy) = + Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy + val ax' = Drule.export_without_context ax + in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (OldTerm.add_term_names (p, [])) a - in dec_sko (subst_bound (Free (fname, T), p)) thx end + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (OldTerm.add_term_names (p, [])) a + in dec_sko (subst_bound (Free (fname, T), p)) thx end | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx @@ -122,29 +140,31 @@ in dec_sko (prop_of th) ([], thy) end (*Traverse a theorem, accumulating Skolem function definitions.*) -fun assume_skolem_funs s th = - let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs = - (*Existential: declare a Skolem function, then insert into body and continue*) - let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) - val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*) - val Ts = map type_of args - val cT = Ts ---> T - val id = skolem_name s sko_count s' - val c = Free (id, cT) - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ xtp) - (*Forms a lambda-abstraction over the formal parameters*) - val def = Logic.mk_equals (c, rhs) - in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end - | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (OldTerm.add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) defs end - | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs - | dec_sko t defs = defs (*Do nothing otherwise*) +fun assume_skolem_funs inline s th = + let + val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) + fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs = + (*Existential: declare a Skolem function, then insert into body and continue*) + let + val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) + val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*) + val Ts = map type_of args + 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) + (*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) + in dec_sko (subst_bound (comb, p)) (def :: defs) end + | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (OldTerm.add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) defs end + | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs + | dec_sko t defs = defs (*Do nothing otherwise*) in dec_sko (prop_of th) [] end; @@ -273,19 +293,25 @@ (*Given the definition of a Skolem function, return a theorem to replace an existential formula by a use of that function. Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun skolem_of_def def = - let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) +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 thy = Thm.theory_of_cterm chilbert val t = Thm.term_of chilbert - val T = case t of - Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T - | _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) + 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]) val cex = Thm.cterm_of thy (HOLogic.exists_const T) val ex_tm = c_mkTrueprop (Thm.capply cex cabs) - and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); - fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1 + 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 in Goal.prove_internal [ex_tm] conc tacf |> forall_intr_list frees |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) @@ -303,9 +329,9 @@ in (th3, ctxt) end; (*Generate Skolem functions for a theorem supplied in nnf*) -fun assume_skolem_of_def s th = - map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th)) - (assume_skolem_funs s th) +fun skolem_theorems_of_assume inline s th = + map (skolem_theorem_of_def inline o Thm.assume o cterm_of (theory_of_thm th)) + (assume_skolem_funs inline s th) (*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) @@ -364,7 +390,7 @@ else gensym "unknown_thm_"; (*Skolemize a named theorem, with Skolem functions as additional premises.*) -fun skolem_thm (s, th) = +fun skolemize_theorem s th = if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse is_theorem_bad_for_atps th then [] @@ -372,7 +398,13 @@ let val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 - val defs = assume_skolem_of_def s nnfth + + 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 cnfs |> map introduce_combinators @@ -402,7 +434,7 @@ fun cnf_axiom thy th0 = let val th = Thm.transfer thy th0 in case lookup_cache thy th of - NONE => map Thm.close_derivation (skolem_thm (fake_name th, th)) + NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th) | SOME cls => cls end; @@ -438,7 +470,8 @@ fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) = let - val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt; + val (cnfs, ctxt) = + Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt val cnfs' = cnfs |> map introduce_combinators |> Variable.export ctxt ctxt0 @@ -455,14 +488,17 @@ if Facts.is_concealed facts name orelse already_seen thy name then I else cons (name, ths)); val new_thms = (new_facts, []) |-> fold (fn (name, ths) => - if member (op =) multi_base_blacklist (Long_Name.base_name name) then I - else fold_index (fn (i, th) => - 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) + if member (op =) multi_base_blacklist (Long_Name.base_name name) then + I + else + fold_index (fn (i, th) => + 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) in - if null new_facts then NONE + if null new_facts then + NONE else let val (defs, thy') = thy diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sat Jun 12 11:12:54 2010 +0200 @@ -29,14 +29,17 @@ 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 exception TRIVIAL val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list val make_axiom_clauses : bool -> theory -> (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list val type_wrapper_name : string - val get_helper_clauses : bool -> theory -> bool -> - hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> - hol_clause list + val get_helper_clauses : + bool -> theory -> bool -> hol_clause list + -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> name_pool option * int @@ -115,28 +118,31 @@ TyVar (make_schematic_type_var x, string_of_indexname x); -fun const_type_of dfg thy (c,t) = - let val (tp,ts) = type_of dfg t - in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end; - (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) -fun combterm_of dfg thy (Const(c,t)) = - let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) - val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list) +fun combterm_of dfg thy (Const (c, T)) = + let + val (tp, ts) = type_of dfg T + val tvar_list = + (if String.isPrefix skolem_Eps_pseudo_theory c then + [] |> Term.add_tvarsT T |> map TVar + else + (c, T) |> Sign.const_typargs thy) + |> map (simp_type_of dfg) + val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list) in (c',ts) end - | combterm_of dfg _ (Free(v,t)) = - let val (tp,ts) = type_of dfg t + | combterm_of dfg _ (Free(v, T)) = + let val (tp,ts) = type_of dfg T val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end - | combterm_of dfg _ (Var(v,t)) = - let val (tp,ts) = type_of dfg t + | combterm_of dfg _ (Var(v, T)) = + let val (tp,ts) = type_of dfg T val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v',ts) end | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q in (CombApp(P',Q'), union (op =) tsP tsQ) end - | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t); + | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t); fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity) | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); @@ -153,36 +159,100 @@ fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; val literals_of_term = literals_of_term_dfg false; +fun skolem_name i j num_T_args = + 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 + let + fun aux skolem_somes + (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) = + 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 + s :: _ => (skolem_somes, s) + | _ => + let + val s = skolem_Eps_pseudo_theory ^ "." ^ + 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 + | aux skolem_somes (t1 $ t2) = + let + val (skolem_somes, t1) = aux skolem_somes t1 + val (skolem_somes, t2) = aux skolem_somes t2 + in (skolem_somes, t1 $ t2) end + | aux skolem_somes (Abs (s, T, t')) = + let val (skolem_somes, t') = aux skolem_somes t' in + (skolem_somes, Abs (s, T, t')) + end + | aux skolem_somes t = (skolem_somes, t) + in aux skolem_somes t end + else + (skolem_somes, t) + (* Trivial problem, which resolution cannot handle (empty clause) *) exception TRIVIAL; (* making axiom and conjecture clauses *) -fun make_clause dfg thy (clause_id, axiom_name, kind, th) = - let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th) - in - if forall isFalse lits then - raise TRIVIAL - else - HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, - kind = kind, literals = lits, ctypes_sorts = ctypes_sorts} - end; - - -fun add_axiom_clause dfg thy (th, (name, id)) = - let val cls = make_clause dfg thy (id, name, Axiom, th) in - not (isTaut cls) ? cons (name, cls) +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 + val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t + in + if forall isFalse lits then + raise TRIVIAL + else + (skolem_somes, + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) end +fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) = + let + val (skolem_somes, cls) = + make_clause dfg thy (id, name, Axiom, th) skolem_somes + in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end + fun make_axiom_clauses dfg thy clauses = - fold (add_axiom_clause dfg thy) clauses [] + ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd -fun make_conjecture_clauses_aux _ _ _ [] = [] - | make_conjecture_clauses_aux dfg thy n (th::ths) = - make_clause dfg thy (n,"conjecture", Conjecture, th) :: - make_conjecture_clauses_aux dfg thy (n+1) ths; - -fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0; - +fun make_conjecture_clauses dfg thy = + let + fun aux _ _ [] = [] + | aux n skolem_somes (th :: ths) = + let + val (skolem_somes, cls) = + make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes + in cls :: aux (n + 1) skolem_somes ths end + in aux 0 [] end (**********************************************************************) (* convert clause into ATP specific formats: *) @@ -415,19 +485,16 @@ fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) = - member (op =) user_lemmas axiom_name ? fold count_literal literals - fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint) -fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = +fun get_helper_clauses dfg thy isFO conjectures axcls = if isFO then [] else let - val axclauses = map #2 (make_axiom_clauses dfg thy axcls) - val ct = init_counters |> fold count_clause conjectures - |> fold (count_user_clause user_lemmas) axclauses + val axclauses = map snd (make_axiom_clauses dfg thy axcls) + val ct = init_counters + |> fold (fold count_clause) [conjectures, axclauses] fun needed c = the (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] @@ -439,9 +506,7 @@ else [] val other = cnf_helper_thms thy [@{thm fequal_imp_equal}, @{thm equal_imp_fequal}] - in - map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) - end; + in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end (*Find the minimal arity of each function mentioned in the term. Also, note which uses are not at top level, to see if hBOOL is needed.*) diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jun 12 11:12:54 2010 +0200 @@ -345,8 +345,8 @@ >> merge_relevance_overrides)) (add_to_relevance_override []) val parse_sledgehammer_command = - (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override - -- Scan.option Parse.nat) #>> sledgehammer_trans + (Scan.optional Parse.short_ident runN -- parse_params + -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans val parse_sledgehammer_params_command = parse_params #>> sledgehammer_params_trans diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jun 12 11:12:54 2010 +0200 @@ -41,12 +41,6 @@ fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" fun is_head_digit s = Char.isDigit (String.sub (s, 0)) -(* Hack: Could return false positives (e.g., a user happens to declare a - constant called "SomeTheory.sko_means_shoe_in_$wedish". *) -val is_skolem_const_name = - Long_Name.base_name - #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix - val index_in_shape : int -> int list list -> int = find_index o exists o curry (op =) fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names @@ -263,9 +257,16 @@ fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c -(*The number of type arguments of a constant, zero if it's monomorphic*) +(* The number of type arguments of a constant, zero if it's monomorphic. For + (instances of) Skolem pseudoconstants, this information is encoded in the + constant name. *) fun num_type_args thy s = - length (Sign.const_typargs thy (s, Sign.the_const_type thy s)) + if String.isPrefix skolem_Eps_pseudo_theory s then + s |> unprefix skolem_Eps_pseudo_theory + |> space_explode skolem_infix |> hd + |> space_explode "_" |> List.last |> Int.fromString |> the + else + (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length fun fix_atp_variable_name s = let @@ -323,9 +324,12 @@ else (* Extra args from "hAPP" come after any arguments given directly to the constant. *) - Sign.const_instance thy (c, - map (type_from_node tfrees) - (drop num_term_args us))) + if String.isPrefix skolem_Eps_pseudo_theory c then + map fastype_of ts ---> HOLogic.typeT + else + Sign.const_instance thy (c, + map (type_from_node tfrees) + (drop num_term_args us))) in list_comb (t, ts) end | NONE => (* a free or schematic variable *) let @@ -580,16 +584,29 @@ | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num | extract_num _ = NONE in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end - -fun apply_command _ 1 = "by " - | apply_command 1 _ = "apply " - | apply_command i _ = "prefer " ^ string_of_int i ^ " apply " -fun metis_command i n [] = apply_command i n ^ "metis" - | metis_command i n ss = - apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")" -fun metis_line i n xs = + +val indent_size = 2 +val no_label = ("", ~1) + +val raw_prefix = "X" +val assum_prefix = "A" +val fact_prefix = "F" + +fun string_for_label (s, num) = s ^ string_of_int num + +fun metis_using [] = "" + | metis_using ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " +fun metis_apply _ 1 = "by " + | metis_apply 1 _ = "apply " + | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " +fun metis_itself [] = "metis" + | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")" +fun metis_command i n (ls, ss) = + metis_using ls ^ metis_apply i n ^ metis_itself ss +fun metis_line i n ss = "Try this command: " ^ - Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" + Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n" fun minimize_line _ [] = "" | minimize_line minimize_command facts = case minimize_command facts of @@ -639,15 +656,6 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "X" -val assum_prefix = "A" -val fact_prefix = "F" - -fun string_for_label (s, num) = s ^ string_of_int num - fun add_fact_from_dep thm_names num = if is_axiom_clause_number thm_names num then apsnd (insert (op =) (Vector.sub (thm_names, num - 1))) @@ -948,7 +956,7 @@ let val ls = ls |> sort_distinct (prod_ord string_ord int_ord) val ss = ss |> map unprefix_chained |> sort_distinct string_ord - in metis_command 1 1 (map string_for_label ls @ ss) end + in metis_command 1 1 (ls, ss) end and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Let (t1, t2)) = diff -r fe6262d929a3 -r e6b1a0693f3f src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Jun 11 16:52:17 2010 +0200 +++ b/src/HOL/Tools/meson.ML Sat Jun 12 11:12:54 2010 +0200 @@ -9,7 +9,6 @@ sig val trace: bool Unsynchronized.ref val term_pair_of: indexname * (typ * 'a) -> term * 'a - val first_order_resolve: thm -> thm -> thm val flexflex_first_order: thm -> thm val size_of_subgoals: thm -> int val too_many_clauses: Proof.context option -> term -> bool @@ -98,11 +97,14 @@ let val thy = theory_of_thm thA val tmA = concl_of thA val Const("==>",_) $ tmB $ _ = prop_of thB - val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) + val tenv = + Pattern.first_order_match thy + (pairself Envir.beta_eta_contract (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 - | NONE => raise THM ("first_order_resolve", 0, [thA, thB])); + | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) fun flexflex_first_order th = case (tpairs_of th) of @@ -316,9 +318,11 @@ exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); fun apply_skolem_ths (th, rls) = - let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls) - | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls) - in tryall rls end; + let + fun tryall [] = raise THM ("apply_skolem_ths", 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.