equal
deleted
inserted
replaced
18 |
18 |
19 |
19 |
20 |
20 |
21 section "set of not yet initialzed classes" |
21 section "set of not yet initialzed classes" |
22 |
22 |
23 constdefs |
23 definition nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" where |
24 |
|
25 nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" |
|
26 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}" |
24 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}" |
27 |
25 |
28 lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}" |
26 lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}" |
29 apply (unfold nyinitcls_def) |
27 apply (unfold nyinitcls_def) |
30 apply fast |
28 apply fast |
113 done |
111 done |
114 |
112 |
115 |
113 |
116 section "init-le" |
114 section "init-le" |
117 |
115 |
118 constdefs |
116 definition init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50) where |
119 init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50) |
|
120 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n" |
117 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n" |
121 |
118 |
122 lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)" |
119 lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)" |
123 apply (unfold init_le_def) |
120 apply (unfold init_le_def) |
124 apply auto |
121 apply auto |
133 apply (rule card_nyinitcls_bound) |
130 apply (rule card_nyinitcls_bound) |
134 done |
131 done |
135 |
132 |
136 section "Most General Triples and Formulas" |
133 section "Most General Triples and Formulas" |
137 |
134 |
138 constdefs |
135 definition remember_init_state :: "state assn" ("\<doteq>") where |
139 |
|
140 remember_init_state :: "state assn" ("\<doteq>") |
|
141 "\<doteq> \<equiv> \<lambda>Y s Z. s = Z" |
136 "\<doteq> \<equiv> \<lambda>Y s Z. s = Z" |
142 |
137 |
143 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op =" |
138 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op =" |
144 apply (unfold remember_init_state_def) |
139 apply (unfold remember_init_state_def) |
145 apply (simp (no_asm)) |
140 apply (simp (no_asm)) |
577 come up with a proper loop invariant, which intuitively states that we are |
572 come up with a proper loop invariant, which intuitively states that we are |
578 currently inside the evaluation of the loop. To define such an invariant, we |
573 currently inside the evaluation of the loop. To define such an invariant, we |
579 unroll the loop in iterated evaluations of the expression and evaluations of |
574 unroll the loop in iterated evaluations of the expression and evaluations of |
580 the loop body. *} |
575 the loop body. *} |
581 |
576 |
582 constdefs |
577 definition unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set" where |
583 unroll:: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set" |
|
584 |
578 |
585 "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2. |
579 "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2. |
586 G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and> |
580 G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and> |
587 G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}" |
581 G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}" |
588 |
582 |