--- a/src/HOL/HoareParallel/OG_Syntax.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/HoareParallel/OG_Syntax.thy Wed Dec 19 16:32:14 2007 +0100
@@ -10,8 +10,8 @@
"_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
translations
- "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
- "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
+ "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
syntax
"_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
@@ -105,14 +105,18 @@
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
+ fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' _ = raise Match;
+
+ fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
- fun annassign_tr' (r :: Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
+ fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| annassign_tr' _ = raise Match;
fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] =
--- a/src/HOL/HoareParallel/RG_Syntax.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/HoareParallel/RG_Syntax.thy Wed Dec 19 16:32:14 2007 +0100
@@ -16,7 +16,7 @@
"_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61)
translations
- "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
+ "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
"SKIP" \<rightleftharpoons> "Basic id"
"c1;; c2" \<rightleftharpoons> "Seq c1 c2"
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
@@ -78,9 +78,13 @@
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"}, _)$t) $ Bound 0) :: ts) =
+ fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' _ = raise Match;
+
+ fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[("Collect", assert_tr'), ("Basic", assign_tr'),
--- a/src/HOL/Isar_examples/Hoare.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Wed Dec 19 16:32:14 2007 +0100
@@ -228,8 +228,8 @@
translations
".{b}." => "Collect .(b)."
- "B [a/\<acute>x]" => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
- "\<acute>x := a" => "Basic .(\<acute>(_update_name x (K_record a)))."
+ "B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
+ "\<acute>x := a" => "Basic .(\<acute>(_update_name x (\<lambda>_. 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,9 +270,13 @@
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
+ fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ | K_tr' _ = raise Match;
+
+ fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
- (Abs (x, dummyT, t) :: ts)
+ (Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[("Collect", assert_tr'), ("Basic", assign_tr'),
@@ -447,7 +451,7 @@
method_setup hoare = {*
Method.no_args
(Method.SIMPLE_METHOD'
- (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_apply"}] )))) *}
+ (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] )))) *}
"verification condition generator for Hoare logic"
end
--- a/src/HOL/Isar_examples/HoareEx.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy Wed Dec 19 16:32:14 2007 +0100
@@ -39,7 +39,7 @@
*}
lemma
- "|- .{\<acute>(N_update (K_record (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+ "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
by (rule assign)
text {*
--- a/src/HOL/Unix/Unix.thy Wed Dec 19 16:32:12 2007 +0100
+++ b/src/HOL/Unix/Unix.thy Wed Dec 19 16:32:14 2007 +0100
@@ -366,7 +366,7 @@
"access root path uid {} = Some file \<Longrightarrow>
uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
- (Some (map_attributes (others_update (K_record perms)) file)) root" |
+ (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root" |
creat:
"path = parent_path @ [name] \<Longrightarrow>