# HG changeset patch
# User schirmer
# Date 1198078334 -3600
# Node ID 45d090186bbe832b37164bb7c6bb3110a13b8ab8
# Parent  45a2ffc5911ea2a1daf6274fbd8fca09ed15ab3f
accomodate to replacement of K_record by %x.c

diff -r 45a2ffc5911e -r 45d090186bbe src/HOL/HoareParallel/OG_Syntax.thy
--- 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",_))] = 
diff -r 45a2ffc5911e -r 45d090186bbe src/HOL/HoareParallel/RG_Syntax.thy
--- 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'),
diff -r 45a2ffc5911e -r 45d090186bbe src/HOL/Isar_examples/Hoare.thy
--- 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
diff -r 45a2ffc5911e -r 45d090186bbe src/HOL/Isar_examples/HoareEx.thy
--- 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 {*
diff -r 45a2ffc5911e -r 45d090186bbe src/HOL/Unix/Unix.thy
--- 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>