1.1 --- a/src/HOL/List.thy	Thu Aug 27 17:09:37 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Aug 27 18:45:58 2009 +0200
     1.3 @@ -3835,4 +3835,117 @@
     1.4    "setsum f (set [i..j::int]) = listsum (map f [i..j])"
     1.5  by (rule setsum_set_distinct_conv_listsum) simp
     1.6  
     1.7 +
     1.8 +text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
     1.9 +and similiarly for @{text"\<exists>"}. *}
    1.10 +
    1.11 +function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.12 +"all_from_to_nat P i j =
    1.13 + (if i < j then if P i then all_from_to_nat P (i+1) j else False
    1.14 +  else True)"
    1.15 +by auto
    1.16 +termination
    1.17 +by (relation "measure(%(P,i,j). j - i)") auto
    1.18 +
    1.19 +declare all_from_to_nat.simps[simp del]
    1.20 +
    1.21 +lemma all_from_to_nat_iff_ball:
    1.22 +  "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
    1.23 +proof(induct P i j rule:all_from_to_nat.induct)
    1.24 +  case (1 P i j)
    1.25 +  let ?yes = "i < j & P i"
    1.26 +  show ?case
    1.27 +  proof (cases)
    1.28 +    assume ?yes
    1.29 +    hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
    1.30 +      by(simp add: all_from_to_nat.simps)
    1.31 +    also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
    1.32 +    also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
    1.33 +    proof
    1.34 +      assume L: ?L
    1.35 +      show ?R
    1.36 +      proof clarify
    1.37 +	fix n assume n: "n : {i..<j}"
    1.38 +	show "P n"
    1.39 +	proof cases
    1.40 +	  assume "n = i" thus "P n" using L by simp
    1.41 +	next
    1.42 +	  assume "n ~= i"
    1.43 +	  hence "i+1 <= n" using n by auto
    1.44 +	  thus "P n" using L n by simp
    1.45 +	qed
    1.46 +      qed
    1.47 +    next
    1.48 +      assume R: ?R thus ?L using `?yes` 1 by auto
    1.49 +    qed
    1.50 +    finally show ?thesis .
    1.51 +  next
    1.52 +    assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
    1.53 +  qed
    1.54 +qed
    1.55 +
    1.56 +
    1.57 +lemma list_all_iff_all_from_to_nat[code_unfold]:
    1.58 +  "list_all P [i..<j] = all_from_to_nat P i j"
    1.59 +by(simp add: all_from_to_nat_iff_ball list_all_iff)
    1.60 +
    1.61 +lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
    1.62 +  "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
    1.63 +by(simp add: all_from_to_nat_iff_ball list_ex_iff)
    1.64 +
    1.65 +
    1.66 +function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
    1.67 +"all_from_to_int P i j =
    1.68 + (if i <= j then if P i then all_from_to_int P (i+1) j else False
    1.69 +  else True)"
    1.70 +by auto
    1.71 +termination
    1.72 +by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
    1.73 +
    1.74 +declare all_from_to_int.simps[simp del]
    1.75 +
    1.76 +lemma all_from_to_int_iff_ball:
    1.77 +  "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
    1.78 +proof(induct P i j rule:all_from_to_int.induct)
    1.79 +  case (1 P i j)
    1.80 +  let ?yes = "i <= j & P i"
    1.81 +  show ?case
    1.82 +  proof (cases)
    1.83 +    assume ?yes
    1.84 +    hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
    1.85 +      by(simp add: all_from_to_int.simps)
    1.86 +    also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
    1.87 +    also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
    1.88 +    proof
    1.89 +      assume L: ?L
    1.90 +      show ?R
    1.91 +      proof clarify
    1.92 +	fix n assume n: "n : {i..j}"
    1.93 +	show "P n"
    1.94 +	proof cases
    1.95 +	  assume "n = i" thus "P n" using L by simp
    1.96 +	next
    1.97 +	  assume "n ~= i"
    1.98 +	  hence "i+1 <= n" using n by auto
    1.99 +	  thus "P n" using L n by simp
   1.100 +	qed
   1.101 +      qed
   1.102 +    next
   1.103 +      assume R: ?R thus ?L using `?yes` 1 by auto
   1.104 +    qed
   1.105 +    finally show ?thesis .
   1.106 +  next
   1.107 +    assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
   1.108 +  qed
   1.109 +qed
   1.110 +
   1.111 +lemma list_all_iff_all_from_to_int[code_unfold]:
   1.112 +  "list_all P [i..j] = all_from_to_int P i j"
   1.113 +by(simp add: all_from_to_int_iff_ball list_all_iff)
   1.114 +
   1.115 +lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
   1.116 +  "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
   1.117 +by(simp add: all_from_to_int_iff_ball list_ex_iff)
   1.118 +
   1.119 +
   1.120  end

     2.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Aug 27 17:09:37 2009 +0200
     2.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Aug 27 18:45:58 2009 +0200
     2.3 @@ -99,6 +99,35 @@
     2.4  values 20 "{(n, m). tranclp succ n m}"
     2.5  *)
     2.6  
     2.7 +subsection{* IMP *}
     2.8 +
     2.9 +types
    2.10 +  var = nat
    2.11 +  state = "int list"
    2.12 +
    2.13 +datatype com =
    2.14 +  Skip |
    2.15 +  Ass var "state => int" |
    2.16 +  Seq com com |
    2.17 +  IF "state => bool" com com |
    2.18 +  While "state => bool" com
    2.19 +
    2.20 +inductive exec :: "com => state => state => bool" where
    2.21 +"exec Skip s s" |
    2.22 +"exec (Ass x e) s (s[x := e(s)])" |
    2.23 +"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
    2.24 +"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
    2.25 +"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
    2.26 +"~b s ==> exec (While b c) s s" |
    2.27 +"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
    2.28 +
    2.29 +code_pred exec .
    2.30 +
    2.31 +values "{t. exec
    2.32 + (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
    2.33 + [3,5] t}"
    2.34 +
    2.35 +
    2.36  subsection{* CCS *}
    2.37  
    2.38  text{* This example formalizes finite CCS processes without communication or