# HG changeset patch # User wenzelm # Date 1565600681 -7200 # Node ID 1881fb38a1ef8c53d7c5ead4c33d83ff8c1d1bef # Parent f0b2635ee17f7023272df21968013bc9b4274f89 misc tuning -- slightly more readable; diff -r f0b2635ee17f -r 1881fb38a1ef src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Aug 11 22:36:34 2019 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Aug 12 11:04:41 2019 +0200 @@ -41,11 +41,10 @@ | _ => (s, false)) fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) = - let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in - ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) - end + let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) + in ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) end | atp_term_of_metis _ (Metis_Term.Var s) = - ATerm ((Metis_Name.toString s, []), []) + ATerm ((Metis_Name.toString s, []), []) fun hol_term_of_metis ctxt type_enc sym_tab = atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE @@ -80,9 +79,9 @@ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' in ts' end -(* ------------------------------------------------------------------------- *) -(* FOL step Inference Rules *) -(* ------------------------------------------------------------------------- *) + + +(** FOL step Inference Rules **) fun lookth th_pairs fth = the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) @@ -91,23 +90,21 @@ fun cterm_incr_types ctxt idx = Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx) + (* INFERENCE RULE: AXIOM *) -(* This causes variables to have an index of 1 by default. See also - "term_of_atp" in "ATP_Proof_Reconstruct". *) +(*This causes variables to have an index of 1 by default. See also + "term_of_atp" in "ATP_Proof_Reconstruct".*) val axiom_inference = Thm.incr_indexes 1 oo lookth + (* INFERENCE RULE: ASSUME *) val EXCLUDED_MIDDLE = @{lemma "P \ \ P \ False" by (rule notE)} fun inst_excluded_middle ctxt i_atom = - let - val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (Thm.prop_of th) [] - in - infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] th - end + let val [vx] = Term.add_vars (Thm.prop_of EXCLUDED_MIDDLE) [] + in infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] EXCLUDED_MIDDLE end fun assume_inference ctxt type_enc concealed sym_tab atom = inst_excluded_middle ctxt @@ -127,7 +124,7 @@ fun subst_translation (x,y) = let val v = find_var x - (* We call "polish_hol_terms" below. *) + (*We call "polish_hol_terms" below.*) val t = hol_term_of_metis ctxt type_enc sym_tab y in SOME (Thm.cterm_of ctxt (Var v), t) @@ -146,8 +143,8 @@ SOME b => SOME (b, t) | NONE => (case unprefix_and_unascii tvar_prefix a of - SOME _ => NONE (* type instantiations are forbidden *) - | NONE => SOME (a, t) (* internal Metis var? *))) + SOME _ => NONE (*type instantiations are forbidden*) + | NONE => SOME (a, t) (*internal Metis var?*))) end val _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) @@ -167,6 +164,7 @@ handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) + (* INFERENCE RULE: RESOLVE *) (*Increment the indexes of only the type variables*) @@ -178,9 +176,9 @@ Thm.instantiate (map inc_tvar tvs, []) th end -(* Like RSN, but we rename apart only the type variables. Vars here typically - have an index of 1, and the use of RSN would increase this typically to 3. - Instantiations of those Vars could then fail. *) +(*Like RSN, but we rename apart only the type variables. Vars here typically + have an index of 1, and the use of RSN would increase this typically to 3. + Instantiations of those Vars could then fail.*) fun resolve_inc_tyvars ctxt tha i thb = let val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha @@ -212,11 +210,11 @@ |> Envir.type_env |> Vartab.dest |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)) in - (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify - "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as - first argument). We then perform unification of the types of variables by hand and try - again. We could do this the first time around but this error occurs seldom and we don't - want to break existing proofs in subtle ways or slow them down. *) + (*The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify + "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as + first argument). We then perform unification of the types of variables by hand and try + again. We could do this the first time around but this error occurs seldom and we don't + want to break existing proofs in subtle ways or slow them down.*) if null ps then raise TERM z else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb)) end @@ -230,8 +228,8 @@ val normalize_literal = simp_not_not o Envir.eta_contract -(* Find the relative location of an untyped term within a list of terms as a - 1-based index. Returns 0 in case of failure. *) +(*Find the relative location of an untyped term within a list of terms as a + 1-based index. Returns 0 in case of failure.*) fun index_of_literal lit haystack = let fun match_lit normalize = @@ -243,18 +241,18 @@ | j => j) + 1 end -(* Permute a rule's premises to move the i-th premise to the last position. *) +(*Permute a rule's premises to move the i-th premise to the last position.*) fun make_last i th = let val n = Thm.nprems_of th in if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th else raise THM ("select_literal", i, [th]) end -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding - to create double negations. The "select" wrapper is a trick to ensure that - "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We - don't use this trick in general because it makes the proof object uglier than - necessary. FIXME. *) +(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding + to create double negations. The "select" wrapper is a trick to ensure that + "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We + don't use this trick in general because it makes the proof object uglier than + necessary. FIXME.*) fun negate_head ctxt th = if exists (fn t => t aconv \<^prop>\\ False\) (Thm.prems_of th) then (th RS @{thm select_FalseI}) @@ -296,6 +294,7 @@ end end + (* INFERENCE RULE: REFL *) val REFL_THM = Thm.incr_indexes 2 @{lemma "t \ t \ False" by (drule notE) (rule refl)} @@ -310,27 +309,28 @@ val c_t = cterm_incr_types ctxt refl_idx i_t in infer_instantiate_types ctxt [(refl_x, c_t)] REFL_THM end + (* INFERENCE RULE: EQUALITY *) val subst_em = @{lemma "s = t \ P s \ \ P t \ False" by (erule notE) (erule subst)} val ssubst_em = @{lemma "s = t \ P t \ \ P s \ False" by (erule notE) (erule ssubst)} fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = - let val thy = Proof_Context.theory_of ctxt - val m_tm = Metis_Term.Fn atom - val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr] - val _ = trace_msg ctxt (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 - fun path_finder_fail tm ps t = - raise METIS_RECONSTRUCT ("equality_inference (path_finder)", - "path = " ^ space_implode " " (map string_of_int ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - (case t of - SOME t => " fol-term: " ^ Metis_Term.toString t - | NONE => "")) - fun path_finder tm [] _ = (tm, Bound 0) - | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = + let + val m_tm = Metis_Term.Fn atom + val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr] + val _ = trace_msg ctxt (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 + fun path_finder_fail tm ps t = + raise METIS_RECONSTRUCT ("equality_inference (path_finder)", + "path = " ^ space_implode " " (map string_of_int ps) ^ + " isa-term: " ^ Syntax.string_of_term ctxt tm ^ + (case t of + SOME t => " fol-term: " ^ Metis_Term.toString t + | NONE => "")) + fun path_finder tm [] _ = (tm, Bound 0) + | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = let val s = s |> Metis_Name.toString |> perhaps (try (unprefix_and_unascii const_prefix @@ -361,18 +361,18 @@ val (r, t) = path_finder tm_p ps (nth ts p) in (r, list_comb (tm1, replace_item_list t p' args)) end end - | path_finder tm ps t = path_finder_fail tm ps (SOME t) - val (tm_subst, body) = path_finder i_atom fp m_tm - val tm_abs = Abs ("x", type_of tm_subst, body) - val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) - val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) - val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst') - val eq_terms = - map (apply2 (Thm.cterm_of ctxt)) - (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) + | path_finder tm ps t = path_finder_fail tm ps (SOME t) + val (tm_subst, body) = path_finder i_atom fp m_tm + val tm_abs = Abs ("x", type_of tm_subst, body) + val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) + val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) + val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) + val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) + val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) + val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst') + val eq_terms = + map (apply2 (Thm.cterm_of ctxt)) + (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) in infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst' end @@ -384,12 +384,12 @@ (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor + inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => - resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor + resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r) + equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r) fun flexflex_first_order ctxt th = (case Thm.tpairs_of th of @@ -398,10 +398,10 @@ let val thy = Proof_Context.theory_of ctxt val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - + fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T) fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t) - + val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] in @@ -416,10 +416,10 @@ fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 -(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate - disjuncts are impossible. In the Isabelle proof, in spite of efforts to - eliminate them, duplicates sometimes appear with slightly different (but - unifiable) types. *) +(*Seldomly needed hack. A Metis clause is represented as a set, so duplicate + disjuncts are impossible. In the Isabelle proof, in spite of efforts to + eliminate them, duplicates sometimes appear with slightly different (but + unifiable) types.*) fun resynchronize ctxt fol_th th = let val num_metis_lits = @@ -447,12 +447,11 @@ end end -fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) - th_pairs = +fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) th_pairs = if not (null th_pairs) andalso Thm.prop_of (snd (hd th_pairs)) aconv \<^prop>\False\ then - (* Isabelle sometimes identifies literals (premises) that are distinct in - Metis (e.g., because of type variables). We give the Isabelle proof the - benefice of the doubt. *) + (*Isabelle sometimes identifies literals (premises) that are distinct in + Metis (e.g., because of type variables). We give the Isabelle proof the + benefice of the doubt.*) th_pairs else let @@ -468,12 +467,12 @@ (fol_th, th) :: th_pairs end -(* It is normally sufficient to apply "assume_tac" to unify the conclusion with - one of the premises. Unfortunately, this sometimes yields "Variable - has two distinct types" errors. To avoid this, we instantiate the - variables before applying "assume_tac". Typical constraints are of the form - ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \\<^sup>? SK_a_b_c_x, - where the nonvariables are goal parameters. *) +(*It is normally sufficient to apply "assume_tac" to unify the conclusion with + one of the premises. Unfortunately, this sometimes yields "Variable + has two distinct types" errors. To avoid this, we instantiate the + variables before applying "assume_tac". Typical constraints are of the form + ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z \\<^sup>? SK_a_b_c_x, + where the nonvariables are goal parameters.*) fun unify_first_prem_with_concl ctxt i th = let val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract @@ -523,15 +522,15 @@ infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th end -val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by assumption} +val copy_prem = @{lemma "P \ (P \ P \ Q) \ Q" by assumption} fun copy_prems_tac ctxt [] ns i = - if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i + if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i | copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i | copy_prems_tac ctxt (m :: ms) ns i = - eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i + eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i -(* Metis generates variables of the form _nnn. *) +(*Metis generates variables of the form _nnn.*) val is_metis_fresh_variable = String.isPrefix "_" fun instantiate_forall_tac ctxt t i st = @@ -539,16 +538,16 @@ val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev fun repair (t as (Var ((s, _), _))) = - (case find_index (fn (s', _) => s' = s) params of - ~1 => t - | j => Bound j) + (case find_index (fn (s', _) => s' = s) params of + ~1 => t + | j => Bound j) | repair (t $ u) = - (case (repair t, repair u) of - (t as Bound j, u as Bound k) => - (* This is a trick to repair the discrepancy between the fully skolemized term that MESON - gives us (where existentials were pulled out) and the reality. *) - if k > j then t else t $ u - | (t, u) => t $ u) + (case (repair t, repair u) of + (t as Bound j, u as Bound k) => + (*This is a trick to repair the discrepancy between the fully skolemized term that MESON + gives us (where existentials were pulled out) and the reality.*) + if k > j then t else t $ u + | (t, u) => t $ u) | repair t = t val t' = t |> repair |> fold (absdummy o snd) params @@ -618,23 +617,26 @@ val tysubst_ord = list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) -structure Int_Tysubst_Table = - Table(type key = int * (indexname * (sort * typ)) list - val ord = prod_ord int_ord tysubst_ord) +structure Int_Tysubst_Table = Table +( + type key = int * (indexname * (sort * typ)) list + val ord = prod_ord int_ord tysubst_ord +) -structure Int_Pair_Graph = - Graph(type key = int * int val ord = prod_ord int_ord int_ord) +structure Int_Pair_Graph = Graph( + type key = int * int + val ord = prod_ord int_ord int_ord +) fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p) -(* Attempts to derive the theorem "False" from a theorem of the form - "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the - specified axioms. The axioms have leading "All" and "Ex" quantifiers, which - must be eliminated first. *) +(*Attempts to derive the theorem "False" from a theorem of the form + "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the + specified axioms. The axioms have leading "All" and "Ex" quantifiers, which + must be eliminated first.*) fun discharge_skolem_premises ctxt axioms prems_imp_false = - if Thm.prop_of prems_imp_false aconv \<^prop>\False\ then - prems_imp_false + if Thm.prop_of prems_imp_false aconv \<^prop>\False\ then prems_imp_false else let val thy = Proof_Context.theory_of ctxt