# HG changeset patch
# User nipkow
# Date 1323807338 -3600
# Node ID dadd139192d172426b0a04d57b99cd1a239d8a07
# Parent  9c232d370244c757eadf70094677f9e827d2b321
added concrete syntax

diff -r 9c232d370244 -r dadd139192d1 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Dec 13 16:53:28 2011 +0100
+++ b/src/HOL/IMP/VC.thy	Tue Dec 13 21:15:38 2011 +0100
@@ -7,16 +7,17 @@
 text{* Annotated commands: commands where loops are annotated with
 invariants. *}
 
-datatype acom = Askip
-              | Aassign vname aexp
-              | Asemi   acom acom
-              | Aif     bexp acom acom
-              | Awhile  assn bexp acom
+datatype acom =
+  ASKIP |
+  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
+  Asemi   acom acom      ("_;/ _"  [60, 61] 60) |
+  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
+  Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
 
 text{* Weakest precondition from annotated commands: *}
 
 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
-"pre Askip Q = Q" |
+"pre ASKIP Q = Q" |
 "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
 "pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
 "pre (Aif b c\<^isub>1 c\<^isub>2) Q =
@@ -27,7 +28,7 @@
 text{* Verification condition: *}
 
 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
-"vc Askip Q = (\<lambda>s. True)" |
+"vc ASKIP Q = (\<lambda>s. True)" |
 "vc (Aassign x a) Q = (\<lambda>s. True)" |
 "vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
 "vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
@@ -38,17 +39,16 @@
 
 text{* Strip annotations: *}
 
-fun astrip :: "acom \<Rightarrow> com" where
-"astrip Askip = SKIP" |
-"astrip (Aassign x a) = (x::=a)" |
-"astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" |
-"astrip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN astrip c\<^isub>1 ELSE astrip c\<^isub>2)" |
-"astrip (Awhile I b c) = (WHILE b DO astrip c)"
-
+fun strip :: "acom \<Rightarrow> com" where
+"strip ASKIP = SKIP" |
+"strip (Aassign x a) = (x::=a)" |
+"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
+"strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
+"strip (Awhile I b c) = (WHILE b DO strip c)"
 
 subsection "Soundness"
 
-lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
+lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
 proof(induction c arbitrary: Q)
   case (Awhile I b c)
   show ?case
@@ -56,15 +56,15 @@
     from `\<forall>s. vc (Awhile I b c) Q s`
     have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
          pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
-    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
-    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
+    have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc])
+    with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}"
       by(rule strengthen_pre)
     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
   qed
 qed (auto intro: hoare.conseq)
 
 corollary vc_sound':
-  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} astrip c {Q}"
+  "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}"
 by (metis strengthen_pre vc_sound)
 
 
@@ -83,12 +83,12 @@
 qed simp_all
 
 lemma vc_complete:
- "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
+ "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. strip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
 proof (induction rule: hoare.induct)
   case Skip
   show ?case (is "\<exists>ac. ?C ac")
-  proof show "?C Askip" by simp qed
+  proof show "?C ASKIP" by simp qed
 next
   case (Assign P a x)
   show ?case (is "\<exists>ac. ?C ac")
@@ -125,7 +125,7 @@
 subsection "An Optimization"
 
 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
-"vcpre Askip Q = (\<lambda>s. True, Q)" |
+"vcpre ASKIP Q = (\<lambda>s. True, Q)" |
 "vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
 "vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;