summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 10 Jan 2001 00:15:33 +0100 | |

changeset 10838 | 9423817dee84 |

parent 10837 | 7d640de604e4 |

child 10839 | 1f93f5a27de6 |

use \<acute>;

--- 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)

--- 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

--- 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