src/Pure/variable.ML
changeset 20303 e25d5a2a50bc
parent 20262 ef3ee6a91c18
child 20509 073a5ed7dd71
     1.1 --- a/src/Pure/variable.ML	Wed Aug 02 22:26:56 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Aug 02 22:26:57 2006 +0200
     1.3 @@ -7,52 +7,56 @@
     1.4  
     1.5  signature VARIABLE =
     1.6  sig
     1.7 -  val is_body: Context.proof -> bool
     1.8 -  val set_body: bool -> Context.proof -> Context.proof
     1.9 -  val restore_body: Context.proof -> Context.proof -> Context.proof
    1.10 -  val names_of: Context.proof -> Name.context
    1.11 -  val fixes_of: Context.proof -> (string * string) list
    1.12 -  val binds_of: Context.proof -> (typ * term) Vartab.table
    1.13 -  val constraints_of: Context.proof -> typ Vartab.table * sort Vartab.table
    1.14 -  val is_declared: Context.proof -> string -> bool
    1.15 -  val is_fixed: Context.proof -> string -> bool
    1.16 -  val newly_fixed: Context.proof -> Context.proof -> string -> bool
    1.17 -  val default_type: Context.proof -> string -> typ option
    1.18 -  val def_type: Context.proof -> bool -> indexname -> typ option
    1.19 -  val def_sort: Context.proof -> indexname -> sort option
    1.20 -  val declare_constraints: term -> Context.proof -> Context.proof
    1.21 -  val declare_internal: term -> Context.proof -> Context.proof
    1.22 -  val declare_term: term -> Context.proof -> Context.proof
    1.23 -  val declare_thm: thm -> Context.proof -> Context.proof
    1.24 -  val thm_context: thm -> Context.proof
    1.25 -  val variant_frees: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.26 -  val add_fixes: string list -> Context.proof -> string list * Context.proof
    1.27 -  val add_fixes_direct: string list -> Context.proof -> Context.proof
    1.28 -  val fix_frees: term -> Context.proof -> Context.proof
    1.29 -  val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.30 -  val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
    1.31 -  val export_inst: Context.proof -> Context.proof -> string list * string list
    1.32 -  val exportT_inst: Context.proof -> Context.proof -> string list
    1.33 -  val export_terms: Context.proof -> Context.proof -> term list -> term list
    1.34 -  val exportT_terms: Context.proof -> Context.proof -> term list -> term list
    1.35 -  val exportT: Context.proof -> Context.proof -> thm list -> thm list
    1.36 -  val export: Context.proof -> Context.proof -> thm list -> thm list
    1.37 -  val importT_inst: term list -> Context.proof -> ((indexname * sort) * typ) list * Context.proof
    1.38 -  val import_inst: bool -> term list -> Context.proof ->
    1.39 -    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Context.proof
    1.40 -  val importT_terms: term list -> Context.proof -> term list * Context.proof
    1.41 -  val import_terms: bool -> term list -> Context.proof -> term list * Context.proof
    1.42 -  val importT: thm list -> Context.proof -> (ctyp list * thm list) * Context.proof
    1.43 -  val import: bool -> thm list -> Context.proof ->
    1.44 -    ((ctyp list * cterm list) * thm list) * Context.proof
    1.45 -  val tradeT: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.46 -  val trade: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.47 -  val focus: cterm -> Context.proof -> (cterm list * cterm) * Context.proof
    1.48 -  val warn_extra_tfrees: Context.proof -> Context.proof -> unit
    1.49 -  val polymorphic: Context.proof -> term list -> term list
    1.50 +  val is_body: Proof.context -> bool
    1.51 +  val set_body: bool -> Proof.context -> Proof.context
    1.52 +  val restore_body: Proof.context -> Proof.context -> Proof.context
    1.53 +  val names_of: Proof.context -> Name.context
    1.54 +  val fixes_of: Proof.context -> (string * string) list
    1.55 +  val binds_of: Proof.context -> (typ * term) Vartab.table
    1.56 +  val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
    1.57 +  val is_declared: Proof.context -> string -> bool
    1.58 +  val is_fixed: Proof.context -> string -> bool
    1.59 +  val newly_fixed: Proof.context -> Proof.context -> string -> bool
    1.60 +  val default_type: Proof.context -> string -> typ option
    1.61 +  val def_type: Proof.context -> bool -> indexname -> typ option
    1.62 +  val def_sort: Proof.context -> indexname -> sort option
    1.63 +  val declare_constraints: term -> Proof.context -> Proof.context
    1.64 +  val declare_internal: term -> Proof.context -> Proof.context
    1.65 +  val declare_term: term -> Proof.context -> Proof.context
    1.66 +  val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
    1.67 +  val declare_thm: thm -> Proof.context -> Proof.context
    1.68 +  val thm_context: thm -> Proof.context
    1.69 +  val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
    1.70    val hidden_polymorphism: term -> typ -> (indexname * sort) list
    1.71 -  val add_binds: (indexname * term option) list -> Context.proof -> Context.proof
    1.72 -  val expand_binds: Context.proof -> term -> term
    1.73 +  val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
    1.74 +  val expand_binds: Proof.context -> term -> term
    1.75 +  val add_fixes: string list -> Proof.context -> string list * Proof.context
    1.76 +  val add_fixes_direct: string list -> Proof.context -> Proof.context
    1.77 +  val fix_frees: term -> Proof.context -> Proof.context
    1.78 +  val invent_fixes: string list -> Proof.context -> string list * Proof.context
    1.79 +  val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
    1.80 +  val export_inst: Proof.context -> Proof.context -> string list * string list
    1.81 +  val exportT_inst: Proof.context -> Proof.context -> string list
    1.82 +  val export_terms: Proof.context -> Proof.context -> term list -> term list
    1.83 +  val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    1.84 +  val exportT: Proof.context -> Proof.context -> thm list -> thm list
    1.85 +  val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
    1.86 +  val export: Proof.context -> Proof.context -> thm list -> thm list
    1.87 +  val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
    1.88 +  val import_inst: bool -> term list -> Proof.context ->
    1.89 +    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
    1.90 +  val importT_terms: term list -> Proof.context -> term list * Proof.context
    1.91 +  val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
    1.92 +  val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
    1.93 +  val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
    1.94 +  val import: bool -> thm list -> Proof.context ->
    1.95 +    ((ctyp list * cterm list) * thm list) * Proof.context
    1.96 +  val tradeT: Proof.context -> (thm list -> thm list) -> thm list -> thm list
    1.97 +  val trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list
    1.98 +  val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
    1.99 +  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
   1.100 +  val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   1.101 +  val polymorphic: Proof.context -> term list -> term list
   1.102  end;
   1.103  
   1.104  structure Variable: VARIABLE =
   1.105 @@ -193,6 +197,8 @@
   1.106    declare_internal t #>
   1.107    declare_constraints t;
   1.108  
   1.109 +val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
   1.110 +
   1.111  fun declare_thm th = fold declare_internal (Thm.full_prop_of th :: Thm.hyps_of th);
   1.112  fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
   1.113  
   1.114 @@ -207,6 +213,38 @@
   1.115  
   1.116  
   1.117  
   1.118 +(** term bindings **)
   1.119 +
   1.120 +fun hidden_polymorphism t T =
   1.121 +  let
   1.122 +    val tvarsT = Term.add_tvarsT T [];
   1.123 +    val extra_tvars = Term.fold_types (Term.fold_atyps
   1.124 +      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   1.125 +  in extra_tvars end;
   1.126 +
   1.127 +fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   1.128 +  | add_bind ((x, i), SOME t) =
   1.129 +      let
   1.130 +        val T = Term.fastype_of t;
   1.131 +        val t' =
   1.132 +          if null (hidden_polymorphism t T) then t
   1.133 +          else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   1.134 +      in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
   1.135 +
   1.136 +val add_binds = fold add_bind;
   1.137 +
   1.138 +fun expand_binds ctxt =
   1.139 +  let
   1.140 +    val binds = binds_of ctxt;
   1.141 +    fun expand (t as Var (xi, T)) =
   1.142 +          (case Vartab.lookup binds xi of
   1.143 +            SOME u => Envir.expand_atom T u
   1.144 +          | NONE => t)
   1.145 +      | expand t = t;
   1.146 +  in Envir.beta_norm o Term.map_aterms expand end;
   1.147 +
   1.148 +
   1.149 +
   1.150  (** fixes **)
   1.151  
   1.152  local
   1.153 @@ -291,6 +329,14 @@
   1.154    map (Term.generalize (export_inst (fold declare_type_occs ts inner) outer)
   1.155      (fold Term.maxidx_term ts ~1 + 1)) ts;
   1.156  
   1.157 +fun export_prf inner outer prf =
   1.158 +  let
   1.159 +    val insts = export_inst (declare_prf prf inner) outer;
   1.160 +    val idx = Proofterm.maxidx_proof prf ~1 + 1;
   1.161 +    val gen_term = Term.generalize_option insts idx;
   1.162 +    val gen_typ = Term.generalizeT_option (#1 insts) idx;
   1.163 +  in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
   1.164 +
   1.165  fun gen_export inst inner outer ths =
   1.166    let
   1.167      val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
   1.168 @@ -335,6 +381,12 @@
   1.169      val ths' = map (Thm.instantiate (instT', [])) ths;
   1.170    in ((map #2 instT', ths'), ctxt') end;
   1.171  
   1.172 +fun import_prf is_open prf ctxt =
   1.173 +  let
   1.174 +    val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []);
   1.175 +    val (insts, ctxt') = import_inst is_open ts ctxt;
   1.176 +  in (Proofterm.instantiate insts prf, ctxt') end;
   1.177 +
   1.178  fun import is_open ths ctxt =
   1.179    let
   1.180      val thy = Context.theory_of_proof ctxt;
   1.181 @@ -374,6 +426,17 @@
   1.182      val goal' = fold forall_elim_prop ps' goal;
   1.183    in ((ps', goal'), ctxt') end;
   1.184  
   1.185 +fun focus_subgoal i st =
   1.186 +  let
   1.187 +    val all_vars = Drule.fold_terms Term.add_vars st [];
   1.188 +    val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   1.189 +  in
   1.190 +    add_binds no_binds #>
   1.191 +    fold (declare_constraints o Var) all_vars #>
   1.192 +    focus (Thm.cprem_of st i)
   1.193 +  end;
   1.194 +
   1.195 +
   1.196  
   1.197  (** implicit polymorphism **)
   1.198  
   1.199 @@ -411,36 +474,4 @@
   1.200      val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
   1.201    in map (Term.generalize (types, []) idx) ts end;
   1.202  
   1.203 -fun hidden_polymorphism t T =
   1.204 -  let
   1.205 -    val tvarsT = Term.add_tvarsT T [];
   1.206 -    val extra_tvars = Term.fold_types (Term.fold_atyps
   1.207 -      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   1.208 -  in extra_tvars end;
   1.209 -
   1.210 -
   1.211 -
   1.212 -(** term bindings **)
   1.213 -
   1.214 -fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   1.215 -  | add_bind ((x, i), SOME t) =
   1.216 -      let
   1.217 -        val T = Term.fastype_of t;
   1.218 -        val t' =
   1.219 -          if null (hidden_polymorphism t T) then t
   1.220 -          else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   1.221 -      in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end;
   1.222 -
   1.223 -val add_binds = fold add_bind;
   1.224 -
   1.225 -fun expand_binds ctxt =
   1.226 -  let
   1.227 -    val binds = binds_of ctxt;
   1.228 -    fun expand (t as Var (xi, T)) =
   1.229 -          (case Vartab.lookup binds xi of
   1.230 -            SOME u => Envir.expand_atom T u
   1.231 -          | NONE => t)
   1.232 -      | expand t = t;
   1.233 -  in Envir.beta_norm o Term.map_aterms expand end;
   1.234 -
   1.235  end;