diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Mar 04 19:53:18 2015 +0100 @@ -88,7 +88,7 @@ the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)) +fun cterm_incr_types thy idx = Thm.cterm_of thy o map_types (Logic.incr_tvar idx) (* INFERENCE RULE: AXIOM *) @@ -103,8 +103,8 @@ fun inst_excluded_middle thy i_atom = let val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (prop_of th) [] - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] + val [vx] = Term.add_vars (Thm.prop_of th) [] + val substs = [(Thm.cterm_of thy (Var vx), Thm.cterm_of thy i_atom)] in cterm_instantiate substs th end @@ -122,7 +122,7 @@ let val thy = Proof_Context.theory_of ctxt val i_th = lookth th_pairs th - val i_th_vars = Term.add_vars (prop_of i_th) [] + val i_th_vars = Term.add_vars (Thm.prop_of i_th) [] fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) fun subst_translation (x,y) = @@ -131,7 +131,7 @@ (* We call "polish_hol_terms" below. *) val t = hol_term_of_metis ctxt type_enc sym_tab y in - SOME (cterm_of thy (Var v), t) + SOME (Thm.cterm_of thy (Var v), t) end handle Option.Option => (trace_msg ctxt (fn () => @@ -160,8 +160,8 @@ val _ = trace_msg ctxt (fn () => cat_lines ("subst_translations:" :: (substs' |> map (fn (x, y) => - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ - Syntax.string_of_term ctxt (term_of y))))) + Syntax.string_of_term ctxt (Thm.term_of x) ^ " |-> " ^ + Syntax.string_of_term ctxt (Thm.term_of y))))) in cterm_instantiate substs' i_th end @@ -175,7 +175,7 @@ let val tvs = Term.add_tvars (Thm.full_prop_of th) [] val thy = Thm.theory_of_thm th - fun inc_tvar ((a, i), s) = apply2 (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) + fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) in Thm.instantiate (map inc_tvar tvs, []) th end @@ -188,7 +188,7 @@ val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha fun res (tha, thb) = (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} - (false, tha, nprems_of tha) i thb + (false, tha, Thm.nprems_of tha) i thb |> Seq.list_of |> distinct Thm.eq_thm of [th] => th | _ => @@ -207,13 +207,13 @@ let val thy = Proof_Context.theory_of ctxt val ps = [] - |> fold (Term.add_vars o prop_of) [tha, thb] + |> fold (Term.add_vars o Thm.prop_of) [tha, thb] |> AList.group (op =) |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts) |> rpair (Envir.empty ~1) |-> fold (Pattern.unify (Context.Proof ctxt)) |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => apply2 (ctyp_of thy) (TVar (x, S), T)) + |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of thy) (TVar (x, S), 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 @@ -248,7 +248,7 @@ (* Permute a rule's premises to move the i-th premise to the last position. *) fun make_last i th = - let val n = nprems_of th in + 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 @@ -259,7 +259,7 @@ 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"}) (prems_of th) then + if exists (fn t => t aconv @{prop "~ False"}) (Thm.prems_of th) then (th RS @{thm select_FalseI}) |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select} else @@ -286,11 +286,11 @@ singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) in - (case index_of_literal (s_not i_atom) (prems_of i_th1) of + (case index_of_literal (s_not i_atom) (Thm.prems_of i_th1) of 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1) | j1 => (trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1); - (case index_of_literal i_atom (prems_of i_th2) of + (case index_of_literal i_atom (Thm.prems_of i_th2) of 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2) | j2 => (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2); @@ -303,7 +303,7 @@ val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); +val refl_x = Thm.cterm_of @{theory} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; fun refl_inference ctxt type_enc concealed sym_tab t = @@ -374,8 +374,8 @@ 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' " ^ Display.string_of_thm ctxt subst') - val eq_terms = map (apply2 (cterm_of thy)) - (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + val eq_terms = map (apply2 (Thm.cterm_of thy)) + (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end @@ -399,9 +399,9 @@ [] => th | pairs => let - val thy = theory_of_thm th - val cert = cterm_of thy - val certT = ctyp_of thy + val thy = Thm.theory_of_thm th + val cert = Thm.cterm_of thy + val certT = Thm.ctyp_of thy val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T) @@ -429,13 +429,13 @@ let val num_metis_lits = count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)) - val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th) + val num_isabelle_lits = count is_isabelle_literal_genuine (Thm.prems_of th) in if num_metis_lits >= num_isabelle_lits then th else let - val (prems0, concl) = th |> prop_of |> Logic.strip_horn + val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped val goal = Logic.list_implies (prems, concl) val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt @@ -454,7 +454,7 @@ fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) th_pairs = - if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then + 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. *) @@ -481,7 +481,7 @@ where the nonvariables are goal parameters. *) fun unify_first_prem_with_concl thy i th = let - val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract + val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract val prem = goal |> Logic.strip_assums_hyp |> hd val concl = goal |> Logic.strip_assums_concl @@ -522,7 +522,7 @@ | _ => I) val t_inst = - [] |> try (unify_terms (prem, concl) #> map (apply2 (cterm_of thy))) + [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of thy))) |> the_default [] (* FIXME *) in cterm_instantiate t_inst th @@ -543,7 +543,7 @@ let val thy = Proof_Context.theory_of ctxt - val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev + 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 @@ -561,7 +561,7 @@ val t' = t |> repair |> fold (absdummy o snd) params fun do_instantiate th = - (case Term.add_vars (prop_of th) [] + (case Term.add_vars (Thm.prop_of th) [] |> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst o fst) of [] => th @@ -576,8 +576,9 @@ Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, tenv = Vartab.empty, tyenv = tyenv} val ty_inst = - Vartab.fold (fn (x, (S, T)) => cons (apply2 (ctyp_of thy) (TVar (x, S), T))) tyenv [] - val t_inst = [apply2 (cterm_of thy o Envir.norm_term env) (Var var, t')] + Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of thy) (TVar (x, S), T))) + tyenv [] + val t_inst = [apply2 (Thm.cterm_of thy o Envir.norm_term env) (Var var, t')] in Drule.instantiate_normalize (ty_inst, t_inst) th end @@ -639,7 +640,7 @@ 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 prop_of prems_imp_false aconv @{prop False} then + if Thm.prop_of prems_imp_false aconv @{prop False} then prems_imp_false else let @@ -685,7 +686,7 @@ clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])) - val prems = Logic.strip_imp_prems (prop_of prems_imp_false) + val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false) val substs = prems |> map2 subst_info_of_prem (1 upto length prems) |> sort (int_ord o apply2 fst) val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs