more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
authorwenzelm
Thu Aug 15 19:35:17 2019 +0200 (4 days ago)
changeset 7054004ef5ee3dd4d
parent 70539 30b3c58a1933
child 70541 f3fbc7f3559d
more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
src/Pure/Thy/export_theory.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 18:21:12 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 19:35:17 2019 +0200
     1.3 @@ -223,8 +223,7 @@
     1.4      fun standard_prop used extra_shyps raw_prop raw_proof =
     1.5        let
     1.6          val raw_proofs = the_list raw_proof;
     1.7 -        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
     1.8 -        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
     1.9 +        val ([prop], proofs) = Proofterm.standard_vars used ([raw_prop], raw_proofs);
    1.10  
    1.11          val args = rev (add_frees used prop []);
    1.12          val typargs = rev (add_tfrees used prop []);
     2.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 18:21:12 2019 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 19:35:17 2019 +0200
     2.3 @@ -168,9 +168,6 @@
     2.4    val standard_vars: Name.context -> term list * proof list -> term list * proof list
     2.5    val standard_vars_term: Name.context -> term -> term
     2.6    val standard_vars_proof: Name.context -> proof -> proof
     2.7 -  val used_frees_type: typ -> Name.context -> Name.context
     2.8 -  val used_frees_term: term -> Name.context -> Name.context
     2.9 -  val used_frees_proof: proof -> Name.context -> Name.context
    2.10  
    2.11    val proof_serial: unit -> proof_serial
    2.12    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    2.13 @@ -2046,25 +2043,25 @@
    2.14    | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
    2.15    | variant_proof _ prf = prf;
    2.16  
    2.17 +val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    2.18 +fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    2.19 +val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    2.20 +
    2.21 +val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
    2.22 +val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
    2.23 +
    2.24  in
    2.25  
    2.26  fun standard_vars used (terms, proofs) =
    2.27    let
    2.28 +    val used' = used
    2.29 +      |> fold used_frees_term terms
    2.30 +      |> fold used_frees_proof proofs;
    2.31      val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
    2.32 -    val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
    2.33 -
    2.34 -    val is_used = Name.is_declared used o Name.clean;
    2.35 -    fun unvarifyT ty = ty |> Term.map_atyps
    2.36 -      (fn TVar ((a, _), S) => TFree (a, S)
    2.37 -        | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
    2.38 -        | T => T);
    2.39 -    fun unvarify tm = tm |> Term.map_aterms
    2.40 -      (fn Var ((x, _), T) => Free (x, T)
    2.41 -        | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
    2.42 -        | t => t);
    2.43 +    val inst = Term_Subst.zero_var_indexes_inst used' (terms @ proof_terms);
    2.44  
    2.45      val terms' = terms
    2.46 -      |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
    2.47 +      |> map (Term_Subst.instantiate inst #> unvarify #> variant_term []);
    2.48      val proofs' = proofs
    2.49        |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
    2.50    in (terms', proofs') end;
    2.51 @@ -2074,10 +2071,6 @@
    2.52  
    2.53  end;
    2.54  
    2.55 -val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    2.56 -fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
    2.57 -val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
    2.58 -
    2.59  
    2.60  (* PThm nodes *)
    2.61  
    2.62 @@ -2109,10 +2102,7 @@
    2.63  
    2.64  fun export_proof thy i prop prf =
    2.65    let
    2.66 -    val free_names = Name.context
    2.67 -      |> used_frees_term prop
    2.68 -      |> used_frees_proof prf;
    2.69 -    val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
    2.70 +    val ([prop'], [prf']) = standard_vars Name.context ([prop], [reconstruct_proof thy prop prf]);
    2.71      val xml = encode_export prop' prf';
    2.72      val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
    2.73    in