--- a/src/Doc/Implementation/Logic.thy Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Jul 30 20:09:25 2019 +0200
@@ -1180,8 +1180,8 @@
@{index_ML_type proof_body} \\
@{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
@{index_ML Proofterm.reconstruct_proof:
- "Proof.context -> term -> proof -> proof"} \\
- @{index_ML Proofterm.expand_proof: "Proof.context ->
+ "theory -> term -> proof -> proof"} \\
+ @{index_ML Proofterm.expand_proof: "theory ->
(string * term option) list -> proof -> proof"} \\
@{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
@{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@@ -1213,7 +1213,7 @@
additionally records full proof terms. Officially named theorems that
contribute to a result are recorded in any case.
- \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<open>ctxt prop prf\<close> turns the implicit
+ \<^descr> \<^ML>\<open>Proofterm.reconstruct_proof\<close>~\<open>thy prop prf\<close> turns the implicit
proof term \<open>prf\<close> into a full proof of the given proposition.
Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not
@@ -1221,7 +1221,7 @@
for proofs that are constructed manually, but not for those produced
automatically by the inference kernel.
- \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
+ \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
reconstructs the proofs of all specified theorems, with the given (full)
proof. Theorems that are not unique specified via their name may be
disambiguated by giving their proposition.
--- a/src/HOL/Extraction.thy Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Extraction.thy Tue Jul 30 20:09:25 2019 +0200
@@ -16,14 +16,12 @@
Extraction.add_types
[("bool", ([], NONE))] #>
Extraction.set_preprocessor (fn thy =>
- let val ctxt = Proof_Context.init_global thy in
- Proofterm.rewrite_proof_notypes
- ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
- Proofterm.rewrite_proof thy
- (RewriteHOLProof.rews,
- ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class ctxt]) o
- ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>)
- end)
+ Proofterm.rewrite_proof_notypes
+ ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
+ Proofterm.rewrite_proof thy
+ (RewriteHOLProof.rews,
+ ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
+ ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
\<close>
lemmas [extraction_expand] =
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Tue Jul 30 20:09:25 2019 +0200
@@ -51,7 +51,6 @@
ML_val \<open>
val thy = \<^theory>;
- val ctxt = \<^context>;
val prf =
Proof_Syntax.read_proof thy true false
"impI \<cdot> _ \<cdot> _ \<bullet> \
@@ -59,8 +58,7 @@
\ conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
\ (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
val thm =
- prf
- |> Proofterm.reconstruct_proof ctxt \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close>
+ Proofterm.reconstruct_proof thy \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close> prf
|> Proof_Checker.thm_of_proof thy
|> Drule.export_without_context;
\<close>
--- a/src/HOL/Proofs/ex/XML_Data.thy Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Tue Jul 30 20:09:25 2019 +0200
@@ -12,8 +12,8 @@
subsection \<open>Export and re-import of global proof terms\<close>
ML \<open>
- fun export_proof ctxt thm =
- Proofterm.encode (Thm.clean_proof_of ctxt true thm);
+ fun export_proof thm =
+ Proofterm.encode (Thm.clean_proof_of true thm);
fun import_proof thy xml =
let
@@ -30,24 +30,24 @@
lemma ex: "A \<longrightarrow> A" ..
ML_val \<open>
- val xml = export_proof \<^context> @{thm ex};
+ val xml = export_proof @{thm ex};
val thm = import_proof thy1 xml;
\<close>
ML_val \<open>
- val xml = export_proof \<^context> @{thm de_Morgan};
+ val xml = export_proof @{thm de_Morgan};
val thm = import_proof thy1 xml;
\<close>
ML_val \<open>
- val xml = export_proof \<^context> @{thm Drinker's_Principle};
+ val xml = export_proof @{thm Drinker's_Principle};
val thm = import_proof thy1 xml;
\<close>
text \<open>Some fairly large proof:\<close>
ML_val \<open>
- val xml = export_proof \<^context> @{thm abs_less_iff};
+ val xml = export_proof @{thm abs_less_iff};
val thm = import_proof thy1 xml;
\<^assert> (size (YXML.string_of_body xml) > 1000000);
\<close>
--- a/src/HOL/Tools/datatype_realizer.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Jul 30 20:09:25 2019 +0200
@@ -129,7 +129,6 @@
|> Global_Theory.store_thm
(Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
- val ctxt' = Proof_Context.init_global thy';
val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
@@ -148,7 +147,7 @@
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ Thm.prems_of thm)
(Proofterm.proof_combP
- (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+ (Thm.reconstruct_proof_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -204,7 +203,6 @@
|> Sign.root_path
|> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
- val ctxt' = Proof_Context.init_global thy';
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf =
@@ -214,10 +212,10 @@
(AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
(Proofterm.proof_combP
- (Thm.reconstruct_proof_of ctxt' thm', map PBound (length prems - 1 downto 0))));
+ (Thm.reconstruct_proof_of thm', map PBound (length prems - 1 downto 0))));
val prf' =
Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Thm.reconstruct_proof_of ctxt' exhaust);
+ (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Thm.reconstruct_proof_of exhaust);
val r' =
Logic.varify_global (Abs ("y", T,
(fold_rev (Term.abs o dest_Free) rs
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 30 20:09:25 2019 +0200
@@ -19,9 +19,11 @@
[name] => name
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
-fun prf_of ctxt thm =
- Thm.reconstruct_proof_of ctxt thm
- |> Proofterm.expand_proof ctxt [("", NONE)]; (* FIXME *)
+fun prf_of thy raw_thm =
+ let val thm = Thm.transfer thy raw_thm in
+ Thm.reconstruct_proof_of thm
+ |> Proofterm.expand_proof (Thm.theory_of_thm thm) [("", NONE)]
+ end;
fun subsets [] = [[]]
| subsets (x::xs) =
@@ -257,7 +259,6 @@
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
let
- val ctxt = Proof_Context.init_global thy;
val rvs = map fst (relevant_vars (Thm.prop_of rule));
val xs = rev (Term.add_vars (Thm.prop_of rule) []);
val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
@@ -269,7 +270,7 @@
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
Extraction.abs_corr_shyps thy rule vs vs2
(ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
- (fold_rev Proofterm.forall_intr_proof' rs (prf_of ctxt rrule)))))
+ (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
end;
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
--- a/src/Pure/Isar/isar_cmd.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Jul 30 20:09:25 2019 +0200
@@ -239,12 +239,13 @@
NONE =>
let
val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
+ val thy = Proof_Context.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
in
Proof_Syntax.pretty_proof ctxt
- (if full then Proofterm.reconstruct_proof ctxt prop prf' else prf')
+ (if full then Proofterm.reconstruct_proof thy prop prf' else prf')
end
| SOME srcs =>
let
--- a/src/Pure/Proof/extraction.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jul 30 20:09:25 2019 +0200
@@ -340,7 +340,7 @@
(if T = nullT then t else list_comb (t, vars')) $ prop);
val r = Logic.list_implies (shyps,
fold_rev Logic.all (map (get_var_type r') vars) r');
- val prf = Proofterm.reconstruct_proof ctxt' r (rd s2);
+ val prf = Proofterm.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -483,7 +483,6 @@
fun extract thm_vss thy =
let
val thy' = add_syntax thy;
- val ctxt' = Proof_Context.init_global thy';
val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
ExtractionData.get thy;
@@ -491,8 +490,8 @@
val rtypes = map fst types;
val typroc = typeof_proc [];
val prep = the_default (K I) prep thy' o
- ProofRewriteRules.elim_defs ctxt' false (map (Thm.transfer thy) defs) o
- Proofterm.expand_proof ctxt' (map (rpair NONE) ("" :: expand));
+ ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
+ Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
fun find_inst prop Ts ts vs =
@@ -515,7 +514,7 @@
Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
fun mk_sprfs cs tye = maps (fn (_, T) =>
- ProofRewriteRules.mk_of_sort_proof ctxt' (map SOME cs)
+ ProofRewriteRules.mk_of_sort_proof thy' (map SOME cs)
(T, Sign.defaultS thy)) tye;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
@@ -616,7 +615,7 @@
val _ = msg d ("Building correctness proof for " ^ quote name ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
- val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf);
+ val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
(rev shyps) NONE prf' prf' defs';
val corr_prf = mkabsp shyps corr_prf0;
@@ -640,7 +639,7 @@
| SOME rs => (case find vs' rs of
SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote name ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+ quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
@@ -655,7 +654,7 @@
SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
@@ -708,7 +707,7 @@
val _ = msg d ("Extracting " ^ quote s ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
- val prf' = prep (Proofterm.reconstruct_proof ctxt' prop prf);
+ val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
(rev shyps) (SOME t) prf' prf' defs';
@@ -756,7 +755,7 @@
| SOME rs => (case find vs' rs of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
@@ -768,7 +767,7 @@
case find vs' (Symtab.lookup_list realizers s) of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Syntax.string_of_term ctxt' (Envir.beta_norm
+ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
@@ -783,7 +782,7 @@
val _ = name <> "" orelse error "extraction: unnamed theorem";
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
quote name ^ " has no computational content")
- in Proofterm.reconstruct_proof ctxt' prop prf end;
+ in Proofterm.reconstruct_proof thy' prop prf end;
val defs =
fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 30 20:09:25 2019 +0200
@@ -10,12 +10,12 @@
val rprocs : bool ->
(typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
- val elim_defs : Proof.context -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
+ val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
- val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
- val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
+ val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+ val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
(Proofterm.proof * Proofterm.proof) option
end;
@@ -250,7 +250,7 @@
| (_, []) => (prf, false)
| (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
-fun elim_defs ctxt r defs prf =
+fun elim_defs thy r defs prf =
let
val defs' = map (Logic.dest_equals o
map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
@@ -265,9 +265,9 @@
then I
else cons (name, SOME prop)
| _ => I) [prf] [];
- in Proofterm.expand_proof ctxt thms end;
+ in Proofterm.expand_proof thy thms end;
in
- rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
+ rewrite_terms (Pattern.rewrite_term thy defs' [])
(fst (insert_refl defnames [] (f prf)))
end;
@@ -340,7 +340,7 @@
(**** expand OfClass proofs ****)
-fun mk_of_sort_proof ctxt hs (T, S) =
+fun mk_of_sort_proof thy hs (T, S) =
let
val hs' = map
(fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
@@ -354,19 +354,18 @@
~1 => error "expand_of_class: missing class hypothesis"
| i => PBound i;
fun reconstruct prf prop = prf |>
- Proofterm.reconstruct_proof ctxt prop |>
- Proofterm.expand_proof ctxt [("", NONE)] |>
+ Proofterm.reconstruct_proof thy prop |>
+ Proofterm.expand_proof thy [("", NONE)] |>
Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
in
map2 reconstruct
- (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
- (OfClass o apfst Type.strip_sorts) (subst T, S))
+ (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
(Logic.mk_of_sort (T, S))
end;
-fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
- mk_of_sort_proof ctxt hs (T, [c]) |>
+fun expand_of_class thy Ts hs (OfClass (T, c)) =
+ mk_of_sort_proof thy hs (T, [c]) |>
hd |> rpair Proofterm.no_skel |> SOME
- | expand_of_class ctxt Ts hs _ = NONE;
+ | expand_of_class thy Ts hs _ = NONE;
end;
--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 30 20:09:25 2019 +0200
@@ -11,7 +11,7 @@
val read_term: theory -> bool -> typ -> string -> term
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
val proof_syntax: Proofterm.proof -> theory -> theory
- val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
+ val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -177,9 +177,9 @@
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
end;
-fun proof_of ctxt full raw_thm =
+fun proof_of full thm =
let
- val thm = Thm.transfer' ctxt raw_thm;
+ val thy = Thm.theory_of_thm thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
val prf' =
@@ -187,7 +187,7 @@
(PThm (_, ((_, prop', _, _), body)), _) =>
if prop = prop' then Proofterm.join_proof body else prf
| _ => prf)
- in if full then Proofterm.reconstruct_proof ctxt prop prf' else prf' end;
+ in if full then Proofterm.reconstruct_proof thy prop prf' else prf' end;
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
@@ -195,6 +195,6 @@
(Proofterm.term_of_proof prf);
fun pretty_clean_proof_of ctxt full thm =
- pretty_proof ctxt (Thm.clean_proof_of ctxt full thm);
+ pretty_proof ctxt (Thm.clean_proof_of full thm);
end;
--- a/src/Pure/more_thm.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/more_thm.ML Tue Jul 30 20:09:25 2019 +0200
@@ -114,8 +114,8 @@
val tag: string * string -> attribute
val untag: string -> attribute
val kind: string -> attribute
- val reconstruct_proof_of: Proof.context -> thm -> Proofterm.proof
- val clean_proof_of: Proof.context -> bool -> thm -> Proofterm.proof
+ val reconstruct_proof_of: thm -> Proofterm.proof
+ val clean_proof_of: bool -> thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val show_consts: bool Config.T
@@ -676,21 +676,20 @@
(** proof terms **)
-fun reconstruct_proof_of ctxt raw_thm =
- let val thm = Thm.transfer' ctxt raw_thm
- in Proofterm.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
+fun reconstruct_proof_of thm =
+ Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun clean_proof_of ctxt full raw_thm =
+fun clean_proof_of full thm =
let
- val thm = Thm.transfer' ctxt raw_thm;
+ val thy = Thm.theory_of_thm thm;
val (_, prop) =
Logic.unconstrainT (Thm.shyps_of thm)
(Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
in
Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
- |> Proofterm.reconstruct_proof ctxt prop
- |> Proofterm.expand_proof ctxt [("", NONE)]
- |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
+ |> Proofterm.reconstruct_proof thy prop
+ |> Proofterm.expand_proof thy [("", NONE)]
+ |> Proofterm.rew_proof thy
|> Proofterm.no_thm_proofs
|> not full ? Proofterm.shrink_proof
end;
--- a/src/Pure/proofterm.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/proofterm.ML Tue Jul 30 20:09:25 2019 +0200
@@ -152,10 +152,10 @@
(typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
val rew_proof: theory -> proof -> proof
- val reconstruct_proof: Proof.context -> term -> proof -> proof
+ val reconstruct_proof: theory -> term -> proof -> proof
val prop_of': term list -> proof -> term
val prop_of: proof -> term
- val expand_proof: Proof.context -> (string * term option) list -> proof -> proof
+ val expand_proof: theory -> (string * term option) list -> proof -> proof
val proof_serial: unit -> proof_serial
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -1629,10 +1629,10 @@
val mk_abs = fold (fn T => fn u => Abs ("", T, u));
-fun unifyT ctxt env T U =
+fun unifyT thy env T U =
let
val Envir.Envir {maxidx, tenv, tyenv} = env;
- val (tyenv', maxidx') = Sign.typ_unify (Proof_Context.theory_of ctxt) (T, U) (tyenv, maxidx);
+ val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
fun chaseT env (T as TVar v) =
@@ -1641,9 +1641,9 @@
| SOME T' => chaseT env T')
| chaseT _ T = T;
-fun infer_type ctxt (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
(t as Const (s, T)) = if T = dummyT then
- (case Sign.const_type (Proof_Context.theory_of ctxt) s of
+ (case Sign.const_type thy s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
| SOME T =>
let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
@@ -1659,61 +1659,60 @@
| SOME T => (Free (s, T), T, vTs, env))
else (t, T, vTs, env)
| infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error"
- | infer_type ctxt env Ts vTs (Abs (s, T, t)) =
+ | infer_type thy env Ts vTs (Abs (s, T, t)) =
let
val (T', env') = if T = dummyT then mk_tvar [] env else (T, env);
- val (t', U, vTs', env'') = infer_type ctxt env' (T' :: Ts) vTs t
+ val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t
in (Abs (s, T', t'), T' --> U, vTs', env'') end
- | infer_type ctxt env Ts vTs (t $ u) =
+ | infer_type thy env Ts vTs (t $ u) =
let
- val (t', T, vTs1, env1) = infer_type ctxt env Ts vTs t;
- val (u', U, vTs2, env2) = infer_type ctxt env1 Ts vTs1 u;
+ val (t', T, vTs1, env1) = infer_type thy env Ts vTs t;
+ val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u;
in (case chaseT env2 T of
- Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT ctxt env2 U U')
+ Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
| _ =>
let val (V, env3) = mk_tvar [] env2
- in (t' $ u', V, vTs2, unifyT ctxt env3 T (U --> V)) end)
+ in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
end
| infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
-fun cantunify ctxt (t, u) =
+fun cantunify thy (t, u) =
error ("Non-unifiable terms:\n" ^
- Syntax.string_of_term ctxt t ^ "\n\n" ^ Syntax.string_of_term ctxt u);
+ Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
-fun decompose ctxt Ts (p as (t, u)) env =
+fun decompose thy Ts (p as (t, u)) env =
let
fun rigrig (a, T) (b, U) uT ts us =
- if a <> b then cantunify ctxt p
- else apfst flat (fold_map (decompose ctxt Ts) (ts ~~ us) (uT env T U))
+ if a <> b then cantunify thy p
+ else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
in
case apply2 (strip_comb o Envir.head_norm env) p of
- ((Const c, ts), (Const d, us)) => rigrig c d (unifyT ctxt) ts us
- | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT ctxt) ts us
+ ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
+ | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
| ((Bound i, ts), (Bound j, us)) =>
rigrig (i, dummyT) (j, dummyT) (K o K) ts us
| ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
- decompose ctxt (T::Ts) (t, u) (unifyT ctxt env T U)
+ decompose thy (T::Ts) (t, u) (unifyT thy env T U)
| ((Abs (_, T, t), []), _) =>
- decompose ctxt (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
+ decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
| (_, (Abs (_, T, u), [])) =>
- decompose ctxt (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
+ decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
| _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
end;
-fun make_constraints_cprf ctxt env cprf =
+fun make_constraints_cprf thy env cprf =
let
fun add_cnstrt Ts prop prf cs env vTs (t, u) =
let
val t' = mk_abs Ts t;
val u' = mk_abs Ts u
in
- (prop, prf, cs, Pattern.unify (Context.Proof ctxt) (t', u') env, vTs)
- handle Pattern.Pattern =>
- let val (cs', env') = decompose ctxt [] (t', u') env
+ (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
+ handle Pattern.Pattern =>
+ let val (cs', env') = decompose thy [] (t', u') env
in (prop, prf, cs @ cs', env', vTs) end
- | Pattern.Unif =>
- cantunify ctxt (Envir.norm_term env t', Envir.norm_term env u')
+ | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u')
end;
fun mk_cnstrts_atom env vTs prop opTs prf =
@@ -1748,7 +1747,7 @@
end
| mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
let
- val (t', _, vTs', env') = infer_type ctxt env Ts vTs t;
+ val (t', _, vTs', env') = infer_type thy env Ts vTs t;
val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf;
in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'')
end
@@ -1771,11 +1770,11 @@
end)
end
| mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
- let val (t', U, vTs1, env1) = infer_type ctxt env Ts vTs t
+ let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
(Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
prf, cnstrts, env2, vTs2) =>
- let val env3 = unifyT ctxt env2 T U
+ let val env3 = unifyT thy env2 T U
in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
end
| (u, prf, cnstrts, env2, vTs2) =>
@@ -1838,11 +1837,13 @@
(* solution of constraints *)
fun solve _ [] bigenv = bigenv
- | solve ctxt cs bigenv =
+ | solve thy cs bigenv =
let
- fun search _ [] = error ("Unsolvable constraints:\n" ^
- Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Syntax.pretty_flexpair ctxt (apply2 (Envir.norm_term bigenv) p)) cs)))
+ fun search _ [] =
+ error ("Unsolvable constraints:\n" ^
+ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
+ Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
+ (apply2 (Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
let
@@ -1850,10 +1851,10 @@
val tn2 = Envir.norm_term bigenv t2
in
if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
- (Pattern.unify (Context.Proof ctxt) (tn1, tn2) env, ps) handle Pattern.Unif =>
- cantunify ctxt (tn1, tn2)
+ (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps)
+ handle Pattern.Unif => cantunify thy (tn1, tn2)
else
- let val (cs', env') = decompose ctxt [] (tn1, tn2) env
+ let val (cs', env') = decompose thy [] (tn1, tn2) env
in if cs' = [(tn1, tn2)] then
apsnd (cons (false, (tn1, tn2), vs)) (search env ps)
else search env' (map (fn q => (true, q, vs)) cs' @ ps)
@@ -1863,7 +1864,7 @@
val Envir.Envir {maxidx, ...} = bigenv;
val (env, cs') = search (Envir.empty maxidx) cs;
in
- solve ctxt (upd_constrs env cs') (Envir.merge (bigenv, env))
+ solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
end;
in
@@ -1871,18 +1872,16 @@
(* reconstruction of proofs *)
-fun reconstruct_proof ctxt prop cprf =
+fun reconstruct_proof thy prop cprf =
let
val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
- val (t, prf, cs, env, _) = make_constraints_cprf ctxt
+ val (t, prf, cs, env, _) = make_constraints_cprf thy
(Envir.empty (maxidx_proof cprf ~1)) cprf';
val cs' =
map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
|> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
- val env' = solve ctxt cs' env
- in
- thawf (norm_proof env' prf)
- end;
+ val env' = solve thy cs' env
+ in thawf (norm_proof env' prf) end;
fun prop_of_atom prop Ts = subst_atomic_types
(map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
@@ -1914,7 +1913,7 @@
(* expand and reconstruct subproofs *)
-fun expand_proof ctxt thms prf =
+fun expand_proof thy thms prf =
let
fun expand maxidx prfs (AbsP (s, t, prf)) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
@@ -1943,7 +1942,7 @@
val prf' =
join_proof body
|> open_proof
- |> reconstruct_proof ctxt prop
+ |> reconstruct_proof thy prop
|> forall_intr_vfs_prf prop;
val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
in
@@ -2020,10 +2019,9 @@
fun export thy i prop proof =
if Options.default_bool "export_proofs" then
let
- val thy_ctxt = Proof_Context.init_global thy;
val xml =
- reconstruct_proof thy_ctxt prop proof
- |> expand_proof thy_ctxt [("", NONE)]
+ reconstruct_proof thy prop proof
+ |> expand_proof thy [("", NONE)]
|> term_of_proof
|> Term_XML.Encode.term;
in