field-update in records is generalised to take a function on the field
authorschirmer
Tue Nov 07 18:25:48 2006 +0100 (2006-11-07)
changeset 21226a607ae87ee81
parent 21225 bf0b1e62cf60
child 21227 76d6d445d69b
field-update in records is generalised to take a function on the field
rather than the new value.
NEWS
src/HOL/HoareParallel/OG_Syntax.thy
src/HOL/HoareParallel/RG_Syntax.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/HoareEx.thy
src/HOL/Record.thy
src/HOL/Tools/record_package.ML
src/HOL/Unix/Unix.thy
     1.1 --- a/NEWS	Tue Nov 07 18:14:53 2006 +0100
     1.2 +++ b/NEWS	Tue Nov 07 18:25:48 2006 +0100
     1.3 @@ -476,6 +476,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Records: generalised field-update to take a function on the field 
     1.8 +rather than the new value: r(|A := x|) is translated to A_update (K x) r
     1.9 +The K-combinator that is internally used is called K_record.
    1.10 +INCOMPATIBILITY: Usage of the plain update functions has to be
    1.11 +adapted.
    1.12 + 
    1.13  * axclass "semiring_0" now contains annihilation axioms 
    1.14  ("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer 
    1.15  structures do not inherit from semiring_0 anymore, because this property 
     2.1 --- a/src/HOL/HoareParallel/OG_Syntax.thy	Tue Nov 07 18:14:53 2006 +0100
     2.2 +++ b/src/HOL/HoareParallel/OG_Syntax.thy	Tue Nov 07 18:25:48 2006 +0100
     2.3 @@ -10,8 +10,8 @@
     2.4    "_AnnAssign"   :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
     2.5  
     2.6  translations
     2.7 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x a)\<guillemotright>"
     2.8 -  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x a)\<guillemotright>"
     2.9 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
    2.10 +  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
    2.11  
    2.12  syntax
    2.13    "_AnnSkip"     :: "'a assn \<Rightarrow> 'a ann_com"              ("_//SKIP" [90] 63)
    2.14 @@ -105,12 +105,12 @@
    2.15        | update_name_tr' (Const x) = Const (upd_tr' x)
    2.16        | update_name_tr' _ = raise Match;
    2.17  
    2.18 -    fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) =
    2.19 +    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    2.20            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    2.21              (Abs (x, dummyT, t) :: ts)
    2.22        | assign_tr' _ = raise Match;
    2.23  
    2.24 -    fun annassign_tr' (r :: Abs (x, _, f $ t $ Bound 0) :: ts) =
    2.25 +    fun annassign_tr' (r :: Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    2.26            quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
    2.27              (Abs (x, dummyT, t) :: ts)
    2.28        | annassign_tr' _ = raise Match;
     3.1 --- a/src/HOL/HoareParallel/RG_Syntax.thy	Tue Nov 07 18:14:53 2006 +0100
     3.2 +++ b/src/HOL/HoareParallel/RG_Syntax.thy	Tue Nov 07 18:25:48 2006 +0100
     3.3 @@ -16,7 +16,7 @@
     3.4    "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
     3.5  
     3.6  translations
     3.7 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x a)\<guillemotright>"
     3.8 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
     3.9    "SKIP" \<rightleftharpoons> "Basic id"
    3.10    "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
    3.11    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    3.12 @@ -78,7 +78,7 @@
    3.13        | update_name_tr' (Const x) = Const (upd_tr' x)
    3.14        | update_name_tr' _ = raise Match;
    3.15  
    3.16 -    fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) =
    3.17 +    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    3.18            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    3.19              (Abs (x, dummyT, t) :: ts)
    3.20        | assign_tr' _ = raise Match;
     4.1 --- a/src/HOL/Isar_examples/Hoare.thy	Tue Nov 07 18:14:53 2006 +0100
     4.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Tue Nov 07 18:25:48 2006 +0100
     4.3 @@ -228,8 +228,8 @@
     4.4  
     4.5  translations
     4.6    ".{b}."                   => "Collect .(b)."
     4.7 -  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x a) \<in> B}."
     4.8 -  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."
     4.9 +  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
    4.10 +  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (K_record a)))."
    4.11    "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
    4.12    "WHILE b INV i DO c OD"   => "While .{b}. i c"
    4.13    "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
    4.14 @@ -270,7 +270,7 @@
    4.15        | update_name_tr' (Const x) = Const (upd_tr' x)
    4.16        | update_name_tr' _ = raise Match;
    4.17  
    4.18 -    fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) =
    4.19 +    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    4.20            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    4.21              (Abs (x, dummyT, t) :: ts)
    4.22        | assign_tr' _ = raise Match;
    4.23 @@ -447,7 +447,8 @@
    4.24  
    4.25  method_setup hoare = {*
    4.26    Method.no_args
    4.27 -    (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
    4.28 +    (Method.SIMPLE_METHOD' HEADGOAL 
    4.29 +       (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *}
    4.30    "verification condition generator for Hoare logic"
    4.31  
    4.32  end
     5.1 --- a/src/HOL/Isar_examples/HoareEx.thy	Tue Nov 07 18:14:53 2006 +0100
     5.2 +++ b/src/HOL/Isar_examples/HoareEx.thy	Tue Nov 07 18:25:48 2006 +0100
     5.3 @@ -39,7 +39,7 @@
     5.4  *}
     5.5  
     5.6  lemma
     5.7 -  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
     5.8 +  "|- .{\<acute>(N_update (K_record (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
     5.9    by (rule assign)
    5.10  
    5.11  text {*
     6.1 --- a/src/HOL/Record.thy	Tue Nov 07 18:14:53 2006 +0100
     6.2 +++ b/src/HOL/Record.thy	Tue Nov 07 18:25:48 2006 +0100
     6.3 @@ -17,6 +17,17 @@
     6.4  lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
     6.5    by simp
     6.6  
     6.7 +constdefs K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
     6.8 +"K_record c x \<equiv> c"
     6.9 +
    6.10 +lemma K_record_apply [simp]: "K_record c x = c"
    6.11 +  by (simp add: K_record_def)
    6.12 +
    6.13 +lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
    6.14 +  by (rule ext) (simp add: K_record_apply comp_def)
    6.15 +
    6.16 +lemma K_record_cong [cong]: "K_record c x = K_record c x"
    6.17 +  by (rule refl)
    6.18  
    6.19  subsection {* Concrete record syntax *}
    6.20  
     7.1 --- a/src/HOL/Tools/record_package.ML	Tue Nov 07 18:14:53 2006 +0100
     7.2 +++ b/src/HOL/Tools/record_package.ML	Tue Nov 07 18:25:48 2006 +0100
     7.3 @@ -5,6 +5,7 @@
     7.4  Extensible records with structural subtyping in HOL.
     7.5  *)
     7.6  
     7.7 +
     7.8  signature BASIC_RECORD_PACKAGE =
     7.9  sig
    7.10    val record_simproc: simproc
    7.11 @@ -54,8 +55,8 @@
    7.12  val meta_allE = thm "Pure.meta_allE";
    7.13  val prop_subst = thm "prop_subst";
    7.14  val Pair_sel_convs = [fst_conv,snd_conv];
    7.15 -
    7.16 -
    7.17 +val K_record_apply = thm "Record.K_record_apply";
    7.18 +val K_comp_convs = [o_apply,K_record_apply]
    7.19  
    7.20  (** name components **)
    7.21  
    7.22 @@ -73,6 +74,7 @@
    7.23  val fields_selN = "fields";
    7.24  val extendN = "extend";
    7.25  val truncateN = "truncate";
    7.26 +val KN = "Record.K_record";
    7.27  
    7.28  (*see typedef_package.ML*)
    7.29  val RepN = "Rep_";
    7.30 @@ -86,11 +88,29 @@
    7.31    let fun varify (a, S) = TVar ((a, midx + 1), S);
    7.32    in map_type_tfree varify end;
    7.33  
    7.34 +fun the_plist (SOME (a,b)) = [a,b]
    7.35 +  | the_plist NONE = raise Option;
    7.36 +
    7.37 +fun domain_type' T =
    7.38 +    domain_type T handle Match => T;
    7.39 +
    7.40 +fun range_type' T =
    7.41 +    range_type T handle Match => T;
    7.42 +
    7.43  (* messages *)
    7.44  
    7.45  val quiet_mode = ref false;
    7.46  fun message s = if ! quiet_mode then () else writeln s;
    7.47  
    7.48 +fun trace_thm str thm =
    7.49 +    tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
    7.50 +
    7.51 +fun trace_thms str thms =
    7.52 +    (tracing str; map (trace_thm "") thms);
    7.53 +
    7.54 +fun trace_term str t =
    7.55 +    tracing (str ^ (Display.raw_string_of_term t));
    7.56 +
    7.57  (* timing *)
    7.58  
    7.59  fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
    7.60 @@ -150,12 +170,13 @@
    7.61  
    7.62  (* updates *)
    7.63  
    7.64 -fun mk_updC sfx sT (c,T) = (suffix sfx c, T --> sT --> sT);
    7.65 +fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT);
    7.66  
    7.67 -fun mk_upd sfx c v s =
    7.68 -  let val sT = fastype_of s;
    7.69 -      val vT = fastype_of v;
    7.70 -  in Const (mk_updC sfx sT (c, vT)) $ v $ s end;
    7.71 +fun mk_upd' sfx c v sT =
    7.72 +  let val vT = domain_type (fastype_of v);
    7.73 +  in Const (mk_updC sfx sT (c, vT)) $ v  end;
    7.74 +
    7.75 +fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s
    7.76  
    7.77  (* types *)
    7.78  
    7.79 @@ -238,7 +259,7 @@
    7.80  
    7.81  structure RecordsData = TheoryDataFun
    7.82  (struct
    7.83 -  val name = "HOL/records";
    7.84 +  val name = "HOL/record"; 
    7.85    type T = record_data;
    7.86  
    7.87    val empty =
    7.88 @@ -480,7 +501,7 @@
    7.89  (* parse translations *)
    7.90  
    7.91  fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
    7.92 -      if c = mark then Syntax.const (suffix sfx name) $ arg
    7.93 +      if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg)
    7.94        else raise TERM ("gen_field_tr: " ^ mark, [t])
    7.95    | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
    7.96  
    7.97 @@ -616,22 +637,24 @@
    7.98        gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
    7.99  
   7.100  
   7.101 -val parse_translation =
   7.102 +val parse_translation = 
   7.103   [("_record_update", record_update_tr),
   7.104    ("_update_name", update_name_tr)];
   7.105  
   7.106 -val adv_parse_translation =
   7.107 +
   7.108 +val adv_parse_translation = 
   7.109   [("_record",adv_record_tr),
   7.110    ("_record_scheme",adv_record_scheme_tr),
   7.111    ("_record_type",adv_record_type_tr),
   7.112    ("_record_type_scheme",adv_record_type_scheme_tr)];
   7.113  
   7.114 +
   7.115  (* print translations *)
   7.116  
   7.117  val print_record_type_abbr = ref true;
   7.118  val print_record_type_as_fields = ref true;
   7.119  
   7.120 -fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   7.121 +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ (Const ("K_record",_)$t) $ u) =
   7.122      (case try (unsuffix sfx) name_field of
   7.123        SOME name =>
   7.124          apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   7.125 @@ -640,8 +663,9 @@
   7.126  
   7.127  fun record_update_tr' tm =
   7.128    let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   7.129 -    Syntax.const "_record_update" $ u $
   7.130 -      foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   7.131 +    if null ts then raise Match
   7.132 +    else Syntax.const "_record_update" $ u $
   7.133 +          foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   7.134    end;
   7.135  
   7.136  fun gen_field_tr' sfx tr' name =
   7.137 @@ -669,13 +693,13 @@
   7.138         | _ => [("",t)])
   7.139  
   7.140      val (flds,(_,more)) = split_last (field_lst t);
   7.141 +    val _ = if null flds then raise Match else ();
   7.142      val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds;
   7.143      val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
   7.144  
   7.145 -  in if null flds then raise Match
   7.146 -     else if unit more
   7.147 -          then Syntax.const record$flds''
   7.148 -          else Syntax.const record_scheme$flds''$more
   7.149 +  in if unit more
   7.150 +     then Syntax.const record$flds''
   7.151 +     else Syntax.const record_scheme$flds''$more
   7.152    end
   7.153  
   7.154  fun gen_record_tr' name =
   7.155 @@ -830,6 +854,77 @@
   7.156        then noopt ()
   7.157        else opt ();
   7.158  
   7.159 +local
   7.160 +fun abstract_over_fun_app (Abs (f,fT,t)) =
   7.161 +  let
   7.162 +     val (f',t') = Term.dest_abs (f,fT,t);
   7.163 +     val T = domain_type fT;
   7.164 +     val (x,T') = hd (Term.variant_frees t' [("x",T)]);
   7.165 +     val f_x = Free (f',fT)$(Free (x,T'));
   7.166 +     fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
   7.167 +       | is_constr _ = false;
   7.168 +     fun subst (t as u$w) = if Free (f',fT)=u 
   7.169 +                            then if is_constr w then f_x 
   7.170 +                                 else raise TERM ("abstract_over_fun_app",[t])
   7.171 +                            else subst u$subst w
   7.172 +       | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
   7.173 +       | subst t = t
   7.174 +     val t'' = abstract_over (f_x,subst t');
   7.175 +     val vars = strip_qnt_vars "all" t'';
   7.176 +     val bdy = strip_qnt_body "all" t'';
   7.177 +     
   7.178 +  in list_abs ((x,T')::vars,bdy) end
   7.179 +  | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
   7.180 +(* Generates a theorem of the kind:
   7.181 + * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* 
   7.182 + *) 
   7.183 +fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
   7.184 +  let
   7.185 +    val rT = domain_type fT;
   7.186 +    val vars = Term.strip_qnt_vars "all" t;
   7.187 +    val Ts = map snd vars;
   7.188 +    val n = length vars;
   7.189 +    fun app_bounds 0 t = t$Bound 0
   7.190 +      | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
   7.191 +
   7.192 +   
   7.193 +    val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
   7.194 +    val prop = Logic.mk_equals
   7.195 +                (list_all ((f,fT)::vars,
   7.196 +                           app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
   7.197 +                 list_all ((fst r,rT)::vars,
   7.198 +                           app_bounds (n - 1) ((Free P)$Bound n))); 
   7.199 +    val prove_standard = quick_and_dirty_prove true thy;
   7.200 +    val thm = prove_standard [] prop (fn prems =>
   7.201 +	 EVERY [rtac equal_intr_rule 1, 
   7.202 +                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
   7.203 +                norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   7.204 +  in thm end
   7.205 +  | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
   7.206 +
   7.207 +in
   7.208 +(* During proof of theorems produced by record_simproc you can end up in
   7.209 + * situations like "!!f ... . ... f r ..." where f is an extension update function.
   7.210 + * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the
   7.211 + * usual split rules for extensions can apply.
   7.212 + *)
   7.213 +val record_split_f_more_simproc =
   7.214 +  Simplifier.simproc HOL.thy "record_split_f_more_simp" ["x"]
   7.215 +    (fn thy => fn _ => fn t =>
   7.216 +      (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
   7.217 +                  (trm as Abs _) =>
   7.218 +         (case rec_id (~1) T of
   7.219 +            "" => NONE
   7.220 +          | n => if T=T'  
   7.221 +                 then (let
   7.222 +                        val P=cterm_of thy (abstract_over_fun_app trm); 
   7.223 +                        val thm = mk_fun_apply_eq trm thy;
   7.224 +                        val PV = cterm_of thy (hd (term_vars (prop_of thm)));
   7.225 +                        val thm' = cterm_instantiate [(PV,P)] thm;
   7.226 +                       in SOME  thm' end handle TERM _ => NONE)
   7.227 +                else NONE) 
   7.228 +       | _ => NONE))
   7.229 +end
   7.230  
   7.231  fun prove_split_simp thy ss T prop =
   7.232    let
   7.233 @@ -842,9 +937,12 @@
   7.234                       all_thm::(case extsplits of [thm] => [] | _ => extsplits)
   7.235                                (* [thm] is the same as all_thm *)
   7.236                   | NONE => extsplits)
   7.237 +    val thms'=K_comp_convs@thms;
   7.238 +    val ss' = (Simplifier.inherit_context ss simpset 
   7.239 +                addsimps thms'
   7.240 +                addsimprocs [record_split_f_more_simproc]);
   7.241    in
   7.242 -    quick_and_dirty_prove true thy [] prop
   7.243 -      (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1)
   7.244 +    quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1)
   7.245    end;
   7.246  
   7.247  
   7.248 @@ -856,10 +954,10 @@
   7.249  in
   7.250  (* record_simproc *)
   7.251  (* Simplifies selections of an record update:
   7.252 - *  (1)  S (r(|S:=k|)) = k respectively
   7.253 - *  (2)  S (r(|X:=k|)) = S r
   7.254 + *  (1)  S (S_update k r) = k (S r)
   7.255 + *  (2)  S (X_update k r) = S r
   7.256   * The simproc skips multiple updates at once, eg:
   7.257 - *  S (r (|S:=k,X:=2,Y:=3|)) = k
   7.258 + *  S (X_update x (Y_update y (S_update k r))) = k (S r)
   7.259   * But be careful in (2) because of the extendibility of records.
   7.260   * - If S is a more-selector we have to make sure that the update on component
   7.261   *   X does not affect the selected subrecord.
   7.262 @@ -881,37 +979,41 @@
   7.263                       NONE => NONE
   7.264                     | SOME u_name
   7.265                       => if u_name = s
   7.266 -                        then let
   7.267 -                               val rv = ("r",rT)
   7.268 -                               val rb = Bound 0
   7.269 -                               val kv = ("k",kT)
   7.270 -                               val kb = Bound 1
   7.271 -                             in SOME (upd$kb$rb,kb,[kv,rv],true) end
   7.272 +                        then (case mk_eq_terms r of 
   7.273 +                               NONE => 
   7.274 +                                 let
   7.275 +                                   val rv = ("r",rT)
   7.276 +                                   val rb = Bound 0
   7.277 +                                   val kv = ("k",kT)
   7.278 +                                   val kb = Bound 1
   7.279 +                                  in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end
   7.280 +                              | SOME (trm,trm',vars) =>
   7.281 +                                 let
   7.282 +                                   val kv = ("k",kT)
   7.283 +                                   val kb = Bound (length vars)
   7.284 +                                 in SOME (upd$kb$trm,kb$trm',kv::vars) end)
   7.285                          else if has_field extfields u_name rangeS
   7.286 -                             orelse has_field extfields s kT
   7.287 +                             orelse has_field extfields s (domain_type kT)
   7.288                               then NONE
   7.289                               else (case mk_eq_terms r of
   7.290 -                                     SOME (trm,trm',vars,update_s)
   7.291 +                                     SOME (trm,trm',vars)
   7.292                                       => let
   7.293                                            val kv = ("k",kT)
   7.294                                            val kb = Bound (length vars)
   7.295 -                                        in SOME (upd$kb$trm,trm',kv::vars,update_s) end
   7.296 +                                        in SOME (upd$kb$trm,trm',kv::vars) end
   7.297                                     | NONE
   7.298                                       => let
   7.299                                            val rv = ("r",rT)
   7.300                                            val rb = Bound 0
   7.301                                            val kv = ("k",kT)
   7.302                                            val kb = Bound 1
   7.303 -                                        in SOME (upd$kb$rb,rb,[kv,rv],false) end))
   7.304 +                                        in SOME (upd$kb$rb,sel$rb,[kv,rv]) end))
   7.305                  | mk_eq_terms r = NONE
   7.306              in
   7.307                (case mk_eq_terms (upd$k$r) of
   7.308 -                 SOME (trm,trm',vars,update_s)
   7.309 -                 => if update_s
   7.310 -                    then SOME (prove_split_simp thy ss domS
   7.311 +                 SOME (trm,trm',vars)
   7.312 +                 => SOME (prove_split_simp thy ss domS
   7.313                                   (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
   7.314 -                    else SOME (prove_split_simp thy ss domS
   7.315 -                                 (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
   7.316                 | NONE => NONE)
   7.317              end
   7.318            | NONE => NONE)
   7.319 @@ -920,7 +1022,8 @@
   7.320  
   7.321  (* record_upd_simproc *)
   7.322  (* simplify multiple updates:
   7.323 - *  (1)  "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)"
   7.324 + *  (1)  "N_update y (M_update g (N_update x (M_update f r))) =
   7.325 +          (N_update (y o x) (M_update (g o f) r))"
   7.326   *  (2)  "r(|M:= M r|) = r"
   7.327   * For (2) special care of "more" updates has to be taken:
   7.328   *    r(|more := m; A := A r|)
   7.329 @@ -938,7 +1041,7 @@
   7.330               fun sel_name u = NameSpace.base (unsuffix updateN u);
   7.331  
   7.332               fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   7.333 -                  if has_field extfields s mT then upd else seed s r
   7.334 +                  if has_field extfields s (domain_type' mT) then upd else seed s r
   7.335                 | seed _ r = r;
   7.336  
   7.337               fun grow u uT k kT vars (sprout,skeleton) =
   7.338 @@ -948,14 +1051,27 @@
   7.339                          in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
   7.340                     else ((sprout,skeleton),vars);
   7.341  
   7.342 -             fun is_upd_same (sprout,skeleton) u ((sel as Const (s,_))$r) =
   7.343 +             fun is_upd_same (sprout,skeleton) u 
   7.344 +                                ((K_rec as Const ("Record.K_record",_))$
   7.345 +                                  ((sel as Const (s,_))$r)) =
   7.346                     if (unsuffix updateN u) = s andalso (seed s sprout) = r
   7.347 -                   then SOME (sel,seed s skeleton)
   7.348 +                   then SOME (K_rec,sel,seed s skeleton)
   7.349                     else NONE
   7.350                 | is_upd_same _ _ _ = NONE
   7.351  
   7.352               fun init_seed r = ((r,Bound 0), [("r", rT)]);
   7.353  
   7.354 +             fun add (n:string) f fmaps = 
   7.355 +               (case AList.lookup (op =) fmaps n of
   7.356 +                  NONE => AList.update (op =) (n,[f]) fmaps
   7.357 +                | SOME fs => AList.update (op =) (n,f::fs) fmaps) 
   7.358 +
   7.359 +             fun comps (n:string) T fmaps = 
   7.360 +               (case AList.lookup (op =) fmaps n of
   7.361 +                 SOME fs => 
   7.362 +                   foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
   7.363 +                | NONE => error ("record_upd_simproc.comps"))
   7.364 +             
   7.365               (* mk_updterm returns either
   7.366                *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
   7.367                *     where vars are the bound variables in the skeleton
   7.368 @@ -979,52 +1095,61 @@
   7.369                           then (case (rest already r) of
   7.370                                   Init ((sprout,skel),vars) =>
   7.371                                   let
   7.372 -                                   val kv = (sel_name u, kT);
   7.373 +                                   val n = sel_name u;
   7.374 +                                   val kv = (n, kT);
   7.375                                     val kb = Bound (length vars);
   7.376                                     val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel);
   7.377 -                                 in Inter (upd$kb$skel,skel,vars',sprout') end
   7.378 -                               | Inter (trm,trm',vars,sprout) =>
   7.379 +                                 in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end
   7.380 +                               | Inter (trm,trm',vars,fmaps,sprout) =>
   7.381                                   let
   7.382 -                                   val kv = (sel_name u, kT);
   7.383 +                                   val n = sel_name u;
   7.384 +                                   val kv = (n, kT);
   7.385                                     val kb = Bound (length vars);
   7.386                                     val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
   7.387 -                                 in Inter(upd$kb$trm,trm',kv::vars',sprout') end)
   7.388 +                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') 
   7.389 +                                 end)
   7.390                           else
   7.391                            (case rest (u::already) r of
   7.392                               Init ((sprout,skel),vars) =>
   7.393                                (case is_upd_same (sprout,skel) u k of
   7.394 -                                 SOME (sel,skel') =>
   7.395 +                                 SOME (K_rec,sel,skel') =>
   7.396                                   let
   7.397                                     val (sprout',vars') = grow u uT k kT vars (sprout,skel);
   7.398 -                                  in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end
   7.399 +                                  in Inter(upd$(K_rec$(sel$skel'))$skel,skel,vars',[],sprout')
   7.400 +                                  end
   7.401                                 | NONE =>
   7.402                                   let
   7.403                                     val kv = (sel_name u, kT);
   7.404                                     val kb = Bound (length vars);
   7.405                                   in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
   7.406 -                           | Inter (trm,trm',vars,sprout) =>
   7.407 +                           | Inter (trm,trm',vars,fmaps,sprout) =>
   7.408                                 (case is_upd_same sprout u k of
   7.409 -                                  SOME (sel,skel) =>
   7.410 +                                  SOME (K_rec,sel,skel) =>
   7.411                                    let
   7.412                                      val (sprout',vars') = grow u uT k kT vars sprout
   7.413 -                                  in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end
   7.414 +                                  in Inter(upd$(K_rec$(sel$skel))$trm,trm',vars',fmaps,sprout')
   7.415 +                                  end
   7.416                                  | NONE =>
   7.417                                    let
   7.418 -                                    val kv = (sel_name u, kT)
   7.419 +                                    val n = sel_name u
   7.420 +                                    val T = domain_type kT
   7.421 +                                    val kv = (n, kT)
   7.422                                      val kb = Bound (length vars)
   7.423                                      val (sprout',vars') = grow u uT k kT (kv::vars) sprout
   7.424 -                                  in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end))
   7.425 -                      end
   7.426 +                                    val fmaps' = add n kb fmaps 
   7.427 +                                  in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
   7.428 +                                           ,vars',fmaps',sprout') end))
   7.429 +                     end
   7.430                   else Init (init_seed t)
   7.431                 | mk_updterm _ _ t = Init (init_seed t);
   7.432  
   7.433           in (case mk_updterm updates [] t of
   7.434 -               Inter (trm,trm',vars,_)
   7.435 +               Inter (trm,trm',vars,_,_)
   7.436                  => SOME (prove_split_simp thy ss rT
   7.437                            (list_all(vars,(equals rT$trm$trm'))))
   7.438               | _ => NONE)
   7.439 -         end
   7.440 -       | _ => NONE));
   7.441 +         end 
   7.442 +       | _ => NONE))
   7.443  end
   7.444  
   7.445  (* record_eq_simproc *)
   7.446 @@ -1172,9 +1297,9 @@
   7.447      val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
   7.448  
   7.449      val simprocs = if has_rec goal then [record_split_simproc P] else [];
   7.450 -
   7.451 +    val thms' = K_comp_convs@thms
   7.452    in st |> ((EVERY split_frees_tacs)
   7.453 -           THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms addsimprocs simprocs) i))
   7.454 +           THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i))
   7.455    end handle Empty => Seq.empty;
   7.456  end;
   7.457  
   7.458 @@ -1307,6 +1432,7 @@
   7.459    let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
   7.460    in #1 (Library.foldl f (([],[],convs),refls)) end;
   7.461  
   7.462 +
   7.463  fun extension_definition full name fields names alphas zeta moreT more vars thy =
   7.464    let
   7.465      val base = Sign.base_name;
   7.466 @@ -1354,10 +1480,11 @@
   7.467      val upd_decls = map (mk_updC updN extT) bfields_more;
   7.468      fun mk_upd_spec (c,T) =
   7.469        let
   7.470 -        val args = map (fn (n,nT) => if n=c then Free (base c,T)
   7.471 +        val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$
   7.472 +                                                  (mk_sel r (suffix ext_dest n,nT))
   7.473                                       else (mk_sel r (suffix ext_dest n,nT)))
   7.474                         fields_more;
   7.475 -      in Const (mk_updC updN extT (c,T))$(Free (base c,T))$r
   7.476 +      in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r
   7.477            :== mk_ext args
   7.478        end;
   7.479      val upd_specs = map mk_upd_spec fields_more;
   7.480 @@ -1409,8 +1536,8 @@
   7.481  
   7.482      (*updates*)
   7.483      fun mk_upd_prop (i,(c,T)) =
   7.484 -      let val x' = Free (Name.variant variants (base c ^ "'"),T)
   7.485 -          val args' = nth_map i (K x') vars_more
   7.486 +      let val x' = Free (Name.variant variants (base c ^ "'"),T --> T)
   7.487 +          val args' = nth_map i  (K (x'$nth vars_more i)) vars_more
   7.488        in mk_upd updN c x' ext === mk_ext args'  end;
   7.489      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   7.490  
   7.491 @@ -1476,11 +1603,14 @@
   7.492                                         upd_conv_props;
   7.493      fun upd_convs_prf_opt () =
   7.494        let
   7.495 +
   7.496          fun mkrefl (c,T) = Thm.reflexive
   7.497 -                            (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T)));
   7.498 +                    (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T)));
   7.499          val refls = map mkrefl fields_more;
   7.500 +        val dest_convs' = map mk_meta_eq dest_convs;
   7.501 +        val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
   7.502 +        
   7.503          val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
   7.504 -        val dest_convs' = map mk_meta_eq dest_convs;
   7.505  
   7.506          fun mkthm (udef,(fld_refl,thms)) =
   7.507            let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
   7.508 @@ -1491,12 +1621,12 @@
   7.509                    (|N=N,M=M,K=K',more=more|)
   7.510                  *)
   7.511                val (_$(_$v$r)$_) = prop_of udef;
   7.512 -              val (_$v'$_) = prop_of fld_refl;
   7.513 +              val (_$(v'$_)$_) = prop_of fld_refl;
   7.514                val udef' = cterm_instantiate
   7.515                              [(cterm_of defs_thy v,cterm_of defs_thy v'),
   7.516                               (cterm_of defs_thy r,cterm_of defs_thy ext)] udef;
   7.517            in  standard (Thm.transitive udef' bdyeq) end;
   7.518 -      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' refls)) end;
   7.519 +      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' map_eqs)) end;
   7.520  
   7.521      val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt;
   7.522  
   7.523 @@ -1517,7 +1647,9 @@
   7.524                  REPEAT (etac meta_allE 1), atac 1]);
   7.525      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   7.526  
   7.527 -    val (([inject',induct',cases',surjective',split_meta'], [dest_convs',upd_convs']),
   7.528 +
   7.529 +    val (([inject',induct',cases',surjective',split_meta'], 
   7.530 +          [dest_convs',upd_convs']),
   7.531        thm_thy) =
   7.532        defs_thy
   7.533        |> (PureThy.add_thms o map Thm.no_attributes)
   7.534 @@ -1714,7 +1846,7 @@
   7.535           else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
   7.536  
   7.537      fun parent_more_upd v s =
   7.538 -      if null parents then v
   7.539 +      if null parents then v$s
   7.540        else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
   7.541             in mk_upd updateN mp v s end;
   7.542  
   7.543 @@ -1733,8 +1865,8 @@
   7.544  
   7.545      fun mk_upd_spec (c,T) =
   7.546        let
   7.547 -        val new = mk_upd updN c (Free (base c,T)) (parent_more r0);
   7.548 -      in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T))$r0
   7.549 +        val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*);
   7.550 +      in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0
   7.551            :== (parent_more_upd new r0)
   7.552        end;
   7.553      val upd_specs = map mk_upd_spec fields_more;
   7.554 @@ -1787,8 +1919,9 @@
   7.555  
   7.556      (*updates*)
   7.557      fun mk_upd_prop (i,(c,T)) =
   7.558 -      let val x' = Free (Name.variant all_variants (base c ^ "'"),T)
   7.559 -          val args' = nth_map (parent_fields_len + i) (K x') all_vars_more
   7.560 +      let val x' = Free (Name.variant all_variants (base c ^ "'"),T-->T);
   7.561 +          val n = parent_fields_len + i;
   7.562 +          val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more
   7.563        in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
   7.564      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   7.565  
   7.566 @@ -2127,7 +2260,7 @@
   7.567    P.type_args -- P.name --
   7.568      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
   7.569  
   7.570 -val recordP =
   7.571 +val recordP =  
   7.572    OuterSyntax.command "record" "define extensible record" K.thy_decl
   7.573      (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
   7.574  
     8.1 --- a/src/HOL/Unix/Unix.thy	Tue Nov 07 18:14:53 2006 +0100
     8.2 +++ b/src/HOL/Unix/Unix.thy	Tue Nov 07 18:25:48 2006 +0100
     8.3 @@ -370,7 +370,7 @@
     8.4      "access root path uid {} = Some file \<Longrightarrow>
     8.5        uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
     8.6        root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
     8.7 -        (Some (map_attributes (others_update perms) file)) root"
     8.8 +        (Some (map_attributes (others_update (K_record perms)) file)) root"
     8.9  
    8.10    creat:
    8.11      "path = parent_path @ [name] \<Longrightarrow>