# HG changeset patch # User nipkow # Date 1389092749 -3600 # Node ID 6d99745afe34028ed7a3fba768bfa54dd9bc6a88 # Parent a20b105bb5d1b3783a7094ae42569946c9aefdcc tuned diff -r a20b105bb5d1 -r 6d99745afe34 src/HOL/IMP/ACom.thy --- a/src/HOL/IMP/ACom.thy Mon Jan 06 23:00:11 2014 +0100 +++ b/src/HOL/IMP/ACom.thy Tue Jan 07 12:05:49 2014 +0100 @@ -15,9 +15,11 @@ While 'a bexp 'a "('a acom)" 'a ("({_}//WHILE _//DO ({_}//_)//{_})" [0, 0, 0, 61, 0] 61) +notation com.SKIP ("SKIP") + text_raw{*\snip{stripdef}{1}{1}{% *} fun strip :: "'a acom \ com" where -"strip (SKIP {P}) = com.SKIP" | +"strip (SKIP {P}) = SKIP" | "strip (x ::= e {P}) = x ::= e" | "strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" | "strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) = @@ -27,7 +29,7 @@ text_raw{*\snip{asizedef}{1}{1}{% *} fun asize :: "com \ nat" where -"asize com.SKIP = 1" | +"asize SKIP = 1" | "asize (x ::= e) = 1" | "asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" | "asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" | @@ -39,7 +41,7 @@ "shift f n = (\p. f(p+n))" fun annotate :: "(nat \ 'a) \ com \ 'a acom" where -"annotate f com.SKIP = SKIP {f 0}" | +"annotate f SKIP = SKIP {f 0}" | "annotate f (x ::= e) = x ::= e {f 0}" | "annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" | "annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = @@ -131,7 +133,7 @@ done lemma strip_eq_SKIP: - "strip C = com.SKIP \ (EX P. C = SKIP {P})" + "strip C = SKIP \ (EX P. C = SKIP {P})" by (cases C) simp_all lemma strip_eq_Assign: diff -r a20b105bb5d1 -r 6d99745afe34 src/HOL/IMP/VCG.thy --- a/src/HOL/IMP/VCG.thy Mon Jan 06 23:00:11 2014 +0100 +++ b/src/HOL/IMP/VCG.thy Tue Jan 07 12:05:49 2014 +0100 @@ -14,11 +14,12 @@ Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) +notation com.SKIP ("SKIP") text{* Strip annotations: *} fun strip :: "acom \ com" where -"strip SKIP = com.SKIP" | +"strip SKIP = SKIP" | "strip (x ::= a) = (x ::= a)" | "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |