tuned
authorkleing
Sun Dec 09 15:26:13 2001 +0100 (2001-12-09)
changeset 12434ff2efde4574d
parent 12433 654acbf26fcc
child 12435 a42be4b09cc3
tuned
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/Denotation.thy	Sun Dec 09 14:37:42 2001 +0100
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Sun Dec 09 15:26:13 2001 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  constdefs
     1.5    Gamma :: "[bexp,com_den] => (com_den => com_den)"
     1.6    "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
     1.7 -                        {(s,t). s=t \<and> \<not>b s})"
     1.8 +                       {(s,t). s=t \<and> \<not>b s})"
     1.9      
    1.10  consts
    1.11    C :: "com => com_den"
    1.12 @@ -23,7 +23,7 @@
    1.13    C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    1.14    C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    1.15    C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    1.16 -                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    1.17 +                                                {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    1.18    C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    1.19  
    1.20  
    1.21 @@ -33,10 +33,10 @@
    1.22    by (unfold Gamma_def mono_def) fast
    1.23  
    1.24  lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
    1.25 -apply (simp (no_asm))
    1.26 -apply (subst lfp_unfold [OF Gamma_mono],
    1.27 -       subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong],
    1.28 -       simp)
    1.29 +apply (simp (no_asm)) 
    1.30 +apply (subst lfp_unfold [OF Gamma_mono]) back back
    1.31 +apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) 
    1.32 +apply simp
    1.33  done
    1.34  
    1.35  (* Operational Semantics implies Denotational Semantics *)
     2.1 --- a/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:37:42 2001 +0100
     2.2 +++ b/src/HOL/IMP/Hoare.thy	Sun Dec 09 15:26:13 2001 +0100
     2.3 @@ -101,10 +101,11 @@
     2.4  apply (simp (no_asm_simp))
     2.5  done
     2.6  
     2.7 -declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp]
     2.8 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
     2.9  
    2.10  (*Not suitable for rewriting: LOOPS!*)
    2.11 -lemma wp_While_if: "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    2.12 +lemma wp_While_if: 
    2.13 +  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    2.14  apply (simp (no_asm))
    2.15  done
    2.16  
    2.17 @@ -132,7 +133,7 @@
    2.18  
    2.19  declare C_while [simp del]
    2.20  
    2.21 -declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!]
    2.22 +lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If 
    2.23  
    2.24  lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
    2.25  apply (induct_tac "c")
     3.1 --- a/src/HOL/IMP/Transition.thy	Sun Dec 09 14:37:42 2001 +0100
     3.2 +++ b/src/HOL/IMP/Transition.thy	Sun Dec 09 15:26:13 2001 +0100
     3.3 @@ -45,19 +45,19 @@
     3.4  *}
     3.5  syntax
     3.6    "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
     3.7 -    ("_ -1-> _" [81,81] 100)
     3.8 +    ("_ -1-> _" [60,60] 60)
     3.9    "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    3.10 -    ("_ -_-> _" [81,81] 100)
    3.11 +    ("_ -_-> _" [60,60,60] 60)
    3.12    "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    3.13 -    ("_ -*-> _" [81,81] 100)
    3.14 +    ("_ -*-> _" [60,60] 60)
    3.15  
    3.16  syntax (xsymbols)
    3.17    "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    3.18 -    ("_ \<longrightarrow>\<^sub>1 _" [81,81] 100)
    3.19 +    ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
    3.20    "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    3.21 -    ("_ -_\<rightarrow>\<^sub>1 _" [81,81] 100)
    3.22 +    ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
    3.23    "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    3.24 -    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [81,81] 100)
    3.25 +    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
    3.26  
    3.27  translations
    3.28    "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
    3.29 @@ -127,7 +127,8 @@
    3.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>))"
    3.31    by (rule, cases set: evalc1, auto)
    3.32  
    3.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>)"
    3.34 +lemma While_1: 
    3.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>)"
    3.36    by (rule, cases set: evalc1, auto)
    3.37  
    3.38  lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
    3.39 @@ -136,15 +137,15 @@
    3.40  subsection "Examples"
    3.41  
    3.42  lemma 
    3.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>"
    3.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>"
    3.45    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
    3.46  proof -
    3.47 -  let ?x  = "x:== \<lambda>s. s x+1"
    3.48 -  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?x; ?w \<ELSE> \<SKIP>"
    3.49 +  let ?c  = "x:== \<lambda>s. s x+1"
    3.50 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
    3.51    assume [simp]: "s x = 0"
    3.52    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
    3.53 -  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?x; ?w, s\<rangle>" by simp 
    3.54 -  also have "\<langle>?x; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
    3.55 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp 
    3.56 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
    3.57    also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
    3.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)
    3.59    also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
    3.60 @@ -152,7 +153,7 @@
    3.61  qed
    3.62  
    3.63  lemma 
    3.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'"
    3.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'"
    3.66    (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
    3.67  proof -
    3.68    let ?c = "x:== \<lambda>s. s x+1"
    3.69 @@ -193,7 +194,11 @@
    3.70    If a configuration does not contain a statement, the program
    3.71    has terminated and there is no next configuration:
    3.72  *}
    3.73 -lemma stuck [dest]: "(None, s) \<longrightarrow>\<^sub>1 y \<Longrightarrow> False" by (auto elim: evalc1.elims)
    3.74 +lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P" 
    3.75 +  by (auto elim: evalc1.elims)
    3.76 +
    3.77 +lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" 
    3.78 +  by (erule rtrancl_induct) auto 
    3.79  
    3.80  (*<*)
    3.81  (* fixme: relpow.simps don't work *)
    3.82 @@ -201,8 +206,7 @@
    3.83  lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
    3.84  lemmas [simp del] = relpow.simps
    3.85  (*>*)
    3.86 -
    3.87 -lemma evalc_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
    3.88 +lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
    3.89    by (cases n) auto
    3.90  
    3.91  lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
    3.92 @@ -252,10 +256,10 @@
    3.93          c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
    3.94          c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
    3.95          i:   "n = i+j"
    3.96 -        by blast
    3.97 +        by fast
    3.98            
    3.99        from c1 c1'
   3.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)
   3.101 +      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
   3.102        with c2 i
   3.103        have "?Q (i+1) j s0" by simp
   3.104        thus ?thesis by blast
   3.105 @@ -591,7 +595,7 @@
   3.106      apply (rename_tac c s')
   3.107      apply simp
   3.108      apply (rule conjI)
   3.109 -     apply (fast dest: stuck)
   3.110 +     apply fast 
   3.111      apply clarify
   3.112      apply (case_tac c)
   3.113      apply (auto intro: rtrancl_into_rtrancl2)
   3.114 @@ -667,16 +671,13 @@
   3.115    apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   3.116    done
   3.117  
   3.118 -lemma rtrancl_stuck: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = (None, s)"
   3.119 -  by (erule rtrancl_induct) (auto dest: stuck)
   3.120 -
   3.121  lemma FB_lemma2 [rule_format]:
   3.122    "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
   3.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" 
   3.124    apply (erule converse_rtrancl_induct2)
   3.125     apply simp
   3.126    apply clarsimp
   3.127 -  apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3)
   3.128 +  apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   3.129    done
   3.130  
   3.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"
     4.1 --- a/src/HOL/IMP/VC.thy	Sun Dec 09 14:37:42 2001 +0100
     4.2 +++ b/src/HOL/IMP/VC.thy	Sun Dec 09 15:26:13 2001 +0100
     4.3 @@ -90,7 +90,8 @@
     4.4  apply fast
     4.5  done
     4.6  
     4.7 -lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
     4.8 +lemma awp_mono [rule_format (no_asm)]: 
     4.9 +  "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    4.10  apply (induct_tac "c")
    4.11      apply (simp_all (no_asm_simp))
    4.12  apply (rule allI, rule allI, rule impI)
    4.13 @@ -99,7 +100,8 @@
    4.14  done
    4.15  
    4.16  
    4.17 -lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    4.18 +lemma vc_mono [rule_format (no_asm)]: 
    4.19 +  "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    4.20  apply (induct_tac "c")
    4.21      apply (simp_all (no_asm_simp))
    4.22  apply safe