# HG changeset patch # User blanchet # Date 1286209894 -7200 # Node ID 0a2091f86eb469bac87ec60d2c1906bd71af214f # Parent 4ee63a30194cc276f98c1ec84147ee45d3946d63 fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset diff -r 4ee63a30194c -r 0a2091f86eb4 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Oct 04 17:30:34 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Oct 04 18:31:34 2010 +0200 @@ -57,6 +57,23 @@ models = []} val resolution_params = {active = active_params, waiting = waiting_params} +fun instantiate_theorem thy inst th = + let + val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst + val instT = + [] |> Vartab.fold (fn (z, (S, T)) => + cons (TVar (z, S), Type.devar tyenv T)) tyenv + val inst = inst |> map (pairself (subst_atomic_types instT)) + val _ = tracing (cat_lines (map (fn (T, U) => + Syntax.string_of_typ @{context} T ^ " |-> " ^ + Syntax.string_of_typ @{context} U) instT)) + val _ = tracing (cat_lines (map (fn (t, u) => + Syntax.string_of_term @{context} t ^ " |-> " ^ + Syntax.string_of_term @{context} u) inst)) + val cinstT = instT |> map (pairself (ctyp_of thy)) + val cinst = inst |> map (pairself (cterm_of thy)) + in th |> Thm.instantiate (cinstT, cinst) end + (* In principle, it should be sufficient to apply "assume_tac" to unify the conclusion with one of the premises. However, in practice, this is unreliable because of the mildly higher-order nature of the unification problems. @@ -68,19 +85,6 @@ val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract val prem = goal |> Logic.strip_assums_hyp |> hd val concl = goal |> Logic.strip_assums_concl - fun add_types Tp instT = - if exists (curry (op =) Tp) instT then instT - else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT - fun unify_types (T, U) = - if T = U then - I - else case (T, U) of - (TVar _, _) => add_types (T, U) - | (_, TVar _) => add_types (U, T) - | (Type (s, Ts), Type (t, Us)) => - if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us) - else raise TYPE ("unify_types", [T, U], []) - | _ => raise TYPE ("unify_types", [T, U], []) fun pair_untyped_aconv (t1, t2) (u1, u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 fun add_terms tp inst = @@ -111,17 +115,7 @@ | (Var _, _) => add_terms (t, u) | (_, Var _) => add_terms (u, t) | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) - - val inst = [] |> unify_terms (prem, concl) - val _ = trace_msg (fn () => cat_lines (map (fn (t, u) => - Syntax.string_of_term @{context} t ^ " |-> " ^ - Syntax.string_of_term @{context} u) inst)) - val instT = fold (fn Tp => unify_types (pairself fastype_of Tp) - handle TERM _ => I) inst [] - val inst = inst |> map (pairself (subst_atomic_types instT)) - val cinstT = instT |> map (pairself (ctyp_of thy)) - val cinst = inst |> map (pairself (cterm_of thy)) - in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end + in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no) fun shuffle_ord p = @@ -147,7 +141,7 @@ val t' = t |> repair |> fold (curry absdummy) (map snd params) fun do_instantiate th = let val var = Term.add_vars (prop_of th) [] |> the_single in - th |> Thm.instantiate ([], [(cterm_of thy (Var var), cterm_of thy t')]) + th |> instantiate_theorem thy [(Var var, t')] end in etac @{thm allE} i @@ -174,11 +168,12 @@ val n = length cluster_substs fun do_cluster_subst cluster_subst = map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1] - val params' = params (*### existentials! *) + val params' = params (* FIXME ### existentials! *) + val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs in - rotate_tac ax_no + rotate_tac first_prem THEN' (EVERY' (maps do_cluster_subst cluster_substs)) - THEN' rotate_tac (~ ax_no - length cluster_substs) + THEN' rotate_tac (~ first_prem - length cluster_substs) THEN' release_clusters_tac thy ax_counts substs params' clusters end @@ -229,7 +224,8 @@ case prem of _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) => let val ax_no = HOLogic.dest_nat num in - (ax_no, (subgoal_no, match_term (nth axioms ax_no |> snd, t))) + (ax_no, (subgoal_no, + match_term (nth axioms ax_no |> the |> snd, t))) end | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]) @@ -267,7 +263,7 @@ error "Cannot replay Metis proof in Isabelle without axiom of \ \choice." val params0 = - [] |> fold Term.add_vars (map snd axioms) + [] |> fold (Term.add_vars o snd) (map_filter I axioms) |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) |> filter (fn (((_, (cluster_no, _)), skolem), _) => cluster_no = 0 andalso skolem) @@ -278,8 +274,7 @@ Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) (Integer.add 1)) substs |> Int_Tysubst_Table.dest -(* for debugging:### -*) +(* for debugging: fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ @@ -290,21 +285,22 @@ val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0) val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) +*) fun rotation_for_subgoal i = find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs in Goal.prove ctxt [] [] @{prop False} - (K (cut_rules_tac (map (fst o nth axioms o fst o fst) ax_counts) 1 + (K (cut_rules_tac + (map (fst o the o nth axioms o fst o fst) ax_counts) 1 THEN print_tac "cut:" THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) - THEN print_tac "eliminated outermost existentials:" THEN copy_prems_tac (map snd ax_counts) [] 1 + THEN print_tac "eliminated exist and copied prems:" THEN release_clusters_tac thy ax_counts substs params0 ordered_clusters 1 THEN print_tac "released clusters:" THEN match_tac [prems_imp_false] 1 THEN print_tac "applied rule:" - THEN print_tac "unified skolems:" THEN ALLGOALS (fn i => rtac @{thm skolem_COMBK_I} i THEN rotate_tac (rotation_for_subgoal i) i @@ -324,7 +320,7 @@ Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) (0 upto length ths0 - 1) ths0 val thss = map (snd o snd) th_cls_pairs - val dischargers = map_filter (fst o snd) th_cls_pairs + val dischargers = map (fst o snd) th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg (fn () => "THEOREM CLAUSES") @@ -371,7 +367,7 @@ (); case result of (_,ith)::_ => - (tracing(*###*) ("Success: " ^ Display.string_of_thm ctxt ith); + (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) | _ => (trace_msg (fn () => "Metis: No result"); []) end