derived operations are now: make, extend, truncate (cf. derived_defs);
authorwenzelm
Thu Oct 25 20:00:11 2001 +0200 (2001-10-25)
changeset 119346c1bf72430b6
parent 11933 acfea249b03c
child 11935 cbcba2092d6b
derived operations are now: make, extend, truncate (cf. derived_defs);
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Thu Oct 25 19:59:00 2001 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Oct 25 20:00:11 2001 +0200
     1.3 @@ -71,7 +71,11 @@
     1.4  val Trueprop = HOLogic.mk_Trueprop;
     1.5  fun All xs t = Term.list_all_free (xs, t);
     1.6  
     1.7 -infix 0 :== === ==>;
     1.8 +infix 9 $$;
     1.9 +infix 0 :== ===;
    1.10 +infixr 0 ==>;
    1.11 +
    1.12 +val (op $$) = Term.list_comb;
    1.13  val (op :==) = Logic.mk_defpair;
    1.14  val (op ===) = Trueprop o HOLogic.mk_eq;
    1.15  val (op ==>) = Logic.mk_implies;
    1.16 @@ -109,8 +113,9 @@
    1.17  val sndN = "_more";
    1.18  val updateN = "_update";
    1.19  val makeN = "make";
    1.20 -val make_schemeN = "make_scheme";
    1.21 -val recordN = "record";
    1.22 +val extendN = "extend";
    1.23 +val truncateN = "truncate";
    1.24 +
    1.25  
    1.26  (*see typedef_package.ML*)
    1.27  val RepN = "Rep_";
    1.28 @@ -203,6 +208,8 @@
    1.29    let val rT = fastype_of r
    1.30    in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
    1.31  
    1.32 +fun mk_named_sels names r = names ~~ map (mk_sel r) names;
    1.33 +
    1.34  val mk_moreC = mk_selC;
    1.35  
    1.36  fun mk_more r c =
    1.37 @@ -225,11 +232,6 @@
    1.38    in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end;
    1.39  
    1.40  
    1.41 -(* make *)
    1.42 -
    1.43 -fun mk_makeC rT (c, Ts) = (c, Ts ---> rT);
    1.44 -
    1.45 -
    1.46  
    1.47  (** concrete syntax for records **)
    1.48  
    1.49 @@ -263,11 +265,10 @@
    1.50    | record_update_tr ts = raise TERM ("record_update_tr", ts);
    1.51  
    1.52  
    1.53 -fun update_name_tr (Free (x, T) :: ts) = Term.list_comb (Free (suffix updateN x, T), ts)
    1.54 -  | update_name_tr (Const (x, T) :: ts) = Term.list_comb (Const (suffix updateN x, T), ts)
    1.55 +fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
    1.56 +  | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
    1.57    | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    1.58 -      Term.list_comb (c $ update_name_tr [t] $
    1.59 -        (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    1.60 +      (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
    1.61    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    1.62  
    1.63  
    1.64 @@ -700,12 +701,15 @@
    1.65      val parent_more = funpow parent_len mk_snd;
    1.66      val idxs = 0 upto (len - 1);
    1.67  
    1.68 +    val parentT = if null parent_fields then [] else [mk_recordT (parent_fields, HOLogic.unitT)];
    1.69 +    val r_parent = if null parent_fields then [] else [Free (rN, hd parentT)];
    1.70 +
    1.71      val rec_schemeT = mk_recordT (all_fields, moreT);
    1.72      val rec_scheme = mk_record (all_named_vars, more);
    1.73      val recT = mk_recordT (all_fields, HOLogic.unitT);
    1.74      val rec_ = mk_record (all_named_vars, HOLogic.unit);
    1.75 -    val r = Free (rN, rec_schemeT);
    1.76 -    val r' = Free (rN, recT);
    1.77 +    val r_scheme = Free (rN, rec_schemeT);
    1.78 +    val r = Free (rN, recT);
    1.79  
    1.80  
    1.81      (* prepare print translation functions *)
    1.82 @@ -720,10 +724,9 @@
    1.83        [mk_moreC rec_schemeT (moreN, moreT)];
    1.84      val update_decls = map (mk_updateC rec_schemeT) bfields @
    1.85        [mk_more_updateC rec_schemeT (moreN, moreT)];
    1.86 -    val make_decls =
    1.87 -      [(mk_makeC rec_schemeT (make_schemeN, all_types @ [moreT])),
    1.88 -       (mk_makeC recT (makeN, all_types))];
    1.89 -    val record_decl = (recordN, rec_schemeT --> recT);
    1.90 +    val make_decl = (makeN, parentT ---> types ---> recT);
    1.91 +    val extend_decl = (extendN, recT --> moreT --> rec_schemeT);
    1.92 +    val truncate_decl = (truncateN, rec_schemeT --> recT);
    1.93  
    1.94  
    1.95      (* prepare definitions *)
    1.96 @@ -735,28 +738,27 @@
    1.97  
    1.98      (*selectors*)
    1.99      fun mk_sel_spec (i, c) =
   1.100 -      mk_sel r c :== mk_fst (funpow i mk_snd (parent_more r));
   1.101 +      mk_sel r_scheme c :== mk_fst (funpow i mk_snd (parent_more r_scheme));
   1.102      val sel_specs =
   1.103        ListPair.map mk_sel_spec (idxs, names) @
   1.104 -        [more_part r :== funpow len mk_snd (parent_more r)];
   1.105 +        [more_part r_scheme :== funpow len mk_snd (parent_more r_scheme)];
   1.106  
   1.107      (*updates*)
   1.108 -    val all_sels = all_names ~~ map (mk_sel r) all_names;
   1.109 +    val all_sels = mk_named_sels all_names r_scheme;
   1.110      fun mk_upd_spec (i, (c, x)) =
   1.111 -      mk_update r (c, x) :==
   1.112 -        mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part r)
   1.113 +      mk_update r_scheme (c, x) :==
   1.114 +        mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part r_scheme)
   1.115      val update_specs =
   1.116        ListPair.map mk_upd_spec (idxs, named_vars) @
   1.117 -        [more_part_update r more :== mk_record (all_sels, more)];
   1.118 +        [more_part_update r_scheme more :== mk_record (all_sels, more)];
   1.119  
   1.120 -    (*makes*)
   1.121 -    val make_scheme = Const (mk_makeC rec_schemeT (full make_schemeN, all_types @ [moreT]));
   1.122 -    val make = Const (mk_makeC recT (full makeN, all_types));
   1.123 -    val make_specs =
   1.124 -      [list_comb (make_scheme, all_vars) $ more :== rec_scheme,
   1.125 -        list_comb (make, all_vars) :== rec_];
   1.126 -    val record_spec =
   1.127 -      Const (full recordN, rec_schemeT --> recT) $ r :== mk_record (all_sels, HOLogic.unit);
   1.128 +    (*derived operations*)
   1.129 +    val make_spec = Const (full makeN, parentT ---> types ---> recT) $$ r_parent $$ vars :==
   1.130 +      mk_record (flat (map (mk_named_sels parent_names) r_parent) @ named_vars, HOLogic.unit);
   1.131 +    val extend_spec = Const (full extendN, recT --> moreT --> rec_schemeT) $ r $ more :==
   1.132 +      mk_record (mk_named_sels all_names r, more);
   1.133 +    val truncate_spec = Const (full truncateN, rec_schemeT --> recT) $ r_scheme :==
   1.134 +      mk_record (all_sels, HOLogic.unit);
   1.135  
   1.136  
   1.137      (* prepare propositions *)
   1.138 @@ -779,9 +781,10 @@
   1.139  
   1.140      (*equality*)
   1.141      fun mk_sel_eq (t, T) =
   1.142 -      let val t' = Term.abstract_over (r, t)
   1.143 +      let val t' = Term.abstract_over (r_scheme, t)
   1.144        in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end;
   1.145 -    val sel_eqs = map2 mk_sel_eq (map (mk_sel r) all_names @ [more_part r], all_types @ [moreT]);
   1.146 +    val sel_eqs =
   1.147 +      map2 mk_sel_eq (map (mk_sel r_scheme) all_names @ [more_part r_scheme], all_types @ [moreT]);
   1.148      val equality_prop =
   1.149        Term.all rec_schemeT $ (Abs ("r", rec_schemeT,
   1.150          Term.all rec_schemeT $ (Abs ("r'", rec_schemeT,
   1.151 @@ -792,13 +795,14 @@
   1.152      val P = Free ("P", rec_schemeT --> HOLogic.boolT);
   1.153      val P' = Free ("P", recT --> HOLogic.boolT);
   1.154      val induct_scheme_prop =
   1.155 -      All (all_xs_more ~~ all_types_more) (Trueprop (P $ rec_scheme)) ==> Trueprop (P $ r);
   1.156 -    val induct_prop = All (all_xs ~~ all_types) (Trueprop (P' $ rec_)) ==> Trueprop (P' $ r');
   1.157 +      All (all_xs_more ~~ all_types_more) (Trueprop (P $ rec_scheme)) ==> Trueprop (P $ r_scheme);
   1.158 +    val induct_prop = All (all_xs ~~ all_types) (Trueprop (P' $ rec_)) ==> Trueprop (P' $ r);
   1.159  
   1.160      (*cases*)
   1.161      val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT));
   1.162 -    val cases_scheme_prop = All (all_xs_more ~~ all_types_more) ((r === rec_scheme) ==> C) ==> C;
   1.163 -    val cases_prop = All (all_xs ~~ all_types) ((r' === rec_) ==> C) ==> C;
   1.164 +    val cases_scheme_prop =
   1.165 +      All (all_xs_more ~~ all_types_more) ((r_scheme === rec_scheme) ==> C) ==> C;
   1.166 +    val cases_prop = All (all_xs ~~ all_types) ((r === rec_) ==> C) ==> C;
   1.167  
   1.168  
   1.169      (* 1st stage: fields_thy *)
   1.170 @@ -813,7 +817,7 @@
   1.171  
   1.172      (* 2nd stage: defs_thy *)
   1.173  
   1.174 -    val (defs_thy, (((sel_defs, update_defs), make_defs), [record_def])) =
   1.175 +    val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
   1.176        fields_thy
   1.177        |> add_record_splits named_splits
   1.178        |> Theory.parent_path
   1.179 @@ -821,11 +825,11 @@
   1.180        |> Theory.add_path bname
   1.181        |> Theory.add_trfuns ([], [], field_tr's, [])
   1.182        |> (Theory.add_consts_i o map Syntax.no_syn)
   1.183 -        (sel_decls @ update_decls @ make_decls @ [record_decl])
   1.184 +        (sel_decls @ update_decls @ [make_decl, extend_decl, truncate_decl])
   1.185        |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
   1.186        |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs
   1.187 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs
   1.188 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) [record_spec];
   1.189 +      |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
   1.190 +        [make_spec, extend_spec, truncate_spec];
   1.191  
   1.192      val defs_sg = Theory.sign_of defs_thy;
   1.193  
   1.194 @@ -868,7 +872,7 @@
   1.195        |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
   1.196          [("select_defs", sel_defs),
   1.197            ("update_defs", update_defs),
   1.198 -          ("make_defs", make_defs),
   1.199 +          ("derived_defs", derived_defs),
   1.200            ("select_convs", sel_convs),
   1.201            ("update_convs", update_convs)]
   1.202        |> (#1 oo PureThy.add_thms)