more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
authorwenzelm
Thu Aug 15 21:18:06 2019 +0200 (4 weeks ago)
changeset 70541f3fbc7f3559d
parent 70540 04ef5ee3dd4d
child 70542 011196c029e1
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
src/Pure/Thy/export_theory.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 19:35:17 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 21:18:06 2019 +0200
     1.3 @@ -222,14 +222,12 @@
     1.4  
     1.5      fun standard_prop used extra_shyps raw_prop raw_proof =
     1.6        let
     1.7 -        val raw_proofs = the_list raw_proof;
     1.8 -        val ([prop], proofs) = Proofterm.standard_vars used ([raw_prop], raw_proofs);
     1.9 -
    1.10 +        val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
    1.11          val args = rev (add_frees used prop []);
    1.12          val typargs = rev (add_tfrees used prop []);
    1.13          val used_typargs = fold (Name.declare o #1) typargs used;
    1.14          val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
    1.15 -      in ((sorts @ typargs, args, prop), try hd proofs) end;
    1.16 +      in ((sorts @ typargs, args, prop), proof) end;
    1.17  
    1.18      val encode_prop =
    1.19        let open XML.Encode Term_XML.Encode
     2.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 19:35:17 2019 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 21:18:06 2019 +0200
     2.3 @@ -165,9 +165,8 @@
     2.4    val prop_of: proof -> term
     2.5    val expand_proof: theory -> (string * term option) list -> proof -> proof
     2.6  
     2.7 -  val standard_vars: Name.context -> term list * proof list -> term list * proof list
     2.8 +  val standard_vars: Name.context -> term * proof option -> term * proof option
     2.9    val standard_vars_term: Name.context -> term -> term
    2.10 -  val standard_vars_proof: Name.context -> proof -> proof
    2.11  
    2.12    val proof_serial: unit -> proof_serial
    2.13    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    2.14 @@ -2049,25 +2048,37 @@
    2.15  
    2.16  val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
    2.17  val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
    2.18 +val unvarify_proof = map_proof_terms unvarify unvarifyT;
    2.19 +
    2.20 +fun hidden_types prop proof =
    2.21 +  let
    2.22 +    val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
    2.23 +    val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
    2.24 +  in rev (fold_proof_terms (fold_types add_hiddenT) add_hiddenT proof []) end;
    2.25 +
    2.26 +fun standard_hidden_types term proof =
    2.27 +  let
    2.28 +    val hidden = hidden_types term proof;
    2.29 +    val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
    2.30 +    fun smash T = if member (op =) hidden T then TVar (("'", idx), Type.sort_of_atyp T) else T;
    2.31 +    val smashT = map_atyps smash;
    2.32 +  in map_proof_terms (map_types smashT) smashT proof end;
    2.33  
    2.34  in
    2.35  
    2.36 -fun standard_vars used (terms, proofs) =
    2.37 +fun standard_vars used (term, opt_proof) =
    2.38    let
    2.39 -    val used' = used
    2.40 -      |> fold used_frees_term terms
    2.41 +    val proofs = the_list (Option.map (standard_hidden_types term) opt_proof);
    2.42 +    val proof_terms = rev (fold (fold_proof_terms cons (cons o Logic.mk_type)) proofs []);
    2.43 +    val used_frees = used
    2.44 +      |> used_frees_term term
    2.45        |> fold used_frees_proof proofs;
    2.46 -    val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
    2.47 -    val inst = Term_Subst.zero_var_indexes_inst used' (terms @ proof_terms);
    2.48 +    val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
    2.49 +    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
    2.50 +    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
    2.51 +  in (term', try hd proofs') end;
    2.52  
    2.53 -    val terms' = terms
    2.54 -      |> map (Term_Subst.instantiate inst #> unvarify #> variant_term []);
    2.55 -    val proofs' = proofs
    2.56 -      |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
    2.57 -  in (terms', proofs') end;
    2.58 -
    2.59 -fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
    2.60 -fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
    2.61 +fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
    2.62  
    2.63  end;
    2.64  
    2.65 @@ -2102,7 +2113,8 @@
    2.66  
    2.67  fun export_proof thy i prop prf =
    2.68    let
    2.69 -    val ([prop'], [prf']) = standard_vars Name.context ([prop], [reconstruct_proof thy prop prf]);
    2.70 +    val (prop', SOME prf') =
    2.71 +      standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
    2.72      val xml = encode_export prop' prf';
    2.73      val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
    2.74    in