--- a/src/HOL/List.thy Thu Aug 27 17:09:37 2009 +0200
+++ b/src/HOL/List.thy Thu Aug 27 18:45:58 2009 +0200
@@ -3835,4 +3835,117 @@
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (rule setsum_set_distinct_conv_listsum) simp
+
+text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
+and similiarly for @{text"\<exists>"}. *}
+
+function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+"all_from_to_nat P i j =
+ (if i < j then if P i then all_from_to_nat P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). j - i)") auto
+
+declare all_from_to_nat.simps[simp del]
+
+lemma all_from_to_nat_iff_ball:
+ "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
+proof(induct P i j rule:all_from_to_nat.induct)
+ case (1 P i j)
+ let ?yes = "i < j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
+ by(simp add: all_from_to_nat.simps)
+ also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..<j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
+ qed
+qed
+
+
+lemma list_all_iff_all_from_to_nat[code_unfold]:
+ "list_all P [i..<j] = all_from_to_nat P i j"
+by(simp add: all_from_to_nat_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
+ "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
+by(simp add: all_from_to_nat_iff_ball list_ex_iff)
+
+
+function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+"all_from_to_int P i j =
+ (if i <= j then if P i then all_from_to_int P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
+
+declare all_from_to_int.simps[simp del]
+
+lemma all_from_to_int_iff_ball:
+ "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
+proof(induct P i j rule:all_from_to_int.induct)
+ case (1 P i j)
+ let ?yes = "i <= j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
+ by(simp add: all_from_to_int.simps)
+ also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
+ qed
+qed
+
+lemma list_all_iff_all_from_to_int[code_unfold]:
+ "list_all P [i..j] = all_from_to_int P i j"
+by(simp add: all_from_to_int_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
+ "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
+by(simp add: all_from_to_int_iff_ball list_ex_iff)
+
+
end
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Aug 27 17:09:37 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Aug 27 18:45:58 2009 +0200
@@ -99,6 +99,35 @@
values 20 "{(n, m). tranclp succ n m}"
*)
+subsection{* IMP *}
+
+types
+ var = nat
+ state = "int list"
+
+datatype com =
+ Skip |
+ Ass var "state => int" |
+ Seq com com |
+ IF "state => bool" com com |
+ While "state => bool" com
+
+inductive exec :: "com => state => state => bool" where
+"exec Skip s s" |
+"exec (Ass x e) s (s[x := e(s)])" |
+"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec (While b c) s s" |
+"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+code_pred exec .
+
+values "{t. exec
+ (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
+ [3,5] t}"
+
+
subsection{* CCS *}
text{* This example formalizes finite CCS processes without communication or