formal markup of constants;
authorwenzelm
Mon Feb 15 20:01:07 2010 +0100 (2010-02-15)
changeset 35133a68e4972fd31
parent 35132 d137efecf793
child 35134 d8d6c2f55c0c
formal markup of constants;
misc tuning;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Mon Feb 15 19:16:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Feb 15 20:01:07 2010 +0100
     1.3 @@ -156,7 +156,8 @@
     1.4      ((isom, cons $ isom), thm_thy)
     1.5    end;
     1.6  
     1.7 -val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN'
     1.8 +val iso_tuple_intros_tac =
     1.9 +  resolve_from_net_tac iso_tuple_intros THEN'
    1.10    CSUBGOAL (fn (cgoal, i) =>
    1.11      let
    1.12        val thy = Thm.theory_of_cterm cgoal;
    1.13 @@ -197,21 +198,21 @@
    1.14  
    1.15  val refl_conj_eq = @{thm refl_conj_eq};
    1.16  
    1.17 -val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"};
    1.18 -val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"};
    1.19 -
    1.20 -val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
    1.21 -val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
    1.22 -val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"};
    1.23 -val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"};
    1.24 -
    1.25 -val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
    1.26 -val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
    1.27 -val updacc_noopE = @{thm "update_accessor_noopE"};
    1.28 -val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
    1.29 -val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
    1.30 -val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
    1.31 -val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"};
    1.32 +val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
    1.33 +val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
    1.34 +
    1.35 +val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
    1.36 +val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
    1.37 +val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
    1.38 +val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
    1.39 +
    1.40 +val updacc_foldE = @{thm update_accessor_congruence_foldE};
    1.41 +val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
    1.42 +val updacc_noopE = @{thm update_accessor_noopE};
    1.43 +val updacc_noop_compE = @{thm update_accessor_noop_compE};
    1.44 +val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
    1.45 +val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
    1.46 +val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
    1.47  
    1.48  val o_eq_dest = @{thm o_eq_dest};
    1.49  val o_eq_id_dest = @{thm o_eq_id_dest};
    1.50 @@ -590,7 +591,7 @@
    1.51      val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
    1.52  
    1.53      val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty);
    1.54 -    val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
    1.55 +    val flds' = map (apsnd (Envir.norm_type subst o varifyT)) flds;
    1.56    in (flds', (more, moreT)) end;
    1.57  
    1.58  fun get_recT_fields thy T =
    1.59 @@ -674,12 +675,14 @@
    1.60  
    1.61  
    1.62  fun record_update_tr [t, u] =
    1.63 -      fold (curry op $) (gen_fields_tr "_updates" "_update" updateN u) t
    1.64 +      fold (curry op $)
    1.65 +        (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t
    1.66    | record_update_tr ts = raise TERM ("record_update_tr", ts);
    1.67  
    1.68  fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
    1.69    | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
    1.70 -  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    1.71 +  | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) =
    1.72 +      (* FIXME @{type_syntax} *)
    1.73        (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
    1.74    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    1.75  
    1.76 @@ -719,7 +722,7 @@
    1.77                      val more' = mk_ext rest;
    1.78                    in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end
    1.79                | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
    1.80 -          | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
    1.81 +          | NONE => raise TERM (msg ^ name ^ " is no proper field", [t]))
    1.82        | mk_ext [] = more;
    1.83    in mk_ext fieldargs end;
    1.84  
    1.85 @@ -784,27 +787,31 @@
    1.86        gen_ext_type_tr sep mark sfx more ctxt t
    1.87    | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
    1.88  
    1.89 -val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
    1.90 -
    1.91 -val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
    1.92 +val adv_record_tr =
    1.93 +  gen_adv_record_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN HOLogic.unit;
    1.94 +
    1.95 +val adv_record_scheme_tr =
    1.96 +  gen_adv_record_scheme_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN;
    1.97  
    1.98  val adv_record_type_tr =
    1.99 -  gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
   1.100 +  gen_adv_record_type_tr
   1.101 +    @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN
   1.102      (Syntax.term_of_typ false (HOLogic.unitT));
   1.103  
   1.104  val adv_record_type_scheme_tr =
   1.105 -  gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   1.106 +  gen_adv_record_type_scheme_tr
   1.107 +    @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN;
   1.108  
   1.109  
   1.110  val parse_translation =
   1.111 - [("_record_update", record_update_tr),
   1.112 -  ("_update_name", update_name_tr)];
   1.113 + [(@{syntax_const "_record_update"}, record_update_tr),
   1.114 +  (@{syntax_const "_update_name"}, update_name_tr)];
   1.115  
   1.116  val adv_parse_translation =
   1.117 - [("_record", adv_record_tr),
   1.118 -  ("_record_scheme", adv_record_scheme_tr),
   1.119 -  ("_record_type", adv_record_type_tr),
   1.120 -  ("_record_type_scheme", adv_record_type_scheme_tr)];
   1.121 + [(@{syntax_const "_record"}, adv_record_tr),
   1.122 +  (@{syntax_const "_record_scheme"}, adv_record_scheme_tr),
   1.123 +  (@{syntax_const "_record_type"}, adv_record_type_tr),
   1.124 +  (@{syntax_const "_record_type_scheme"}, adv_record_type_scheme_tr)];
   1.125  
   1.126  
   1.127  (* print translations *)
   1.128 @@ -821,11 +828,6 @@
   1.129            | Abs (_, _, t) =>
   1.130                if null (loose_bnos t) then t else raise Match
   1.131            | _ => raise Match);
   1.132 -
   1.133 -          (* FIXME ? *)
   1.134 -          (* (case k of (Const ("K_record", _) $ t) => t
   1.135 -                   | Abs (x, _, Const ("K_record", _) $ t $ Bound 0) => t
   1.136 -                   | _ => raise Match)*)
   1.137        in
   1.138          (case try (unsuffix sfx) name_field of
   1.139            SOME name =>
   1.140 @@ -835,11 +837,11 @@
   1.141    | gen_field_upds_tr' _ _ tm = ([], tm);
   1.142  
   1.143  fun record_update_tr' tm =
   1.144 -  let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   1.145 +  let val (ts, u) = gen_field_upds_tr' @{syntax_const "_update"} updateN tm in
   1.146      if null ts then raise Match
   1.147      else
   1.148 -      Syntax.const "_record_update" $ u $
   1.149 -        foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   1.150 +      Syntax.const @{syntax_const "_record_update"} $ u $
   1.151 +        foldr1 (fn (v, w) => Syntax.const @{syntax_const "_updates"} $ v $ w) (rev ts)
   1.152    end;
   1.153  
   1.154  fun gen_field_tr' sfx tr' name =
   1.155 @@ -880,9 +882,10 @@
   1.156  fun gen_record_tr' name =
   1.157    let
   1.158      val name_sfx = suffix extN name;
   1.159 -    val unit = (fn Const (@{const_syntax "Product_Type.Unity"}, _) => true | _ => false);
   1.160 +    val unit = fn Const (@{const_syntax Product_Type.Unity}, _) => true | _ => false;
   1.161      fun tr' ctxt ts =
   1.162 -      record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
   1.163 +      record_tr' @{syntax_const "_fields"} @{syntax_const "_field"}
   1.164 +        @{syntax_const "_record"} @{syntax_const "_record_scheme"} unit ctxt
   1.165          (list_comb (Syntax.const name_sfx, ts));
   1.166    in (name_sfx, tr') end;
   1.167  
   1.168 @@ -901,6 +904,7 @@
   1.169      (*tm is term representation of a (nested) field type. We first reconstruct the
   1.170        type from tm so that we can continue on the type level rather then the term level*)
   1.171  
   1.172 +    (* FIXME !??? *)
   1.173      (*WORKAROUND:
   1.174        If a record type occurs in an error message of type inference there
   1.175        may be some internal frees donoted by ??:
   1.176 @@ -967,7 +971,8 @@
   1.177                          val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
   1.178                          val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
   1.179                        in flds'' @ field_lst more end
   1.180 -                      handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)])
   1.181 +                      handle Type.TYPE_MATCH => [("", T)]
   1.182 +                        | Library.UnequalLengths => [("", T)])
   1.183                    | NONE => [("", T)])
   1.184                | NONE => [("", T)])
   1.185            | NONE => [("", T)])
   1.186 @@ -989,8 +994,9 @@
   1.187    let
   1.188      val name_sfx = suffix ext_typeN name;
   1.189      fun tr' ctxt ts =
   1.190 -      record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme"
   1.191 -        ctxt (list_comb (Syntax.const name_sfx, ts))
   1.192 +      record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"}
   1.193 +        @{syntax_const "_record_type"} @{syntax_const "_record_type_scheme"}
   1.194 +        ctxt (list_comb (Syntax.const name_sfx, ts));
   1.195    in (name_sfx, tr') end;
   1.196  
   1.197  
   1.198 @@ -998,7 +1004,8 @@
   1.199    let
   1.200      val name_sfx = suffix ext_typeN name;
   1.201      val default_tr' =
   1.202 -      record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme";
   1.203 +      record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"}
   1.204 +        @{syntax_const "_record_type"} @{syntax_const "_record_type_scheme"};
   1.205      fun tr' ctxt ts =
   1.206        record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
   1.207          (list_comb (Syntax.const name_sfx, ts));
   1.208 @@ -1040,11 +1047,11 @@
   1.209      val B = range_type X;
   1.210      val C = range_type (fastype_of f);
   1.211      val T = (B --> C) --> (A --> B) --> A --> C;
   1.212 -  in Const ("Fun.comp", T) $ f $ g end;
   1.213 +  in Const (@{const_name Fun.comp}, T) $ f $ g end;
   1.214  
   1.215  fun mk_comp_id f =
   1.216    let val T = range_type (fastype_of f)
   1.217 -  in mk_comp (Const ("Fun.id", T --> T)) f end;
   1.218 +  in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end;
   1.219  
   1.220  fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   1.221    | get_upd_funs _ = [];
   1.222 @@ -1055,6 +1062,7 @@
   1.223      val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
   1.224      fun get_simp upd =
   1.225        let
   1.226 +        (* FIXME fresh "f" (!?) *)
   1.227          val T = domain_type (fastype_of upd);
   1.228          val lhs = mk_comp acc (upd $ Free ("f", T));
   1.229          val rhs =
   1.230 @@ -1077,6 +1085,7 @@
   1.231  
   1.232  fun get_updupd_simp thy defset u u' comp =
   1.233    let
   1.234 +    (* FIXME fresh "f" (!?) *)
   1.235      val f = Free ("f", domain_type (fastype_of u));
   1.236      val f' = Free ("f'", domain_type (fastype_of u'));
   1.237      val lhs = mk_comp (u $ f) (u' $ f');
   1.238 @@ -1306,7 +1315,8 @@
   1.239                    K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
   1.240                  val (isnoop, skelf') = is_upd_noop s f term;
   1.241                  val funT = domain_type T;
   1.242 -                fun mk_comp_local (f, f') = Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
   1.243 +                fun mk_comp_local (f, f') =
   1.244 +                  Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
   1.245                in
   1.246                  if isnoop then
   1.247                    (upd $ skelf' $ lhs, rhs, vars,
   1.248 @@ -1359,7 +1369,7 @@
   1.249  val record_eq_simproc =
   1.250    Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
   1.251      (fn thy => fn _ => fn t =>
   1.252 -      (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   1.253 +      (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
   1.254          (case rec_id ~1 T of
   1.255            "" => NONE
   1.256          | name =>
   1.257 @@ -1381,7 +1391,10 @@
   1.258      (fn thy => fn _ => fn t =>
   1.259        (case t of
   1.260          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   1.261 -          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
   1.262 +          if quantifier = @{const_name All} orelse
   1.263 +            quantifier = @{const_name all} orelse
   1.264 +            quantifier = @{const_name Ex}
   1.265 +          then
   1.266              (case rec_id ~1 T of
   1.267                "" => NONE
   1.268              | _ =>
   1.269 @@ -1392,9 +1405,9 @@
   1.270                      | SOME (all_thm, All_thm, Ex_thm, _) =>
   1.271                          SOME
   1.272                            (case quantifier of
   1.273 -                            "all" => all_thm
   1.274 -                          | "All" => All_thm RS eq_reflection
   1.275 -                          | "Ex" => Ex_thm RS eq_reflection
   1.276 +                            @{const_name all} => all_thm
   1.277 +                          | @{const_name All} => All_thm RS eq_reflection
   1.278 +                          | @{const_name Ex} => Ex_thm RS eq_reflection
   1.279                            | _ => error "record_split_simproc"))
   1.280                    else NONE
   1.281                  end)
   1.282 @@ -1419,22 +1432,23 @@
   1.283                  else raise TERM ("", [x]);
   1.284                val sel' = Const (sel, Tsel) $ Bound 0;
   1.285                val (l, r) = if lr then (sel', x') else (x', sel');
   1.286 -            in Const ("op =", Teq) $ l $ r end
   1.287 +            in Const (@{const_name "op ="}, Teq) $ l $ r end
   1.288            else raise TERM ("", [Const (sel, Tsel)]);
   1.289  
   1.290 -        fun dest_sel_eq (Const ("op =", Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
   1.291 +        fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
   1.292                (true, Teq, (sel, Tsel), X)
   1.293 -          | dest_sel_eq (Const ("op =", Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
   1.294 +          | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
   1.295                (false, Teq, (sel, Tsel), X)
   1.296            | dest_sel_eq _ = raise TERM ("", []);
   1.297        in
   1.298          (case t of
   1.299 -          Const ("Ex", Tex) $ Abs (s, T, t) =>
   1.300 +          Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
   1.301             (let
   1.302 -              val eq = mkeq (dest_sel_eq t) 0;
   1.303 -              val prop =
   1.304 -                list_all ([("r", T)],
   1.305 -                  Logic.mk_equals (Const ("Ex", Tex) $ Abs (s, T, eq), HOLogic.true_const));
   1.306 +             val eq = mkeq (dest_sel_eq t) 0;
   1.307 +             val prop =
   1.308 +               list_all ([("r", T)],
   1.309 +                 Logic.mk_equals
   1.310 +                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
   1.311              in SOME (prove prop) end
   1.312              handle TERM _ => NONE)
   1.313          | _ => NONE)
   1.314 @@ -1459,7 +1473,8 @@
   1.315  
   1.316      val has_rec = exists_Const
   1.317        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.318 -          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
   1.319 +          (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
   1.320 +          is_recT T
   1.321          | _ => false);
   1.322  
   1.323      fun mk_split_free_tac free induct_thm i =
   1.324 @@ -1508,13 +1523,13 @@
   1.325  
   1.326      val has_rec = exists_Const
   1.327        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.328 -          (s = "all" orelse s = "All") andalso is_recT T
   1.329 +          (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T
   1.330          | _ => false);
   1.331  
   1.332      fun is_all t =
   1.333        (case t of
   1.334          Const (quantifier, _) $ _ =>
   1.335 -          if quantifier = "All" orelse quantifier = "all" then ~1 else 0
   1.336 +          if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0
   1.337        | _ => 0);
   1.338    in
   1.339      if has_rec goal then
   1.340 @@ -1945,6 +1960,7 @@
   1.341      val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
   1.342      val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
   1.343  
   1.344 +
   1.345      (* prepare definitions *)
   1.346  
   1.347      (*record (scheme) type abbreviation*)
   1.348 @@ -1955,7 +1971,6 @@
   1.349      val ext_defs = ext_def :: map #extdef parents;
   1.350  
   1.351      (*Theorems from the iso_tuple intros.
   1.352 -      This is complex enough to deserve a full comment.
   1.353        By unfolding ext_defs from r_rec0 we create a tree of constructor
   1.354        calls (many of them Pair, but others as well). The introduction
   1.355        rules for update_accessor_eq_assist can unify two different ways