--- a/src/HOL/IMP/VC.thy Tue Dec 13 23:23:51 2011 +0100
+++ b/src/HOL/IMP/VC.thy Tue Dec 13 23:22:27 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;
--- a/src/HOL/List.thy Tue Dec 13 23:23:51 2011 +0100
+++ b/src/HOL/List.thy Tue Dec 13 23:22:27 2011 +0100
@@ -1354,6 +1354,10 @@
apply (case_tac n, auto)
done
+lemma nth_tl:
+ assumes "n < length (tl x)" shows "tl x ! n = x ! Suc n"
+using assms by (induct x) auto
+
lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
by(cases xs) simp_all
@@ -1545,6 +1549,12 @@
lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
by(simp add:last_append)
+lemma last_tl: "xs = [] \<or> tl xs \<noteq> [] \<Longrightarrow>last (tl xs) = last xs"
+by (induct xs) simp_all
+
+lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"
+by (induct xs) simp_all
+
lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
by(rule rev_exhaust[of xs]) simp_all
@@ -1578,6 +1588,15 @@
apply (auto split:nat.split)
done
+lemma nth_butlast:
+ assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"
+proof (cases xs)
+ case (Cons y ys)
+ moreover from assms have "butlast xs ! n = (butlast xs @ [last xs]) ! n"
+ by (simp add: nth_append)
+ ultimately show ?thesis using append_butlast_last_id by simp
+qed simp
+
lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
by(induct xs)(auto simp:neq_Nil_conv)
@@ -1899,6 +1918,17 @@
"(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
by (induct xs) auto
+lemma dropWhile_append3:
+ "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
+by (induct xs) auto
+
+lemma dropWhile_last:
+ "x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> last (dropWhile P xs) = last xs"
+by (auto simp add: dropWhile_append3 in_set_conv_decomp)
+
+lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
+by (induct xs) (auto split: split_if_asm)
+
lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
by (induct xs) (auto split: split_if_asm)
@@ -2890,6 +2920,30 @@
apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
done
+lemma not_distinct_conv_prefix:
+ defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"
+ shows "\<not>distinct as \<longleftrightarrow> (\<exists>xs y ys. dec as xs y ys)" (is "?L = ?R")
+proof
+ assume "?L" then show "?R"
+ proof (induct "length as" arbitrary: as rule: less_induct)
+ case less
+ obtain xs ys zs y where decomp: "as = (xs @ y # ys) @ y # zs"
+ using not_distinct_decomp[OF less.prems] by auto
+ show ?case
+ proof (cases "distinct (xs @ y # ys)")
+ case True
+ with decomp have "dec as (xs @ y # ys) y zs" by (simp add: dec_def)
+ then show ?thesis by blast
+ next
+ case False
+ with less decomp obtain xs' y' ys' where "dec (xs @ y # ys) xs' y' ys'"
+ by atomize_elim auto
+ with decomp have "dec as xs' y' (ys' @ y # zs)" by (simp add: dec_def)
+ then show ?thesis by blast
+ qed
+ qed
+qed (auto simp: dec_def)
+
lemma length_remdups_concat:
"length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
by (simp add: distinct_card [symmetric])