uniform standard_vars for terms and proof terms;
authorwenzelm
Wed Aug 14 19:21:34 2019 +0200 (2 months ago)
changeset 705292ecbbe6b35db
parent 70528 9b3610fe74d6
child 70530 81a8eba6639c
uniform standard_vars for terms and proof terms;
src/Pure/Thy/export_theory.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Wed Aug 14 11:14:27 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Wed Aug 14 19:21:34 2019 +0200
     1.3 @@ -44,52 +44,6 @@
     1.4        in ([], triple int string int (ass, delim, pri)) end];
     1.5  
     1.6  
     1.7 -(* standardization of variables: only frees and named bounds *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun declare_names (Abs (_, _, b)) = declare_names b
    1.12 -  | declare_names (t $ u) = declare_names t #> declare_names u
    1.13 -  | declare_names (Const (c, _)) = Name.declare (Long_Name.base_name c)
    1.14 -  | declare_names (Free (x, _)) = Name.declare x
    1.15 -  | declare_names _ = I;
    1.16 -
    1.17 -fun variant_abs bs (Abs (x, T, t)) =
    1.18 -      let
    1.19 -        val names = fold Name.declare bs (declare_names t Name.context);
    1.20 -        val x' = #1 (Name.variant x names);
    1.21 -        val t' = variant_abs (x' :: bs) t;
    1.22 -      in Abs (x', T, t') end
    1.23 -  | variant_abs bs (t $ u) = variant_abs bs t $ variant_abs bs u
    1.24 -  | variant_abs _ t = t;
    1.25 -
    1.26 -in
    1.27 -
    1.28 -fun standard_vars used =
    1.29 -  let
    1.30 -    fun zero_var_indexes tm =
    1.31 -      Term_Subst.instantiate (Term_Subst.zero_var_indexes_inst used [tm]) tm;
    1.32 -
    1.33 -    fun unvarifyT ty = ty |> Term.map_atyps
    1.34 -      (fn TVar ((a, _), S) => TFree (a, S)
    1.35 -        | T as TFree (a, _) =>
    1.36 -            if Name.is_declared used a then T
    1.37 -            else raise TYPE (Logic.bad_fixed a, [ty], []));
    1.38 -
    1.39 -    fun unvarify tm = tm |> Term.map_aterms
    1.40 -      (fn Var ((x, _), T) => Free (x, T)
    1.41 -        | t as Free (x, _) =>
    1.42 -            if Name.is_declared used x then t
    1.43 -            else raise TERM (Logic.bad_fixed x, [tm])
    1.44 -        | t => t);
    1.45 -
    1.46 -  in zero_var_indexes #> map_types unvarifyT #> unvarify #> variant_abs [] end;
    1.47 -
    1.48 -val standard_vars_global = standard_vars Name.context;
    1.49 -
    1.50 -end;
    1.51 -
    1.52 -
    1.53  (* free variables: not declared in the context *)
    1.54  
    1.55  val is_free = not oo Name.is_declared;
    1.56 @@ -253,7 +207,8 @@
    1.57          val U = Logic.unvarifyT_global T;
    1.58          val U0 = Type.strip_sorts U;
    1.59          val recursion = primrec_types thy_ctxt (c, U);
    1.60 -        val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
    1.61 +        val abbrev' = abbrev
    1.62 +          |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
    1.63          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
    1.64          val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
    1.65        in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
    1.66 @@ -277,7 +232,7 @@
    1.67  
    1.68      fun encode_prop used (Ss, raw_prop) =
    1.69        let
    1.70 -        val prop = standard_vars used raw_prop;
    1.71 +        val prop = Proofterm.standard_vars_term used raw_prop;
    1.72          val args = rev (add_frees used prop []);
    1.73          val typargs = rev (add_tfrees used prop []);
    1.74          val used' = fold (Name.declare o #1) typargs used;
     2.1 --- a/src/Pure/proofterm.ML	Wed Aug 14 11:14:27 2019 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Wed Aug 14 19:21:34 2019 +0200
     2.3 @@ -162,6 +162,10 @@
     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_term: Name.context -> term -> term
     2.9 +  val standard_vars_proof: Name.context -> proof -> proof
    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    val thm_proof: theory -> (class * class -> proof) ->
    2.14 @@ -1979,6 +1983,82 @@
    2.15  
    2.16  (** theorems **)
    2.17  
    2.18 +(* standardization of variables for export: only frees and named bounds *)
    2.19 +
    2.20 +local
    2.21 +
    2.22 +fun declare_names_term (Abs (_, _, b)) = declare_names_term b
    2.23 +  | declare_names_term (t $ u) = declare_names_term t #> declare_names_term u
    2.24 +  | declare_names_term (Const (c, _)) = Name.declare (Long_Name.base_name c)
    2.25 +  | declare_names_term (Free (x, _)) = Name.declare x
    2.26 +  | declare_names_term _ = I;
    2.27 +
    2.28 +val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
    2.29 +
    2.30 +fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf
    2.31 +  | declare_names_proof (AbsP (_, t, prf)) = declare_names_term' t #> declare_names_proof prf
    2.32 +  | declare_names_proof (prf % t) = declare_names_proof prf #> declare_names_term' t
    2.33 +  | declare_names_proof (prf1 %% prf2) = declare_names_proof prf1 #> declare_names_proof prf2
    2.34 +  | declare_names_proof _ = I;
    2.35 +
    2.36 +fun variant names bs x =
    2.37 +  #1 (Name.variant x (fold Name.declare bs names));
    2.38 +
    2.39 +fun variant_term bs (Abs (x, T, t)) =
    2.40 +      let
    2.41 +        val x' = variant (declare_names_term t Name.context) bs x;
    2.42 +        val t' = variant_term (x' :: bs) t;
    2.43 +      in Abs (x', T, t') end
    2.44 +  | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
    2.45 +  | variant_term _ t = t;
    2.46 +
    2.47 +fun variant_proof bs (Abst (x, T, prf)) =
    2.48 +      let
    2.49 +        val x' = variant (declare_names_proof prf Name.context) bs x;
    2.50 +        val prf' = variant_proof (x' :: bs) prf;
    2.51 +      in Abst (x', T, prf') end
    2.52 +  | variant_proof bs (AbsP (x, t, prf)) =
    2.53 +      let
    2.54 +        val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
    2.55 +        val t' = Option.map (variant_term bs) t;
    2.56 +        val prf' = variant_proof (x' :: bs) prf;
    2.57 +      in AbsP (x', t', prf') end
    2.58 +  | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
    2.59 +  | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
    2.60 +  | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
    2.61 +  | variant_proof _ prf = prf;
    2.62 +
    2.63 +in
    2.64 +
    2.65 +fun standard_vars used (terms, proofs) =
    2.66 +  let
    2.67 +    val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
    2.68 +    val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
    2.69 +
    2.70 +    val is_used = Name.is_declared used o Name.clean;
    2.71 +    fun unvarifyT ty = ty |> Term.map_atyps
    2.72 +      (fn TVar ((a, _), S) => TFree (a, S)
    2.73 +        | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
    2.74 +        | T => T);
    2.75 +    fun unvarify tm = tm |> Term.map_aterms
    2.76 +      (fn Var ((x, _), T) => Free (x, T)
    2.77 +        | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
    2.78 +        | t => t);
    2.79 +
    2.80 +    val terms' = terms
    2.81 +      |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
    2.82 +    val proofs' = proofs
    2.83 +      |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
    2.84 +  in (terms', proofs') end;
    2.85 +
    2.86 +fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
    2.87 +fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
    2.88 +
    2.89 +end;
    2.90 +
    2.91 +
    2.92 +(* PThm nodes *)
    2.93 +
    2.94  val proof_serial = Counter.make ();
    2.95  
    2.96  local
    2.97 @@ -2021,9 +2101,18 @@
    2.98  
    2.99  end;
   2.100  
   2.101 +val declare_freesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   2.102 +fun declare_frees t =
   2.103 +  fold_types declare_freesT t #>
   2.104 +  fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t;
   2.105 +
   2.106  fun export_proof thy i prop prf =
   2.107    let
   2.108 -    val xml = reconstruct_proof thy prop prf |> encode_export prop;
   2.109 +    val free_names = Name.context
   2.110 +      |> declare_frees prop
   2.111 +      |> fold_proof_terms declare_frees declare_freesT prf;
   2.112 +    val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
   2.113 +    val xml = encode_export prop' prf';
   2.114      val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   2.115    in
   2.116      chunks |> Export.export_params