# HG changeset patch # User schirmer # Date 1198078332 -3600 # Node ID 45a2ffc5911ea2a1daf6274fbd8fca09ed15ab3f # Parent df9c8074ff09bcfb989c3f529cdb8914337b85b9 replaced K_record by lambda term %x. c diff -r df9c8074ff09 -r 45a2ffc5911e NEWS --- a/NEWS Tue Dec 18 22:21:42 2007 +0100 +++ b/NEWS Wed Dec 19 16:32:12 2007 +0100 @@ -49,6 +49,10 @@ and makes them available separately. See "HOL/ex/Induction_Scheme.thy" for examples, +* Records. Removed K_record, and replaced it by pure lambda term +%x. c. The simplifier setup is now more robust against eta +expansion. +INCOMPATIBILITY: in cases explicitly referring to K_record. *** System *** diff -r df9c8074ff09 -r 45a2ffc5911e src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Dec 18 22:21:42 2007 +0100 +++ b/src/HOL/Record.thy Wed Dec 19 16:32:12 2007 +0100 @@ -19,15 +19,8 @@ lemma rec_True_simp: "(True \ PROP P) \ PROP P" by simp -constdefs - K_record:: "'a \ 'b \ 'a" - K_record_apply [simp, code func]: "K_record c x \ c" - -lemma K_record_comp [simp]: "(K_record c \ f) = K_record c" - by (rule ext) (simp add: K_record_apply comp_def) - -lemma K_record_cong [cong]: "K_record c x = K_record c x" - by (rule refl) +lemma K_record_comp: "(\x. c) \ f = (\x. c)" + by (simp add: comp_def) subsection {* Concrete record syntax *} diff -r df9c8074ff09 -r 45a2ffc5911e src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Dec 18 22:21:42 2007 +0100 +++ b/src/HOL/Tools/record_package.ML Wed Dec 19 16:32:12 2007 +0100 @@ -34,7 +34,6 @@ val makeN: string val moreN: string val ext_dest: string - val KN:string val last_extT: typ -> (string * typ list) option val dest_recTs : typ -> (string * typ list) list @@ -64,8 +63,8 @@ val meta_allE = thm "Pure.meta_allE"; val prop_subst = thm "prop_subst"; val Pair_sel_convs = [fst_conv,snd_conv]; -val K_record_apply = thm "Record.K_record_apply"; -val K_comp_convs = [o_apply,K_record_apply] +val K_record_comp = thm "K_record_comp"; +val K_comp_convs = [o_apply, K_record_comp] (** name components **) @@ -83,7 +82,6 @@ val fields_selN = "fields"; val extendN = "extend"; val truncateN = "truncate"; -val KN = "Record.K_record"; (*see typedef_package.ML*) val RepN = "Rep_"; @@ -526,7 +524,7 @@ (* parse translations *) fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = - if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg) + if c = mark then Syntax.const (suffix sfx name) $ (Abs ("_",dummyT, arg)) else raise TERM ("gen_field_tr: " ^ mark, [t]) | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); @@ -673,11 +671,21 @@ val print_record_type_abbr = ref true; val print_record_type_as_fields = ref true; -fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ (Const ("K_record",_)$t) $ u) = +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) = + let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) + => if null (loose_bnos t) then t else raise Match + | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match + | _ => raise Match) + + (* (case k of (Const ("K_record",_)$t) => t + | Abs (x,_,Const ("K_record",_)$t$Bound 0) => t + | _ => raise Match)*) + in (case try (unsuffix sfx) name_field of SOME name => apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u) | NONE => ([], tm)) + end | gen_field_upds_tr' _ _ tm = ([], tm); fun record_update_tr' tm = @@ -966,6 +974,28 @@ fun has_field extfields f T = exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T); + +fun K_skeleton n (T as Type (_,[_,kT])) (b as Bound i) (Abs (x,xT,t)) = + if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b) + | K_skeleton n T b _ = ((n,T),b); + +(* +fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = + ((n,kT),K_rec$b) + | K_skeleton n _ (Bound i) + (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) = + ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0))) + | K_skeleton n T b _ = ((n,T),b); + *) + +fun normalize_rhs thm = + let + val ss = HOL_basic_ss addsimps K_comp_convs; + val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd; + val _ = tracing ("rhs:"^(Pretty.string_of (Display.pretty_cterm rhs))); + val rhs' = (Simplifier.rewrite ss rhs); + val _ = tracing ("rhs':"^(Pretty.string_of (Display.pretty_thm rhs'))); + in Thm.transitive thm rhs' end; in (* record_simproc *) (* Simplifies selections of an record update: @@ -999,13 +1029,11 @@ let val rv = ("r",rT) val rb = Bound 0 - val kv = ("k",kT) - val kb = Bound 1 + val (kv,kb) = K_skeleton "k" kT (Bound 1) k; in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end | SOME (trm,trm',vars) => let - val kv = ("k",kT) - val kb = Bound (length vars) + val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; in SOME (upd$kb$trm,kb$trm',kv::vars) end) else if has_field extfields u_name rangeS orelse has_field extfields s (domain_type kT) @@ -1013,15 +1041,14 @@ else (case mk_eq_terms r of SOME (trm,trm',vars) => let - val kv = ("k",kT) - val kb = Bound (length vars) + val (kv,kb) = + K_skeleton "k" kT (Bound (length vars)) k; in SOME (upd$kb$trm,trm',kv::vars) end | NONE => let val rv = ("r",rT) val rb = Bound 0 - val kv = ("k",kT) - val kb = Bound 1 + val (kv,kb) = K_skeleton "k" kT (Bound 1) k; in SOME (upd$kb$rb,sel$rb,[kv,rv]) end)) | mk_eq_terms r = NONE in @@ -1061,18 +1088,24 @@ fun grow u uT k kT vars (sprout,skeleton) = if sel_name u = moreN - then let val kv = ("k", kT); - val kb = Bound (length vars); + then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end else ((sprout,skeleton),vars); - fun is_upd_same (sprout,skeleton) u - ((K_rec as Const ("Record.K_record",_))$ - ((sel as Const (s,_))$r)) = + + fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) = + if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE + | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) = + (* eta expanded variant *) + if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE + | dest_k _ = NONE; + + fun is_upd_same (sprout,skeleton) u k = + (case dest_k k of SOME (x,T,sel,s,r) => if (unsuffix updateN u) = s andalso (seed s sprout) = r - then SOME (K_rec,sel,seed s skeleton) + then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton) else NONE - | is_upd_same _ _ _ = NONE + | NONE => NONE); fun init_seed r = ((r,Bound 0), [("r", rT)]); @@ -1111,15 +1144,13 @@ Init ((sprout,skel),vars) => let val n = sel_name u; - val kv = (n, kT); - val kb = Bound (length vars); + val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel); in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end | Inter (trm,trm',vars,fmaps,sprout) => let val n = sel_name u; - val kv = (n, kT); - val kb = Bound (length vars); + val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; val (sprout',vars') = grow u uT k kT (kv::vars) sprout; in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') end) @@ -1130,26 +1161,25 @@ SOME (K_rec,sel,skel') => let val (sprout',vars') = grow u uT k kT vars (sprout,skel); - in Inter(upd$(K_rec$(sel$skel'))$skel,skel,vars',[],sprout') + in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout') end | NONE => let - val kv = (sel_name u, kT); - val kb = Bound (length vars); + val n = sel_name u; + val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) | Inter (trm,trm',vars,fmaps,sprout) => (case is_upd_same sprout u k of SOME (K_rec,sel,skel) => let val (sprout',vars') = grow u uT k kT vars sprout - in Inter(upd$(K_rec$(sel$skel))$trm,trm',vars',fmaps,sprout') + in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout') end | NONE => let val n = sel_name u val T = domain_type kT - val kv = (n, kT) - val kb = Bound (length vars) + val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; val (sprout',vars') = grow u uT k kT (kv::vars) sprout val fmaps' = add n kb fmaps in Inter (upd$kb$trm,upd$comps n T fmaps'$trm' @@ -1160,8 +1190,9 @@ in (case mk_updterm updates [] t of Inter (trm,trm',vars,_,_) - => SOME (prove_split_simp thy ss rT - (list_all(vars,(equals rT$trm$trm')))) + => SOME (normalize_rhs + (prove_split_simp thy ss rT + (list_all(vars,(equals rT$trm$trm'))))) | _ => NONE) end | _ => NONE))