# HG changeset patch # User schirmer # Date 1162920348 -3600 # Node ID a607ae87ee81cb9a83016eece5f42f0a7b13729e # Parent bf0b1e62cf60b33aba183930900606750853fcfe field-update in records is generalised to take a function on the field rather than the new value. diff -r bf0b1e62cf60 -r a607ae87ee81 NEWS --- a/NEWS Tue Nov 07 18:14:53 2006 +0100 +++ b/NEWS Tue Nov 07 18:25:48 2006 +0100 @@ -476,6 +476,12 @@ *** HOL *** +* Records: generalised field-update to take a function on the field +rather than the new value: r(|A := x|) is translated to A_update (K x) r +The K-combinator that is internally used is called K_record. +INCOMPATIBILITY: Usage of the plain update functions has to be +adapted. + * axclass "semiring_0" now contains annihilation axioms ("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer structures do not inherit from semiring_0 anymore, because this property diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/HoareParallel/OG_Syntax.thy --- a/src/HOL/HoareParallel/OG_Syntax.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/HoareParallel/OG_Syntax.thy Tue Nov 07 18:25:48 2006 +0100 @@ -10,8 +10,8 @@ "_AnnAssign" :: "'a assn \ idt \ 'b \ 'a com" ("(_ \_ :=/ _)" [90,70,65] 61) translations - "\\x := a" \ "Basic \\\(_update_name x a)\" - "r \\x := a" \ "AnnBasic r \\\(_update_name x a)\" + "\\x := a" \ "Basic \\\(_update_name x (K_record a))\" + "r \\x := a" \ "AnnBasic r \\\(_update_name x (K_record a))\" syntax "_AnnSkip" :: "'a assn \ 'a ann_com" ("_//SKIP" [90] 63) @@ -105,12 +105,12 @@ | update_name_tr' (Const x) = Const (upd_tr' x) | update_name_tr' _ = raise Match; - fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) = + fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) (Abs (x, dummyT, t) :: ts) | assign_tr' _ = raise Match; - fun annassign_tr' (r :: Abs (x, _, f $ t $ Bound 0) :: ts) = + fun annassign_tr' (r :: Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f) (Abs (x, dummyT, t) :: ts) | annassign_tr' _ = raise Match; diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/HoareParallel/RG_Syntax.thy --- a/src/HOL/HoareParallel/RG_Syntax.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/HoareParallel/RG_Syntax.thy Tue Nov 07 18:25:48 2006 +0100 @@ -16,7 +16,7 @@ "_Wait" :: "'a bexp \ 'a com" ("(0WAIT _ END)" 61) translations - "\\x := a" \ "Basic \\\(_update_name x a)\" + "\\x := a" \ "Basic \\\(_update_name x (K_record a))\" "SKIP" \ "Basic id" "c1;; c2" \ "Seq c1 c2" "IF b THEN c1 ELSE c2 FI" \ "Cond .{b}. c1 c2" @@ -78,7 +78,7 @@ | update_name_tr' (Const x) = Const (upd_tr' x) | update_name_tr' _ = raise Match; - fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) = + fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) (Abs (x, dummyT, t) :: ts) | assign_tr' _ = raise Match; diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/Isar_examples/Hoare.thy --- a/src/HOL/Isar_examples/Hoare.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/Isar_examples/Hoare.thy Tue Nov 07 18:25:48 2006 +0100 @@ -228,8 +228,8 @@ translations ".{b}." => "Collect .(b)." - "B [a/\x]" => ".{\(_update_name x a) \ B}." - "\x := a" => "Basic .(\(_update_name x a))." + "B [a/\x]" => ".{\(_update_name x (K_record a)) \ B}." + "\x := a" => "Basic .(\(_update_name x (K_record a)))." "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2" "WHILE b INV i DO c OD" => "While .{b}. i c" "WHILE b DO c OD" == "WHILE b INV arbitrary DO c OD" @@ -270,7 +270,7 @@ | update_name_tr' (Const x) = Const (upd_tr' x) | update_name_tr' _ = raise Match; - fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) = + fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) (Abs (x, dummyT, t) :: ts) | assign_tr' _ = raise Match; @@ -447,7 +447,8 @@ method_setup hoare = {* Method.no_args - (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *} + (Method.SIMPLE_METHOD' HEADGOAL + (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *} "verification condition generator for Hoare logic" end diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/Isar_examples/HoareEx.thy --- a/src/HOL/Isar_examples/HoareEx.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/Isar_examples/HoareEx.thy Tue Nov 07 18:25:48 2006 +0100 @@ -39,7 +39,7 @@ *} lemma - "|- .{\(N_update (2 * \N)) : .{\N = 10}.}. \N := 2 * \N .{\N = 10}." + "|- .{\(N_update (K_record (2 * \N))) : .{\N = 10}.}. \N := 2 * \N .{\N = 10}." by (rule assign) text {* diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/Record.thy Tue Nov 07 18:25:48 2006 +0100 @@ -17,6 +17,17 @@ lemma rec_True_simp: "(True \ PROP P) \ PROP P" by simp +constdefs K_record:: "'a \ 'b \ 'a" +"K_record c x \ c" + +lemma K_record_apply [simp]: "K_record c x = c" + by (simp add: K_record_def) + +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) subsection {* Concrete record syntax *} diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Nov 07 18:25:48 2006 +0100 @@ -5,6 +5,7 @@ Extensible records with structural subtyping in HOL. *) + signature BASIC_RECORD_PACKAGE = sig val record_simproc: simproc @@ -54,8 +55,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] (** name components **) @@ -73,6 +74,7 @@ val fields_selN = "fields"; val extendN = "extend"; val truncateN = "truncate"; +val KN = "Record.K_record"; (*see typedef_package.ML*) val RepN = "Rep_"; @@ -86,11 +88,29 @@ let fun varify (a, S) = TVar ((a, midx + 1), S); in map_type_tfree varify end; +fun the_plist (SOME (a,b)) = [a,b] + | the_plist NONE = raise Option; + +fun domain_type' T = + domain_type T handle Match => T; + +fun range_type' T = + range_type T handle Match => T; + (* messages *) val quiet_mode = ref false; fun message s = if ! quiet_mode then () else writeln s; +fun trace_thm str thm = + tracing (str ^ (Pretty.string_of (Display.pretty_thm thm))); + +fun trace_thms str thms = + (tracing str; map (trace_thm "") thms); + +fun trace_term str t = + tracing (str ^ (Display.raw_string_of_term t)); + (* timing *) fun timeit_msg s x = if !timing then (warning s; timeit x) else x (); @@ -150,12 +170,13 @@ (* updates *) -fun mk_updC sfx sT (c,T) = (suffix sfx c, T --> sT --> sT); +fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT); -fun mk_upd sfx c v s = - let val sT = fastype_of s; - val vT = fastype_of v; - in Const (mk_updC sfx sT (c, vT)) $ v $ s end; +fun mk_upd' sfx c v sT = + let val vT = domain_type (fastype_of v); + in Const (mk_updC sfx sT (c, vT)) $ v end; + +fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s (* types *) @@ -238,7 +259,7 @@ structure RecordsData = TheoryDataFun (struct - val name = "HOL/records"; + val name = "HOL/record"; type T = record_data; val empty = @@ -480,7 +501,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) $ arg + if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg) else raise TERM ("gen_field_tr: " ^ mark, [t]) | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); @@ -616,22 +637,24 @@ gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN; -val parse_translation = +val parse_translation = [("_record_update", record_update_tr), ("_update_name", update_name_tr)]; -val adv_parse_translation = + +val adv_parse_translation = [("_record",adv_record_tr), ("_record_scheme",adv_record_scheme_tr), ("_record_type",adv_record_type_tr), ("_record_type_scheme",adv_record_type_scheme_tr)]; + (* print translations *) 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, _) $ t $ u) = +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ (Const ("K_record",_)$t) $ u) = (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) @@ -640,8 +663,9 @@ fun record_update_tr' tm = let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in - Syntax.const "_record_update" $ u $ - foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) + if null ts then raise Match + else Syntax.const "_record_update" $ u $ + foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) end; fun gen_field_tr' sfx tr' name = @@ -669,13 +693,13 @@ | _ => [("",t)]) val (flds,(_,more)) = split_last (field_lst t); + val _ = if null flds then raise Match else (); val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds; val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; - in if null flds then raise Match - else if unit more - then Syntax.const record$flds'' - else Syntax.const record_scheme$flds''$more + in if unit more + then Syntax.const record$flds'' + else Syntax.const record_scheme$flds''$more end fun gen_record_tr' name = @@ -830,6 +854,77 @@ then noopt () else opt (); +local +fun abstract_over_fun_app (Abs (f,fT,t)) = + let + val (f',t') = Term.dest_abs (f,fT,t); + val T = domain_type fT; + val (x,T') = hd (Term.variant_frees t' [("x",T)]); + val f_x = Free (f',fT)$(Free (x,T')); + fun is_constr (Const (c,_)$_) = can (unsuffix extN) c + | is_constr _ = false; + fun subst (t as u$w) = if Free (f',fT)=u + then if is_constr w then f_x + else raise TERM ("abstract_over_fun_app",[t]) + else subst u$subst w + | subst (Abs (x,T,t)) = (Abs (x,T,subst t)) + | subst t = t + val t'' = abstract_over (f_x,subst t'); + val vars = strip_qnt_vars "all" t''; + val bdy = strip_qnt_body "all" t''; + + in list_abs ((x,T')::vars,bdy) end + | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]); +(* Generates a theorem of the kind: + * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* + *) +fun mk_fun_apply_eq (Abs (f, fT, t)) thy = + let + val rT = domain_type fT; + val vars = Term.strip_qnt_vars "all" t; + val Ts = map snd vars; + val n = length vars; + fun app_bounds 0 t = t$Bound 0 + | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t + + + val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)]; + val prop = Logic.mk_equals + (list_all ((f,fT)::vars, + app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))), + list_all ((fst r,rT)::vars, + app_bounds (n - 1) ((Free P)$Bound n))); + val prove_standard = quick_and_dirty_prove true thy; + val thm = prove_standard [] prop (fn prems => + EVERY [rtac equal_intr_rule 1, + norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1, + norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]); + in thm end + | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]); + +in +(* During proof of theorems produced by record_simproc you can end up in + * situations like "!!f ... . ... f r ..." where f is an extension update function. + * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the + * usual split rules for extensions can apply. + *) +val record_split_f_more_simproc = + Simplifier.simproc HOL.thy "record_split_f_more_simp" ["x"] + (fn thy => fn _ => fn t => + (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$ + (trm as Abs _) => + (case rec_id (~1) T of + "" => NONE + | n => if T=T' + then (let + val P=cterm_of thy (abstract_over_fun_app trm); + val thm = mk_fun_apply_eq trm thy; + val PV = cterm_of thy (hd (term_vars (prop_of thm))); + val thm' = cterm_instantiate [(PV,P)] thm; + in SOME thm' end handle TERM _ => NONE) + else NONE) + | _ => NONE)) +end fun prove_split_simp thy ss T prop = let @@ -842,9 +937,12 @@ all_thm::(case extsplits of [thm] => [] | _ => extsplits) (* [thm] is the same as all_thm *) | NONE => extsplits) + val thms'=K_comp_convs@thms; + val ss' = (Simplifier.inherit_context ss simpset + addsimps thms' + addsimprocs [record_split_f_more_simproc]); in - quick_and_dirty_prove true thy [] prop - (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1) + quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1) end; @@ -856,10 +954,10 @@ in (* record_simproc *) (* Simplifies selections of an record update: - * (1) S (r(|S:=k|)) = k respectively - * (2) S (r(|X:=k|)) = S r + * (1) S (S_update k r) = k (S r) + * (2) S (X_update k r) = S r * The simproc skips multiple updates at once, eg: - * S (r (|S:=k,X:=2,Y:=3|)) = k + * S (X_update x (Y_update y (S_update k r))) = k (S r) * But be careful in (2) because of the extendibility of records. * - If S is a more-selector we have to make sure that the update on component * X does not affect the selected subrecord. @@ -881,37 +979,41 @@ NONE => NONE | SOME u_name => if u_name = s - then let - val rv = ("r",rT) - val rb = Bound 0 - val kv = ("k",kT) - val kb = Bound 1 - in SOME (upd$kb$rb,kb,[kv,rv],true) end + then (case mk_eq_terms r of + NONE => + let + val rv = ("r",rT) + val rb = Bound 0 + val kv = ("k",kT) + val kb = Bound 1 + 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) + in SOME (upd$kb$trm,kb$trm',kv::vars) end) else if has_field extfields u_name rangeS - orelse has_field extfields s kT + orelse has_field extfields s (domain_type kT) then NONE else (case mk_eq_terms r of - SOME (trm,trm',vars,update_s) + SOME (trm,trm',vars) => let val kv = ("k",kT) val kb = Bound (length vars) - in SOME (upd$kb$trm,trm',kv::vars,update_s) end + 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 - in SOME (upd$kb$rb,rb,[kv,rv],false) end)) + in SOME (upd$kb$rb,sel$rb,[kv,rv]) end)) | mk_eq_terms r = NONE in (case mk_eq_terms (upd$k$r) of - SOME (trm,trm',vars,update_s) - => if update_s - then SOME (prove_split_simp thy ss domS + SOME (trm,trm',vars) + => SOME (prove_split_simp thy ss domS (list_all(vars,(equals rangeS$(sel$trm)$trm')))) - else SOME (prove_split_simp thy ss domS - (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm'))))) | NONE => NONE) end | NONE => NONE) @@ -920,7 +1022,8 @@ (* record_upd_simproc *) (* simplify multiple updates: - * (1) "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" + * (1) "N_update y (M_update g (N_update x (M_update f r))) = + (N_update (y o x) (M_update (g o f) r))" * (2) "r(|M:= M r|) = r" * For (2) special care of "more" updates has to be taken: * r(|more := m; A := A r|) @@ -938,7 +1041,7 @@ fun sel_name u = NameSpace.base (unsuffix updateN u); fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = - if has_field extfields s mT then upd else seed s r + if has_field extfields s (domain_type' mT) then upd else seed s r | seed _ r = r; fun grow u uT k kT vars (sprout,skeleton) = @@ -948,14 +1051,27 @@ 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 ((sel as Const (s,_))$r) = + fun is_upd_same (sprout,skeleton) u + ((K_rec as Const ("Record.K_record",_))$ + ((sel as Const (s,_))$r)) = if (unsuffix updateN u) = s andalso (seed s sprout) = r - then SOME (sel,seed s skeleton) + then SOME (K_rec,sel,seed s skeleton) else NONE | is_upd_same _ _ _ = NONE fun init_seed r = ((r,Bound 0), [("r", rT)]); + fun add (n:string) f fmaps = + (case AList.lookup (op =) fmaps n of + NONE => AList.update (op =) (n,[f]) fmaps + | SOME fs => AList.update (op =) (n,f::fs) fmaps) + + fun comps (n:string) T fmaps = + (case AList.lookup (op =) fmaps n of + SOME fs => + foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs + | NONE => error ("record_upd_simproc.comps")) + (* mk_updterm returns either * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made, * where vars are the bound variables in the skeleton @@ -979,52 +1095,61 @@ then (case (rest already r) of Init ((sprout,skel),vars) => let - val kv = (sel_name u, kT); + val n = sel_name u; + val kv = (n, kT); val kb = Bound (length vars); val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel); - in Inter (upd$kb$skel,skel,vars',sprout') end - | Inter (trm,trm',vars,sprout) => + in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end + | Inter (trm,trm',vars,fmaps,sprout) => let - val kv = (sel_name u, kT); + val n = sel_name u; + val kv = (n, kT); val kb = Bound (length vars); val (sprout',vars') = grow u uT k kT (kv::vars) sprout; - in Inter(upd$kb$trm,trm',kv::vars',sprout') end) + in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') + end) else (case rest (u::already) r of Init ((sprout,skel),vars) => (case is_upd_same (sprout,skel) u k of - SOME (sel,skel') => + SOME (K_rec,sel,skel') => let val (sprout',vars') = grow u uT k kT vars (sprout,skel); - in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end + 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); in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) - | Inter (trm,trm',vars,sprout) => + | Inter (trm,trm',vars,fmaps,sprout) => (case is_upd_same sprout u k of - SOME (sel,skel) => + SOME (K_rec,sel,skel) => let val (sprout',vars') = grow u uT k kT vars sprout - in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end + in Inter(upd$(K_rec$(sel$skel))$trm,trm',vars',fmaps,sprout') + end | NONE => let - val kv = (sel_name u, kT) + val n = sel_name u + val T = domain_type kT + val kv = (n, kT) val kb = Bound (length vars) val (sprout',vars') = grow u uT k kT (kv::vars) sprout - in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end)) - end + val fmaps' = add n kb fmaps + in Inter (upd$kb$trm,upd$comps n T fmaps'$trm' + ,vars',fmaps',sprout') end)) + end else Init (init_seed t) | mk_updterm _ _ t = Init (init_seed t); in (case mk_updterm updates [] t of - Inter (trm,trm',vars,_) + Inter (trm,trm',vars,_,_) => SOME (prove_split_simp thy ss rT (list_all(vars,(equals rT$trm$trm')))) | _ => NONE) - end - | _ => NONE)); + end + | _ => NONE)) end (* record_eq_simproc *) @@ -1172,9 +1297,9 @@ val split_frees_tacs = List.mapPartial (split_free_tac P i) frees; val simprocs = if has_rec goal then [record_split_simproc P] else []; - + val thms' = K_comp_convs@thms in st |> ((EVERY split_frees_tacs) - THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms addsimprocs simprocs) i)) + THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)) end handle Empty => Seq.empty; end; @@ -1307,6 +1432,7 @@ let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs); in #1 (Library.foldl f (([],[],convs),refls)) end; + fun extension_definition full name fields names alphas zeta moreT more vars thy = let val base = Sign.base_name; @@ -1354,10 +1480,11 @@ val upd_decls = map (mk_updC updN extT) bfields_more; fun mk_upd_spec (c,T) = let - val args = map (fn (n,nT) => if n=c then Free (base c,T) + val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$ + (mk_sel r (suffix ext_dest n,nT)) else (mk_sel r (suffix ext_dest n,nT))) fields_more; - in Const (mk_updC updN extT (c,T))$(Free (base c,T))$r + in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r :== mk_ext args end; val upd_specs = map mk_upd_spec fields_more; @@ -1409,8 +1536,8 @@ (*updates*) fun mk_upd_prop (i,(c,T)) = - let val x' = Free (Name.variant variants (base c ^ "'"),T) - val args' = nth_map i (K x') vars_more + let val x' = Free (Name.variant variants (base c ^ "'"),T --> T) + val args' = nth_map i (K (x'$nth vars_more i)) vars_more in mk_upd updN c x' ext === mk_ext args' end; val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); @@ -1476,11 +1603,14 @@ upd_conv_props; fun upd_convs_prf_opt () = let + fun mkrefl (c,T) = Thm.reflexive - (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T))); + (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T))); val refls = map mkrefl fields_more; + val dest_convs' = map mk_meta_eq dest_convs; + val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs'); + val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext)); - val dest_convs' = map mk_meta_eq dest_convs; fun mkthm (udef,(fld_refl,thms)) = let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms); @@ -1491,12 +1621,12 @@ (|N=N,M=M,K=K',more=more|) *) val (_$(_$v$r)$_) = prop_of udef; - val (_$v'$_) = prop_of fld_refl; + val (_$(v'$_)$_) = prop_of fld_refl; val udef' = cterm_instantiate [(cterm_of defs_thy v,cterm_of defs_thy v'), (cterm_of defs_thy r,cterm_of defs_thy ext)] udef; in standard (Thm.transitive udef' bdyeq) end; - in map mkthm (rev upd_defs ~~ (mixit dest_convs' refls)) end; + in map mkthm (rev upd_defs ~~ (mixit dest_convs' map_eqs)) end; val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt; @@ -1517,7 +1647,9 @@ REPEAT (etac meta_allE 1), atac 1]); val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; - val (([inject',induct',cases',surjective',split_meta'], [dest_convs',upd_convs']), + + val (([inject',induct',cases',surjective',split_meta'], + [dest_convs',upd_convs']), thm_thy) = defs_thy |> (PureThy.add_thms o map Thm.no_attributes) @@ -1714,7 +1846,7 @@ else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT); fun parent_more_upd v s = - if null parents then v + if null parents then v$s else let val mp = NameSpace.qualified (#name (List.last parents)) moreN; in mk_upd updateN mp v s end; @@ -1733,8 +1865,8 @@ fun mk_upd_spec (c,T) = let - val new = mk_upd updN c (Free (base c,T)) (parent_more r0); - in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T))$r0 + val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*); + in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0 :== (parent_more_upd new r0) end; val upd_specs = map mk_upd_spec fields_more; @@ -1787,8 +1919,9 @@ (*updates*) fun mk_upd_prop (i,(c,T)) = - let val x' = Free (Name.variant all_variants (base c ^ "'"),T) - val args' = nth_map (parent_fields_len + i) (K x') all_vars_more + let val x' = Free (Name.variant all_variants (base c ^ "'"),T-->T); + val n = parent_fields_len + i; + val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); @@ -2127,7 +2260,7 @@ P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); -val recordP = +val recordP = OuterSyntax.command "record" "define extensible record" K.thy_decl (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); diff -r bf0b1e62cf60 -r a607ae87ee81 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Tue Nov 07 18:14:53 2006 +0100 +++ b/src/HOL/Unix/Unix.thy Tue Nov 07 18:25:48 2006 +0100 @@ -370,7 +370,7 @@ "access root path uid {} = Some file \ uid = 0 \ uid = owner (attributes file) \ root \(Chmod uid perms path)\ update path - (Some (map_attributes (others_update perms) file)) root" + (Some (map_attributes (others_update (K_record perms)) file)) root" creat: "path = parent_path @ [name] \