tuned proofs;
authorwenzelm
Thu Dec 08 20:15:50 2005 +0100 (2005-12-08)
changeset 183722bffdf62fe7f
parent 18371 d93fdf00f8a6
child 18373 995cc683d95c
tuned proofs;
src/HOL/IMP/Compiler0.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Examples.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Machines.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/While_Combinator.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/Product_Type.thy
src/HOL/Real/Rational.thy
src/HOL/Transitive_Closure.thy
src/HOL/Unix/Unix.thy
src/ZF/Induct/Brouwer.thy
src/ZF/Induct/Ntree.thy
     1.1 --- a/src/HOL/IMP/Compiler0.thy	Thu Dec 08 20:15:41 2005 +0100
     1.2 +++ b/src/HOL/IMP/Compiler0.thy	Thu Dec 08 20:15:50 2005 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4    "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
     1.5                 ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
     1.6  
     1.7 -translations  
     1.8 +translations
     1.9    "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
    1.10    "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
    1.11    "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
    1.12 @@ -80,69 +80,64 @@
    1.13  
    1.14  subsection "Context lifting lemmas"
    1.15  
    1.16 -text {* 
    1.17 +text {*
    1.18    Some lemmas for lifting an execution into a prefix and suffix
    1.19    of instructions; only needed for the first proof.
    1.20  *}
    1.21  lemma app_right_1:
    1.22 -  assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.23 +  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.24    shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.25 -proof -
    1.26 - from A show ?thesis
    1.27 - by induct force+
    1.28 -qed
    1.29 +  using prems
    1.30 +  by induct auto
    1.31  
    1.32  lemma app_left_1:
    1.33 -  assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.34 +  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.35    shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
    1.36 -proof -
    1.37 - from A show ?thesis
    1.38 - by induct force+
    1.39 -qed
    1.40 +  using prems
    1.41 +  by induct auto
    1.42  
    1.43  declare rtrancl_induct2 [induct set: rtrancl]
    1.44  
    1.45  lemma app_right:
    1.46 -assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.47 -shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.48 -proof -
    1.49 - from A show ?thesis
    1.50 - proof induct
    1.51 -   show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
    1.52 - next
    1.53 -   fix s1' i1' s2 i2
    1.54 -   assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
    1.55 -          "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.56 -   thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.57 -     by(blast intro:app_right_1 rtrancl_trans)
    1.58 - qed
    1.59 +  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.60 +  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.61 +  using prems
    1.62 +proof induct
    1.63 +  show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
    1.64 +next
    1.65 +  fix s1' i1' s2 i2
    1.66 +  assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
    1.67 +    and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.68 +  thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.69 +    by (blast intro: app_right_1 rtrancl_trans)
    1.70  qed
    1.71  
    1.72  lemma app_left:
    1.73 -assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.74 -shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
    1.75 -proof -
    1.76 -  from A show ?thesis
    1.77 -  proof induct
    1.78 -    show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
    1.79 -  next
    1.80 -    fix s1' i1' s2 i2
    1.81 -    assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
    1.82 -           "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.83 -    thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
    1.84 -      by(blast intro:app_left_1 rtrancl_trans)
    1.85 - qed
    1.86 +  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
    1.87 +  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
    1.88 +using prems
    1.89 +proof induct
    1.90 +  show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
    1.91 +next
    1.92 +  fix s1' i1' s2 i2
    1.93 +  assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
    1.94 +    and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
    1.95 +  thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
    1.96 +    by (blast intro: app_left_1 rtrancl_trans)
    1.97  qed
    1.98  
    1.99  lemma app_left2:
   1.100    "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
   1.101 -   is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
   1.102 -  by (simp add:app_left)
   1.103 +    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
   1.104 +  by (simp add: app_left)
   1.105  
   1.106  lemma app1_left:
   1.107 -  "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   1.108 -   instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
   1.109 -  by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
   1.110 +  assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
   1.111 +  shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
   1.112 +proof -
   1.113 +  from app_left [OF prems, of "[instr]"]
   1.114 +  show ?thesis by simp
   1.115 +qed
   1.116  
   1.117  subsection "Compiler correctness"
   1.118  
   1.119 @@ -154,69 +149,68 @@
   1.120    The first proof; The statement is very intuitive,
   1.121    but application of induction hypothesis requires the above lifting lemmas
   1.122  *}
   1.123 -theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.124 -shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
   1.125 -proof -
   1.126 -  from A show ?thesis
   1.127 -  proof induct
   1.128 -    show "\<And>s. ?P \<SKIP> s s" by simp
   1.129 -  next
   1.130 -    show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
   1.131 -  next
   1.132 -    fix c0 c1 s0 s1 s2
   1.133 -    assume "?P c0 s0 s1"
   1.134 -    hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
   1.135 -      by(rule app_right)
   1.136 -    moreover assume "?P c1 s1 s2"
   1.137 -    hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
   1.138 -           \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.139 -    proof -
   1.140 -      show "\<And>is1 is2 s1 s2 i2.
   1.141 -	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   1.142 -	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
   1.143 -	using app_left[of _ 0] by simp
   1.144 -    qed
   1.145 -    ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
   1.146 -                       \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.147 -      by (rule rtrancl_trans)
   1.148 -    thus "?P (c0; c1) s0 s2" by simp
   1.149 -  next
   1.150 -    fix b c0 c1 s0 s1
   1.151 -    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.152 -    assume "b s0" and IH: "?P c0 s0 s1"
   1.153 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.154 -    also from IH
   1.155 -    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
   1.156 -      by(auto intro:app1_left app_right)
   1.157 -    also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.158 -      by(auto)
   1.159 -    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.160 -  next
   1.161 -    fix b c0 c1 s0 s1
   1.162 -    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.163 -    assume "\<not>b s0" and IH: "?P c1 s0 s1"
   1.164 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
   1.165 -    also from IH
   1.166 -    have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.167 -      by(force intro!:app_left2 app1_left)
   1.168 -    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.169 -  next
   1.170 -    fix b c and s::state
   1.171 -    assume "\<not>b s"
   1.172 -    thus "?P (\<WHILE> b \<DO> c) s s" by force
   1.173 -  next
   1.174 -    fix b c and s0::state and s1 s2
   1.175 -    let ?comp = "compile(\<WHILE> b \<DO> c)"
   1.176 -    assume "b s0" and
   1.177 -      IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
   1.178 -    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.179 -    also from IHc
   1.180 -    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
   1.181 -      by(auto intro:app1_left app_right)
   1.182 -    also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
   1.183 -    also note IHw
   1.184 -    finally show "?P (\<WHILE> b \<DO> c) s0 s2".
   1.185 +theorem
   1.186 +  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   1.187 +  shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
   1.188 +  using prems
   1.189 +proof induct
   1.190 +  show "\<And>s. ?P \<SKIP> s s" by simp
   1.191 +next
   1.192 +  show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
   1.193 +next
   1.194 +  fix c0 c1 s0 s1 s2
   1.195 +  assume "?P c0 s0 s1"
   1.196 +  hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
   1.197 +    by (rule app_right)
   1.198 +  moreover assume "?P c1 s1 s2"
   1.199 +  hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
   1.200 +    \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.201 +  proof -
   1.202 +    show "\<And>is1 is2 s1 s2 i2.
   1.203 +      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
   1.204 +      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
   1.205 +      using app_left[of _ 0] by simp
   1.206    qed
   1.207 +  ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
   1.208 +      \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
   1.209 +    by (rule rtrancl_trans)
   1.210 +  thus "?P (c0; c1) s0 s2" by simp
   1.211 +next
   1.212 +  fix b c0 c1 s0 s1
   1.213 +  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.214 +  assume "b s0" and IH: "?P c0 s0 s1"
   1.215 +  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.216 +  also from IH
   1.217 +  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
   1.218 +    by(auto intro:app1_left app_right)
   1.219 +  also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.220 +    by(auto)
   1.221 +  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.222 +next
   1.223 +  fix b c0 c1 s0 s1
   1.224 +  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
   1.225 +  assume "\<not>b s0" and IH: "?P c1 s0 s1"
   1.226 +  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
   1.227 +  also from IH
   1.228 +  have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
   1.229 +    by (force intro!: app_left2 app1_left)
   1.230 +  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
   1.231 +next
   1.232 +  fix b c and s::state
   1.233 +  assume "\<not>b s"
   1.234 +  thus "?P (\<WHILE> b \<DO> c) s s" by force
   1.235 +next
   1.236 +  fix b c and s0::state and s1 s2
   1.237 +  let ?comp = "compile(\<WHILE> b \<DO> c)"
   1.238 +  assume "b s0" and
   1.239 +    IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
   1.240 +  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
   1.241 +  also from IHc
   1.242 +  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
   1.243 +    by (auto intro: app1_left app_right)
   1.244 +  also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
   1.245 +  also note IHw
   1.246 +  finally show "?P (\<WHILE> b \<DO> c) s0 s2".
   1.247  qed
   1.248  
   1.249  text {*
     2.1 --- a/src/HOL/IMP/Denotation.thy	Thu Dec 08 20:15:41 2005 +0100
     2.2 +++ b/src/HOL/IMP/Denotation.thy	Thu Dec 08 20:15:50 2005 +0100
     2.3 @@ -12,9 +12,9 @@
     2.4  
     2.5  constdefs
     2.6    Gamma :: "[bexp,com_den] => (com_den => com_den)"
     2.7 -  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
     2.8 +  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
     2.9                         {(s,t). s=t \<and> \<not>b s})"
    2.10 -    
    2.11 +
    2.12  consts
    2.13    C :: "com => com_den"
    2.14  
    2.15 @@ -33,7 +33,7 @@
    2.16    by (unfold Gamma_def mono_def) fast
    2.17  
    2.18  lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
    2.19 -apply (simp (no_asm)) 
    2.20 +apply simp
    2.21  apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
    2.22  apply (simp add: Gamma_def)
    2.23  done
    2.24 @@ -42,7 +42,7 @@
    2.25  
    2.26  lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    2.27  (* start with rule induction *)
    2.28 -apply (erule evalc.induct)
    2.29 +apply (induct set: evalc)
    2.30  apply auto
    2.31  (* while *)
    2.32  apply (unfold Gamma_def)
    2.33 @@ -54,15 +54,14 @@
    2.34  
    2.35  (* Denotational Semantics implies Operational Semantics *)
    2.36  
    2.37 -lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    2.38 -apply (induct_tac "c")
    2.39 +lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    2.40 +apply (induct c fixing: s t)
    2.41  
    2.42 -apply (simp_all (no_asm_use))
    2.43 +apply simp_all
    2.44  apply fast
    2.45  apply fast
    2.46  
    2.47  (* while *)
    2.48 -apply (intro strip)
    2.49  apply (erule lfp_induct [OF _ Gamma_mono])
    2.50  apply (unfold Gamma_def)
    2.51  apply fast
    2.52 @@ -72,7 +71,6 @@
    2.53  (**** Proof of Equivalence ****)
    2.54  
    2.55  lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    2.56 -apply (fast elim: com2 dest: com1)
    2.57 -done
    2.58 +  by (fast elim: com2 dest: com1)
    2.59  
    2.60  end
     3.1 --- a/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:41 2005 +0100
     3.2 +++ b/src/HOL/IMP/Examples.thy	Thu Dec 08 20:15:50 2005 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  
     3.5  theory Examples imports Natural begin
     3.6  
     3.7 -constdefs  
     3.8 +constdefs
     3.9    factorial :: "loc => loc => com"
    3.10    "factorial a b == b :== (%s. 1);
    3.11                      \<WHILE> (%s. s a ~= 0) \<DO>
    3.12 @@ -18,16 +18,16 @@
    3.13  
    3.14  subsection "An example due to Tony Hoare"
    3.15  
    3.16 -lemma lemma1 [rule_format (no_asm)]: 
    3.17 -  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
    3.18 -  !c. w = While P c \<longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    3.19 -apply (erule evalc.induct)
    3.20 -apply auto
    3.21 -done
    3.22 +lemma lemma1:
    3.23 +  assumes 1: "!x. P x \<longrightarrow> Q x"
    3.24 +    and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
    3.25 +  shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    3.26 +  using 2 apply induct
    3.27 +  using 1 apply auto
    3.28 +  done
    3.29  
    3.30 -
    3.31 -lemma lemma2 [rule_format (no_asm)]: 
    3.32 -  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>  
    3.33 +lemma lemma2 [rule_format (no_asm)]:
    3.34 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
    3.35    !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    3.36  apply (erule evalc.induct)
    3.37  apply (simp_all (no_asm_simp))
    3.38 @@ -36,19 +36,16 @@
    3.39  apply auto
    3.40  done
    3.41  
    3.42 -
    3.43 -lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
    3.44 +lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
    3.45    (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    3.46    by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    3.47  
    3.48  
    3.49  subsection "Factorial"
    3.50  
    3.51 -lemma factorial_3: "a~=b ==>  
    3.52 -  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    3.53 -apply (unfold factorial_def)
    3.54 -apply simp
    3.55 -done
    3.56 +lemma factorial_3: "a~=b ==>
    3.57 +    \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    3.58 +  by (simp add: factorial_def)
    3.59  
    3.60  text {* the same in single step mode: *}
    3.61  lemmas [simp del] = evalc_cases
    3.62 @@ -82,5 +79,5 @@
    3.63  apply (rule evalc.intros)
    3.64  apply simp
    3.65  done
    3.66 -  
    3.67 +
    3.68  end
     4.1 --- a/src/HOL/IMP/Expr.thy	Thu Dec 08 20:15:41 2005 +0100
     4.2 +++ b/src/HOL/IMP/Expr.thy	Thu Dec 08 20:15:50 2005 +0100
     4.3 @@ -134,12 +134,11 @@
     4.4    by (rule,cases set: evalb) auto
     4.5  
     4.6  
     4.7 -lemma aexp_iff:
     4.8 -  "!!n. ((a,s) -a-> n) = (A a s = n)"
     4.9 -  by (induct a) auto
    4.10 +lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
    4.11 +  by (induct a fixing: n) auto
    4.12  
    4.13  lemma bexp_iff:
    4.14 -  "!!w. ((b,s) -b-> w) = (B b s = w)"
    4.15 -  by (induct b) (auto simp add: aexp_iff)
    4.16 +  "((b,s) -b-> w) = (B b s = w)"
    4.17 +  by (induct b fixing: w) (auto simp add: aexp_iff)
    4.18  
    4.19  end
     5.1 --- a/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:41 2005 +0100
     5.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:50 2005 +0100
     5.3 @@ -32,7 +32,7 @@
     5.4  constdefs wp :: "com => assn => assn"
     5.5            "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
     5.6  
     5.7 -(*  
     5.8 +(*
     5.9  Soundness (and part of) relative completeness of Hoare rules
    5.10  wrt denotational semantics
    5.11  *)
    5.12 @@ -52,7 +52,7 @@
    5.13  
    5.14  lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    5.15  apply (unfold hoare_valid_def)
    5.16 -apply (erule hoare.induct)
    5.17 +apply (induct set: hoare)
    5.18       apply (simp_all (no_asm_simp))
    5.19    apply fast
    5.20   apply fast
    5.21 @@ -80,7 +80,7 @@
    5.22  apply fast
    5.23  done
    5.24  
    5.25 -lemma wp_If: 
    5.26 +lemma wp_If:
    5.27   "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    5.28  apply (unfold wp_def)
    5.29  apply (simp (no_asm))
    5.30 @@ -88,7 +88,7 @@
    5.31  apply fast
    5.32  done
    5.33  
    5.34 -lemma wp_While_True: 
    5.35 +lemma wp_While_True:
    5.36    "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    5.37  apply (unfold wp_def)
    5.38  apply (subst C_While_If)
    5.39 @@ -104,12 +104,11 @@
    5.40  lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    5.41  
    5.42  (*Not suitable for rewriting: LOOPS!*)
    5.43 -lemma wp_While_if: 
    5.44 +lemma wp_While_if:
    5.45    "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    5.46 -apply (simp (no_asm))
    5.47 -done
    5.48 +  by simp
    5.49  
    5.50 -lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =  
    5.51 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    5.52     (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    5.53  apply (simp (no_asm))
    5.54  apply (rule iffI)
    5.55 @@ -131,18 +130,17 @@
    5.56  
    5.57  declare C_while [simp del]
    5.58  
    5.59 -lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If 
    5.60 +lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
    5.61  
    5.62 -lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
    5.63 -apply (induct_tac "c")
    5.64 +lemma wp_is_pre: "|- {wp c Q} c {Q}"
    5.65 +apply (induct c fixing: Q)
    5.66      apply (simp_all (no_asm))
    5.67      apply fast+
    5.68   apply (blast intro: hoare_conseq1)
    5.69 -apply safe
    5.70  apply (rule hoare_conseq2)
    5.71   apply (rule hoare.While)
    5.72   apply (rule hoare_conseq1)
    5.73 -  prefer 2 apply (fast)
    5.74 +  prefer 2 apply fast
    5.75    apply safe
    5.76   apply simp
    5.77  apply simp
     6.1 --- a/src/HOL/IMP/Machines.thy	Thu Dec 08 20:15:41 2005 +0100
     6.2 +++ b/src/HOL/IMP/Machines.thy	Thu Dec 08 20:15:50 2005 +0100
     6.3 @@ -1,28 +1,31 @@
     6.4 +
     6.5 +(* $Id$ *)
     6.6 +
     6.7  theory Machines imports Natural begin
     6.8  
     6.9  lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
    6.10 -by(fast intro:rtrancl.intros elim:rtranclE)
    6.11 +  by (fast intro: rtrancl.intros elim: rtranclE)
    6.12  
    6.13  lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
    6.14 -by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
    6.15 +  by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
    6.16  
    6.17  lemmas converse_rel_powE = rel_pow_E2
    6.18  
    6.19  lemma R_O_Rn_commute: "R O R^n = R^n O R"
    6.20 -by(induct_tac n, simp, simp add: O_assoc[symmetric])
    6.21 +  by (induct n) (simp, simp add: O_assoc [symmetric])
    6.22  
    6.23  lemma converse_in_rel_pow_eq:
    6.24 -"((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
    6.25 +  "((x,z) \<in> R^n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R^m))"
    6.26  apply(rule iffI)
    6.27   apply(blast elim:converse_rel_powE)
    6.28  apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
    6.29  done
    6.30  
    6.31  lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
    6.32 -by(induct n, simp, simp add:O_assoc)
    6.33 +  by (induct n) (simp, simp add: O_assoc)
    6.34  
    6.35  lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
    6.36 -by(simp add:rel_pow_plus rel_compI)
    6.37 +  by (simp add: rel_pow_plus rel_compI)
    6.38  
    6.39  subsection "Instructions"
    6.40  
    6.41 @@ -33,7 +36,7 @@
    6.42  
    6.43  subsection "M0 with PC"
    6.44  
    6.45 -consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" 
    6.46 +consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
    6.47  syntax
    6.48    "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    6.49                 ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
    6.50 @@ -58,7 +61,7 @@
    6.51    "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    6.52                 ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    6.53  
    6.54 -translations  
    6.55 +translations
    6.56    "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
    6.57    "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
    6.58    "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
    6.59 @@ -97,7 +100,7 @@
    6.60    "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
    6.61                 ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
    6.62  
    6.63 -translations  
    6.64 +translations
    6.65    "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
    6.66    "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
    6.67    "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
    6.68 @@ -156,7 +159,7 @@
    6.69  lemma direction1:
    6.70   "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
    6.71    rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
    6.72 -apply(erule stepa1.induct)
    6.73 +apply(induct set: stepa1)
    6.74     apply(simp add:exec01.SET)
    6.75    apply(fastsimp intro:exec01.JMPFT)
    6.76   apply simp
    6.77 @@ -187,9 +190,9 @@
    6.78  *)
    6.79  lemma direction2:
    6.80   "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
    6.81 - \<forall>p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
    6.82 +  rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
    6.83            rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
    6.84 -apply(erule exec01.induct)
    6.85 +apply(induct fixing: p q p' q' set: exec01)
    6.86     apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
    6.87     apply(drule sym)
    6.88     apply simp
    6.89 @@ -216,6 +219,6 @@
    6.90  theorem M_eqiv:
    6.91  "(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
    6.92   (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
    6.93 -by(fast dest:direction1 direction2)
    6.94 +  by (blast dest: direction1 direction2)
    6.95  
    6.96  end
     7.1 --- a/src/HOL/IMP/Natural.thy	Thu Dec 08 20:15:41 2005 +0100
     7.2 +++ b/src/HOL/IMP/Natural.thy	Thu Dec 08 20:15:50 2005 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  
     7.5  subsection "Execution of commands"
     7.6  
     7.7 -consts  evalc   :: "(com \<times> state \<times> state) set" 
     7.8 +consts  evalc   :: "(com \<times> state \<times> state) set"
     7.9  syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
    7.10  
    7.11  syntax (xsymbols)
    7.12 @@ -21,7 +21,7 @@
    7.13    "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    7.14  
    7.15  text {*
    7.16 -  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
    7.17 +  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
    7.18    in state @{text s}, terminates in state @{text s'}}. Formally,
    7.19    @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
    7.20    @{text "(c,s,s')"} is part of the relation @{text evalc}}:
    7.21 @@ -39,7 +39,7 @@
    7.22    The big-step execution relation @{text evalc} is defined inductively:
    7.23  *}
    7.24  inductive evalc
    7.25 -  intros 
    7.26 +  intros
    7.27    Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
    7.28    Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
    7.29  
    7.30 @@ -49,7 +49,7 @@
    7.31    IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
    7.32  
    7.33    WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
    7.34 -  WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'  
    7.35 +  WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
    7.36                 \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
    7.37  
    7.38  lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
    7.39 @@ -60,7 +60,7 @@
    7.40  @{thm [display] evalc.induct [no_vars]}
    7.41  
    7.42  
    7.43 -(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's 
    7.44 +(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
    7.45    meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
    7.46  *}
    7.47  
    7.48 @@ -70,35 +70,35 @@
    7.49    syntactic category there is always only one rule applicable. That
    7.50    means we can use the rules in both directions. The proofs for this
    7.51    are all the same: one direction is trivial, the other one is shown
    7.52 -  by using the @{text evalc} rules backwards: 
    7.53 +  by using the @{text evalc} rules backwards:
    7.54  *}
    7.55 -lemma skip: 
    7.56 +lemma skip:
    7.57    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    7.58    by (rule, erule evalc.elims) auto
    7.59  
    7.60 -lemma assign: 
    7.61 -  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])" 
    7.62 +lemma assign:
    7.63 +  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
    7.64    by (rule, erule evalc.elims) auto
    7.65  
    7.66 -lemma semi: 
    7.67 +lemma semi:
    7.68    "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
    7.69    by (rule, erule evalc.elims) auto
    7.70  
    7.71 -lemma ifTrue: 
    7.72 -  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" 
    7.73 +lemma ifTrue:
    7.74 +  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
    7.75    by (rule, erule evalc.elims) auto
    7.76  
    7.77 -lemma ifFalse: 
    7.78 +lemma ifFalse:
    7.79    "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
    7.80    by (rule, erule evalc.elims) auto
    7.81  
    7.82 -lemma whileFalse: 
    7.83 +lemma whileFalse:
    7.84    "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
    7.85 -  by (rule, erule evalc.elims) auto  
    7.86 +  by (rule, erule evalc.elims) auto
    7.87  
    7.88 -lemma whileTrue: 
    7.89 -  "b s \<Longrightarrow> 
    7.90 -  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' = 
    7.91 +lemma whileTrue:
    7.92 +  "b s \<Longrightarrow>
    7.93 +  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
    7.94    (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
    7.95    by (rule, erule evalc.elims) auto
    7.96  
    7.97 @@ -112,7 +112,7 @@
    7.98    big-step semantics when \emph{@{text c} started in @{text s} terminates
    7.99    in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   7.100    in the same @{text s'}}. Formally:
   7.101 -*} 
   7.102 +*}
   7.103  constdefs
   7.104    equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
   7.105    "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
   7.106 @@ -120,7 +120,7 @@
   7.107  text {*
   7.108    Proof rules telling Isabelle to unfold the definition
   7.109    if there is something to be proved about equivalent
   7.110 -  statements: *} 
   7.111 +  statements: *}
   7.112  lemma equivI [intro!]:
   7.113    "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
   7.114    by (unfold equiv_c_def) blast
   7.115 @@ -141,7 +141,7 @@
   7.116    "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
   7.117  proof -
   7.118    -- "to show the equivalence, we look at the derivation tree for"
   7.119 -  -- "each side and from that construct a derivation tree for the other side"  
   7.120 +  -- "each side and from that construct a derivation tree for the other side"
   7.121    { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
   7.122      -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
   7.123      -- "then both statements do nothing:"
   7.124 @@ -159,8 +159,8 @@
   7.125        -- "then the whole @{text \<IF>}"
   7.126        with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
   7.127      }
   7.128 -    ultimately 
   7.129 -    -- "both cases together give us what we want:"      
   7.130 +    ultimately
   7.131 +    -- "both cases together give us what we want:"
   7.132      have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   7.133    }
   7.134    moreover
   7.135 @@ -180,9 +180,9 @@
   7.136          "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
   7.137        -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
   7.138        with b
   7.139 -      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue) 
   7.140 +      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
   7.141      }
   7.142 -    ultimately 
   7.143 +    ultimately
   7.144      -- "both cases together again give us what we want:"
   7.145      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   7.146    }
   7.147 @@ -196,91 +196,89 @@
   7.148  text {*
   7.149  The following proof presents all the details:
   7.150  *}
   7.151 -theorem com_det: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
   7.152 -proof clarify -- "transform the goal into canonical form"
   7.153 -  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   7.154 -  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
   7.155 -  proof (induct set: evalc)
   7.156 -    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.157 -    thus "u = s" by simp
   7.158 -  next
   7.159 -    fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.160 -    thus "u = s[x \<mapsto> a s]" by simp      
   7.161 -  next
   7.162 -    fix c0 c1 s s1 s2 u
   7.163 -    assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.164 -    assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.165 +theorem com_det:
   7.166 +  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.167 +  shows "u = t"
   7.168 +  using prems
   7.169 +proof (induct fixing: u set: evalc)
   7.170 +  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.171 +  thus "u = s" by simp
   7.172 +next
   7.173 +  fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.174 +  thus "u = s[x \<mapsto> a s]" by simp
   7.175 +next
   7.176 +  fix c0 c1 s s1 s2 u
   7.177 +  assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.178 +  assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.179  
   7.180 -    assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
   7.181 -    then obtain s' where
   7.182 +  assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
   7.183 +  then obtain s' where
   7.184        c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   7.185 -      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u" 
   7.186 -      by auto
   7.187 +      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
   7.188 +    by auto
   7.189  
   7.190 -    from c0 IH0 have "s'=s2" by blast
   7.191 -    with c1 IH1 show "u=s1" by blast
   7.192 -  next
   7.193 -    fix b c0 c1 s s1 u
   7.194 -    assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
   7.195 +  from c0 IH0 have "s'=s2" by blast
   7.196 +  with c1 IH1 show "u=s1" by blast
   7.197 +next
   7.198 +  fix b c0 c1 s s1 u
   7.199 +  assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.200  
   7.201 -    assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.202 -    hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   7.203 -    with IH show "u = s1" by blast
   7.204 -  next
   7.205 -    fix b c0 c1 s s1 u
   7.206 -    assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
   7.207 +  assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.208 +  hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   7.209 +  with IH show "u = s1" by blast
   7.210 +next
   7.211 +  fix b c0 c1 s s1 u
   7.212 +  assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.213  
   7.214 -    assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.215 -    hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   7.216 -    with IH show "u = s1" by blast
   7.217 -  next
   7.218 -    fix b c s u
   7.219 -    assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.220 -    thus "u = s" by simp
   7.221 -  next
   7.222 -    fix b c s s1 s2 u
   7.223 -    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.224 -    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.225 -    
   7.226 -    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.227 -    then obtain s' where
   7.228 +  assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.229 +  hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
   7.230 +  with IH show "u = s1" by blast
   7.231 +next
   7.232 +  fix b c s u
   7.233 +  assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.234 +  thus "u = s" by simp
   7.235 +next
   7.236 +  fix b c s s1 s2 u
   7.237 +  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.238 +  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.239 +
   7.240 +  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.241 +  then obtain s' where
   7.242        c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   7.243 -      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" 
   7.244 -      by auto
   7.245 -    
   7.246 -    from c "IH\<^sub>c" have "s' = s2" by blast
   7.247 -    with w "IH\<^sub>w" show "u = s1" by blast
   7.248 -  qed
   7.249 +      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   7.250 +    by auto
   7.251 +
   7.252 +  from c "IH\<^sub>c" have "s' = s2" by blast
   7.253 +  with w "IH\<^sub>w" show "u = s1" by blast
   7.254  qed
   7.255  
   7.256  
   7.257  text {*
   7.258    This is the proof as you might present it in a lecture. The remaining
   7.259 -  cases are simple enough to be proved automatically: 
   7.260 -*} 
   7.261 -theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t" 
   7.262 -proof clarify
   7.263 -  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   7.264 -  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
   7.265 -  proof (induct set: evalc)
   7.266 -    -- "the simple @{text \<SKIP>} case for demonstration:"
   7.267 -    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.268 -    thus "u = s" by simp
   7.269 -  next
   7.270 -    -- "and the only really interesting case, @{text \<WHILE>}:"
   7.271 -    fix b c s s1 s2 u
   7.272 -    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.273 -    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.274 -    
   7.275 -    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.276 -    then obtain s' where
   7.277 +  cases are simple enough to be proved automatically:
   7.278 +*}
   7.279 +theorem
   7.280 +  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.281 +  shows "u = t"
   7.282 +  using prems
   7.283 +proof (induct fixing: u)
   7.284 +  -- "the simple @{text \<SKIP>} case for demonstration:"
   7.285 +  fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.286 +  thus "u = s" by simp
   7.287 +next
   7.288 +  -- "and the only really interesting case, @{text \<WHILE>}:"
   7.289 +  fix b c s s1 s2 u
   7.290 +  assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
   7.291 +  assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
   7.292 +
   7.293 +  assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
   7.294 +  then obtain s' where
   7.295        c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
   7.296        w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
   7.297 -      by auto
   7.298 -    
   7.299 -    from c "IH\<^sub>c" have "s' = s2" by blast
   7.300 -    with w "IH\<^sub>w" show "u = s1" by blast
   7.301 -  qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
   7.302 -qed
   7.303 +    by auto
   7.304 +
   7.305 +  from c "IH\<^sub>c" have "s' = s2" by blast
   7.306 +  with w "IH\<^sub>w" show "u = s1" by blast
   7.307 +qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
   7.308  
   7.309  end
     8.1 --- a/src/HOL/IMP/Transition.thy	Thu Dec 08 20:15:41 2005 +0100
     8.2 +++ b/src/HOL/IMP/Transition.thy	Thu Dec 08 20:15:50 2005 +0100
     8.3 @@ -15,16 +15,16 @@
     8.4    We formalize the transition semantics as in \cite{Nielson}. This
     8.5    makes some of the rules a bit more intuitive, but also requires
     8.6    some more (internal) formal overhead.
     8.7 -  
     8.8 -  Since configurations that have terminated are written without 
     8.9 -  a statement, the transition relation is not 
    8.10 +
    8.11 +  Since configurations that have terminated are written without
    8.12 +  a statement, the transition relation is not
    8.13    @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
    8.14    but instead:
    8.15  *}
    8.16  consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
    8.17  
    8.18  text {*
    8.19 -  Some syntactic sugar that we will use to hide the 
    8.20 +  Some syntactic sugar that we will use to hide the
    8.21    @{text option} part in configurations:
    8.22  *}
    8.23  syntax
    8.24 @@ -65,21 +65,21 @@
    8.25  
    8.26  translations
    8.27    "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
    8.28 -  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" 
    8.29 -  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" 
    8.30 +  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n"
    8.31 +  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*"
    8.32  
    8.33 -  -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, 
    8.34 +  -- {* Isabelle/HOL converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
    8.35          so we also include: *}
    8.36 -  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"   
    8.37 +  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"
    8.38    "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
    8.39 -  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" 
    8.40 +  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*"
    8.41  
    8.42  text {*
    8.43    Now, finally, we are set to write down the rules for our small step semantics:
    8.44  *}
    8.45  inductive evalc1
    8.46    intros
    8.47 -  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"  
    8.48 +  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
    8.49    Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
    8.50  
    8.51    Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
    8.52 @@ -96,42 +96,40 @@
    8.53  (* fixme: move to Relation_Power.thy *)
    8.54  lemma rel_pow_Suc_E2 [elim!]:
    8.55    "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
    8.56 -  by (drule rel_pow_Suc_D2) blast
    8.57 +  by (blast dest: rel_pow_Suc_D2)
    8.58  
    8.59  lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
    8.60 -proof -
    8.61 -  assume "p \<in> R\<^sup>*"
    8.62 -  moreover obtain x y where p: "p = (x,y)" by (cases p)
    8.63 -  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
    8.64 -  hence "\<exists>n. (x,y) \<in> R^n"
    8.65 +proof (induct p)
    8.66 +  fix x y
    8.67 +  assume "(x, y) \<in> R\<^sup>*"
    8.68 +  thus "\<exists>n. (x, y) \<in> R^n"
    8.69    proof induct
    8.70 -    fix a have "(a,a) \<in> R^0" by simp
    8.71 -    thus "\<exists>n. (a,a) \<in> R ^ n" ..
    8.72 +    fix a have "(a, a) \<in> R^0" by simp
    8.73 +    thus "\<exists>n. (a, a) \<in> R ^ n" ..
    8.74    next
    8.75 -    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
    8.76 -    then obtain n where "(a,b) \<in> R^n" ..
    8.77 -    moreover assume "(b,c) \<in> R"
    8.78 -    ultimately have "(a,c) \<in> R^(Suc n)" by auto
    8.79 -    thus "\<exists>n. (a,c) \<in> R^n" ..
    8.80 +    fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
    8.81 +    then obtain n where "(a, b) \<in> R^n" ..
    8.82 +    moreover assume "(b, c) \<in> R"
    8.83 +    ultimately have "(a, c) \<in> R^(Suc n)" by auto
    8.84 +    thus "\<exists>n. (a, c) \<in> R^n" ..
    8.85    qed
    8.86 -  with p show ?thesis by hypsubst
    8.87 -qed  
    8.88 -(*>*)    
    8.89 +qed
    8.90 +(*>*)
    8.91  text {*
    8.92 -  As for the big step semantics you can read these rules in a 
    8.93 +  As for the big step semantics you can read these rules in a
    8.94    syntax directed way:
    8.95  *}
    8.96 -lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" 
    8.97 -  by (rule, cases set: evalc1, auto)      
    8.98 +lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
    8.99 +  by (rule, cases set: evalc1, auto)
   8.100  
   8.101  lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
   8.102    by (rule, cases set: evalc1, auto)
   8.103  
   8.104 -lemma Cond_1: 
   8.105 +lemma Cond_1:
   8.106    "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
   8.107    by (rule, cases set: evalc1, auto)
   8.108  
   8.109 -lemma While_1: 
   8.110 +lemma While_1:
   8.111    "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
   8.112    by (rule, cases set: evalc1, auto)
   8.113  
   8.114 @@ -140,7 +138,7 @@
   8.115  
   8.116  subsection "Examples"
   8.117  
   8.118 -lemma 
   8.119 +lemma
   8.120    "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
   8.121    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
   8.122  proof -
   8.123 @@ -148,45 +146,45 @@
   8.124    let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
   8.125    assume [simp]: "s x = 0"
   8.126    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   8.127 -  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp 
   8.128 -  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
   8.129 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
   8.130 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp
   8.131    also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
   8.132    also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
   8.133    also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
   8.134    finally show ?thesis ..
   8.135  qed
   8.136  
   8.137 -lemma 
   8.138 +lemma
   8.139    "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
   8.140    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
   8.141  proof -
   8.142    let ?c = "x:== \<lambda>s. s x+1"
   8.143 -  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"  
   8.144 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
   8.145    assume [simp]: "s x = 2"
   8.146    note update_def [simp]
   8.147    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
   8.148    also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
   8.149 -  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
   8.150 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp
   8.151    also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
   8.152    also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
   8.153 -  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
   8.154 +  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp
   8.155    also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
   8.156    also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
   8.157 -  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp) 
   8.158 +  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp
   8.159    oops
   8.160  
   8.161  subsection "Basic properties"
   8.162  
   8.163 -text {* 
   8.164 +text {*
   8.165    There are no \emph{stuck} programs:
   8.166  *}
   8.167  lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
   8.168  proof (induct c)
   8.169    -- "case Semi:"
   8.170 -  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" 
   8.171 +  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
   8.172    then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
   8.173    then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
   8.174 -    by (cases y, cases "fst y", auto)
   8.175 +    by (cases y, cases "fst y") auto
   8.176    thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
   8.177  next
   8.178    -- "case If:"
   8.179 @@ -198,22 +196,22 @@
   8.180    If a configuration does not contain a statement, the program
   8.181    has terminated and there is no next configuration:
   8.182  *}
   8.183 -lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" 
   8.184 +lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
   8.185    by (auto elim: evalc1.elims)
   8.186  
   8.187 -lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" 
   8.188 -  by (erule rtrancl_induct) auto 
   8.189 +lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
   8.190 +  by (induct set: rtrancl) auto
   8.191  
   8.192  (*<*)
   8.193 -(* fixme: relpow.simps don't work *)
   8.194 +(* FIXME: relpow.simps don't work *)
   8.195  lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
   8.196 -lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
   8.197 +lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
   8.198  lemmas [simp del] = relpow.simps
   8.199  (*>*)
   8.200  lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   8.201    by (cases n) auto
   8.202  
   8.203 -lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
   8.204 +lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"
   8.205    by (cases n) auto
   8.206  
   8.207  subsection "Equivalence to natural semantics (after Nielson and Nielson)"
   8.208 @@ -223,72 +221,70 @@
   8.209    decomposition and composition.
   8.210  *}
   8.211  lemma semiD:
   8.212 -  "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> 
   8.213 +  "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
   8.214    \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
   8.215 -  (is "PROP ?P n")
   8.216 -proof (induct n)
   8.217 -  show "PROP ?P 0" by simp
   8.218 +proof (induct n fixing: c1 c2 s s'')
   8.219 +  case 0
   8.220 +  then show ?case by simp
   8.221  next
   8.222 -  fix n assume IH: "PROP ?P n"
   8.223 -  show "PROP ?P (Suc n)"
   8.224 -  proof -
   8.225 -    fix c1 c2 s s''
   8.226 -    assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   8.227 -    then obtain y where
   8.228 +  case (Suc n)
   8.229 +
   8.230 +  from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
   8.231 +  obtain y where
   8.232        1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
   8.233        n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   8.234 -      by blast
   8.235 +    by blast
   8.236  
   8.237 -    from 1
   8.238 -    show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
   8.239 -      (is "\<exists>i j s'. ?Q i j s'")
   8.240 -    proof (cases set: evalc1)
   8.241 -      case Semi1
   8.242 -      then obtain s' where
   8.243 +  from 1
   8.244 +  show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
   8.245 +    (is "\<exists>i j s'. ?Q i j s'")
   8.246 +  proof (cases set: evalc1)
   8.247 +    case Semi1
   8.248 +    then obtain s' where
   8.249          "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   8.250 -        by auto
   8.251 -      with 1 n have "?Q 1 n s'" by simp
   8.252 -      thus ?thesis by blast
   8.253 -    next
   8.254 -      case Semi2
   8.255 -      then obtain c1' s' where
   8.256 +      by auto
   8.257 +    with 1 n have "?Q 1 n s'" by simp
   8.258 +    thus ?thesis by blast
   8.259 +  next
   8.260 +    case Semi2
   8.261 +    then obtain c1' s' where
   8.262          y:  "y = \<langle>c1'; c2, s'\<rangle>" and
   8.263          c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
   8.264 -        by auto
   8.265 -      with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp 
   8.266 -      with IH obtain i j s0 where 
   8.267 +      by auto
   8.268 +    with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
   8.269 +    with Suc.hyps obtain i j s0 where
   8.270          c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
   8.271          c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   8.272          i:   "n = i+j"
   8.273 -        by fast
   8.274 -          
   8.275 -      from c1 c1'
   8.276 -      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
   8.277 -      with c2 i
   8.278 -      have "?Q (i+1) j s0" by simp
   8.279 -      thus ?thesis by blast
   8.280 -    qed auto -- "the remaining cases cannot occur"
   8.281 -  qed
   8.282 +      by fast
   8.283 +
   8.284 +    from c1 c1'
   8.285 +    have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
   8.286 +    with c2 i
   8.287 +    have "?Q (i+1) j s0" by simp
   8.288 +    thus ?thesis by blast
   8.289 +  qed auto -- "the remaining cases cannot occur"
   8.290  qed
   8.291  
   8.292  
   8.293 -lemma semiI: 
   8.294 -  "\<And>c0 s s''. \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.295 -proof (induct n)
   8.296 -  fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   8.297 -  hence False by simp
   8.298 -  thus "?thesis c0 s s''" ..
   8.299 +lemma semiI:
   8.300 +  "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.301 +proof (induct n fixing: c0 s s'')
   8.302 +  case 0
   8.303 +  from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
   8.304 +  have False by simp
   8.305 +  thus ?case ..
   8.306  next
   8.307 -  fix c0 s s'' n 
   8.308 -  assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
   8.309 -  assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.310 -  assume IH: "\<And>c0 s s''.
   8.311 -    \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.312 -  from c0 obtain y where 
   8.313 +  case (Suc n)
   8.314 +  note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
   8.315 +  note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
   8.316 +  note IH = `\<And>c0 s s''.
   8.317 +    \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
   8.318 +  from c0 obtain y where
   8.319      1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
   8.320    from 1 obtain c0' s0' where
   8.321 -    "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" 
   8.322 -    by (cases y, cases "fst y", auto)
   8.323 +      "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
   8.324 +    by (cases y, cases "fst y") auto
   8.325    moreover
   8.326    { assume y: "y = \<langle>s0'\<rangle>"
   8.327      with n have "s'' = s0'" by simp
   8.328 @@ -312,57 +308,55 @@
   8.329  text {*
   8.330    The easy direction of the equivalence proof:
   8.331  *}
   8.332 -lemma evalc_imp_evalc1: 
   8.333 -  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.334 -proof -
   8.335 -  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.336 -  thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.337 -  proof induct
   8.338 -    fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
   8.339 -  next
   8.340 -    fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
   8.341 -  next
   8.342 -    fix c0 c1 s s'' s'
   8.343 -    assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   8.344 -    then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   8.345 -    moreover
   8.346 -    assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.347 -    ultimately
   8.348 -    show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
   8.349 -  next
   8.350 -    fix s::state and b c0 c1 s'
   8.351 -    assume "b s"
   8.352 -    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
   8.353 -    also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" 
   8.354 -    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   8.355 -  next
   8.356 -    fix s::state and b c0 c1 s'
   8.357 -    assume "\<not>b s"
   8.358 -    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
   8.359 -    also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.360 -    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   8.361 -  next
   8.362 -    fix b c and s::state
   8.363 -    assume b: "\<not>b s"
   8.364 -    let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
   8.365 -    have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   8.366 -    also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
   8.367 -    also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
   8.368 -    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   8.369 -  next
   8.370 -    fix b c s s'' s'
   8.371 -    let ?w  = "\<WHILE> b \<DO> c"
   8.372 -    let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
   8.373 -    assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.374 -    assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   8.375 -    assume b: "b s"
   8.376 -    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   8.377 -    also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
   8.378 -    also 
   8.379 -    from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   8.380 -    with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
   8.381 -    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
   8.382 -  qed
   8.383 +lemma evalc_imp_evalc1:
   8.384 +  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.385 +  shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.386 +  using prems
   8.387 +proof induct
   8.388 +  fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
   8.389 +next
   8.390 +  fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
   8.391 +next
   8.392 +  fix c0 c1 s s'' s'
   8.393 +  assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   8.394 +  then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   8.395 +  moreover
   8.396 +  assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.397 +  ultimately
   8.398 +  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
   8.399 +next
   8.400 +  fix s::state and b c0 c1 s'
   8.401 +  assume "b s"
   8.402 +  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
   8.403 +  also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.404 +  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   8.405 +next
   8.406 +  fix s::state and b c0 c1 s'
   8.407 +  assume "\<not>b s"
   8.408 +  hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
   8.409 +  also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.410 +  finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
   8.411 +next
   8.412 +  fix b c and s::state
   8.413 +  assume b: "\<not>b s"
   8.414 +  let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
   8.415 +  have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   8.416 +  also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
   8.417 +  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
   8.418 +  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
   8.419 +next
   8.420 +  fix b c s s'' s'
   8.421 +  let ?w  = "\<WHILE> b \<DO> c"
   8.422 +  let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
   8.423 +  assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.424 +  assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
   8.425 +  assume b: "b s"
   8.426 +  have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
   8.427 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
   8.428 +  also
   8.429 +  from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   8.430 +  with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
   8.431 +  finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
   8.432  qed
   8.433  
   8.434  text {*
   8.435 @@ -373,42 +367,42 @@
   8.436  proof
   8.437    assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.438    show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
   8.439 -next  
   8.440 +next
   8.441    assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   8.442    then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   8.443    moreover
   8.444 -  have "\<And>c s s'. \<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
   8.445 -  proof (induct rule: nat_less_induct)
   8.446 +  have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.447 +  proof (induct fixing: c s s' rule: less_induct)
   8.448      fix n
   8.449 -    assume IH: "\<forall>m. m < n \<longrightarrow> (\<forall>c s s'. \<langle>c, s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s')"
   8.450 +    assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.451      fix c s s'
   8.452      assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   8.453      then obtain m where n: "n = Suc m" by (cases n) auto
   8.454 -    with c obtain y where 
   8.455 +    with c obtain y where
   8.456        c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
   8.457 -    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
   8.458 +    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   8.459      proof (cases c)
   8.460        case SKIP
   8.461        with c n show ?thesis by auto
   8.462 -    next 
   8.463 +    next
   8.464        case Assign
   8.465        with c n show ?thesis by auto
   8.466      next
   8.467        fix c1 c2 assume semi: "c = (c1; c2)"
   8.468        with c obtain i j s'' where
   8.469 -        c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   8.470 -        c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
   8.471 -        ij: "n = i+j"
   8.472 +          c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
   8.473 +          c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
   8.474 +          ij: "n = i+j"
   8.475          by (blast dest: semiD)
   8.476 -      from c1 c2 obtain 
   8.477 +      from c1 c2 obtain
   8.478          "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
   8.479        with ij obtain
   8.480          i: "i < n" and j: "j < n" by simp
   8.481 -      from c1 i IH
   8.482 -      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
   8.483 +      from IH i c1
   8.484 +      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
   8.485        moreover
   8.486 -      from c2 j IH
   8.487 -      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   8.488 +      from IH j c2
   8.489 +      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
   8.490        moreover
   8.491        note semi
   8.492        ultimately
   8.493 @@ -417,33 +411,33 @@
   8.494        fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
   8.495        { assume True: "b s = True"
   8.496          with If c n
   8.497 -        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   8.498 +        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
   8.499          with n IH
   8.500          have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   8.501          with If True
   8.502 -        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   8.503 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   8.504        }
   8.505        moreover
   8.506        { assume False: "b s = False"
   8.507          with If c n
   8.508 -        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
   8.509 +        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
   8.510          with n IH
   8.511          have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   8.512          with If False
   8.513 -        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
   8.514 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   8.515        }
   8.516        ultimately
   8.517        show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
   8.518      next
   8.519        fix b c' assume w: "c = \<WHILE> b \<DO> c'"
   8.520 -      with c n 
   8.521 +      with c n
   8.522        have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
   8.523          (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
   8.524        with n IH
   8.525        have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   8.526        moreover note unfold_while [of b c']
   8.527        -- {* @{thm unfold_while [of b c']} *}
   8.528 -      ultimately      
   8.529 +      ultimately
   8.530        have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
   8.531        with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
   8.532      qed
   8.533 @@ -458,11 +452,11 @@
   8.534  declare rel_pow_0_E [elim!]
   8.535  
   8.536  text {*
   8.537 -  Winskel's small step rules are a bit different \cite{Winskel}; 
   8.538 +  Winskel's small step rules are a bit different \cite{Winskel};
   8.539    we introduce their equivalents as derived rules:
   8.540  *}
   8.541  lemma whileFalse1 [intro]:
   8.542 -  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")  
   8.543 +  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
   8.544  proof -
   8.545    assume "\<not>b s"
   8.546    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
   8.547 @@ -472,7 +466,7 @@
   8.548  qed
   8.549  
   8.550  lemma whileTrue1 [intro]:
   8.551 -  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" 
   8.552 +  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
   8.553    (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
   8.554  proof -
   8.555    assume "b s"
   8.556 @@ -481,8 +475,8 @@
   8.557    finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
   8.558  qed
   8.559  
   8.560 -inductive_cases evalc1_SEs: 
   8.561 -  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" 
   8.562 +inductive_cases evalc1_SEs:
   8.563 +  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t"
   8.564    "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
   8.565    "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   8.566    "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
   8.567 @@ -493,53 +487,53 @@
   8.568  declare evalc1_SEs [elim!]
   8.569  
   8.570  lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   8.571 -apply (erule evalc.induct)
   8.572 +apply (induct set: evalc)
   8.573  
   8.574 --- SKIP 
   8.575 +-- SKIP
   8.576  apply blast
   8.577  
   8.578 --- ASSIGN 
   8.579 +-- ASSIGN
   8.580  apply fast
   8.581  
   8.582 --- SEMI 
   8.583 +-- SEMI
   8.584  apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
   8.585  
   8.586 --- IF 
   8.587 +-- IF
   8.588  apply (fast intro: converse_rtrancl_into_rtrancl)
   8.589  apply (fast intro: converse_rtrancl_into_rtrancl)
   8.590  
   8.591 --- WHILE 
   8.592 +-- WHILE
   8.593  apply fast
   8.594  apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
   8.595  
   8.596  done
   8.597  
   8.598  
   8.599 -lemma lemma2 [rule_format (no_asm)]: 
   8.600 -  "\<forall>c d s u. \<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<longrightarrow> (\<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n)"
   8.601 -apply (induct_tac "n")
   8.602 +lemma lemma2:
   8.603 +  "\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
   8.604 +apply (induct n fixing: c d s u)
   8.605   -- "case n = 0"
   8.606   apply fastsimp
   8.607  -- "induction step"
   8.608 -apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
   8.609 +apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
   8.610              elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
   8.611  done
   8.612  
   8.613 -lemma evalc1_impl_evalc [rule_format (no_asm)]: 
   8.614 -  "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   8.615 -apply (induct_tac "c")
   8.616 +lemma evalc1_impl_evalc:
   8.617 +  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   8.618 +apply (induct c fixing: s t)
   8.619  apply (safe dest!: rtrancl_imp_UN_rel_pow)
   8.620  
   8.621  -- SKIP
   8.622  apply (simp add: SKIP_n)
   8.623  
   8.624 --- ASSIGN 
   8.625 +-- ASSIGN
   8.626  apply (fastsimp elim: rel_pow_E2)
   8.627  
   8.628  -- SEMI
   8.629  apply (fast dest!: rel_pow_imp_rtrancl lemma2)
   8.630  
   8.631 --- IF 
   8.632 +-- IF
   8.633  apply (erule rel_pow_E2)
   8.634  apply simp
   8.635  apply (fast dest!: rel_pow_imp_rtrancl)
   8.636 @@ -548,7 +542,7 @@
   8.637  apply (rename_tac b c s t n)
   8.638  apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
   8.639  apply (rule_tac x = "s" in spec)
   8.640 -apply (induct_tac "n" rule: nat_less_induct)
   8.641 +apply (induct_tac n rule: nat_less_induct)
   8.642  apply (intro strip)
   8.643  apply (erule rel_pow_E2)
   8.644   apply simp
   8.645 @@ -560,10 +554,11 @@
   8.646   apply (erule rel_pow_E2)
   8.647    apply simp
   8.648   apply (clarify dest!: lemma2)
   8.649 + apply atomize
   8.650   apply (erule allE, erule allE, erule impE, assumption)
   8.651   apply (erule_tac x=mb in allE, erule impE, fastsimp)
   8.652   apply blast
   8.653 --- WhileFalse 
   8.654 +-- WhileFalse
   8.655  apply (erule rel_pow_E2)
   8.656   apply simp
   8.657  apply (simp add: SKIP_n)
   8.658 @@ -572,8 +567,7 @@
   8.659  
   8.660  text {* proof of the equivalence of evalc and evalc1 *}
   8.661  lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
   8.662 -apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
   8.663 -done
   8.664 +  by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
   8.665  
   8.666  
   8.667  subsection "A proof without n"
   8.668 @@ -582,49 +576,50 @@
   8.669    The inductions are a bit awkward to write in this section,
   8.670    because @{text None} as result statement in the small step
   8.671    semantics doesn't have a direct counterpart in the big step
   8.672 -  semantics. 
   8.673 +  semantics.
   8.674  
   8.675    Winskel's small step rule set (using the @{text "\<SKIP>"} statement
   8.676    to indicate termination) is better suited for this proof.
   8.677  *}
   8.678  
   8.679 -lemma my_lemma1 [rule_format (no_asm)]: 
   8.680 -  "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<Longrightarrow> \<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.681 +lemma my_lemma1:
   8.682 +  assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
   8.683 +    and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.684 +  shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.685  proof -
   8.686    -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
   8.687 -  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow> 
   8.688 -       \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.689 -    apply (erule converse_rtrancl_induct2)
   8.690 +  from prems
   8.691 +  have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.692 +    apply (induct rule: converse_rtrancl_induct2)
   8.693       apply simp
   8.694      apply (rename_tac c s')
   8.695      apply simp
   8.696      apply (rule conjI)
   8.697 -     apply fast 
   8.698 +     apply fast
   8.699      apply clarify
   8.700      apply (case_tac c)
   8.701      apply (auto intro: converse_rtrancl_into_rtrancl)
   8.702      done
   8.703 -  moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
   8.704 -  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
   8.705 +  then show ?thesis by simp
   8.706  qed
   8.707  
   8.708  lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
   8.709 -apply (erule evalc.induct)
   8.710 +apply (induct set: evalc)
   8.711  
   8.712 --- SKIP 
   8.713 +-- SKIP
   8.714  apply fast
   8.715  
   8.716  -- ASSIGN
   8.717  apply fast
   8.718  
   8.719 --- SEMI 
   8.720 +-- SEMI
   8.721  apply (fast intro: my_lemma1)
   8.722  
   8.723  -- IF
   8.724  apply (fast intro: converse_rtrancl_into_rtrancl)
   8.725 -apply (fast intro: converse_rtrancl_into_rtrancl) 
   8.726 +apply (fast intro: converse_rtrancl_into_rtrancl)
   8.727  
   8.728 --- WHILE 
   8.729 +-- WHILE
   8.730  apply fast
   8.731  apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
   8.732  
   8.733 @@ -645,18 +640,18 @@
   8.734  
   8.735  Lemma 2
   8.736  ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
   8.737 -  => 
   8.738 +  =>
   8.739  <c,s> -c-> t
   8.740  
   8.741  This is proved by rule induction on the  -*-> relation
   8.742 -and the induction step makes use of a third lemma: 
   8.743 +and the induction step makes use of a third lemma:
   8.744  
   8.745  Lemma 3
   8.746  ((c,s) --> (c',s')) /\ <c',s'> -c'-> t
   8.747 -  => 
   8.748 +  =>
   8.749  <c,s> -c-> t
   8.750  
   8.751 -This captures the essence of the proof, as it shows that <c',s'> 
   8.752 +This captures the essence of the proof, as it shows that <c',s'>
   8.753  behaves as the continuation of <c,s> with respect to the natural
   8.754  semantics.
   8.755  The proof of Lemma 3 goes by rule induction on the --> relation,
   8.756 @@ -668,24 +663,22 @@
   8.757  
   8.758  inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
   8.759  
   8.760 -lemma FB_lemma3 [rule_format]:
   8.761 -  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
   8.762 -  (\<forall>t. \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t)"
   8.763 -  apply (erule evalc1.induct)
   8.764 -  apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   8.765 -  done
   8.766 +lemma FB_lemma3:
   8.767 +  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
   8.768 +  \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
   8.769 +  by (induct fixing: t set: evalc1)
   8.770 +    (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   8.771  
   8.772 -lemma FB_lemma2 [rule_format]:
   8.773 -  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
   8.774 -   \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t" 
   8.775 -  apply (erule converse_rtrancl_induct2)
   8.776 +lemma FB_lemma2:
   8.777 +  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
   8.778 +   \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
   8.779 +  apply (induct rule: converse_rtrancl_induct2)
   8.780     apply simp
   8.781    apply clarsimp
   8.782    apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   8.783    done
   8.784  
   8.785  lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   8.786 -  apply (fastsimp dest: FB_lemma2)
   8.787 -  done
   8.788 +  by (fastsimp dest: FB_lemma2)
   8.789  
   8.790  end
     9.1 --- a/src/HOL/IMP/VC.thy	Thu Dec 08 20:15:41 2005 +0100
     9.2 +++ b/src/HOL/IMP/VC.thy	Thu Dec 08 20:15:50 2005 +0100
     9.3 @@ -28,14 +28,14 @@
     9.4    "awp Askip Q = Q"
     9.5    "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
     9.6    "awp (Asemi c d) Q = awp c (awp d Q)"
     9.7 -  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
     9.8 +  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
     9.9    "awp (Awhile b I c) Q = I"
    9.10  
    9.11  primrec
    9.12    "vc Askip Q = (\<lambda>s. True)"
    9.13    "vc (Aass x a) Q = (\<lambda>s. True)"
    9.14    "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
    9.15 -  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)" 
    9.16 +  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
    9.17    "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
    9.18                                (I s & b s --> awp c I s) & vc c I s)"
    9.19  
    9.20 @@ -69,49 +69,50 @@
    9.21  
    9.22  lemma l: "!s. P s --> P s" by fast
    9.23  
    9.24 -lemma vc_sound: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    9.25 -apply (induct_tac "c")
    9.26 +lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    9.27 +apply (induct c fixing: Q)
    9.28      apply (simp_all (no_asm))
    9.29      apply fast
    9.30     apply fast
    9.31    apply fast
    9.32   (* if *)
    9.33 + apply atomize
    9.34   apply (tactic "Deepen_tac 4 1")
    9.35  (* while *)
    9.36 -apply (intro allI impI) 
    9.37 +apply atomize
    9.38 +apply (intro allI impI)
    9.39  apply (rule conseq)
    9.40    apply (rule l)
    9.41   apply (rule While)
    9.42   defer
    9.43   apply fast
    9.44 -apply (rule_tac P="awp acom fun2" in conseq)
    9.45 +apply (rule_tac P="awp c fun2" in conseq)
    9.46    apply fast
    9.47   apply fast
    9.48  apply fast
    9.49  done
    9.50  
    9.51 -lemma awp_mono [rule_format (no_asm)]: 
    9.52 +lemma awp_mono [rule_format (no_asm)]:
    9.53    "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    9.54 -apply (induct_tac "c")
    9.55 +apply (induct c)
    9.56      apply (simp_all (no_asm_simp))
    9.57  apply (rule allI, rule allI, rule impI)
    9.58  apply (erule allE, erule allE, erule mp)
    9.59  apply (erule allE, erule allE, erule mp, assumption)
    9.60  done
    9.61  
    9.62 -
    9.63 -lemma vc_mono [rule_format (no_asm)]: 
    9.64 +lemma vc_mono [rule_format (no_asm)]:
    9.65    "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    9.66 -apply (induct_tac "c")
    9.67 +apply (induct c)
    9.68      apply (simp_all (no_asm_simp))
    9.69  apply safe
    9.70 -apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) 
    9.71 +apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
    9.72  prefer 2 apply assumption
    9.73  apply (fast elim: awp_mono)
    9.74  done
    9.75  
    9.76  lemma vc_complete: assumes der: "|- {P}c{Q}"
    9.77 -  shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
    9.78 +  shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
    9.79    (is "? ac. ?Eq P c Q ac")
    9.80  using der
    9.81  proof induct
    9.82 @@ -149,9 +150,7 @@
    9.83    case conseq thus ?case by(fast elim!: awp_mono vc_mono)
    9.84  qed
    9.85  
    9.86 -lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
    9.87 -apply (induct_tac "c")
    9.88 -apply (simp_all (no_asm_simp) add: Let_def)
    9.89 -done
    9.90 +lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
    9.91 +  by (induct c fixing: Q) (simp_all add: Let_def)
    9.92  
    9.93  end
    10.1 --- a/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:41 2005 +0100
    10.2 +++ b/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:50 2005 +0100
    10.3 @@ -163,15 +163,13 @@
    10.4  *}
    10.5  
    10.6  theorem quot_cond_function:
    10.7 -  "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
    10.8 -    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
    10.9 -      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
   10.10 -    P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   10.11 -  (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
   10.12 +  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   10.13 +    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   10.14 +      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   10.15 +    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   10.16 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   10.17  proof -
   10.18 -  assume cong: "PROP ?cong"
   10.19 -  assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   10.20 -  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   10.21 +  from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   10.22    also have "... = g a b"
   10.23    proof (rule cong)
   10.24      show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   10.25 @@ -185,18 +183,16 @@
   10.26  qed
   10.27  
   10.28  theorem quot_function:
   10.29 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   10.30 -    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
   10.31 -    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   10.32 -proof -
   10.33 -  case rule_context from this TrueI
   10.34 -  show ?thesis by (rule quot_cond_function)
   10.35 -qed
   10.36 +  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   10.37 +    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   10.38 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   10.39 +  using prems and TrueI
   10.40 +  by (rule quot_cond_function)
   10.41  
   10.42  theorem quot_function':
   10.43    "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   10.44      (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   10.45      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   10.46 -  by  (rule quot_function) (simp only: quot_equality)+
   10.47 +  by (rule quot_function) (simp_all only: quot_equality)
   10.48  
   10.49  end
    11.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:41 2005 +0100
    11.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 08 20:15:50 2005 +0100
    11.3 @@ -67,8 +67,9 @@
    11.4  
    11.5  hide const while_aux
    11.6  
    11.7 -lemma def_while_unfold: assumes fdef: "f == while test do"
    11.8 -      shows "f x = (if test x then f(do x) else x)"
    11.9 +lemma def_while_unfold:
   11.10 +  assumes fdef: "f == while test do"
   11.11 +  shows "f x = (if test x then f(do x) else x)"
   11.12  proof -
   11.13    have "f x = while test do x" using fdef by simp
   11.14    also have "\<dots> = (if test x then while test do (do x) else x)"
   11.15 @@ -82,22 +83,16 @@
   11.16   The proof rule for @{term while}, where @{term P} is the invariant.
   11.17  *}
   11.18  
   11.19 -theorem while_rule_lemma[rule_format]:
   11.20 -  "[| !!s. P s ==> b s ==> P (c s);
   11.21 -      !!s. P s ==> \<not> b s ==> Q s;
   11.22 -      wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
   11.23 -    P s --> Q (while b c s)"
   11.24 -proof -
   11.25 -  case rule_context
   11.26 -  assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   11.27 -  show ?thesis
   11.28 -    apply (induct s rule: wf [THEN wf_induct])
   11.29 -    apply simp
   11.30 -    apply clarify
   11.31 -    apply (subst while_unfold)
   11.32 -    apply (simp add: rule_context)
   11.33 -    done
   11.34 -qed
   11.35 +theorem while_rule_lemma:
   11.36 +  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
   11.37 +    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
   11.38 +    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   11.39 +  shows "P s \<Longrightarrow> Q (while b c s)"
   11.40 +  apply (induct s rule: wf [THEN wf_induct])
   11.41 +  apply simp
   11.42 +  apply (subst while_unfold)
   11.43 +  apply (simp add: invariant terminate)
   11.44 +  done
   11.45  
   11.46  theorem while_rule:
   11.47    "[| P s;
   11.48 @@ -148,7 +143,7 @@
   11.49  back into equality. *}
   11.50  
   11.51  lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
   11.52 -by blast
   11.53 +  by blast
   11.54  
   11.55  theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   11.56    P {0, 4, 2}"
    12.1 --- a/src/HOL/MicroJava/BV/Err.thy	Thu Dec 08 20:15:41 2005 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Thu Dec 08 20:15:50 2005 +0100
    12.3 @@ -257,15 +257,14 @@
    12.4  done
    12.5  
    12.6  lemma OK_plus_OK_eq_Err_conv [simp]:
    12.7 -  "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> 
    12.8 -  ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
    12.9 +  assumes "x:A" and "y:A" and "semilat(err A, le r, fe)"
   12.10 +  shows "((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   12.11  proof -
   12.12    have plus_le_conv3: "\<And>A x y z f r. 
   12.13      \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
   12.14      \<Longrightarrow> x <=_r z \<and> y <=_r z"
   12.15      by (rule semilat.plus_le_conv [THEN iffD1])
   12.16 -  case rule_context
   12.17 -  thus ?thesis
   12.18 +  from prems show ?thesis
   12.19    apply (rule_tac iffI)
   12.20     apply clarify
   12.21     apply (drule OK_le_err_OK [THEN iffD2])
    13.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 08 20:15:41 2005 +0100
    13.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Thu Dec 08 20:15:50 2005 +0100
    13.3 @@ -159,9 +159,9 @@
    13.4    done
    13.5  
    13.6  lemma (in semilat) merges_pres_le_ub:
    13.7 -shows "\<lbrakk> set ts <= A; set ss <= A;
    13.8 -         \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
    13.9 -  \<Longrightarrow> merges f ps ss <=[r] ts"
   13.10 +  assumes "set ts <= A" and "set ss <= A"
   13.11 +    and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
   13.12 +  shows "merges f ps ss <=[r] ts"
   13.13  proof -
   13.14    { fix t ts ps
   13.15      have
   13.16 @@ -182,8 +182,7 @@
   13.17      done 
   13.18    } note this [dest]
   13.19    
   13.20 -  case rule_context
   13.21 -  thus ?thesis by blast
   13.22 +  from prems show ?thesis by blast
   13.23  qed
   13.24  
   13.25  
    14.1 --- a/src/HOL/MicroJava/BV/Product.thy	Thu Dec 08 20:15:41 2005 +0100
    14.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Thu Dec 08 20:15:50 2005 +0100
    14.3 @@ -72,15 +72,15 @@
    14.4  
    14.5  
    14.6  lemma plus_eq_Err_conv [simp]:
    14.7 -  "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk> 
    14.8 -  \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
    14.9 +  assumes "x:A" and "y:A"
   14.10 +    and "semilat(err A, Err.le r, lift2 f)"
   14.11 +  shows "(x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   14.12  proof -
   14.13    have plus_le_conv2:
   14.14      "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
   14.15                   OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
   14.16      by (rule semilat.plus_le_conv [THEN iffD1])
   14.17 -  case rule_context
   14.18 -  thus ?thesis
   14.19 +  from prems show ?thesis
   14.20    apply (rule_tac iffI)
   14.21     apply clarify
   14.22     apply (drule OK_le_err_OK [THEN iffD2])
    15.1 --- a/src/HOL/Product_Type.thy	Thu Dec 08 20:15:41 2005 +0100
    15.2 +++ b/src/HOL/Product_Type.thy	Thu Dec 08 20:15:50 2005 +0100
    15.3 @@ -223,14 +223,13 @@
    15.4    done
    15.5  
    15.6  lemma Pair_inject:
    15.7 -  "(a, b) = (a', b') ==> (a = a' ==> b = b' ==> R) ==> R"
    15.8 -proof -
    15.9 -  case rule_context [unfolded Pair_def]
   15.10 -  show ?thesis
   15.11 -    apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
   15.12 -    apply (rule rule_context ProdI)+
   15.13 -    .
   15.14 -qed
   15.15 +  assumes "(a, b) = (a', b')"
   15.16 +    and "a = a' ==> b = b' ==> R"
   15.17 +  shows R
   15.18 +  apply (insert prems [unfolded Pair_def])
   15.19 +  apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
   15.20 +  apply (assumption | rule ProdI)+
   15.21 +  done
   15.22  
   15.23  lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
   15.24    by (blast elim!: Pair_inject)
   15.25 @@ -507,11 +506,11 @@
   15.26  lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
   15.27  by (simp only: split_tupled_all, simp)
   15.28  
   15.29 -lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
   15.30 -proof -
   15.31 -  case rule_context [unfolded split_def]
   15.32 -  show ?thesis by (rule rule_context surjective_pairing)+
   15.33 -qed
   15.34 +lemma mem_splitE:
   15.35 +  assumes major: "z: split c p"
   15.36 +    and cases: "!!x y. [| p = (x,y); z: c x y |] ==> Q"
   15.37 +  shows Q
   15.38 +  by (rule major [unfolded split_def] cases surjective_pairing)+
   15.39  
   15.40  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
   15.41  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
   15.42 @@ -533,15 +532,14 @@
   15.43  *}
   15.44  
   15.45  lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   15.46 -by (rule ext, fast)
   15.47 +  by (rule ext) fast
   15.48  
   15.49  lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   15.50 -by (rule ext, fast)
   15.51 +  by (rule ext) fast
   15.52  
   15.53  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   15.54    -- {* Allows simplifications of nested splits in case of independent predicates. *}
   15.55 -  apply (rule ext, blast)
   15.56 -  done
   15.57 +  by (rule ext) blast
   15.58  
   15.59  (* Do NOT make this a simp rule as it
   15.60     a) only helps in special situations
   15.61 @@ -549,7 +547,7 @@
   15.62  *)
   15.63  lemma split_comp_eq: 
   15.64  "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   15.65 -by (rule ext, auto)
   15.66 +  by (rule ext) auto
   15.67  
   15.68  lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   15.69    by blast
   15.70 @@ -595,20 +593,15 @@
   15.71    done
   15.72  
   15.73  lemma prod_fun_imageE [elim!]:
   15.74 -  "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P
   15.75 -    |] ==> P"
   15.76 -proof -
   15.77 -  case rule_context
   15.78 -  assume major: "c: (prod_fun f g)`r"
   15.79 -  show ?thesis
   15.80 -    apply (rule major [THEN imageE])
   15.81 -    apply (rule_tac p = x in PairE)
   15.82 -    apply (rule rule_context)
   15.83 -     prefer 2
   15.84 -     apply blast
   15.85 -    apply (blast intro: prod_fun)
   15.86 -    done
   15.87 -qed
   15.88 +  assumes major: "c: (prod_fun f g)`r"
   15.89 +    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
   15.90 +  shows P
   15.91 +  apply (rule major [THEN imageE])
   15.92 +  apply (rule_tac p = x in PairE)
   15.93 +  apply (rule cases)
   15.94 +   apply (blast intro: prod_fun)
   15.95 +  apply blast
   15.96 +  done
   15.97  
   15.98  
   15.99  constdefs
  15.100 @@ -619,10 +612,10 @@
  15.101   "upd_snd f == prod_fun id f"
  15.102  
  15.103  lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
  15.104 -by (simp add: upd_fst_def)
  15.105 +  by (simp add: upd_fst_def)
  15.106  
  15.107  lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
  15.108 -by (simp add: upd_snd_def)
  15.109 +  by (simp add: upd_snd_def)
  15.110  
  15.111  text {*
  15.112    \bigskip Disjoint union of a family of sets -- Sigma.
  15.113 @@ -644,10 +637,10 @@
  15.114  *}
  15.115  
  15.116  lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
  15.117 -by blast
  15.118 +  by blast
  15.119  
  15.120  lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
  15.121 -by blast
  15.122 +  by blast
  15.123  
  15.124  lemma SigmaE2:
  15.125      "[| (a, b) : Sigma A B;
  15.126 @@ -658,7 +651,7 @@
  15.127  lemma Sigma_cong:
  15.128       "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
  15.129        \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
  15.130 -by auto
  15.131 +  by auto
  15.132  
  15.133  lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
  15.134    by blast
    16.1 --- a/src/HOL/Real/Rational.thy	Thu Dec 08 20:15:41 2005 +0100
    16.2 +++ b/src/HOL/Real/Rational.thy	Thu Dec 08 20:15:50 2005 +0100
    16.3 @@ -332,16 +332,13 @@
    16.4  qed
    16.5  
    16.6  theorem rat_function:
    16.7 -  "(!!q r. f q r == g (fraction_of q) (fraction_of r)) ==>
    16.8 -    (!!a b a' b' c d c' d'.
    16.9 +  assumes "!!q r. f q r == g (fraction_of q) (fraction_of r)"
   16.10 +    and "!!a b a' b' c d c' d'.
   16.11        \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==>
   16.12        b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==>
   16.13 -      g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
   16.14 -    f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
   16.15 -proof -
   16.16 -  case rule_context from this TrueI
   16.17 -  show ?thesis by (rule rat_cond_function)
   16.18 -qed
   16.19 +      g (fract a b) (fract c d) = g (fract a' b') (fract c' d')"
   16.20 +  shows "f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
   16.21 +  using prems and TrueI by (rule rat_cond_function)
   16.22  
   16.23  
   16.24  subsubsection {* Standard operations on rational numbers *}
    17.1 --- a/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:41 2005 +0100
    17.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:50 2005 +0100
    17.3 @@ -81,7 +81,7 @@
    17.4  lemmas rtrancl_induct2 =
    17.5    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    17.6                   consumes 1, case_names refl step]
    17.7 - 
    17.8 +
    17.9  lemma trans_rtrancl: "trans(r^*)"
   17.10    -- {* transitivity of transitive closure!! -- by induction *}
   17.11  proof (rule transI)
   17.12 @@ -94,21 +94,17 @@
   17.13  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   17.14  
   17.15  lemma rtranclE:
   17.16 -  "[| (a::'a,b) : r^*;  (a = b) ==> P;
   17.17 -      !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
   17.18 -   |] ==> P"
   17.19 +  assumes major: "(a::'a,b) : r^*"
   17.20 +    and cases: "(a = b) ==> P"
   17.21 +      "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
   17.22 +  shows P
   17.23    -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
   17.24 -proof -
   17.25 -  assume major: "(a::'a,b) : r^*"
   17.26 -  case rule_context
   17.27 -  show ?thesis
   17.28 -    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
   17.29 -     apply (rule_tac [2] major [THEN rtrancl_induct])
   17.30 -      prefer 2 apply (blast!)
   17.31 -      prefer 2 apply (blast!)
   17.32 -    apply (erule asm_rl exE disjE conjE prems)+
   17.33 -    done
   17.34 -qed
   17.35 +  apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
   17.36 +   apply (rule_tac [2] major [THEN rtrancl_induct])
   17.37 +    prefer 2 apply blast
   17.38 +   prefer 2 apply blast
   17.39 +  apply (erule asm_rl exE disjE conjE cases)+
   17.40 +  done
   17.41  
   17.42  lemma converse_rtrancl_into_rtrancl:
   17.43    "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
   17.44 @@ -187,21 +183,16 @@
   17.45                   consumes 1, case_names refl step]
   17.46  
   17.47  lemma converse_rtranclE:
   17.48 -  "[| (x,z):r^*;
   17.49 -      x=z ==> P;
   17.50 -      !!y. [| (x,y):r; (y,z):r^* |] ==> P
   17.51 -   |] ==> P"
   17.52 -proof -
   17.53 -  assume major: "(x,z):r^*"
   17.54 -  case rule_context
   17.55 -  show ?thesis
   17.56 -    apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   17.57 -     apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   17.58 -      prefer 2 apply iprover
   17.59 -     prefer 2 apply iprover
   17.60 -    apply (erule asm_rl exE disjE conjE prems)+
   17.61 -    done
   17.62 -qed
   17.63 +  assumes major: "(x,z):r^*"
   17.64 +    and cases: "x=z ==> P"
   17.65 +      "!!y. [| (x,y):r; (y,z):r^* |] ==> P"
   17.66 +  shows P
   17.67 +  apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   17.68 +   apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   17.69 +    prefer 2 apply iprover
   17.70 +   prefer 2 apply iprover
   17.71 +  apply (erule asm_rl exE disjE conjE cases)+
   17.72 +  done
   17.73  
   17.74  ML_setup {*
   17.75    bind_thm ("converse_rtranclE2", split_rule
   17.76 @@ -258,17 +249,12 @@
   17.77  qed
   17.78  
   17.79  lemma trancl_trans_induct:
   17.80 -  "[| (x,y) : r^+;
   17.81 -      !!x y. (x,y) : r ==> P x y;
   17.82 -      !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
   17.83 -   |] ==> P x y"
   17.84 +  assumes major: "(x,y) : r^+"
   17.85 +    and cases: "!!x y. (x,y) : r ==> P x y"
   17.86 +      "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z"
   17.87 +  shows "P x y"
   17.88    -- {* Another induction rule for trancl, incorporating transitivity *}
   17.89 -proof -
   17.90 -  assume major: "(x,y) : r^+"
   17.91 -  case rule_context
   17.92 -  show ?thesis
   17.93 -    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
   17.94 -qed
   17.95 +  by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
   17.96  
   17.97  inductive_cases tranclE: "(a, b) : r^+"
   17.98  
   17.99 @@ -279,9 +265,9 @@
  17.100    -- {* Transitivity of @{term "r^+"} *}
  17.101  proof (rule transI)
  17.102    fix x y z
  17.103 -  assume "(x, y) \<in> r^+"
  17.104 +  assume xy: "(x, y) \<in> r^+"
  17.105    assume "(y, z) \<in> r^+"
  17.106 -  thus "(x, z) \<in> r^+" by induct (iprover!)+
  17.107 +  thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
  17.108  qed
  17.109  
  17.110  lemmas trancl_trans = trans_trancl [THEN transD, standard]
  17.111 @@ -323,19 +309,15 @@
  17.112      intro!: trancl_converseI trancl_converseD)
  17.113  
  17.114  lemma converse_trancl_induct:
  17.115 -  "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
  17.116 -      !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]
  17.117 -    ==> P(a)"
  17.118 -proof -
  17.119 -  assume major: "(a,b) : r^+"
  17.120 -  case rule_context
  17.121 -  show ?thesis
  17.122 -    apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
  17.123 -     apply (rule prems)
  17.124 -     apply (erule converseD)
  17.125 -    apply (blast intro: prems dest!: trancl_converseD)
  17.126 -    done
  17.127 -qed
  17.128 +  assumes major: "(a,b) : r^+"
  17.129 +    and cases: "!!y. (y,b) : r ==> P(y)"
  17.130 +      "!!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y)"
  17.131 +  shows "P a"
  17.132 +  apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
  17.133 +   apply (rule cases)
  17.134 +   apply (erule converseD)
  17.135 +  apply (blast intro: prems dest!: trancl_converseD)
  17.136 +  done
  17.137  
  17.138  lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
  17.139    apply (erule converse_trancl_induct, auto)
  17.140 @@ -343,15 +325,14 @@
  17.141    done
  17.142  
  17.143  lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
  17.144 -by(blast elim: tranclE dest: trancl_into_rtrancl)
  17.145 +  by (blast elim: tranclE dest: trancl_into_rtrancl)
  17.146  
  17.147  lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
  17.148    by (blast dest: r_into_trancl)
  17.149  
  17.150  lemma trancl_subset_Sigma_aux:
  17.151      "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
  17.152 -  apply (erule rtrancl_induct, auto)
  17.153 -  done
  17.154 +  by (induct rule: rtrancl_induct) auto
  17.155  
  17.156  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
  17.157    apply (rule subsetI)
  17.158 @@ -477,16 +458,16 @@
  17.159      val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
  17.160      val rtrancl_trans = thm "rtrancl_trans";
  17.161  
  17.162 -  fun decomp (Trueprop $ t) = 
  17.163 -    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 
  17.164 -	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
  17.165 -	      | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
  17.166 -	      | decr r = (r,"r");
  17.167 -	    val (rel,r) = decr rel;
  17.168 -	in SOME (a,b,rel,r) end
  17.169 -      | dec _ =  NONE 
  17.170 +  fun decomp (Trueprop $ t) =
  17.171 +    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
  17.172 +        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
  17.173 +              | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
  17.174 +              | decr r = (r,"r");
  17.175 +            val (rel,r) = decr rel;
  17.176 +        in SOME (a,b,rel,r) end
  17.177 +      | dec _ =  NONE
  17.178      in dec t end;
  17.179 -  
  17.180 +
  17.181    end); (* struct *)
  17.182  
  17.183  change_simpset (fn ss => ss
  17.184 @@ -499,7 +480,7 @@
  17.185  
  17.186  method_setup trancl =
  17.187    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
  17.188 -  {* simple transitivity reasoner *}	    
  17.189 +  {* simple transitivity reasoner *}
  17.190  method_setup rtrancl =
  17.191    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
  17.192    {* simple transitivity reasoner *}
    18.1 --- a/src/HOL/Unix/Unix.thy	Thu Dec 08 20:15:41 2005 +0100
    18.2 +++ b/src/HOL/Unix/Unix.thy	Thu Dec 08 20:15:50 2005 +0100
    18.3 @@ -255,16 +255,16 @@
    18.4      lookup root path = Some file"
    18.5    by (simp add: access_def split: option.splits if_splits)
    18.6  
    18.7 -lemma access_update_other: "path' \<parallel> path \<Longrightarrow>
    18.8 -  access (update path' opt root) path uid perms = access root path uid perms"
    18.9 +lemma access_update_other:
   18.10 +  assumes parallel: "path' \<parallel> path"
   18.11 +  shows "access (update path' opt root) path uid perms = access root path uid perms"
   18.12  proof -
   18.13 -  assume "path' \<parallel> path"
   18.14 -  then obtain y z xs ys zs where
   18.15 +  from parallel obtain y z xs ys zs where
   18.16        "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
   18.17      by (blast dest: parallel_decomp)
   18.18 -  hence "lookup (update path' opt root) path = lookup root path"
   18.19 +  then have "lookup (update path' opt root) path = lookup root path"
   18.20      by (blast intro: lookup_update_other)
   18.21 -  thus ?thesis by (simp only: access_def)
   18.22 +  then show ?thesis by (simp only: access_def)
   18.23  qed
   18.24  
   18.25  
   18.26 @@ -437,36 +437,35 @@
   18.27    relation.
   18.28  *}
   18.29  
   18.30 -theorem transition_uniq: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root \<midarrow>x\<rightarrow> root'' \<Longrightarrow> root' = root''"
   18.31 -proof -
   18.32 -  assume root: "root \<midarrow>x\<rightarrow> root'"
   18.33 -  assume "root \<midarrow>x\<rightarrow> root''"
   18.34 -  thus "root' = root''"
   18.35 -  proof cases
   18.36 -    case read
   18.37 -    with root show ?thesis by cases auto
   18.38 -  next
   18.39 -    case write
   18.40 -    with root show ?thesis by cases auto
   18.41 -  next
   18.42 -    case chmod
   18.43 -    with root show ?thesis by cases auto
   18.44 -  next
   18.45 -    case creat
   18.46 -    with root show ?thesis by cases auto
   18.47 -  next
   18.48 -    case unlink
   18.49 -    with root show ?thesis by cases auto
   18.50 -  next
   18.51 -    case mkdir
   18.52 -    with root show ?thesis by cases auto
   18.53 -  next
   18.54 -    case rmdir
   18.55 -    with root show ?thesis by cases auto
   18.56 -  next
   18.57 -    case readdir
   18.58 -    with root show ?thesis by cases fastsimp+
   18.59 -  qed
   18.60 +theorem transition_uniq:
   18.61 +  assumes root': "root \<midarrow>x\<rightarrow> root'"
   18.62 +    and root'': "root \<midarrow>x\<rightarrow> root''"
   18.63 +  shows "root' = root''"
   18.64 +  using root''
   18.65 +proof cases
   18.66 +  case read
   18.67 +  with root' show ?thesis by cases auto
   18.68 +next
   18.69 +  case write
   18.70 +  with root' show ?thesis by cases auto
   18.71 +next
   18.72 +  case chmod
   18.73 +  with root' show ?thesis by cases auto
   18.74 +next
   18.75 +  case creat
   18.76 +  with root' show ?thesis by cases auto
   18.77 +next
   18.78 +  case unlink
   18.79 +  with root' show ?thesis by cases auto
   18.80 +next
   18.81 +  case mkdir
   18.82 +  with root' show ?thesis by cases auto
   18.83 +next
   18.84 +  case rmdir
   18.85 +  with root' show ?thesis by cases auto
   18.86 +next
   18.87 +  case readdir
   18.88 +  with root' show ?thesis by cases fastsimp+
   18.89  qed
   18.90  
   18.91  text {*
   18.92 @@ -476,24 +475,20 @@
   18.93  *}
   18.94  
   18.95  theorem transition_type_safe:
   18.96 -  "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
   18.97 -    \<Longrightarrow> \<exists>att dir. root' = Env att dir"
   18.98 -proof -
   18.99 -  assume tr: "root \<midarrow>x\<rightarrow> root'"
  18.100 -  assume inv: "\<exists>att dir. root = Env att dir"
  18.101 -  show ?thesis
  18.102 -  proof (cases "path_of x")
  18.103 -    case Nil
  18.104 -    with tr inv show ?thesis
  18.105 -      by cases (auto simp add: access_def split: if_splits)
  18.106 -  next
  18.107 -    case Cons
  18.108 -    from tr obtain opt where
  18.109 -        "root' = root \<or> root' = update (path_of x) opt root"
  18.110 -      by cases auto
  18.111 -    with inv Cons show ?thesis
  18.112 -      by (auto simp add: update_eq split: list.splits)
  18.113 -  qed
  18.114 +  assumes tr: "root \<midarrow>x\<rightarrow> root'"
  18.115 +    and inv: "\<exists>att dir. root = Env att dir"
  18.116 +  shows "\<exists>att dir. root' = Env att dir"
  18.117 +proof (cases "path_of x")
  18.118 +  case Nil
  18.119 +  with tr inv show ?thesis
  18.120 +    by cases (auto simp add: access_def split: if_splits)
  18.121 +next
  18.122 +  case Cons
  18.123 +  from tr obtain opt where
  18.124 +      "root' = root \<or> root' = update (path_of x) opt root"
  18.125 +    by cases auto
  18.126 +  with inv Cons show ?thesis
  18.127 +    by (auto simp add: update_eq split: list.splits)
  18.128  qed
  18.129  
  18.130  text {*
  18.131 @@ -539,21 +534,21 @@
  18.132  lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
  18.133  proof
  18.134    assume "root =[]\<Rightarrow> root'"
  18.135 -  thus "root = root'" by cases simp_all
  18.136 +  then show "root = root'" by cases simp_all
  18.137  next
  18.138    assume "root = root'"
  18.139 -  thus "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
  18.140 +  then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
  18.141  qed
  18.142  
  18.143  lemma transitions_cons_eq:
  18.144    "root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')"
  18.145  proof
  18.146    assume "root =(x # xs)\<Rightarrow> root''"
  18.147 -  thus "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
  18.148 +  then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
  18.149      by cases auto
  18.150  next
  18.151    assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
  18.152 -  thus "root =(x # xs)\<Rightarrow> root''"
  18.153 +  then show "root =(x # xs)\<Rightarrow> root''"
  18.154      by (blast intro: transitions.cons)
  18.155  qed
  18.156  
  18.157 @@ -568,13 +563,13 @@
  18.158    by (simp add: transitions_nil_eq)
  18.159  
  18.160  lemma transitions_consD:
  18.161 -  "root =(x # xs)\<Rightarrow> root'' \<Longrightarrow> root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root''"
  18.162 +  assumes list: "root =(x # xs)\<Rightarrow> root''"
  18.163 +    and hd: "root \<midarrow>x\<rightarrow> root'"
  18.164 +  shows "root' =xs\<Rightarrow> root''"
  18.165  proof -
  18.166 -  assume "root =(x # xs)\<Rightarrow> root''"
  18.167 -  then obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
  18.168 +  from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
  18.169      by cases simp_all
  18.170 -  assume "root \<midarrow>x\<rightarrow> root'"
  18.171 -  with r' have "r' = root'" by (rule transition_uniq)
  18.172 +  from r' hd have "r' = root'" by (rule transition_uniq)
  18.173    with root'' show "root' =xs\<Rightarrow> root''" by simp
  18.174  qed
  18.175  
  18.176 @@ -586,26 +581,20 @@
  18.177  *}
  18.178  
  18.179  lemma transitions_invariant:
  18.180 -  "(\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
  18.181 -    root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
  18.182 -proof -
  18.183 -  assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
  18.184 -  assume "root =xs\<Rightarrow> root'"
  18.185 -  thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
  18.186 -  proof (induct root xs root')
  18.187 -    fix root assume "Q root"
  18.188 -    thus "Q root" .
  18.189 -  next
  18.190 -    fix root root' root'' and x xs
  18.191 -    assume root': "root \<midarrow>x\<rightarrow> root'"
  18.192 -    assume hyp: "PROP ?P root' xs root''"
  18.193 -    assume Q: "Q root"
  18.194 -    assume P: "\<forall>x \<in> set (x # xs). P x"
  18.195 -    hence "P x" by simp
  18.196 -    with root' Q have Q': "Q root'" by (rule r)
  18.197 -    from P have "\<forall>x \<in> set xs. P x" by simp
  18.198 -    with Q' show "Q root''" by (rule hyp)
  18.199 -  qed
  18.200 +  assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
  18.201 +    and trans: "root =xs\<Rightarrow> root'"
  18.202 +  shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
  18.203 +  using trans
  18.204 +proof induct
  18.205 +  case nil
  18.206 +  show ?case by assumption
  18.207 +next
  18.208 +  case (cons root root' root'' x xs)
  18.209 +  note P = `\<forall>x \<in> set (x # xs). P x`
  18.210 +  then have "P x" by simp
  18.211 +  with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r)
  18.212 +  from P have "\<forall>x \<in> set xs. P x" by simp
  18.213 +  with Q' show "Q root''" by (rule cons.hyps)
  18.214  qed
  18.215  
  18.216  text {*
  18.217 @@ -675,31 +664,23 @@
  18.218    executed we may destruct it backwardly into individual transitions.
  18.219  *}
  18.220  
  18.221 -lemma can_exec_snocD: "\<And>root. can_exec root (xs @ [y])
  18.222 +lemma can_exec_snocD: "can_exec root (xs @ [y])
  18.223      \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
  18.224 -  (is "PROP ?P xs" is "\<And>root. ?A root xs \<Longrightarrow> ?C root xs")
  18.225 -proof (induct xs)
  18.226 -  fix root
  18.227 -  {
  18.228 -    assume "?A root []"
  18.229 -    thus "?C root []"
  18.230 -      by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
  18.231 -  next
  18.232 -    fix x xs
  18.233 -    assume hyp: "PROP ?P xs"
  18.234 -    assume asm: "?A root (x # xs)"
  18.235 -    show "?C root (x # xs)"
  18.236 -    proof -
  18.237 -      from asm obtain r root'' where x: "root \<midarrow>x\<rightarrow> r" and
  18.238 -          xs_y: "r =(xs @ [y])\<Rightarrow> root''"
  18.239 -        by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
  18.240 -      from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
  18.241 -        by (unfold can_exec_def) blast
  18.242 -      from x xs have "root =(x # xs)\<Rightarrow> root'"
  18.243 -        by (rule transitions.cons)
  18.244 -      with y show ?thesis by blast
  18.245 -    qed
  18.246 -  }
  18.247 +proof (induct xs fixing: root)
  18.248 +  case Nil
  18.249 +  then show ?case
  18.250 +    by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
  18.251 +next
  18.252 +  case (Cons x xs)
  18.253 +  from `can_exec root ((x # xs) @ [y])` obtain r root'' where
  18.254 +      x: "root \<midarrow>x\<rightarrow> r" and
  18.255 +      xs_y: "r =(xs @ [y])\<Rightarrow> root''"
  18.256 +    by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
  18.257 +  from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
  18.258 +    by (unfold can_exec_def) blast
  18.259 +  from x xs have "root =(x # xs)\<Rightarrow> root'"
  18.260 +    by (rule transitions.cons)
  18.261 +  with y show ?case by blast
  18.262  qed
  18.263  
  18.264  
  18.265 @@ -803,16 +784,12 @@
  18.266  *}
  18.267  
  18.268  theorem general_procedure:
  18.269 -  "(\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False) \<Longrightarrow>
  18.270 -    (\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root) \<Longrightarrow>
  18.271 -    (\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
  18.272 -    init users =bs\<Rightarrow> root \<Longrightarrow>
  18.273 -      \<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
  18.274 +  assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
  18.275 +    and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
  18.276 +    and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
  18.277 +    and init_result: "init users =bs\<Rightarrow> root"
  18.278 +  shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
  18.279  proof -
  18.280 -  assume cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
  18.281 -  assume init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
  18.282 -  assume preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
  18.283 -  assume init_result: "init users =bs\<Rightarrow> root"
  18.284    {
  18.285      fix xs
  18.286      assume Ps: "\<forall>x \<in> set xs. P x"
  18.287 @@ -825,7 +802,7 @@
  18.288        by (rule transitions_invariant)
  18.289      from this y have False by (rule cannot_y)
  18.290    }
  18.291 -  thus ?thesis by blast
  18.292 +  then show ?thesis by blast
  18.293  qed
  18.294  
  18.295  text {*
  18.296 @@ -930,38 +907,36 @@
  18.297    we just have to inspect rather special cases.
  18.298  *}
  18.299  
  18.300 -lemma (in invariant)
  18.301 -  cannot_rmdir: "invariant root bogus_path \<Longrightarrow>
  18.302 -    root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root' \<Longrightarrow> False"
  18.303 +lemma (in invariant) cannot_rmdir:
  18.304 +  assumes inv: "invariant root bogus_path"
  18.305 +    and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
  18.306 +  shows False
  18.307  proof -
  18.308 -  assume "invariant root bogus_path"
  18.309 -  then obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
  18.310 +  from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
  18.311      by (unfold invariant_def) blast
  18.312    moreover
  18.313 -  assume "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
  18.314 -  then obtain att where
  18.315 +  from rmdir obtain att where
  18.316        "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
  18.317      by cases auto
  18.318 -  hence "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
  18.319 +  then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
  18.320      by (simp only: access_empty_lookup lookup_append_some) simp
  18.321    ultimately show False by (simp add: bogus_path_def)
  18.322  qed
  18.323  
  18.324  lemma (in invariant)
  18.325 -  init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
  18.326 -proof -
  18.327 -  note eval = facts access_def init_def
  18.328 -  case rule_context thus ?thesis
  18.329 -    apply (unfold bogus_def bogus_path_def)
  18.330 -    apply (drule transitions_consD, rule transition.intros,
  18.331 +  assumes init: "init users =bogus\<Rightarrow> root"
  18.332 +  notes eval = facts access_def init_def
  18.333 +  shows init_invariant: "invariant root bogus_path"
  18.334 +  using init
  18.335 +  apply (unfold bogus_def bogus_path_def)
  18.336 +  apply (drule transitions_consD, rule transition.intros,
  18.337        (force simp add: eval)+, (simp add: eval)?)+
  18.338 -      -- "evaluate all operations"
  18.339 -    apply (drule transitions_nilD)
  18.340 -      -- "reach final result"
  18.341 -    apply (simp add: invariant_def eval)
  18.342 -      -- "check the invariant"
  18.343 -    done
  18.344 -qed
  18.345 +    -- "evaluate all operations"
  18.346 +  apply (drule transitions_nilD)
  18.347 +    -- "reach final result"
  18.348 +  apply (simp add: invariant_def eval)
  18.349 +    -- "check the invariant"
  18.350 +  done
  18.351  
  18.352  text {*
  18.353    \medskip At last we are left with the main effort to show that the
  18.354 @@ -971,14 +946,12 @@
  18.355    required here.
  18.356  *}
  18.357  
  18.358 -lemma (in invariant)
  18.359 -  preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
  18.360 -    invariant root path \<Longrightarrow> uid_of x = user\<^isub>1 \<Longrightarrow> invariant root' path"
  18.361 +lemma (in invariant) preserve_invariant:
  18.362 +  assumes tr: "root \<midarrow>x\<rightarrow> root'"
  18.363 +    and inv: "invariant root path"
  18.364 +    and uid: "uid_of x = user\<^isub>1"
  18.365 +  shows "invariant root' path"
  18.366  proof -
  18.367 -  assume tr: "root \<midarrow>x\<rightarrow> root'"
  18.368 -  assume inv: "invariant root path"
  18.369 -  assume uid: "uid_of x = user\<^isub>1"
  18.370 -
  18.371    from inv obtain att dir where
  18.372        inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
  18.373        inv2: "dir \<noteq> empty" and
  18.374 @@ -1019,7 +992,7 @@
  18.375          with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
  18.376          have False
  18.377            by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
  18.378 -        thus ?thesis ..
  18.379 +        then show ?thesis ..
  18.380        next
  18.381          fix z zs assume ys: "ys = z # zs"
  18.382          have "lookup root' path = lookup root path"
  18.383 @@ -1085,7 +1058,7 @@
  18.384                have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
  18.385                    lookup root ((path @ [y]) @ us) \<noteq> None"
  18.386                  by cases (auto dest: access_some_lookup)
  18.387 -              thus ?thesis by (blast dest!: lookup_some_append)
  18.388 +              then show ?thesis by (blast dest!: lookup_some_append)
  18.389              qed
  18.390              finally show ?thesis .
  18.391            qed
    19.1 --- a/src/ZF/Induct/Brouwer.thy	Thu Dec 08 20:15:41 2005 +0100
    19.2 +++ b/src/ZF/Induct/Brouwer.thy	Thu Dec 08 20:15:50 2005 +0100
    19.3 @@ -22,24 +22,20 @@
    19.4    by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
    19.5      elim: brouwer.cases [unfolded brouwer.con_defs])
    19.6  
    19.7 -lemma brouwer_induct2:
    19.8 -  "[| b \<in> brouwer;
    19.9 -      P(Zero);
   19.10 -      !!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b));
   19.11 -      !!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i)
   19.12 -           |] ==> P(Lim(h))
   19.13 -   |] ==> P(b)"
   19.14 +lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]:
   19.15 +  assumes b: "b \<in> brouwer"
   19.16 +    and cases:
   19.17 +      "P(Zero)"
   19.18 +      "!!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b))"
   19.19 +      "!!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
   19.20 +  shows "P(b)"
   19.21    -- {* A nicer induction rule than the standard one. *}
   19.22 -proof -
   19.23 -  case rule_context
   19.24 -  assume "b \<in> brouwer"
   19.25 -  thus ?thesis
   19.26 -    apply induct
   19.27 -    apply (assumption | rule rule_context)+
   19.28 +  using b
   19.29 +  apply induct
   19.30 +    apply (assumption | rule cases)+
   19.31       apply (fast elim: fun_weaken_type)
   19.32      apply (fast dest: apply_type)
   19.33      done
   19.34 -qed
   19.35  
   19.36  
   19.37  subsection {* The Martin-Löf wellordering type *}
   19.38 @@ -58,22 +54,17 @@
   19.39      elim: Well.cases [unfolded Well.con_defs])
   19.40  
   19.41  
   19.42 -lemma Well_induct2:
   19.43 -  "[| w \<in> Well(A, B);
   19.44 -      !!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y)
   19.45 -           |] ==> P(Sup(a,f))
   19.46 -   |] ==> P(w)"
   19.47 +lemma Well_induct2 [consumes 1, case_names step]:
   19.48 +  assumes w: "w \<in> Well(A, B)"
   19.49 +    and step: "!!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
   19.50 +  shows "P(w)"
   19.51    -- {* A nicer induction rule than the standard one. *}
   19.52 -proof -
   19.53 -  case rule_context
   19.54 -  assume "w \<in> Well(A, B)"
   19.55 -  thus ?thesis
   19.56 -    apply induct
   19.57 -    apply (assumption | rule rule_context)+
   19.58 -     apply (fast elim: fun_weaken_type)
   19.59 -    apply (fast dest: apply_type)
   19.60 -    done
   19.61 -qed
   19.62 +  using w
   19.63 +  apply induct
   19.64 +  apply (assumption | rule step)+
   19.65 +   apply (fast elim: fun_weaken_type)
   19.66 +  apply (fast dest: apply_type)
   19.67 +  done
   19.68  
   19.69  lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
   19.70    -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
    20.1 --- a/src/ZF/Induct/Ntree.thy	Thu Dec 08 20:15:41 2005 +0100
    20.2 +++ b/src/ZF/Induct/Ntree.thy	Thu Dec 08 20:15:50 2005 +0100
    20.3 @@ -49,42 +49,36 @@
    20.4    by (blast intro: ntree.intros [unfolded ntree.con_defs]
    20.5      elim: ntree.cases [unfolded ntree.con_defs])
    20.6  
    20.7 -lemma ntree_induct [induct set: ntree]:
    20.8 -  "[| t \<in> ntree(A);
    20.9 -      !!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  \<forall>i \<in> n. P(h`i)
   20.10 -               |] ==> P(Branch(x,h))
   20.11 -   |] ==> P(t)"
   20.12 +lemma ntree_induct [consumes 1, case_names Branch, induct set: ntree]:
   20.13 +  assumes t: "t \<in> ntree(A)"
   20.14 +    and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  \<forall>i \<in> n. P(h`i)
   20.15 +      |] ==> P(Branch(x,h))"
   20.16 +  shows "P(t)"
   20.17    -- {* A nicer induction rule than the standard one. *}
   20.18 -proof -
   20.19 -  case rule_context
   20.20 -  assume "t \<in> ntree(A)"
   20.21 -  thus ?thesis
   20.22 -    apply induct
   20.23 -    apply (erule UN_E)
   20.24 -    apply (assumption | rule rule_context)+
   20.25 -     apply (fast elim: fun_weaken_type)
   20.26 -    apply (fast dest: apply_type)
   20.27 -    done
   20.28 -qed
   20.29 +  using t
   20.30 +  apply induct
   20.31 +  apply (erule UN_E)
   20.32 +  apply (assumption | rule step)+
   20.33 +   apply (fast elim: fun_weaken_type)
   20.34 +  apply (fast dest: apply_type)
   20.35 +  done
   20.36  
   20.37 -lemma ntree_induct_eqn:
   20.38 -  "[| t \<in> ntree(A);  f \<in> ntree(A)->B;  g \<in> ntree(A)->B;
   20.39 -      !!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  f O h = g O h |] ==>
   20.40 -               f ` Branch(x,h) = g ` Branch(x,h)
   20.41 -   |] ==> f`t=g`t"
   20.42 +lemma ntree_induct_eqn [consumes 1]:
   20.43 +  assumes t: "t \<in> ntree(A)"
   20.44 +    and f: "f \<in> ntree(A)->B"
   20.45 +    and g: "g \<in> ntree(A)->B"
   20.46 +    and step: "!!x n h. [| x \<in> A;  n \<in> nat;  h \<in> n -> ntree(A);  f O h = g O h |] ==>
   20.47 +      f ` Branch(x,h) = g ` Branch(x,h)"
   20.48 +  shows "f`t=g`t"
   20.49    -- {* Induction on @{term "ntree(A)"} to prove an equation *}
   20.50 -proof -
   20.51 -  case rule_context
   20.52 -  assume "t \<in> ntree(A)"
   20.53 -  thus ?thesis
   20.54 -    apply induct
   20.55 -    apply (assumption | rule rule_context)+
   20.56 -    apply (insert rule_context)
   20.57 -    apply (rule fun_extension)
   20.58 -      apply (assumption | rule comp_fun)+
   20.59 -    apply (simp add: comp_fun_apply)
   20.60 +  using t
   20.61 +  apply induct
   20.62 +  apply (assumption | rule step)+
   20.63 +  apply (insert f g)
   20.64 +  apply (rule fun_extension)
   20.65 +  apply (assumption | rule comp_fun)+
   20.66 +  apply (simp add: comp_fun_apply)
   20.67    done
   20.68 -qed
   20.69  
   20.70  text {*
   20.71    \medskip Lemmas to justify using @{text Ntree} in other recursive
   20.72 @@ -127,9 +121,8 @@
   20.73    by (simp add: ntree_copy_def ntree_rec_Branch)
   20.74  
   20.75  lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
   20.76 -  apply (induct_tac z)
   20.77 -  apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
   20.78 -  done
   20.79 +  by (induct z set: ntree)
   20.80 +    (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
   20.81  
   20.82  
   20.83  text {*
   20.84 @@ -140,25 +133,21 @@
   20.85    by (fast intro!: maptree.intros [unfolded maptree.con_defs]
   20.86      elim: maptree.cases [unfolded maptree.con_defs])
   20.87  
   20.88 -lemma maptree_induct [induct set: maptree]:
   20.89 -  "[| t \<in> maptree(A);
   20.90 -      !!x n h. [| x \<in> A;  h \<in> maptree(A) -||> maptree(A);
   20.91 +lemma maptree_induct [consumes 1, induct set: maptree]:
   20.92 +  assumes t: "t \<in> maptree(A)"
   20.93 +    and step: "!!x n h. [| x \<in> A;  h \<in> maptree(A) -||> maptree(A);
   20.94                    \<forall>y \<in> field(h). P(y)
   20.95 -               |] ==> P(Sons(x,h))
   20.96 -   |] ==> P(t)"
   20.97 +               |] ==> P(Sons(x,h))"
   20.98 +  shows "P(t)"
   20.99    -- {* A nicer induction rule than the standard one. *}
  20.100 -proof -
  20.101 -  case rule_context
  20.102 -  assume "t \<in> maptree(A)"
  20.103 -  thus ?thesis
  20.104 -    apply induct
  20.105 -    apply (assumption | rule rule_context)+
  20.106 -     apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
  20.107 -    apply (drule FiniteFun.dom_subset [THEN subsetD])
  20.108 -    apply (drule Fin.dom_subset [THEN subsetD])
  20.109 -    apply fast
  20.110 -    done
  20.111 -qed
  20.112 +  using t
  20.113 +  apply induct
  20.114 +  apply (assumption | rule step)+
  20.115 +  apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
  20.116 +  apply (drule FiniteFun.dom_subset [THEN subsetD])
  20.117 +  apply (drule Fin.dom_subset [THEN subsetD])
  20.118 +  apply fast
  20.119 +  done
  20.120  
  20.121  
  20.122  text {*
  20.123 @@ -169,22 +158,18 @@
  20.124    by (fast intro!: maptree2.intros [unfolded maptree2.con_defs]
  20.125      elim: maptree2.cases [unfolded maptree2.con_defs])
  20.126  
  20.127 -lemma maptree2_induct [induct set: maptree2]:
  20.128 -  "[| t \<in> maptree2(A, B);
  20.129 -      !!x n h. [| x \<in> A;  h \<in> B -||> maptree2(A,B);  \<forall>y \<in> range(h). P(y)
  20.130 -               |] ==> P(Sons2(x,h))
  20.131 -   |] ==> P(t)"
  20.132 -proof -
  20.133 -  case rule_context
  20.134 -  assume "t \<in> maptree2(A, B)"
  20.135 -  thus ?thesis
  20.136 -    apply induct
  20.137 -    apply (assumption | rule rule_context)+
  20.138 -     apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
  20.139 -    apply (drule FiniteFun.dom_subset [THEN subsetD])
  20.140 -    apply (drule Fin.dom_subset [THEN subsetD])
  20.141 -    apply fast
  20.142 -    done
  20.143 -qed
  20.144 +lemma maptree2_induct [consumes 1, induct set: maptree2]:
  20.145 +  assumes t: "t \<in> maptree2(A, B)"
  20.146 +    and step: "!!x n h. [| x \<in> A;  h \<in> B -||> maptree2(A,B);  \<forall>y \<in> range(h). P(y)
  20.147 +               |] ==> P(Sons2(x,h))"
  20.148 +  shows "P(t)"
  20.149 +  using t
  20.150 +  apply induct
  20.151 +  apply (assumption | rule step)+
  20.152 +   apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
  20.153 +   apply (drule FiniteFun.dom_subset [THEN subsetD])
  20.154 +   apply (drule Fin.dom_subset [THEN subsetD])
  20.155 +   apply fast
  20.156 +   done
  20.157  
  20.158  end