src/Pure/Isar/proof_context.ML
changeset 19270 d928b5468c43
parent 19143 a64fef2d7073
child 19274 b85e16bd70d0
equal deleted inserted replaced
19269:620616bc7632 19270:d928b5468c43
    68   val read_tyname: context -> string -> typ
    68   val read_tyname: context -> string -> typ
    69   val read_const: context -> string -> term
    69   val read_const: context -> string -> term
    70   val rename_frees: context -> term list -> (string * 'a) list -> (string * 'a) list
    70   val rename_frees: context -> term list -> (string * 'a) list -> (string * 'a) list
    71   val warn_extra_tfrees: context -> context -> context
    71   val warn_extra_tfrees: context -> context -> context
    72   val generalize: context -> context -> term list -> term list
    72   val generalize: context -> context -> term list -> term list
       
    73   val monomorphic: context -> term list -> term list
    73   val polymorphic: context -> term list -> term list
    74   val polymorphic: context -> term list -> term list
       
    75   val hidden_polymorphism: term -> typ -> (indexname * sort) list
    74   val export_standard: context -> context -> thm -> thm
    76   val export_standard: context -> context -> thm -> thm
    75   val exports: context -> context -> thm -> thm Seq.seq
    77   val exports: context -> context -> thm -> thm Seq.seq
    76   val goal_exports: context -> context -> thm -> thm Seq.seq
    78   val goal_exports: context -> context -> thm -> thm Seq.seq
    77   val drop_schematic: indexname * term option -> indexname * term option
    79   val drop_schematic: indexname * term option -> indexname * term option
    78   val add_binds: (indexname * string option) list -> context -> context
    80   val add_binds: (indexname * string option) list -> context -> context
   718   in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
   720   in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
   719 
   721 
   720 
   722 
   721 (* polymorphic terms *)
   723 (* polymorphic terms *)
   722 
   724 
       
   725 fun monomorphic ctxt ts =
       
   726   let
       
   727     val tvars = fold Term.add_tvars ts [];
       
   728     val tfrees = map TFree (rename_frees ctxt ts (map (apfst fst) tvars));
       
   729     val specialize = Term.instantiate ((tvars ~~ tfrees), []);
       
   730   in map specialize ts end;
       
   731 
   723 fun polymorphic ctxt ts =
   732 fun polymorphic ctxt ts =
   724   generalize (ctxt |> fold declare_term ts) ctxt ts;
   733   generalize (ctxt |> fold declare_term ts) ctxt ts;
   725 
   734 
   726 fun extra_tvars t T =
   735 fun hidden_polymorphism t T =
   727   let val tvarsT = Term.add_tvarsT T [] in
   736   let
   728     Term.fold_types (Term.fold_atyps
   737     val tvarsT = Term.add_tvarsT T [];
   729       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t []
   738     val extra_tvars = Term.fold_types (Term.fold_atyps
   730   end;
   739       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
       
   740   in extra_tvars end;
   731 
   741 
   732 
   742 
   733 
   743 
   734 (** export theorems **)
   744 (** export theorems **)
   735 
   745 
   779 
   789 
   780 fun upd_bind ((x, i), t) =
   790 fun upd_bind ((x, i), t) =
   781   let
   791   let
   782     val T = Term.fastype_of t;
   792     val T = Term.fastype_of t;
   783     val t' =
   793     val t' =
   784       if null (extra_tvars t T) then t
   794       if null (hidden_polymorphism t T) then t
   785       else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   795       else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   786   in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
   796   in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
   787 
   797 
   788 fun del_upd_bind (xi, NONE) = del_bind xi
   798 fun del_upd_bind (xi, NONE) = del_bind xi
   789   | del_upd_bind (xi, SOME t) = upd_bind (xi, t);
   799   | del_upd_bind (xi, SOME t) = upd_bind (xi, t);
  1086     val thy = theory_of ctxt and naming = naming_of ctxt;
  1096     val thy = theory_of ctxt and naming = naming_of ctxt;
  1087     val ([(c, _, mx)], _) = prep_vars [(raw_c, NONE, raw_mx)] ctxt;
  1097     val ([(c, _, mx)], _) = prep_vars [(raw_c, NONE, raw_mx)] ctxt;
  1088     val [t] = polymorphic ctxt [prep_term ctxt raw_t];
  1098     val [t] = polymorphic ctxt [prep_term ctxt raw_t];
  1089     val T = Term.fastype_of t;
  1099     val T = Term.fastype_of t;
  1090     val _ =
  1100     val _ =
  1091       if null (extra_tvars t T) then ()
  1101       if null (hidden_polymorphism t T) then ()
  1092       else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
  1102       else error ("Extra type variables on rhs of abbreviation: " ^ quote c);
  1093   in
  1103   in
  1094     ctxt
  1104     ctxt
  1095     |> declare_term t
  1105     |> declare_term t
  1096     |> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t)))
  1106     |> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t)))