src/HOL/IMP/Transition.thy
changeset 12434 ff2efde4574d
parent 12431 07ec657249e5
child 12546 0c90e581379f
     1.1 --- a/src/HOL/IMP/Transition.thy	Sun Dec 09 14:37:42 2001 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Sun Dec 09 15:26:13 2001 +0100
     1.3 @@ -45,19 +45,19 @@
     1.4  *}
     1.5  syntax
     1.6    "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
     1.7 -    ("_ -1-> _" [81,81] 100)
     1.8 +    ("_ -1-> _" [60,60] 60)
     1.9    "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.10 -    ("_ -_-> _" [81,81] 100)
    1.11 +    ("_ -_-> _" [60,60,60] 60)
    1.12    "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.13 -    ("_ -*-> _" [81,81] 100)
    1.14 +    ("_ -*-> _" [60,60] 60)
    1.15  
    1.16  syntax (xsymbols)
    1.17    "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.18 -    ("_ \<longrightarrow>\<^sub>1 _" [81,81] 100)
    1.19 +    ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
    1.20    "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    1.21 -    ("_ -_\<rightarrow>\<^sub>1 _" [81,81] 100)
    1.22 +    ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
    1.23    "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    1.24 -    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [81,81] 100)
    1.25 +    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
    1.26  
    1.27  translations
    1.28    "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
    1.29 @@ -127,7 +127,8 @@
    1.30    "\<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>))"
    1.31    by (rule, cases set: evalc1, auto)
    1.32  
    1.33 -lemma While_1: "\<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>)"
    1.34 +lemma While_1: 
    1.35 +  "\<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>)"
    1.36    by (rule, cases set: evalc1, auto)
    1.37  
    1.38  lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
    1.39 @@ -136,15 +137,15 @@
    1.40  subsection "Examples"
    1.41  
    1.42  lemma 
    1.43 -  "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>"
    1.44 +  "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>"
    1.45    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
    1.46  proof -
    1.47 -  let ?x  = "x:== \<lambda>s. s x+1"
    1.48 -  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?x; ?w \<ELSE> \<SKIP>"
    1.49 +  let ?c  = "x:== \<lambda>s. s x+1"
    1.50 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
    1.51    assume [simp]: "s x = 0"
    1.52    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
    1.53 -  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?x; ?w, s\<rangle>" by simp 
    1.54 -  also have "\<langle>?x; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
    1.55 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp 
    1.56 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
    1.57    also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
    1.58    also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
    1.59    also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
    1.60 @@ -152,7 +153,7 @@
    1.61  qed
    1.62  
    1.63  lemma 
    1.64 -  "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'"
    1.65 +  "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'"
    1.66    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
    1.67  proof -
    1.68    let ?c = "x:== \<lambda>s. s x+1"
    1.69 @@ -193,7 +194,11 @@
    1.70    If a configuration does not contain a statement, the program
    1.71    has terminated and there is no next configuration:
    1.72  *}
    1.73 -lemma stuck [dest]: "(None, s) \<longrightarrow>\<^sub>1 y \<Longrightarrow> False" by (auto elim: evalc1.elims)
    1.74 +lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" 
    1.75 +  by (auto elim: evalc1.elims)
    1.76 +
    1.77 +lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" 
    1.78 +  by (erule rtrancl_induct) auto 
    1.79  
    1.80  (*<*)
    1.81  (* fixme: relpow.simps don't work *)
    1.82 @@ -201,8 +206,7 @@
    1.83  lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
    1.84  lemmas [simp del] = relpow.simps
    1.85  (*>*)
    1.86 -
    1.87 -lemma evalc_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
    1.88 +lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
    1.89    by (cases n) auto
    1.90  
    1.91  lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
    1.92 @@ -252,10 +256,10 @@
    1.93          c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
    1.94          c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
    1.95          i:   "n = i+j"
    1.96 -        by blast
    1.97 +        by fast
    1.98            
    1.99        from c1 c1'
   1.100 -      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto simp del: relpow.simps intro: rel_pow_Suc_I2)
   1.101 +      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
   1.102        with c2 i
   1.103        have "?Q (i+1) j s0" by simp
   1.104        thus ?thesis by blast
   1.105 @@ -591,7 +595,7 @@
   1.106      apply (rename_tac c s')
   1.107      apply simp
   1.108      apply (rule conjI)
   1.109 -     apply (fast dest: stuck)
   1.110 +     apply fast 
   1.111      apply clarify
   1.112      apply (case_tac c)
   1.113      apply (auto intro: rtrancl_into_rtrancl2)
   1.114 @@ -667,16 +671,13 @@
   1.115    apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   1.116    done
   1.117  
   1.118 -lemma rtrancl_stuck: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = (None, s)"
   1.119 -  by (erule rtrancl_induct) (auto dest: stuck)
   1.120 -
   1.121  lemma FB_lemma2 [rule_format]:
   1.122    "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
   1.123     \<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" 
   1.124    apply (erule converse_rtrancl_induct2)
   1.125     apply simp
   1.126    apply clarsimp
   1.127 -  apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3)
   1.128 +  apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   1.129    done
   1.130  
   1.131  lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"