src/HOL/IMP/Collecting1.thy
 author paulson Mon May 23 15:33:24 2016 +0100 (2016-05-23) changeset 63114 27afe7af7379 parent 52019 a4cbca8f7342 child 67406 23307fd33906 permissions -rw-r--r--
Lots of new material for multivariate analysis
```     1 theory Collecting1
```
```     2 imports Collecting
```
```     3 begin
```
```     4
```
```     5 subsection "A small step semantics on annotated commands"
```
```     6
```
```     7 text{* The idea: the state is propagated through the annotated command as an
```
```     8 annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
```
```     9 to show that this semantics approximates the collecting semantics. *}
```
```    10
```
```    11 lemma step_preserves_le:
```
```    12   "\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow>
```
```    13    step S' cs' \<le> cs"
```
```    14 by (metis mono2_step)
```
```    15
```
```    16 lemma steps_empty_preserves_le: assumes "step S cs = cs"
```
```    17 shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"
```
```    18 proof(induction n arbitrary: cs')
```
```    19   case 0 thus ?case by simp
```
```    20 next
```
```    21   case (Suc n) thus ?case
```
```    22     using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]
```
```    23     by(simp add:funpow_swap1)
```
```    24 qed
```
```    25
```
```    26
```
```    27 definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state set acom" where
```
```    28 "steps s c n = ((step {})^^n) (step {s} (annotate (\<lambda>p. {}) c))"
```
```    29
```
```    30 lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"
```
```    31 shows "steps s (strip cs) n \<le> cs"
```
```    32 proof-
```
```    33   let ?bot = "annotate (\<lambda>p. {}) (strip cs)"
```
```    34   have "?bot \<le> cs" by(induction cs) auto
```
```    35   from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`
```
```    36   have 1: "step {s} ?bot \<le> cs" by simp
```
```    37   from steps_empty_preserves_le[OF assms(1) 1]
```
```    38   show ?thesis by(simp add: steps_def)
```
```    39 qed
```
```    40
```
```    41 theorem steps_approx_CS: "steps s c n \<le> CS c"
```
```    42 by (metis CS_unfold UNIV_I steps_approx_fix_step strip_CS)
```
```    43
```
```    44 end
```