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