src/HOL/IMP/Collecting1.thy
author paulson <lp15@cam.ac.uk>
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