# HG changeset patch
# User wenzelm
# Date 979082133 -3600
# Node ID 9423817dee84283b7fa51bc9c6813789c0407a9d
# Parent 7d640de604e4f839ac5943fc4a504fc8b63dc779
use \<acute>;
diff -r 7d640de604e4 -r 9423817dee84 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Wed Jan 10 00:15:33 2001 +0100
@@ -218,9 +218,9 @@
syntax
"_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000)
+ "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
"_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000)
- "_Assign" :: "idt => 'b => 'a com" ("(`_ :=/ _)" [70, 65] 61)
+ "_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
"_Cond" :: "'a bexp => 'a com => 'a com => 'a com"
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
"_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com"
@@ -233,7 +233,7 @@
translations
".{b}." => "Collect .(b)."
- "`x := a" => "Basic .(`(_update_name x a))."
+ "\<acute>x := a" => "Basic .(\<acute>(_update_name x a))."
"IF b THEN c1 ELSE c2 FI" => "Cond (Collect .(b).) c1 c2"
"WHILE b INV i DO c OD" => "While (Collect .(b).) i c"
"WHILE b DO c OD" == "WHILE b INV arbitrary DO c OD"
@@ -308,17 +308,17 @@
by (unfold Valid_def) blast
lemma [trans]:
- "|- .{`P}. c Q ==> (!!s. P' s --> P s) ==> |- .{`P'}. c Q"
+ "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
by (simp add: Valid_def)
lemma [trans]:
- "(!!s. P' s --> P s) ==> |- .{`P}. c Q ==> |- .{`P'}. c Q"
+ "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
by (simp add: Valid_def)
lemma [trans]:
- "|- P c .{`Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{`Q'}."
+ "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
by (simp add: Valid_def)
lemma [trans]:
- "(!!s. Q s --> Q' s) ==> |- P c .{`Q}. ==> |- P c .{`Q'}."
+ "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
by (simp add: Valid_def)
@@ -335,7 +335,7 @@
thus ?thesis by simp
qed
-lemma assign: "|- .{`(x_update `a) : P}. `x := `a P"
+lemma assign: "|- .{\<acute>(x_update \<acute>a) : P}. \<acute>x := \<acute>a P"
by (rule basic)
text {*
@@ -345,7 +345,7 @@
$x$, Isabelle/HOL provides a functions $x$ (selector) and
$\idt{x{\dsh}update}$ (update). Above, there is only a place-holder
appearing for the latter kind of function: due to concrete syntax
- \isa{`x := `a} also contains \isa{x\_update}.\footnote{Note that due
+ \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
to the external nature of HOL record fields, we could not even state
a general theorem relating selector and update functions (if this
were required here); this would only work for any particular instance
@@ -369,9 +369,9 @@
lemmas [trans, intro?] = cond
lemma [trans, intro?]:
- "|- .{`P & `b}. c1 Q
- ==> |- .{`P & ~ `b}. c2 Q
- ==> |- .{`P}. IF `b THEN c1 ELSE c2 FI Q"
+ "|- .{\<acute>P & \<acute>b}. c1 Q
+ ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
+ ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
by (rule cond) (simp_all add: Valid_def)
text {*
@@ -388,13 +388,13 @@
lemma [intro?]:
- "|- .{`P & `b}. c .{`P}.
- ==> |- .{`P}. WHILE `b INV .{`P}. DO c OD .{`P & ~ `b}."
+ "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
+ ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
by (simp add: while Collect_conj_eq Collect_neg_eq)
lemma [intro?]:
- "|- .{`P & `b}. c .{`P}.
- ==> |- .{`P}. WHILE `b DO c OD .{`P & ~ `b}."
+ "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
+ ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
by (simp add: while Collect_conj_eq Collect_neg_eq)
diff -r 7d640de604e4 -r 9423817dee84 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy Wed Jan 10 00:15:33 2001 +0100
@@ -39,7 +39,7 @@
*}
lemma
- "|- .{`(N_update (2 * `N)) : .{`N = #10}.}. `N := 2 * `N .{`N = #10}."
+ "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
by (rule assign)
text {*
@@ -49,31 +49,31 @@
``obvious'' consequences as well.
*}
-lemma "|- .{True}. `N := #10 .{`N = #10}."
+lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
by hoare
-lemma "|- .{2 * `N = #10}. `N := 2 * `N .{`N = #10}."
+lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
by hoare
-lemma "|- .{`N = #5}. `N := 2 * `N .{`N = #10}."
+lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
by hoare simp
-lemma "|- .{`N + 1 = a + 1}. `N := `N + 1 .{`N = a + 1}."
+lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
by hoare
-lemma "|- .{`N = a}. `N := `N + 1 .{`N = a + 1}."
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
by hoare simp
-lemma "|- .{a = a & b = b}. `M := a; `N := b .{`M = a & `N = b}."
+lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
by hoare
-lemma "|- .{True}. `M := a; `N := b .{`M = a & `N = b}."
+lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
by hoare simp
lemma
-"|- .{`M = a & `N = b}.
- `I := `M; `M := `N; `N := `I
- .{`M = b & `N = a}."
+"|- .{\<acute>M = a & \<acute>N = b}.
+ \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
+ .{\<acute>M = b & \<acute>N = a}."
by hoare simp
text {*
@@ -83,10 +83,10 @@
relating record selectors and updates schematically.
*}
-lemma "|- .{`N = a}. `N := `N .{`N = a}."
+lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
by hoare
-lemma "|- .{`x = a}. `x := `x .{`x = a}."
+lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
oops
lemma
@@ -101,27 +101,27 @@
\name{hoare} method is able to handle this case, too.
*}
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
proof -
- have ".{`M = `N}. <= .{`M + 1 ~= `N}."
+ have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
by auto
- also have "|- ... `M := `M + 1 .{`M ~= `N}."
+ also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
by hoare
finally show ?thesis .
qed
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
proof -
have "!!m n. m = n --> m + 1 ~= n"
-- {* inclusion of assertions expressed in ``pure'' logic, *}
-- {* without mentioning the state space *}
by simp
- also have "|- .{`M + 1 ~= `N}. `M := `M + 1 .{`M ~= `N}."
+ also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
by hoare
finally show ?thesis .
qed
-lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
+lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
by hoare simp
@@ -135,24 +135,24 @@
*}
lemma
- "|- .{`M = 0 & `S = 0}.
- WHILE `M ~= a
- DO `S := `S + b; `M := `M + 1 OD
- .{`S = a * b}."
+ "|- .{\<acute>M = 0 & \<acute>S = 0}.
+ WHILE \<acute>M ~= a
+ DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+ .{\<acute>S = a * b}."
proof -
let "|- _ ?while _" = ?thesis
- let ".{`?inv}." = ".{`S = `M * b}."
+ let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
- have ".{`M = 0 & `S = 0}. <= .{`?inv}." by auto
- also have "|- ... ?while .{`?inv & ~ (`M ~= a)}."
+ have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
+ also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
proof
- let ?c = "`S := `S + b; `M := `M + 1"
- have ".{`?inv & `M ~= a}. <= .{`S + b = (`M + 1) * b}."
+ let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
+ have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
by auto
- also have "|- ... ?c .{`?inv}." by hoare
- finally show "|- .{`?inv & `M ~= a}. ?c .{`?inv}." .
+ also have "|- ... ?c .{\<acute>?inv}." by hoare
+ finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
qed
- also have "... <= .{`S = a * b}." by auto
+ also have "... <= .{\<acute>S = a * b}." by auto
finally show ?thesis .
qed
@@ -164,11 +164,11 @@
*}
lemma
- "|- .{`M = 0 & `S = 0}.
- WHILE `M ~= a
- INV .{`S = `M * b}.
- DO `S := `S + b; `M := `M + 1 OD
- .{`S = a * b}."
+ "|- .{\<acute>M = 0 & \<acute>S = 0}.
+ WHILE \<acute>M ~= a
+ INV .{\<acute>S = \<acute>M * b}.
+ DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
+ .{\<acute>S = a * b}."
by hoare auto
@@ -202,34 +202,34 @@
theorem
"|- .{True}.
- `S := 0; `I := 1;
- WHILE `I ~= n
+ \<acute>S := 0; \<acute>I := 1;
+ WHILE \<acute>I ~= n
DO
- `S := `S + `I;
- `I := `I + 1
+ \<acute>S := \<acute>S + \<acute>I;
+ \<acute>I := \<acute>I + 1
OD
- .{`S = (SUM j<n. j)}."
+ .{\<acute>S = (SUM j<n. j)}."
(is "|- _ (_; ?while) _")
proof -
let ?sum = "\<lambda>k. SUM j<k. j"
let ?inv = "\<lambda>s i. s = ?sum i"
- have "|- .{True}. `S := 0; `I := 1 .{?inv `S `I}."
+ have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
proof -
have "True --> 0 = ?sum 1"
by simp
- also have "|- .{...}. `S := 0; `I := 1 .{?inv `S `I}."
+ also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
by hoare
finally show ?thesis .
qed
- also have "|- ... ?while .{?inv `S `I & ~ `I ~= n}."
+ also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
proof
- let ?body = "`S := `S + `I; `I := `I + 1"
+ let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)"
by simp
- also have "|- .{`S + `I = ?sum (`I + 1)}. ?body .{?inv `S `I}."
+ also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
by hoare
- finally show "|- .{?inv `S `I & `I ~= n}. ?body .{?inv `S `I}." .
+ finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
qed
also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
by simp
@@ -243,14 +243,14 @@
theorem
"|- .{True}.
- `S := 0; `I := 1;
- WHILE `I ~= n
- INV .{`S = (SUM j<`I. j)}.
+ \<acute>S := 0; \<acute>I := 1;
+ WHILE \<acute>I ~= n
+ INV .{\<acute>S = (SUM j<\<acute>I. j)}.
DO
- `S := `S + `I;
- `I := `I + 1
+ \<acute>S := \<acute>S + \<acute>I;
+ \<acute>I := \<acute>I + 1
OD
- .{`S = (SUM j<n. j)}."
+ .{\<acute>S = (SUM j<n. j)}."
proof -
let ?sum = "\<lambda>k. SUM j<k. j"
let ?inv = "\<lambda>s i. s = ?sum i"
@@ -274,14 +274,14 @@
theorem
"|- .{True}.
- `S := 0; `I := 1;
- WHILE `I ~= n
- INV .{`S = (SUM j<`I. j)}.
+ \<acute>S := 0; \<acute>I := 1;
+ WHILE \<acute>I ~= n
+ INV .{\<acute>S = (SUM j<\<acute>I. j)}.
DO
- `S := `S + `I;
- `I := `I + 1
+ \<acute>S := \<acute>S + \<acute>I;
+ \<acute>I := \<acute>I + 1
OD
- .{`S = (SUM j<n. j)}."
+ .{\<acute>S = (SUM j<n. j)}."
by hoare auto
end
\ No newline at end of file
diff -r 7d640de604e4 -r 9423817dee84 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy Wed Jan 10 00:14:52 2001 +0100
+++ b/src/HOL/ex/Multiquote.thy Wed Jan 10 00:15:33 2001 +0100
@@ -13,7 +13,7 @@
syntax
"_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("�_" [1000] 1000)
+ "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
parse_translation {*
let
@@ -35,14 +35,14 @@
text {* basic examples *}
term ".(a + b + c)."
-term ".(a + b + c + �x + �y + 1)."
-term ".(�(f w) + �x)."
-term ".(f �x �y z)."
+term ".(a + b + c + \<acute>x + \<acute>y + 1)."
+term ".(\<acute>(f w) + \<acute>x)."
+term ".(f \<acute>x \<acute>y z)."
text {* advanced examples *}
-term ".(.(� �x + �y).)."
-term ".(.(� �x + �y). o �f)."
-term ".(�(f o �g))."
-term ".(.( � �(f o �g) ).)."
+term ".(.(\<acute>\<acute>x + \<acute>y).)."
+term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
+term ".(\<acute>(f o \<acute>g))."
+term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
end