src/Pure/Isar/proof_context.ML
changeset 28082 37350f301128
parent 28017 4919bd124a58
child 28087 a9cccdd9d521
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 02 14:10:31 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 02 14:10:32 2008 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4    val get_skolem: Proof.context -> string -> string
     1.5    val revert_skolem: Proof.context -> string -> string
     1.6    val infer_type: Proof.context -> string -> typ
     1.7 -  val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
     1.8 +  val inferred_param: string -> Proof.context -> typ * Proof.context
     1.9    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    1.10    val read_tyname: Proof.context -> string -> typ
    1.11    val read_const_proper: Proof.context -> string -> term
    1.12 @@ -101,29 +101,29 @@
    1.13    val sticky_prefix: string -> Proof.context -> Proof.context
    1.14    val restore_naming: Proof.context -> Proof.context -> Proof.context
    1.15    val reset_naming: Proof.context -> Proof.context
    1.16 -  val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    1.17    val note_thmss: string ->
    1.18 -    ((bstring * attribute list) * (Facts.ref * attribute list) list) list ->
    1.19 -      Proof.context -> (bstring * thm list) list * Proof.context
    1.20 +    ((Name.binding * attribute list) * (Facts.ref * attribute list) list) list ->
    1.21 +      Proof.context -> (string * thm list) list * Proof.context
    1.22    val note_thmss_i: string ->
    1.23 -    ((bstring * attribute list) * (thm list * attribute list) list) list ->
    1.24 -      Proof.context -> (bstring * thm list) list * Proof.context
    1.25 -  val read_vars: (string * string option * mixfix) list -> Proof.context ->
    1.26 -    (string * typ option * mixfix) list * Proof.context
    1.27 -  val cert_vars: (string * typ option * mixfix) list -> Proof.context ->
    1.28 -    (string * typ option * mixfix) list * Proof.context
    1.29 -  val add_fixes: (string * string option * mixfix) list ->
    1.30 +    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    1.31 +      Proof.context -> (string * thm list) list * Proof.context
    1.32 +  val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
    1.33 +  val read_vars: (Name.binding * string option * mixfix) list -> Proof.context ->
    1.34 +    (Name.binding * typ option * mixfix) list * Proof.context
    1.35 +  val cert_vars: (Name.binding * typ option * mixfix) list -> Proof.context ->
    1.36 +    (Name.binding * typ option * mixfix) list * Proof.context
    1.37 +  val add_fixes: (Name.binding * string option * mixfix) list ->
    1.38      Proof.context -> string list * Proof.context
    1.39 -  val add_fixes_i: (string * typ option * mixfix) list ->
    1.40 +  val add_fixes_i: (Name.binding * typ option * mixfix) list ->
    1.41      Proof.context -> string list * Proof.context
    1.42    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
    1.43    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
    1.44    val add_assms: Assumption.export ->
    1.45 -    ((string * attribute list) * (string * string list) list) list ->
    1.46 -    Proof.context -> (bstring * thm list) list * Proof.context
    1.47 +    ((Name.binding * attribute list) * (string * string list) list) list ->
    1.48 +    Proof.context -> (string * thm list) list * Proof.context
    1.49    val add_assms_i: Assumption.export ->
    1.50 -    ((string * attribute list) * (term * term list) list) list ->
    1.51 -    Proof.context -> (bstring * thm list) list * Proof.context
    1.52 +    ((Name.binding * attribute list) * (term * term list) list) list ->
    1.53 +    Proof.context -> (string * thm list) list * Proof.context
    1.54    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
    1.55    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
    1.56    val get_case: Proof.context -> string -> string option list -> RuleCases.T
    1.57 @@ -403,10 +403,13 @@
    1.58  
    1.59  fun inferred_param x ctxt =
    1.60    let val T = infer_type ctxt x
    1.61 -  in ((x, T), ctxt |> Variable.declare_term (Free (x, T))) end;
    1.62 +  in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
    1.63  
    1.64  fun inferred_fixes ctxt =
    1.65 -  fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt;
    1.66 +  let
    1.67 +    val xs = rev (map #2 (Variable.fixes_of ctxt));
    1.68 +    val (Ts, ctxt') = fold_map inferred_param xs ctxt;
    1.69 +  in (xs ~~ Ts, ctxt') end;
    1.70  
    1.71  
    1.72  (* type and constant names *)
    1.73 @@ -933,31 +936,35 @@
    1.74  
    1.75  (* facts *)
    1.76  
    1.77 +local
    1.78 +
    1.79  fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
    1.80    | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
    1.81        (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
    1.82  
    1.83 -fun put_thms do_props thms ctxt =
    1.84 -  ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;
    1.85 -
    1.86 -local
    1.87 -
    1.88 -fun gen_note_thmss get k = fold_map (fn ((bname, more_attrs), raw_facts) => fn ctxt =>
    1.89 +fun gen_note_thmss get k = fold_map (fn ((binding, more_attrs), raw_facts) => fn ctxt =>
    1.90    let
    1.91 +    val bname = Name.name_of binding;
    1.92 +    val pos = Name.pos_of binding;
    1.93      val name = full_name ctxt bname;
    1.94 -    val facts = PureThy.name_thmss false name (map (apfst (get ctxt)) raw_facts);
    1.95 +    val _ = Position.report (Markup.local_fact_decl name) pos;
    1.96 +
    1.97 +    val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    1.98      fun app (th, attrs) x =
    1.99 -      swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ [Thm.kind k])) (x, th));
   1.100 +      swap (foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
   1.101      val (res, ctxt') = fold_map app facts ctxt;
   1.102 -    val thms = PureThy.name_thms false false name (flat res);
   1.103 +    val thms = PureThy.name_thms false false pos name (flat res);
   1.104      val Mode {stmt, ...} = get_mode ctxt;
   1.105 -  in ((bname, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
   1.106 +  in ((name, thms), ctxt' |> update_thms stmt (bname, SOME thms)) end);
   1.107  
   1.108  in
   1.109  
   1.110  fun note_thmss k = gen_note_thmss get_fact k;
   1.111  fun note_thmss_i k = gen_note_thmss (K I) k;
   1.112  
   1.113 +fun put_thms do_props thms ctxt =
   1.114 +  ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;
   1.115 +
   1.116  end;
   1.117  
   1.118  
   1.119 @@ -973,8 +980,9 @@
   1.120  local
   1.121  
   1.122  fun prep_vars prep_typ internal =
   1.123 -  fold_map (fn (raw_x, raw_T, raw_mx) => fn ctxt =>
   1.124 +  fold_map (fn (raw_binding, raw_T, raw_mx) => fn ctxt =>
   1.125      let
   1.126 +      val raw_x = Name.name_of raw_binding;
   1.127        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
   1.128        val _ = Syntax.is_identifier (no_skolem internal x) orelse
   1.129          error ("Illegal variable name: " ^ quote x);
   1.130 @@ -983,8 +991,8 @@
   1.131          if internal then T
   1.132          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
   1.133        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
   1.134 -      val var = (x, opt_T, mx);
   1.135 -    in (var, ctxt |> declare_var var |> #2) end);
   1.136 +      val var = (Name.map_name (K x) raw_binding, opt_T, mx);
   1.137 +    in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
   1.138  
   1.139  in
   1.140  
   1.141 @@ -1080,13 +1088,14 @@
   1.142  fun gen_fixes prep raw_vars ctxt =
   1.143    let
   1.144      val (vars, _) = prep raw_vars ctxt;
   1.145 -    val (xs', ctxt') = Variable.add_fixes (map #1 vars) ctxt;
   1.146 -  in
   1.147 -    ctxt'
   1.148 -    |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   1.149 -    |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix)
   1.150 -    |> pair xs'
   1.151 -  end;
   1.152 +    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
   1.153 +    val ctxt'' =
   1.154 +      ctxt'
   1.155 +      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
   1.156 +      |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
   1.157 +    val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
   1.158 +      Position.report (Markup.fixed_decl x') (Name.pos_of binding));
   1.159 +  in (xs', ctxt'') end;
   1.160  
   1.161  in
   1.162  
   1.163 @@ -1103,7 +1112,7 @@
   1.164  
   1.165  fun bind_fixes xs ctxt =
   1.166    let
   1.167 -    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs);
   1.168 +    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Name.binding x, NONE, NoSyn)) xs);
   1.169      fun bind (t as Free (x, T)) =
   1.170            if member (op =) xs x then
   1.171              (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)