# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID b16693484c5d927f9aaf7941b32f5ac80e4ebcf8 # Parent faece9668bce4381d4848239779f4ed64efb3db1 reveal Skolems in new Metis diff -r faece9668bce -r b16693484c5d src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 @@ -556,7 +556,7 @@ (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the formula. *) -fun raw_prop_from_atp ctxt textual sym_tab phi = +fun prop_from_atp ctxt textual sym_tab phi = let fun do_formula pos phi = case phi of @@ -587,9 +587,9 @@ #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) -fun prop_from_atp ctxt textual sym_tab = +fun uncombined_etc_prop_from_atp ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt in - raw_prop_from_atp ctxt textual sym_tab + prop_from_atp ctxt textual sym_tab #> textual ? uncombine_term thy #> infer_formula_types ctxt end @@ -601,12 +601,11 @@ fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt = let val thy = Proof_Context.theory_of ctxt - (* FIXME: prop or term? *) - val t1 = raw_prop_from_atp ctxt true sym_tab phi1 + val t1 = prop_from_atp ctxt true sym_tab phi1 val vars = snd (strip_comb t1) val frees = map unvarify_term vars val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = raw_prop_from_atp ctxt true sym_tab phi2 + val t2 = prop_from_atp ctxt true sym_tab phi2 val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt @@ -616,7 +615,7 @@ fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) end | decode_line sym_tab (Inference (name, u, deps)) ctxt = - let val t = u |> prop_from_atp ctxt true sym_tab in + let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in (Inference (name, t, deps), fold Variable.declare_term (OldTerm.term_frees t) ctxt) end diff -r faece9668bce -r b16693484c5d src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 @@ -18,7 +18,8 @@ val verbose : bool Config.T val verbose_warning : Proof.context -> string -> unit val hol_clause_from_metis : - Proof.context -> int Symtab.table -> Metis_Thm.thm -> term + Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm + -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term * term -> bool val replay_one_inference : @@ -74,7 +75,7 @@ end; fun infer_types ctxt = - Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt); + Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) (* We use 1 rather than 0 because variable references in clauses may otherwise conflict with variable constraints in the goal...at least, type inference @@ -223,7 +224,8 @@ | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, []) fun hol_term_from_metis_MX ctxt sym_tab = - atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE + atp_term_from_metis + #> term_from_atp ctxt false sym_tab NONE fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt @@ -236,19 +238,24 @@ | atp_clause_from_metis lits = lits |> map atp_literal_from_metis |> mk_aconns AOr -fun hol_clause_from_metis ctxt sym_tab = +fun reveal_old_skolems_and_infer_types ctxt old_skolems = + map (reveal_old_skolem_terms old_skolems) + #> infer_types ctxt + +fun hol_clause_from_metis ctxt sym_tab old_skolems = Metis_Thm.clause #> Metis_LiteralSet.toList #> atp_clause_from_metis #> prop_from_atp ctxt false sym_tab + #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems) fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms = let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms val _ = trace_msg ctxt (fn () => " calling type inference:") val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = ts |> map (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt + val ts' = + ts |> reveal_old_skolems_and_infer_types ctxt old_skolems val _ = app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) @@ -308,7 +315,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 "reveal_old_skolem_terms" and "infer_types" below. *) + (* We call "reveal_old_skolems_and_infer_types" below. *) val t = hol_term_from_metis ctxt mode sym_tab y in SOME (cterm_of thy (Var v), t) end handle Option.Option => @@ -327,9 +334,9 @@ | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg ctxt (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 (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt + val (vars, tms) = + ListPair.unzip (map_filter subst_translation substs) + ||> reveal_old_skolems_and_infer_types ctxt old_skolems 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 ctxt (fn () => diff -r faece9668bce -r b16693484c5d src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 @@ -59,9 +59,9 @@ "t => t'", where "t" and "t'" are the same term modulo type tags. In Isabelle, type tags are stripped away, so we are left with "t = t" or "t => t". Type tag idempotence is also handled this way. *) -fun reflexive_or_trivial_from_metis ctxt sym_tab mth = +fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth = let val thy = Proof_Context.theory_of ctxt in - case hol_clause_from_metis ctxt sym_tab mth of + case hol_clause_from_metis ctxt sym_tab old_skolems mth of Const (@{const_name HOL.eq}, _) $ _ $ t => t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq} | Const (@{const_name disj}, _) $ t1 $ t2 => @@ -105,7 +105,7 @@ val (mode, sym_tab, {axioms, old_skolems, ...}) = prepare_metis_problem ctxt mode type_sys cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = - reflexive_or_trivial_from_metis ctxt sym_tab mth + reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")