--- a/src/Pure/Thy/export_theory.ML Wed Aug 14 11:14:27 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML Wed Aug 14 19:21:34 2019 +0200
@@ -44,52 +44,6 @@
in ([], triple int string int (ass, delim, pri)) end];
-(* standardization of variables: only frees and named bounds *)
-
-local
-
-fun declare_names (Abs (_, _, b)) = declare_names b
- | declare_names (t $ u) = declare_names t #> declare_names u
- | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
- | declare_names (Free (x, _)) = Name.declare x
- | declare_names _ = I;
-
-fun variant_abs bs (Abs (x, T, t)) =
- let
- val names = fold Name.declare bs (declare_names t Name.context);
- val x' = #1 (Name.variant x names);
- val t' = variant_abs (x' :: bs) t;
- in Abs (x', T, t') end
- | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
- | variant_abs _ t = t;
-
-in
-
-fun standard_vars used =
- let
- fun zero_var_indexes tm =
- Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm;
-
- fun unvarifyT ty = ty |> Term.map_atyps
- (fn TVar ((a, _), S) => TFree (a, S)
- | T as TFree (a, _) =>
- if Name.is_declared used a then T
- else raise TYPE (Logic.bad_fixed a, [ty], []));
-
- fun unvarify tm = tm |> Term.map_aterms
- (fn Var ((x, _), T) => Free (x, T)
- | t as Free (x, _) =>
- if Name.is_declared used x then t
- else raise TERM (Logic.bad_fixed x, [tm])
- | t => t);
-
- in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end;
-
-val standard_vars_global = standard_vars Name.context;
-
-end;
-
-
(* free variables: not declared in the context *)
val is_free = not oo Name.is_declared;
@@ -253,7 +207,8 @@
val U = Logic.unvarifyT_global T;
val U0 = Type.strip_sorts U;
val recursion = primrec_types thy_ctxt (c, U);
- val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
+ val abbrev' = abbrev
+ |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
@@ -277,7 +232,7 @@
fun encode_prop used (Ss, raw_prop) =
let
- val prop = standard_vars used raw_prop;
+ val prop = Proofterm.standard_vars_term used raw_prop;
val args = rev (add_frees used prop []);
val typargs = rev (add_tfrees used prop []);
val used' = fold (Name.declare o #1) typargs used;
--- a/src/Pure/proofterm.ML Wed Aug 14 11:14:27 2019 +0200
+++ b/src/Pure/proofterm.ML Wed Aug 14 19:21:34 2019 +0200
@@ -162,6 +162,10 @@
val prop_of: proof -> term
val expand_proof: theory -> (string * term option) list -> proof -> proof
+ val standard_vars: Name.context -> term list * proof list -> term list * proof list
+ val standard_vars_term: Name.context -> term -> term
+ val standard_vars_proof: Name.context -> proof -> proof
+
val proof_serial: unit -> proof_serial
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
@@ -1979,6 +1983,82 @@
(** theorems **)
+(* standardization of variables for export: only frees and named bounds *)
+
+local
+
+fun declare_names_term (Abs (_, _, b)) = declare_names_term b
+ | declare_names_term (t $ u) = declare_names_term t #> declare_names_term u
+ | declare_names_term (Const (c, _)) = Name.declare (Long_Name.base_name c)
+ | declare_names_term (Free (x, _)) = Name.declare x
+ | declare_names_term _ = I;
+
+val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
+
+fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf
+ | declare_names_proof (AbsP (_, t, prf)) = declare_names_term' t #> declare_names_proof prf
+ | declare_names_proof (prf % t) = declare_names_proof prf #> declare_names_term' t
+ | declare_names_proof (prf1 %% prf2) = declare_names_proof prf1 #> declare_names_proof prf2
+ | declare_names_proof _ = I;
+
+fun variant names bs x =
+ #1 (Name.variant x (fold Name.declare bs names));
+
+fun variant_term bs (Abs (x, T, t)) =
+ let
+ val x' = variant (declare_names_term t Name.context) bs x;
+ val t' = variant_term (x' :: bs) t;
+ in Abs (x', T, t') end
+ | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
+ | variant_term _ t = t;
+
+fun variant_proof bs (Abst (x, T, prf)) =
+ let
+ val x' = variant (declare_names_proof prf Name.context) bs x;
+ val prf' = variant_proof (x' :: bs) prf;
+ in Abst (x', T, prf') end
+ | variant_proof bs (AbsP (x, t, prf)) =
+ let
+ val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
+ val t' = Option.map (variant_term bs) t;
+ val prf' = variant_proof (x' :: bs) prf;
+ in AbsP (x', t', prf') end
+ | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
+ | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
+ | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
+ | variant_proof _ prf = prf;
+
+in
+
+fun standard_vars used (terms, proofs) =
+ let
+ val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
+ val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
+
+ val is_used = Name.is_declared used o Name.clean;
+ fun unvarifyT ty = ty |> Term.map_atyps
+ (fn TVar ((a, _), S) => TFree (a, S)
+ | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
+ | T => T);
+ fun unvarify tm = tm |> Term.map_aterms
+ (fn Var ((x, _), T) => Free (x, T)
+ | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
+ | t => t);
+
+ val terms' = terms
+ |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
+ val proofs' = proofs
+ |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
+ in (terms', proofs') end;
+
+fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
+fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
+
+end;
+
+
+(* PThm nodes *)
+
val proof_serial = Counter.make ();
local
@@ -2021,9 +2101,18 @@
end;
+val declare_freesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
+fun declare_frees t =
+ fold_types declare_freesT t #>
+ fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t;
+
fun export_proof thy i prop prf =
let
- val xml = reconstruct_proof thy prop prf |> encode_export prop;
+ val free_names = Name.context
+ |> declare_frees prop
+ |> fold_proof_terms declare_frees declare_freesT prf;
+ val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
+ val xml = encode_export prop' prf';
val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
in
chunks |> Export.export_params