reverted to classical syntax for K_record
authorhaftmann
Fri Apr 20 17:58:25 2007 +0200 (2007-04-20)
changeset 22759e4a3f49eb924
parent 22758 a7790c8e3c14
child 22760 6eafeffe801c
reverted to classical syntax for K_record
src/HOL/HoareParallel/OG_Syntax.thy
src/HOL/HoareParallel/RG_Syntax.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Record.thy
     1.1 --- a/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 17:58:24 2007 +0200
     1.2 +++ b/src/HOL/HoareParallel/OG_Syntax.thy	Fri Apr 20 17:58:25 2007 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    "_AnnAssign"   :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
     1.5  
     1.6  translations
     1.7 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
     1.8 -  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
     1.9 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
    1.10 +  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
    1.11  
    1.12  syntax
    1.13    "_AnnSkip"     :: "'a assn \<Rightarrow> 'a ann_com"              ("_//SKIP" [90] 63)
     2.1 --- a/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:24 2007 +0200
     2.2 +++ b/src/HOL/HoareParallel/RG_Syntax.thy	Fri Apr 20 17:58:25 2007 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
     2.5  
     2.6  translations
     2.7 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>"
     2.8 +  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>"
     2.9    "SKIP" \<rightleftharpoons> "Basic id"
    2.10    "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
    2.11    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    2.12 @@ -78,7 +78,7 @@
    2.13        | update_name_tr' (Const x) = Const (upd_tr' x)
    2.14        | update_name_tr' _ = raise Match;
    2.15  
    2.16 -    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    2.17 +    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"}, _)$t) $ Bound 0) :: ts) =
    2.18            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    2.19              (Abs (x, dummyT, t) :: ts)
    2.20        | assign_tr' _ = raise Match;
     3.1 --- a/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:24 2007 +0200
     3.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:25 2007 +0200
     3.3 @@ -228,8 +228,8 @@
     3.4  
     3.5  translations
     3.6    ".{b}."                   => "Collect .(b)."
     3.7 -  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (CONST K_record a)) \<in> B}."
     3.8 -  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (CONST K_record a)))."
     3.9 +  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
    3.10 +  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (K_record a)))."
    3.11    "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
    3.12    "WHILE b INV i DO c OD"   => "While .{b}. i c"
    3.13    "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
    3.14 @@ -270,7 +270,7 @@
    3.15        | update_name_tr' (Const x) = Const (upd_tr' x)
    3.16        | update_name_tr' _ = raise Match;
    3.17  
    3.18 -    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    3.19 +    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
    3.20            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    3.21              (Abs (x, dummyT, t) :: ts)
    3.22        | assign_tr' _ = raise Match;
    3.23 @@ -448,7 +448,7 @@
    3.24  method_setup hoare = {*
    3.25    Method.no_args
    3.26      (Method.SIMPLE_METHOD'
    3.27 -       (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *}
    3.28 +       (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_apply"}] )))) *}
    3.29    "verification condition generator for Hoare logic"
    3.30  
    3.31  end
     4.1 --- a/src/HOL/Record.thy	Fri Apr 20 17:58:24 2007 +0200
     4.2 +++ b/src/HOL/Record.thy	Fri Apr 20 17:58:25 2007 +0200
     4.3 @@ -17,10 +17,9 @@
     4.4  lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
     4.5    by simp
     4.6  
     4.7 -definition
     4.8 +constdefs
     4.9    K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    4.10 -where
    4.11 -  K_record_apply [simp]: "K_record c x = c"
    4.12 +  K_record_apply [simp, code func]: "K_record c x \<equiv> c"
    4.13  
    4.14  lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
    4.15    by (rule ext) (simp add: K_record_apply comp_def)