src/HOL/Tools/record_package.ML
changeset 25705 45a2ffc5911e
parent 25179 b84f3c3c27f2
child 26065 d80a49f51b94
     1.1 --- a/src/HOL/Tools/record_package.ML	Tue Dec 18 22:21:42 2007 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Wed Dec 19 16:32:12 2007 +0100
     1.3 @@ -34,7 +34,6 @@
     1.4    val makeN: string
     1.5    val moreN: string
     1.6    val ext_dest: string
     1.7 -  val KN:string
     1.8  
     1.9    val last_extT: typ -> (string * typ list) option
    1.10    val dest_recTs : typ -> (string * typ list) list
    1.11 @@ -64,8 +63,8 @@
    1.12  val meta_allE = thm "Pure.meta_allE";
    1.13  val prop_subst = thm "prop_subst";
    1.14  val Pair_sel_convs = [fst_conv,snd_conv];
    1.15 -val K_record_apply = thm "Record.K_record_apply";
    1.16 -val K_comp_convs = [o_apply,K_record_apply]
    1.17 +val K_record_comp = thm "K_record_comp";
    1.18 +val K_comp_convs = [o_apply, K_record_comp]
    1.19  
    1.20  (** name components **)
    1.21  
    1.22 @@ -83,7 +82,6 @@
    1.23  val fields_selN = "fields";
    1.24  val extendN = "extend";
    1.25  val truncateN = "truncate";
    1.26 -val KN = "Record.K_record";
    1.27  
    1.28  (*see typedef_package.ML*)
    1.29  val RepN = "Rep_";
    1.30 @@ -526,7 +524,7 @@
    1.31  (* parse translations *)
    1.32  
    1.33  fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
    1.34 -      if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg)
    1.35 +      if c = mark then Syntax.const (suffix sfx name) $ (Abs ("_",dummyT, arg))
    1.36        else raise TERM ("gen_field_tr: " ^ mark, [t])
    1.37    | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
    1.38  
    1.39 @@ -673,11 +671,21 @@
    1.40  val print_record_type_abbr = ref true;
    1.41  val print_record_type_as_fields = ref true;
    1.42  
    1.43 -fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ (Const ("K_record",_)$t) $ u) =
    1.44 +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
    1.45 +  let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) 
    1.46 +                  => if null (loose_bnos t) then t else raise Match
    1.47 +               | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match
    1.48 +               | _ => raise Match)
    1.49 +
    1.50 +      (* (case k of (Const ("K_record",_)$t) => t
    1.51 +               | Abs (x,_,Const ("K_record",_)$t$Bound 0) => t
    1.52 +               | _ => raise Match)*)
    1.53 +  in
    1.54      (case try (unsuffix sfx) name_field of
    1.55        SOME name =>
    1.56          apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
    1.57       | NONE => ([], tm))
    1.58 +  end
    1.59    | gen_field_upds_tr' _ _ tm = ([], tm);
    1.60  
    1.61  fun record_update_tr' tm =
    1.62 @@ -966,6 +974,28 @@
    1.63  fun has_field extfields f T =
    1.64       exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN))
    1.65         (dest_recTs T);
    1.66 +
    1.67 +fun K_skeleton n (T as Type (_,[_,kT])) (b as Bound i) (Abs (x,xT,t)) =
    1.68 +     if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b)
    1.69 +  | K_skeleton n T b _ = ((n,T),b);
    1.70 +
    1.71 +(*
    1.72 +fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = 
    1.73 +      ((n,kT),K_rec$b)
    1.74 +  | K_skeleton n _ (Bound i) 
    1.75 +      (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) =
    1.76 +        ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0)))
    1.77 +  | K_skeleton n T b  _ = ((n,T),b);
    1.78 + *)
    1.79 +
    1.80 +fun normalize_rhs thm =
    1.81 +  let
    1.82 +     val ss = HOL_basic_ss addsimps K_comp_convs; 
    1.83 +     val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd;
    1.84 +     val _ = tracing ("rhs:"^(Pretty.string_of (Display.pretty_cterm rhs)));
    1.85 +     val rhs' = (Simplifier.rewrite ss rhs);
    1.86 +     val _ = tracing ("rhs':"^(Pretty.string_of (Display.pretty_thm rhs')));
    1.87 +  in Thm.transitive thm rhs' end;
    1.88  in
    1.89  (* record_simproc *)
    1.90  (* Simplifies selections of an record update:
    1.91 @@ -999,13 +1029,11 @@
    1.92                                   let
    1.93                                     val rv = ("r",rT)
    1.94                                     val rb = Bound 0
    1.95 -                                   val kv = ("k",kT)
    1.96 -                                   val kb = Bound 1
    1.97 +                                   val (kv,kb) = K_skeleton "k" kT (Bound 1) k;
    1.98                                    in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end
    1.99                                | SOME (trm,trm',vars) =>
   1.100                                   let
   1.101 -                                   val kv = ("k",kT)
   1.102 -                                   val kb = Bound (length vars)
   1.103 +                                   val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k;
   1.104                                   in SOME (upd$kb$trm,kb$trm',kv::vars) end)
   1.105                          else if has_field extfields u_name rangeS
   1.106                               orelse has_field extfields s (domain_type kT)
   1.107 @@ -1013,15 +1041,14 @@
   1.108                               else (case mk_eq_terms r of
   1.109                                       SOME (trm,trm',vars)
   1.110                                       => let
   1.111 -                                          val kv = ("k",kT)
   1.112 -                                          val kb = Bound (length vars)
   1.113 +                                          val (kv,kb) = 
   1.114 +                                                 K_skeleton "k" kT (Bound (length vars)) k;
   1.115                                          in SOME (upd$kb$trm,trm',kv::vars) end
   1.116                                     | NONE
   1.117                                       => let
   1.118                                            val rv = ("r",rT)
   1.119                                            val rb = Bound 0
   1.120 -                                          val kv = ("k",kT)
   1.121 -                                          val kb = Bound 1
   1.122 +                                          val (kv,kb) = K_skeleton "k" kT (Bound 1) k;
   1.123                                          in SOME (upd$kb$rb,sel$rb,[kv,rv]) end))
   1.124                  | mk_eq_terms r = NONE
   1.125              in
   1.126 @@ -1061,18 +1088,24 @@
   1.127  
   1.128               fun grow u uT k kT vars (sprout,skeleton) =
   1.129                     if sel_name u = moreN
   1.130 -                   then let val kv = ("k", kT);
   1.131 -                            val kb = Bound (length vars);
   1.132 +                   then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k;
   1.133                          in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
   1.134                     else ((sprout,skeleton),vars);
   1.135  
   1.136 -             fun is_upd_same (sprout,skeleton) u
   1.137 -                                ((K_rec as Const ("Record.K_record",_))$
   1.138 -                                  ((sel as Const (s,_))$r)) =
   1.139 +
   1.140 +             fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) =
   1.141 +                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   1.142 +               | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) =
   1.143 +                  (* eta expanded variant *)
   1.144 +                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   1.145 +               | dest_k _ = NONE;
   1.146 +
   1.147 +             fun is_upd_same (sprout,skeleton) u k =
   1.148 +               (case dest_k k of SOME (x,T,sel,s,r) =>
   1.149                     if (unsuffix updateN u) = s andalso (seed s sprout) = r
   1.150 -                   then SOME (K_rec,sel,seed s skeleton)
   1.151 +                   then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton)
   1.152                     else NONE
   1.153 -               | is_upd_same _ _ _ = NONE
   1.154 +                | NONE => NONE);
   1.155  
   1.156               fun init_seed r = ((r,Bound 0), [("r", rT)]);
   1.157  
   1.158 @@ -1111,15 +1144,13 @@
   1.159                                   Init ((sprout,skel),vars) =>
   1.160                                   let
   1.161                                     val n = sel_name u;
   1.162 -                                   val kv = (n, kT);
   1.163 -                                   val kb = Bound (length vars);
   1.164 +                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.165                                     val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel);
   1.166                                   in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end
   1.167                                 | Inter (trm,trm',vars,fmaps,sprout) =>
   1.168                                   let
   1.169                                     val n = sel_name u;
   1.170 -                                   val kv = (n, kT);
   1.171 -                                   val kb = Bound (length vars);
   1.172 +                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.173                                     val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
   1.174                                   in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
   1.175                                   end)
   1.176 @@ -1130,26 +1161,25 @@
   1.177                                   SOME (K_rec,sel,skel') =>
   1.178                                   let
   1.179                                     val (sprout',vars') = grow u uT k kT vars (sprout,skel);
   1.180 -                                  in Inter(upd$(K_rec$(sel$skel'))$skel,skel,vars',[],sprout')
   1.181 +                                  in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout')
   1.182                                    end
   1.183                                 | NONE =>
   1.184                                   let
   1.185 -                                   val kv = (sel_name u, kT);
   1.186 -                                   val kb = Bound (length vars);
   1.187 +                                   val n = sel_name u;
   1.188 +                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.189                                   in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
   1.190                             | Inter (trm,trm',vars,fmaps,sprout) =>
   1.191                                 (case is_upd_same sprout u k of
   1.192                                    SOME (K_rec,sel,skel) =>
   1.193                                    let
   1.194                                      val (sprout',vars') = grow u uT k kT vars sprout
   1.195 -                                  in Inter(upd$(K_rec$(sel$skel))$trm,trm',vars',fmaps,sprout')
   1.196 +                                  in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout')
   1.197                                    end
   1.198                                  | NONE =>
   1.199                                    let
   1.200                                      val n = sel_name u
   1.201                                      val T = domain_type kT
   1.202 -                                    val kv = (n, kT)
   1.203 -                                    val kb = Bound (length vars)
   1.204 +                                    val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   1.205                                      val (sprout',vars') = grow u uT k kT (kv::vars) sprout
   1.206                                      val fmaps' = add n kb fmaps
   1.207                                    in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
   1.208 @@ -1160,8 +1190,9 @@
   1.209  
   1.210           in (case mk_updterm updates [] t of
   1.211                 Inter (trm,trm',vars,_,_)
   1.212 -                => SOME (prove_split_simp thy ss rT
   1.213 -                          (list_all(vars,(equals rT$trm$trm'))))
   1.214 +                => SOME (normalize_rhs 
   1.215 +                          (prove_split_simp thy ss rT
   1.216 +                            (list_all(vars,(equals rT$trm$trm')))))
   1.217               | _ => NONE)
   1.218           end
   1.219         | _ => NONE))