use \<acute>;
authorwenzelm
Wed Jan 10 00:15:33 2001 +0100 (2001-01-10)
changeset 108389423817dee84
parent 10837 7d640de604e4
child 10839 1f93f5a27de6
use \<acute>;
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/HoareEx.thy
src/HOL/ex/Multiquote.thy
     1.1 --- a/src/HOL/Isar_examples/Hoare.thy	Wed Jan 10 00:14:52 2001 +0100
     1.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Wed Jan 10 00:15:33 2001 +0100
     1.3 @@ -218,9 +218,9 @@
     1.4  
     1.5  syntax
     1.6    "_quote"       :: "'b => ('a => 'b)"        ("(.'(_').)" [0] 1000)
     1.7 -  "_antiquote"   :: "('a => 'b) => 'b"        ("`_" [1000] 1000)
     1.8 +  "_antiquote"   :: "('a => 'b) => 'b"        ("\<acute>_" [1000] 1000)
     1.9    "_Assert"      :: "'a => 'a set"            ("(.{_}.)" [0] 1000)
    1.10 -  "_Assign"      :: "idt => 'b => 'a com"     ("(`_ :=/ _)" [70, 65] 61)
    1.11 +  "_Assign"      :: "idt => 'b => 'a com"     ("(\<acute>_ :=/ _)" [70, 65] 61)
    1.12    "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
    1.13          ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
    1.14    "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
    1.15 @@ -233,7 +233,7 @@
    1.16  
    1.17  translations
    1.18    ".{b}."                   => "Collect .(b)."
    1.19 -  "`x := a"                 => "Basic .(`(_update_name x a))."
    1.20 +  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."
    1.21    "IF b THEN c1 ELSE c2 FI" => "Cond (Collect .(b).) c1 c2"
    1.22    "WHILE b INV i DO c OD"   => "While (Collect .(b).) i c"
    1.23    "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
    1.24 @@ -308,17 +308,17 @@
    1.25    by (unfold Valid_def) blast
    1.26  
    1.27  lemma [trans]:
    1.28 -    "|- .{`P}. c Q ==> (!!s. P' s --> P s) ==> |- .{`P'}. c Q"
    1.29 +    "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
    1.30    by (simp add: Valid_def)
    1.31  lemma [trans]:
    1.32 -    "(!!s. P' s --> P s) ==> |- .{`P}. c Q ==> |- .{`P'}. c Q"
    1.33 +    "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
    1.34    by (simp add: Valid_def)
    1.35  
    1.36  lemma [trans]:
    1.37 -    "|- P c .{`Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{`Q'}."
    1.38 +    "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
    1.39    by (simp add: Valid_def)
    1.40  lemma [trans]:
    1.41 -    "(!!s. Q s --> Q' s) ==> |- P c .{`Q}. ==> |- P c .{`Q'}."
    1.42 +    "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
    1.43    by (simp add: Valid_def)
    1.44  
    1.45  
    1.46 @@ -335,7 +335,7 @@
    1.47    thus ?thesis by simp
    1.48  qed
    1.49  
    1.50 -lemma assign: "|- .{`(x_update `a) : P}. `x := `a P"
    1.51 +lemma assign: "|- .{\<acute>(x_update \<acute>a) : P}. \<acute>x := \<acute>a P"
    1.52    by (rule basic)
    1.53  
    1.54  text {*
    1.55 @@ -345,7 +345,7 @@
    1.56   $x$, Isabelle/HOL provides a functions $x$ (selector) and
    1.57   $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
    1.58   appearing for the latter kind of function: due to concrete syntax
    1.59 - \isa{`x := `a} also contains \isa{x\_update}.\footnote{Note that due
    1.60 + \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
    1.61   to the external nature of HOL record fields, we could not even state
    1.62   a general theorem relating selector and update functions (if this
    1.63   were required here); this would only work for any particular instance
    1.64 @@ -369,9 +369,9 @@
    1.65  lemmas [trans, intro?] = cond
    1.66  
    1.67  lemma [trans, intro?]:
    1.68 -  "|- .{`P & `b}. c1 Q
    1.69 -      ==> |- .{`P & ~ `b}. c2 Q
    1.70 -      ==> |- .{`P}. IF `b THEN c1 ELSE c2 FI Q"
    1.71 +  "|- .{\<acute>P & \<acute>b}. c1 Q
    1.72 +      ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
    1.73 +      ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
    1.74      by (rule cond) (simp_all add: Valid_def)
    1.75  
    1.76  text {*
    1.77 @@ -388,13 +388,13 @@
    1.78  
    1.79  
    1.80  lemma [intro?]:
    1.81 -  "|- .{`P & `b}. c .{`P}.
    1.82 -    ==> |- .{`P}. WHILE `b INV .{`P}. DO c OD .{`P & ~ `b}."
    1.83 +  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
    1.84 +    ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
    1.85    by (simp add: while Collect_conj_eq Collect_neg_eq)
    1.86  
    1.87  lemma [intro?]:
    1.88 -  "|- .{`P & `b}. c .{`P}.
    1.89 -    ==> |- .{`P}. WHILE `b DO c OD .{`P & ~ `b}."
    1.90 +  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
    1.91 +    ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
    1.92    by (simp add: while Collect_conj_eq Collect_neg_eq)
    1.93  
    1.94  
     2.1 --- a/src/HOL/Isar_examples/HoareEx.thy	Wed Jan 10 00:14:52 2001 +0100
     2.2 +++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Jan 10 00:15:33 2001 +0100
     2.3 @@ -39,7 +39,7 @@
     2.4  *}
     2.5  
     2.6  lemma
     2.7 -  "|- .{`(N_update (2 * `N)) : .{`N = #10}.}. `N := 2 * `N .{`N = #10}."
     2.8 +  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
     2.9    by (rule assign)
    2.10  
    2.11  text {*
    2.12 @@ -49,31 +49,31 @@
    2.13   ``obvious'' consequences as well.
    2.14  *}
    2.15  
    2.16 -lemma "|- .{True}. `N := #10 .{`N = #10}."
    2.17 +lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
    2.18    by hoare
    2.19  
    2.20 -lemma "|- .{2 * `N = #10}. `N := 2 * `N .{`N = #10}."
    2.21 +lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    2.22    by hoare
    2.23  
    2.24 -lemma "|- .{`N = #5}. `N := 2 * `N .{`N = #10}."
    2.25 +lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    2.26    by hoare simp
    2.27  
    2.28 -lemma "|- .{`N + 1 = a + 1}. `N := `N + 1 .{`N = a + 1}."
    2.29 +lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    2.30    by hoare
    2.31  
    2.32 -lemma "|- .{`N = a}. `N := `N + 1 .{`N = a + 1}."
    2.33 +lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    2.34    by hoare simp
    2.35  
    2.36 -lemma "|- .{a = a & b = b}. `M := a; `N := b .{`M = a & `N = b}."
    2.37 +lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
    2.38    by hoare
    2.39  
    2.40 -lemma "|- .{True}. `M := a; `N := b .{`M = a & `N = b}."
    2.41 +lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
    2.42    by hoare simp
    2.43  
    2.44  lemma
    2.45 -"|- .{`M = a & `N = b}.
    2.46 -    `I := `M; `M := `N; `N := `I
    2.47 -    .{`M = b & `N = a}."
    2.48 +"|- .{\<acute>M = a & \<acute>N = b}.
    2.49 +    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
    2.50 +    .{\<acute>M = b & \<acute>N = a}."
    2.51    by hoare simp
    2.52  
    2.53  text {*
    2.54 @@ -83,10 +83,10 @@
    2.55   relating record selectors and updates schematically.
    2.56  *}
    2.57  
    2.58 -lemma "|- .{`N = a}. `N := `N .{`N = a}."
    2.59 +lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
    2.60    by hoare
    2.61  
    2.62 -lemma "|- .{`x = a}. `x := `x .{`x = a}."
    2.63 +lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
    2.64    oops
    2.65  
    2.66  lemma
    2.67 @@ -101,27 +101,27 @@
    2.68   \name{hoare} method is able to handle this case, too.
    2.69  *}
    2.70  
    2.71 -lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
    2.72 +lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    2.73  proof -
    2.74 -  have ".{`M = `N}. <= .{`M + 1 ~= `N}."
    2.75 +  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
    2.76      by auto
    2.77 -  also have "|- ... `M := `M + 1 .{`M ~= `N}."
    2.78 +  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    2.79      by hoare
    2.80    finally show ?thesis .
    2.81  qed
    2.82  
    2.83 -lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
    2.84 +lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    2.85  proof -
    2.86    have "!!m n. m = n --> m + 1 ~= n"
    2.87        -- {* inclusion of assertions expressed in ``pure'' logic, *}
    2.88        -- {* without mentioning the state space *}
    2.89      by simp
    2.90 -  also have "|- .{`M + 1 ~= `N}. `M := `M + 1 .{`M ~= `N}."
    2.91 +  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    2.92      by hoare
    2.93    finally show ?thesis .
    2.94  qed
    2.95  
    2.96 -lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
    2.97 +lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    2.98    by hoare simp
    2.99  
   2.100  
   2.101 @@ -135,24 +135,24 @@
   2.102  *}
   2.103  
   2.104  lemma
   2.105 -  "|- .{`M = 0 & `S = 0}.
   2.106 -      WHILE `M ~= a
   2.107 -      DO `S := `S + b; `M := `M + 1 OD
   2.108 -      .{`S = a * b}."
   2.109 +  "|- .{\<acute>M = 0 & \<acute>S = 0}.
   2.110 +      WHILE \<acute>M ~= a
   2.111 +      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
   2.112 +      .{\<acute>S = a * b}."
   2.113  proof -
   2.114    let "|- _ ?while _" = ?thesis
   2.115 -  let ".{`?inv}." = ".{`S = `M * b}."
   2.116 +  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
   2.117  
   2.118 -  have ".{`M = 0 & `S = 0}. <= .{`?inv}." by auto
   2.119 -  also have "|- ... ?while .{`?inv & ~ (`M ~= a)}."
   2.120 +  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
   2.121 +  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
   2.122    proof
   2.123 -    let ?c = "`S := `S + b; `M := `M + 1"
   2.124 -    have ".{`?inv & `M ~= a}. <= .{`S + b = (`M + 1) * b}."
   2.125 +    let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
   2.126 +    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
   2.127        by auto
   2.128 -    also have "|- ... ?c .{`?inv}." by hoare
   2.129 -    finally show "|- .{`?inv & `M ~= a}. ?c .{`?inv}." .
   2.130 +    also have "|- ... ?c .{\<acute>?inv}." by hoare
   2.131 +    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
   2.132    qed
   2.133 -  also have "... <= .{`S = a * b}." by auto
   2.134 +  also have "... <= .{\<acute>S = a * b}." by auto
   2.135    finally show ?thesis .
   2.136  qed
   2.137  
   2.138 @@ -164,11 +164,11 @@
   2.139  *}
   2.140  
   2.141  lemma
   2.142 -  "|- .{`M = 0 & `S = 0}.
   2.143 -      WHILE `M ~= a
   2.144 -      INV .{`S = `M * b}.
   2.145 -      DO `S := `S + b; `M := `M + 1 OD
   2.146 -      .{`S = a * b}."
   2.147 +  "|- .{\<acute>M = 0 & \<acute>S = 0}.
   2.148 +      WHILE \<acute>M ~= a
   2.149 +      INV .{\<acute>S = \<acute>M * b}.
   2.150 +      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
   2.151 +      .{\<acute>S = a * b}."
   2.152    by hoare auto
   2.153  
   2.154  
   2.155 @@ -202,34 +202,34 @@
   2.156  
   2.157  theorem
   2.158    "|- .{True}.
   2.159 -      `S := 0; `I := 1;
   2.160 -      WHILE `I ~= n
   2.161 +      \<acute>S := 0; \<acute>I := 1;
   2.162 +      WHILE \<acute>I ~= n
   2.163        DO
   2.164 -        `S := `S + `I;
   2.165 -        `I := `I + 1
   2.166 +        \<acute>S := \<acute>S + \<acute>I;
   2.167 +        \<acute>I := \<acute>I + 1
   2.168        OD
   2.169 -      .{`S = (SUM j<n. j)}."
   2.170 +      .{\<acute>S = (SUM j<n. j)}."
   2.171    (is "|- _ (_; ?while) _")
   2.172  proof -
   2.173    let ?sum = "\<lambda>k. SUM j<k. j"
   2.174    let ?inv = "\<lambda>s i. s = ?sum i"
   2.175  
   2.176 -  have "|- .{True}. `S := 0; `I := 1 .{?inv `S `I}."
   2.177 +  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   2.178    proof -
   2.179      have "True --> 0 = ?sum 1"
   2.180        by simp
   2.181 -    also have "|- .{...}. `S := 0; `I := 1 .{?inv `S `I}."
   2.182 +    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   2.183        by hoare
   2.184      finally show ?thesis .
   2.185    qed
   2.186 -  also have "|- ... ?while .{?inv `S `I & ~ `I ~= n}."
   2.187 +  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
   2.188    proof
   2.189 -    let ?body = "`S := `S + `I; `I := `I + 1"
   2.190 +    let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
   2.191      have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
   2.192        by simp
   2.193 -    also have "|- .{`S + `I = ?sum (`I + 1)}. ?body .{?inv `S `I}."
   2.194 +    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
   2.195        by hoare
   2.196 -    finally show "|- .{?inv `S `I & `I ~= n}. ?body .{?inv `S `I}." .
   2.197 +    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
   2.198    qed
   2.199    also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
   2.200      by simp
   2.201 @@ -243,14 +243,14 @@
   2.202  
   2.203  theorem
   2.204    "|- .{True}.
   2.205 -      `S := 0; `I := 1;
   2.206 -      WHILE `I ~= n
   2.207 -      INV .{`S = (SUM j<`I. j)}.
   2.208 +      \<acute>S := 0; \<acute>I := 1;
   2.209 +      WHILE \<acute>I ~= n
   2.210 +      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
   2.211        DO
   2.212 -        `S := `S + `I;
   2.213 -        `I := `I + 1
   2.214 +        \<acute>S := \<acute>S + \<acute>I;
   2.215 +        \<acute>I := \<acute>I + 1
   2.216        OD
   2.217 -      .{`S = (SUM j<n. j)}."
   2.218 +      .{\<acute>S = (SUM j<n. j)}."
   2.219  proof -
   2.220    let ?sum = "\<lambda>k. SUM j<k. j"
   2.221    let ?inv = "\<lambda>s i. s = ?sum i"
   2.222 @@ -274,14 +274,14 @@
   2.223  
   2.224  theorem
   2.225    "|- .{True}.
   2.226 -      `S := 0; `I := 1;
   2.227 -      WHILE `I ~= n
   2.228 -      INV .{`S = (SUM j<`I. j)}.
   2.229 +      \<acute>S := 0; \<acute>I := 1;
   2.230 +      WHILE \<acute>I ~= n
   2.231 +      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
   2.232        DO
   2.233 -        `S := `S + `I;
   2.234 -        `I := `I + 1
   2.235 +        \<acute>S := \<acute>S + \<acute>I;
   2.236 +        \<acute>I := \<acute>I + 1
   2.237        OD
   2.238 -      .{`S = (SUM j<n. j)}."
   2.239 +      .{\<acute>S = (SUM j<n. j)}."
   2.240    by hoare auto
   2.241  
   2.242  end
   2.243 \ No newline at end of file
     3.1 --- a/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:14:52 2001 +0100
     3.2 +++ b/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:15:33 2001 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  syntax
     3.6    "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
     3.7 -  "_antiquote" :: "('a => 'b) => 'b"         ("_" [1000] 1000)
     3.8 +  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
     3.9  
    3.10  parse_translation {*
    3.11    let
    3.12 @@ -35,14 +35,14 @@
    3.13  
    3.14  text {* basic examples *}
    3.15  term ".(a + b + c)."
    3.16 -term ".(a + b + c + x + y + 1)."
    3.17 -term ".((f w) + x)."
    3.18 -term ".(f x y z)."
    3.19 +term ".(a + b + c + \<acute>x + \<acute>y + 1)."
    3.20 +term ".(\<acute>(f w) + \<acute>x)."
    3.21 +term ".(f \<acute>x \<acute>y z)."
    3.22  
    3.23  text {* advanced examples *}
    3.24 -term ".(.( x + y).)."
    3.25 -term ".(.( x + y). o f)."
    3.26 -term ".((f o g))."
    3.27 -term ".(.(  (f o g) ).)."
    3.28 +term ".(.(\<acute>\<acute>x + \<acute>y).)."
    3.29 +term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
    3.30 +term ".(\<acute>(f o \<acute>g))."
    3.31 +term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
    3.32  
    3.33  end