# HG changeset patch # User kleing # Date 1007907973 -3600 # Node ID ff2efde4574d7d14434781271c65cf39a180ea6d # Parent 654acbf26fcc3b9cb5e9507900ef46440a1b91fe tuned diff -r 654acbf26fcc -r ff2efde4574d src/HOL/IMP/Denotation.thy --- a/src/HOL/IMP/Denotation.thy Sun Dec 09 14:37:42 2001 +0100 +++ b/src/HOL/IMP/Denotation.thy Sun Dec 09 15:26:13 2001 +0100 @@ -13,7 +13,7 @@ constdefs Gamma :: "[bexp,com_den] => (com_den => com_den)" "Gamma b cd == (\phi. {(s,t). (s,t) \ (phi O cd) \ b s} \ - {(s,t). s=t \ \b s})" + {(s,t). s=t \ \b s})" consts C :: "com => com_den" @@ -23,7 +23,7 @@ C_assign: "C (x :== a) = {(s,t). t = s[x\a(s)]}" C_comp: "C (c0;c1) = C(c1) O C(c0)" C_if: "C (\ b \ c1 \ c2) = {(s,t). (s,t) \ C c1 \ b s} \ - {(s,t). (s,t) \ C c2 \ \b s}" + {(s,t). (s,t) \ C c2 \ \b s}" C_while: "C(\ b \ c) = lfp (Gamma b (C c))" @@ -33,10 +33,10 @@ by (unfold Gamma_def mono_def) fast lemma C_While_If: "C(\ b \ c) = C(\ b \ c;\ b \ c \ \)" -apply (simp (no_asm)) -apply (subst lfp_unfold [OF Gamma_mono], - subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong], - simp) +apply (simp (no_asm)) +apply (subst lfp_unfold [OF Gamma_mono]) back back +apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) +apply simp done (* Operational Semantics implies Denotational Semantics *) diff -r 654acbf26fcc -r ff2efde4574d src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Sun Dec 09 14:37:42 2001 +0100 +++ b/src/HOL/IMP/Hoare.thy Sun Dec 09 15:26:13 2001 +0100 @@ -101,10 +101,11 @@ apply (simp (no_asm_simp)) done -declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp] +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False (*Not suitable for rewriting: LOOPS!*) -lemma wp_While_if: "wp (\ b \ c) Q s = (if b s then wp (c;\ b \ c) Q s else Q s)" +lemma wp_While_if: + "wp (\ b \ c) Q s = (if b s then wp (c;\ b \ c) Q s else Q s)" apply (simp (no_asm)) done @@ -132,7 +133,7 @@ declare C_while [simp del] -declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!] +lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}" apply (induct_tac "c") diff -r 654acbf26fcc -r ff2efde4574d src/HOL/IMP/Transition.thy --- a/src/HOL/IMP/Transition.thy Sun Dec 09 14:37:42 2001 +0100 +++ b/src/HOL/IMP/Transition.thy Sun Dec 09 15:26:13 2001 +0100 @@ -45,19 +45,19 @@ *} syntax "@evalc1" :: "[(com option\state),(com option\state)] \ bool" - ("_ -1-> _" [81,81] 100) + ("_ -1-> _" [60,60] 60) "@evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" - ("_ -_-> _" [81,81] 100) + ("_ -_-> _" [60,60,60] 60) "@evalc*" :: "[(com option\state),(com option\state)] \ bool" - ("_ -*-> _" [81,81] 100) + ("_ -*-> _" [60,60] 60) syntax (xsymbols) "@evalc1" :: "[(com option\state),(com option\state)] \ bool" - ("_ \\<^sub>1 _" [81,81] 100) + ("_ \\<^sub>1 _" [60,60] 61) "@evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" - ("_ -_\\<^sub>1 _" [81,81] 100) + ("_ -_\\<^sub>1 _" [60,60,60] 60) "@evalc*" :: "[(com option\state),(com option\state)] \ bool" - ("_ \\<^sub>1\<^sup>* _" [81,81] 100) + ("_ \\<^sub>1\<^sup>* _" [60,60] 60) translations "cs \\<^sub>1 cs'" == "(cs,cs') \ evalc1" @@ -127,7 +127,8 @@ "\\ b \ c1 \ c2, s\ \\<^sub>1 y = ((b s \ y = \c1, s\) \ (\b s \ y = \c2, s\))" by (rule, cases set: evalc1, auto) -lemma While_1: "\\ b \ c, s\ \\<^sub>1 y = (y = \\ b \ c; \ b \ c \ \, s\)" +lemma While_1: + "\\ b \ c, s\ \\<^sub>1 y = (y = \\ b \ c; \ b \ c \ \, s\)" by (rule, cases set: evalc1, auto) lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1 @@ -136,15 +137,15 @@ subsection "Examples" lemma - "s x = 0 \ \\ \s. s x \ 1 \ x:== \s. s x+1, s\ \\<^sub>1\<^sup>* \s[x \ 1]\" + "s x = 0 \ \\ \s. s x \ 1 \ (x:== \s. s x+1), s\ \\<^sub>1\<^sup>* \s[x \ 1]\" (is "_ \ \?w, _\ \\<^sub>1\<^sup>* _") proof - - let ?x = "x:== \s. s x+1" - let ?if = "\ \s. s x \ 1 \ ?x; ?w \ \" + let ?c = "x:== \s. s x+1" + let ?if = "\ \s. s x \ 1 \ ?c; ?w \ \" assume [simp]: "s x = 0" have "\?w, s\ \\<^sub>1 \?if, s\" .. - also have "\?if, s\ \\<^sub>1 \?x; ?w, s\" by simp - also have "\?x; ?w, s\ \\<^sub>1 \?w, s[x \ 1]\" by (rule Semi1, simp) + also have "\?if, s\ \\<^sub>1 \?c; ?w, s\" by simp + also have "\?c; ?w, s\ \\<^sub>1 \?w, s[x \ 1]\" by (rule Semi1, simp) also have "\?w, s[x \ 1]\ \\<^sub>1 \?if, s[x \ 1]\" .. also have "\?if, s[x \ 1]\ \\<^sub>1 \\, s[x \ 1]\" by (simp add: update_def) also have "\\, s[x \ 1]\ \\<^sub>1 \s[x \ 1]\" .. @@ -152,7 +153,7 @@ qed lemma - "s x = 2 \ \\ \s. s x \ 1 \ x:== \s. s x+1, s\ \\<^sub>1\<^sup>* s'" + "s x = 2 \ \\ \s. s x \ 1 \ (x:== \s. s x+1), s\ \\<^sub>1\<^sup>* s'" (is "_ \ \?w, _\ \\<^sub>1\<^sup>* s'") proof - let ?c = "x:== \s. s x+1" @@ -193,7 +194,11 @@ If a configuration does not contain a statement, the program has terminated and there is no next configuration: *} -lemma stuck [dest]: "(None, s) \\<^sub>1 y \ False" by (auto elim: evalc1.elims) +lemma stuck [elim!]: "\s\ \\<^sub>1 y \ P" + by (auto elim: evalc1.elims) + +lemma evalc_None_retrancl [simp, dest!]: "\s\ \\<^sub>1\<^sup>* s' \ s' = \s\" + by (erule rtrancl_induct) auto (*<*) (* fixme: relpow.simps don't work *) @@ -201,8 +206,7 @@ lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp lemmas [simp del] = relpow.simps (*>*) - -lemma evalc_None_0 [simp]: "\s\ -n\\<^sub>1 y = (n = 0 \ y = \s\)" +lemma evalc1_None_0 [simp, dest!]: "\s\ -n\\<^sub>1 y = (n = 0 \ y = \s\)" by (cases n) auto lemma SKIP_n: "\\, s\ -n\\<^sub>1 \s'\ \ s' = s \ n=1" @@ -252,10 +256,10 @@ c1': "\c1',s'\ -i\\<^sub>1 \s0\" and c2: "\c2,s0\ -j\\<^sub>1 \s''\" and i: "n = i+j" - by blast + by fast from c1 c1' - have "\c1,s\ -(i+1)\\<^sub>1 \s0\" by (auto simp del: relpow.simps intro: rel_pow_Suc_I2) + have "\c1,s\ -(i+1)\\<^sub>1 \s0\" by (auto intro: rel_pow_Suc_I2) with c2 i have "?Q (i+1) j s0" by simp thus ?thesis by blast @@ -591,7 +595,7 @@ apply (rename_tac c s') apply simp apply (rule conjI) - apply (fast dest: stuck) + apply fast apply clarify apply (case_tac c) apply (auto intro: rtrancl_into_rtrancl2) @@ -667,16 +671,13 @@ apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while]) done -lemma rtrancl_stuck: "\s\ \\<^sub>1\<^sup>* s' \ s' = (None, s)" - by (erule rtrancl_induct) (auto dest: stuck) - lemma FB_lemma2 [rule_format]: "(c,s) \\<^sub>1\<^sup>* (c',s') \ c \ None \ \if c' = None then \ else the c',s'\ \\<^sub>c t \ \the c,s\ \\<^sub>c t" apply (erule converse_rtrancl_induct2) apply simp apply clarsimp - apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3) + apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3) done lemma evalc1_impl_evalc: "\c,s\ \\<^sub>1\<^sup>* \t\ \ \c,s\ \\<^sub>c t" diff -r 654acbf26fcc -r ff2efde4574d src/HOL/IMP/VC.thy --- a/src/HOL/IMP/VC.thy Sun Dec 09 14:37:42 2001 +0100 +++ b/src/HOL/IMP/VC.thy Sun Dec 09 15:26:13 2001 +0100 @@ -90,7 +90,8 @@ apply fast done -lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)" +lemma awp_mono [rule_format (no_asm)]: + "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)" apply (induct_tac "c") apply (simp_all (no_asm_simp)) apply (rule allI, rule allI, rule impI) @@ -99,7 +100,8 @@ done -lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)" +lemma vc_mono [rule_format (no_asm)]: + "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)" apply (induct_tac "c") apply (simp_all (no_asm_simp)) apply safe