src/HOL/IMP/Collecting1.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46334 3858dc8eabd8
child 52019 a4cbca8f7342
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     1
theory Collecting1
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     2
imports Collecting
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     3
begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     4
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     5
subsection "A small step semantics on annotated commands"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     6
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     7
text{* The idea: the state is propagated through the annotated command as an
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
     8
annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
     9
to show that this semantics approximates the collecting semantics. *}
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    10
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    11
lemma step_preserves_le:
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    12
  "\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow>
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    13
   step S' cs' \<le> cs"
46334
nipkow
parents: 46070
diff changeset
    14
by (metis mono2_step)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    15
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    16
lemma steps_empty_preserves_le: assumes "step S cs = cs"
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    17
shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    18
proof(induction n arbitrary: cs')
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    19
  case 0 thus ?case by simp
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    20
next
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    21
  case (Suc n) thus ?case
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    22
    using Suc.IH[OF step_preserves_le[OF assms empty_subsetI Suc.prems]]
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    23
    by(simp add:funpow_swap1)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    24
qed
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    25
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    26
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    27
definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state set acom" where
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    28
"steps s c n = ((step {})^^n) (step {s} (anno {} c))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    29
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    30
lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    31
shows "steps s (strip cs) n \<le> cs"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    32
proof-
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    33
  let ?bot = "anno {} (strip cs)"
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    34
  have "?bot \<le> cs" by(induction cs) auto
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    35
  from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    36
  have 1: "step {s} ?bot \<le> cs" by simp
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
    37
  from steps_empty_preserves_le[OF assms(1) 1]
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    38
  show ?thesis by(simp add: steps_def)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    39
qed
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    40
46070
nipkow
parents: 45655
diff changeset
    41
theorem steps_approx_CS: "steps s c n \<le> CS c"
nipkow
parents: 45655
diff changeset
    42
by (metis CS_unfold UNIV_I steps_approx_fix_step strip_CS)
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    43
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    44
end